wip

frontend/package.yaml

@@ -88,7 +88,6 @@ library:
   - Glob
   - filepath
   - bifunctors
-  - raw-strings-qq
   - text-replace
   - directory
   - syb >=0.6
@@ -97,6 +96,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,16 +62,20 @@ 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 () ()
+  => Module
   -> 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
+check mod@Mod{ moduleAST = ast, moduleHiddenNames = hidden } = do
+  evalChecker (initState { allHiddenNames = hidden }) $ 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
@@ -79,63 +84,67 @@ check ast@(AST _ _ _ hidden _) = do
       -- 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 dataDecls defs imports hidden name, 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 +312,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 +1995,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
-          }
+          }

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

@@ -9,11 +9,9 @@
 module Language.Granule.Checker.Primitives where
 
 import Data.List.NonEmpty (NonEmpty(..))
-import Text.RawString.QQ (r)
 
-import Language.Granule.Syntax.Def
-import Language.Granule.Syntax.Identifiers
-import Language.Granule.Syntax.Parser (parseDefs)
+import Language.Granule.Syntax.Def as Def
+import Language.Granule.Syntax.QuasiQuoter
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Expr (Operator(..))
@@ -36,7 +34,7 @@ capabilities =
    [(mkId "Console", funTy (tyCon "String") (tyCon "()"))
   , (mkId "TimeDate", funTy (tyCon "()") (tyCon "String"))]
 
-    
+
 
 -- Associates type constuctors names to their:
 --    * kind
@@ -80,7 +78,7 @@ typeConstructors =
     , (mkId "One",      (tyCon "LNL", [], False))
     , (mkId "Many",     (tyCon "LNL", [], False))
     -- Security levels
-    
+
     -- Note that Private/Public can be members of Sec (and map to Hi/Lo) or if 'SecurityLevels' is
     -- turned on then they are part of the 'Level' semiring
     , (mkId "Private",  (extensionDependent [(SecurityLevels, tyCon "Level")] (tyCon "Sec"), [], False))
@@ -195,7 +193,7 @@ dataTypes =
           , dataConstrId = mkId "&"
           , dataConstrParams = [TyVar (mkId "a"), TyVar (mkId "b")]
          }]}
-    ] ++ builtinDataTypesParsed
+    ] ++ Def.dataTypes builtinAST
 
 binaryOperators :: Operator -> NonEmpty Type
 binaryOperators = \case
@@ -240,8 +238,8 @@ binaryOperators = \case
         , funTy (TyCon $ mkId "DFloat") (funTy (TyCon $ mkId "DFloat") (TyCon $ mkId "Bool"))]
 
 -- TODO make a proper quasi quoter that parses this at compile time
-builtinSrc :: String
-builtinSrc = [r|
+builtinAST :: AST () ()
+builtinAST = [gr|
 
 import Prelude
 
@@ -582,13 +580,13 @@ uniqueBind
   . (*a -> !b) -> !a -> !b
 uniqueBind = BUILTIN
 
-uniquePush 
-  : forall {a b : Type} 
+uniquePush
+  : forall {a b : Type}
   . *(a, b)  -> (*a, *b)
 uniquePush = BUILTIN
 
-uniquePull 
-  : forall {a b : Type} 
+uniquePull
+  : forall {a b : Type}
   . (*a, *b) -> *(a, b)
 uniquePull = BUILTIN
 
@@ -672,20 +670,12 @@ projR = BUILTIN
 
 |]
 
-
-builtinDataTypesParsed :: [DataDecl]
 builtins :: [(Id, TypeScheme)]
-(builtinDataTypesParsed, builtins) =
-  (types, map unDef defs)
-    where
-      AST types defs _ _ _ = case parseDefs "builtins" builtinSrc of
-        Right (ast, _) -> ast
-        Left err -> error err
+builtins = map unDef $ definitions builtinAST
 
-      unDef :: Def () () -> (Id, TypeScheme)
-      unDef (Def _ name _ _ (Forall _ bs cs t)) = (name, Forall nullSpanBuiltin bs cs t)
+unDef :: Def () () -> (Id, TypeScheme)
+unDef (Def _ name _ _ (Forall _ bs cs t)) = (name, Forall nullSpanBuiltin bs cs t)
 
 -- List of primitives that can't be promoted in CBV
 unpromotables :: [String]
 unpromotables = ["newFloatArray", "forkLinear", "forkLinear'", "forkMulticast", "forkReplicate", "forkReplicateExactly"]
-

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

@@ -30,7 +30,6 @@ import Language.Granule.Context
 import Language.Granule.Syntax.Def
 import Language.Granule.Syntax.Expr hiding (Substitutable)
 import Language.Granule.Syntax.Helpers hiding (freshIdentifierBase)
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Pattern
 -- import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Span
@@ -371,7 +370,7 @@ substituteValue ctxt (PromoteF ty expr) =
 substituteValue ctxt (PureF ty expr) =
     do  ty' <- substitute ctxt ty
         return $ Pure ty' expr
-substituteValue ctxt (NecF ty expr) = 
+substituteValue ctxt (NecF ty expr) =
     do ty' <- substitute ctxt ty
        return $ Nec ty' expr
 substituteValue ctxt (ConstrF ty ident vs) =