wip

compiler/app/Language/Granule/Compiler.hs

@@ -248,6 +248,13 @@ parseGrConfig = info (go <**> helper) $ briefDesc
             , show solverTimeoutMillis <> "ms."
             ]
 
+        globalsCachePath <-
+          optional $ strOption
+            $ long "cache-path"
+            <> help ("Path to the cache file. Defaults to "
+                    <> show cachePath)
+            <> metavar "PATH"
+
         globalsIncludePath <-
           optional $ strOption
             $ long "include-path"

frontend/package.yaml

@@ -23,10 +23,11 @@ ghc-options:
 
 default-extensions:
 - ImplicitParams
-- ViewPatterns
 - LambdaCase
-- TupleSections
 - NamedFieldPuns
+- ScopedTypeVariables
+- TupleSections
+- ViewPatterns
 
 library:
   source-dirs: src
@@ -88,7 +89,6 @@ library:
   - Glob
   - filepath
   - bifunctors
-  - raw-strings-qq
   - text-replace
   - directory
   - syb >=0.6
@@ -97,6 +97,8 @@ library:
   - split
   - logict >= 0.7.1.0
   - clock
+  - algebraic-graphs
+  - template-haskell
 
 tests:
   frontend-spec:

frontend/src/Language/Granule/Checker/Checker.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
 
 {-# options_ghc -fno-warn-incomplete-uni-patterns -Wno-deprecations #-}
 
@@ -46,9 +47,9 @@ import Language.Granule.Checker.TypeAliases
 import Language.Granule.Checker.Variables
 import Language.Granule.Context
 
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Helpers (freeVars, hasHole)
 import Language.Granule.Syntax.Def
+import Language.Granule.Syntax.Program
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Pattern (Pattern(..))
 import Language.Granule.Syntax.Pretty
@@ -61,81 +62,102 @@ import qualified Language.Granule.Synthesis.Synth as Syn
 
 import Language.Granule.Utils
 
+import Debug.Trace
+import System.Directory (getModificationTime)
+import Control.Exception (try, SomeException)
+
 -- Checking (top-level)
 check :: (?globals :: Globals)
-  => AST () ()
-  -> IO (Either (NonEmpty CheckerError) (AST () Type, [Def () ()]))
-check ast@(AST _ _ _ hidden _) = do
-  evalChecker (initState { allHiddenNames = hidden }) $ (do
-      ast@(AST dataDecls defs imports hidden name) <- return $ replaceTypeAliases ast
+  => Module
+  -> IO (Either (NonEmpty CheckerError) (AST () Type, ModuleSignature))
+check mod@Mod{ moduleAST = ast } =
+  case moduleSignature mod of
+    Just sig -> do
+  -- case moduleMetadata of
+  --   ModMeta
+  --     -- { moduleMetaFilePath = Just sourceFilePath
+  --     { moduleMetaFileModificationTime = Just sourceFileModificationTime
+  --     -- , moduleMetaSignatureFilePath = Just interfaceFilePath
+  --     , moduleMetaSignatureFileModificationTime = Just interfaceFileModificationTime
+  --     }
+  --     | interfaceFileModificationTime > sourceFileModificationTime
+  --     , Just sig <- moduleSignature mod
+
+
+  evalChecker (initState { allHiddenNames = moduleHiddenNames mod }) $ do
+      ast <- return $ replaceTypeAliases ast
       _    <- checkNameClashes ast
-      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataDecls)
-      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataDecls)
+      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataTypes ast)
+      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataTypes ast)
       debugM "extensions" (show $ globalsExtensions ?globals)
       debugM "check" "kindCheckDef"
-      defs <- runAll kindCheckDef defs
+      defs <- runAll kindCheckDef (definitions ast)
       let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
       defs <- runAll (checkDef defCtxt) defs
       -- Add on any definitions computed by the type checker (derived)
       st <- get
       let derivedDefs = map (snd . snd) (derivedDefinitions st)
-      pure $ (AST dataDecls defs imports hidden name, derivedDefs))
+      -- traceM $ show $ AST dataDecls defs imports hidden name
+      -- traceM $ show derivedDefs
+      pure (AST{ dataTypes = dataTypes ast, definitions = defs }, derivedDefs)
 
--- Synthing the type of a single expression in the context of an asy
+-- Synthing the type of a single expression in the context of a Module
 synthExprInIsolation :: (?globals :: Globals)
-  => AST () ()
+  => Module
   -> Expr () ()
   -> IO (Either (NonEmpty CheckerError) (Either (TypeScheme , [Def () ()]) Type))
-synthExprInIsolation ast@(AST dataDecls defs imports hidden name) expr =
-  evalChecker (initState { allHiddenNames = hidden }) $ do
-      _    <- checkNameClashes ast
-      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataDecls)
-      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataDecls)
-      defs <- runAll kindCheckDef defs
-
-      let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
-
-      -- also check the defs
-      defs <- runAll (checkDef defCtxt) defs
-
-      -- Since we need to return a type scheme, have a look first
-      -- for top-level identifiers with their schemes
-      case expr of
-        -- Lookup in data constructors
-        (Val s _ _ (Constr _ c [])) -> do
-          mConstructor <- lookupDataConstructor s c
-          case mConstructor of
-            Just (tySch, _) -> return $ Left (tySch, [])
-            Nothing -> do
-              st <- get
-              -- Or see if this is a kind constructors
-              case lookup c (typeConstructors st) of
-                Just (k, _, _) -> return $ Right k
-                Nothing -> throw UnboundDataConstructor{ errLoc = s, errId = c }
-
-        -- Lookup in definitions
-        (Val s _ _ (Var _ x)) -> do
-          case lookup x (defCtxt <> Primitives.builtins) of
-            Just tyScheme -> return $ Left (tyScheme, [])
-            Nothing -> throw UnboundVariableError{ errLoc = s, errId = x }
-
-        -- Otherwise, do synth
-        _ -> do
-          (ty, _, subst, _) <- synthExpr defCtxt [] Positive expr
-          --
-          -- Solve the generated constraints
-          checkerState <- get
-
-          let predicate = Conj $ predicateStack checkerState
-          predicate <- substitute subst predicate
-          solveConstraints predicate (getSpan expr) (mkId "grepl")
-
-
-          let derivedDefs = map (snd . snd) (derivedDefinitions checkerState)
-
-          -- Apply the outcoming substitution
-          ty' <- substitute subst ty
-          return $ Left (Forall nullSpanNoFile [] [] ty', derivedDefs)
+synthExprInIsolation
+  mod@Mod{ moduleAST = ast@AST{ dataTypes = dataDecls, definitions = defs } }
+  expr =
+    evalChecker (initState { allHiddenNames = moduleHiddenNames mod }) $ do
+        _    <- checkNameClashes ast
+        _    <- runAll checkTyCon (Primitives.dataTypes ++ dataDecls)
+        _    <- runAll checkDataCons (Primitives.dataTypes ++ dataDecls)
+        defs <- runAll kindCheckDef defs
+
+        let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
+
+        -- also check the defs
+        defs <- runAll (checkDef defCtxt) defs
+
+        -- Since we need to return a type scheme, have a look first
+        -- for top-level identifiers with their schemes
+        case expr of
+          -- Lookup in data constructors
+          (Val s _ _ (Constr _ c [])) -> do
+            mConstructor <- lookupDataConstructor s c
+            case mConstructor of
+              Just (tySch, _) -> return $ Left (tySch, [])
+              Nothing -> do
+                st <- get
+                -- Or see if this is a kind constructors
+                case lookup c (typeConstructors st) of
+                  Just (k, _, _) -> return $ Right k
+                  Nothing -> throw UnboundDataConstructor{ errLoc = s, errId = c }
+
+          -- Lookup in definitions
+          (Val s _ _ (Var _ x)) -> do
+            case lookup x (defCtxt <> Primitives.builtins) of
+              Just tyScheme -> return $ Left (tyScheme, [])
+              Nothing -> throw UnboundVariableError{ errLoc = s, errId = x }
+
+          -- Otherwise, do synth
+          _ -> do
+            (ty, _, subst, _) <- synthExpr defCtxt [] Positive expr
+            --
+            -- Solve the generated constraints
+            checkerState <- get
+
+            let predicate = Conj $ predicateStack checkerState
+            predicate <- substitute subst predicate
+            solveConstraints predicate (getSpan expr) (mkId "grepl")
+
+
+            let derivedDefs = map (snd . snd) (derivedDefinitions checkerState)
+
+            -- Apply the outcoming substitution
+            ty' <- substitute subst ty
+            return $ Left (Forall nullSpanNoFile [] [] ty', derivedDefs)
 
 -- TODO: we are checking for name clashes again here. Where is the best place
 -- to do this check?
@@ -303,6 +325,8 @@ checkDef defCtxt (Def s defName rf el@(EquationList _ _ _ equations)
     checkGuardsForImpossibility s defName
     checkGuardsForExhaustivity s defName ty equations
     let el' = el { equations = elaboratedEquations }
+    traceM "\n\n********\n"
+    traceM $ show $ Def s defName rf el' tys
     pure $ Def s defName rf el' tys
   where
     elaborateEquation :: Equation () () -> Checker (Equation () Type)
@@ -1984,6 +2008,11 @@ checkGuardsForImpossibility s name = do
     debugM "impossibility" $ "about to try" <> pretty thm
     -- Try to prove the theorem
     constructors <- allDataConstructorNames
+
+    -- traceM $ show (thm, tyVars, constructors)
+
+    _ <- liftIO $ try @SomeException $ getModificationTime ""
+
     (_, result) <- liftIO $ provePredicate thm tyVars constructors
 
     p <- simplifyPred thm

frontend/src/Language/Granule/Checker/Kinding.hs

@@ -19,7 +19,6 @@ import Data.Maybe (fromMaybe)
 import Language.Granule.Context
 
 import Language.Granule.Syntax.Def
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Type

frontend/src/Language/Granule/Checker/Monad.hs

@@ -17,6 +17,7 @@ module Language.Granule.Checker.Monad where
 import Data.Maybe (mapMaybe)
 import Data.Either (partitionEithers)
 import Data.Foldable (toList)
+import Data.Functor ( ($>) )
 import Data.List (intercalate, transpose)
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.Map as M
@@ -32,10 +33,9 @@ import Language.Granule.Checker.Predicates
 import qualified Language.Granule.Checker.Primitives as Primitives
 import Language.Granule.Context
 
-import Language.Granule.Syntax.Def
+import Language.Granule.Syntax.Program
 import Language.Granule.Syntax.Expr (Operator, Expr)
 import Language.Granule.Syntax.Helpers (FreshenerState(..), freshen, Term(..))
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Pattern
 import Language.Granule.Syntax.Pretty
@@ -70,7 +70,7 @@ runAll f xs = do
   st <- get
   (results, st) <- liftIO $ runAllCheckers st (map f xs)
   case partitionEithers results of
-    ([], successes) -> put st *> pure successes
+    ([], successes) -> put st $> successes
     -- everything succeeded, so `put` the state and carry on
     (err:errs, _) -> throwError $ sconcat (err:|errs)
     -- combine all errors and fail
@@ -179,7 +179,7 @@ data CheckerState = CS
             , derivStack :: [Derivation]
 
             -- Names from modules which are hidden
-            , allHiddenNames :: M.Map Id Id
+            , allHiddenNames :: M.Map Id ModuleName
 
             -- The type of the current equation.
             , equationTy :: Maybe Type
@@ -230,7 +230,7 @@ lookupDataConstructor sp constrName = do
     Nothing -> return $ lookup constrName (dataConstructors st)
     Just mod ->
       -- If the constructor is hidden but we are inside that module...
-      if sourceName mod == takeBaseName (filename sp)
+      if mod == takeBaseName (filename sp)
         -- .. then its fine
         then return $ lookup constrName (dataConstructors st)
         -- Otheriwe this is truly hidden

frontend/src/Language/Granule/Checker/NameClash.hs

@@ -5,11 +5,10 @@ import Control.Monad.Except (throwError)
 import Data.List.NonEmpty (NonEmpty(..))
 import Language.Granule.Checker.Monad
 import Language.Granule.Syntax.Def
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Utils
 
 checkNameClashes :: AST () () -> Checker ()
-checkNameClashes (AST dataDecls defs _ _ _) =
+checkNameClashes AST{ dataTypes = dataDecls, definitions = defs } =
     case concat [typeConstructorErrs, dataConstructorErrs, defErrs] of
       [] -> pure ()
       (d:ds) -> throwError (d:|ds)
@@ -49,4 +48,4 @@ checkNameClashes (AST dataDecls defs _ _ _) =
           { errLoc = defSpan x2
           , errDef = x2
           , otherDefs = xs
-          }
+          }