Browse Source

Add some very rudimentary elaboration support

hydraz 1 year ago
parent
commit
6824d1cb4a
5 changed files with 96 additions and 4 deletions
  1. 2 2
      README.md
  2. 6 1
      example.dtt
  3. 44 0
      src/Elab.hs
  4. 21 0
      src/Elab/Implicits.hs
  5. 23 1
      src/Main.hs

+ 2 - 2
README.md

@@ -4,12 +4,12 @@ A simple dependent type theory which can be used to verify very simple
 theorems.
 
 `dtt` does not have:
-  - inductive data types (use postulations if possible)
   - recursive definitions (TODO: a totality checker so we can allow this)
-  - pattern matching
   - Σ types
   - a standard library
 
 `dtt` does have:
   - Π types
   - unification-based type equality
+  - pattern matching
+  - inductive data types (use postulations if possible)

+ 6 - 1
example.dtt

@@ -3,7 +3,12 @@ inductive Nat : Set 0 of {
 }.
 
 inductive Pair : Set 0 -> Set 0 -> Set 0 of {
-  MkPair : (α: Set 0) -> (a: α) -> (β: Set 0) -> (b: β) -> Pair α β
+  MkPair : (a: α) -> (b: β) -> Pair α β
+}.
+
+inductive Sum : Set 0 -> Set 0 -> Set 0 of {
+  Left  : α -> Sum α β;
+  Right : β -> Sum α β
 }.
 
 inductive Eq : Set 0 -> Set 0 -> Set 0 of {

+ 44 - 0
src/Elab.hs

@@ -0,0 +1,44 @@
+{-# LANGUAGE RankNTypes #-}
+module Elab where
+  
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Reader
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+import Control.Monad
+
+import Types.Context
+import Syntax
+
+type Elab r p
+  = ( Member (Exc TypeError) r
+    , Member (Reader Context) r
+    , Member Fresh r )
+  => p -> Type
+  -> Eff r Type
+
+elabOne :: ( Member (Exc TypeError) r
+           , Member (Reader Context) r
+           , Member Fresh r )
+        => Elab r p
+        -> p -> Type -> Eff r Type
+elabOne = id
+
+elabProg :: ( Member (Exc TypeError) r
+           , Member (Reader Context) r
+           , Member Fresh r )
+         => Elab r p
+         -> p -> Program -> Eff r Program
+elabProg ac p (Postulate v t:xs) = do
+  t' <- elabOne ac p t
+  (Postulate v t':) <$> elabProg ac p xs
+elabProg ac p (Define v t:xs) = (Define v t:) <$> elabProg ac p xs
+elabProg ac p (DataDecl (MkInductive nm ty cs):xs) = do
+  cs' <- forM cs $ \(n, v) -> do
+    v' <- elabOne ac p v
+    pure (n, v')
+  ty' <- elabOne ac p ty
+  (DataDecl (MkInductive nm ty' cs'):) <$> elabProg ac p xs
+elabProg ac p (Eval t:xs) = (Eval t:) <$> elabProg ac p xs
+elabProg _ _ [] = pure []

+ 21 - 0
src/Elab/Implicits.hs

@@ -0,0 +1,21 @@
+module Elab.Implicits where
+
+import Types.Context
+import Syntax.Subst
+import Syntax
+
+import Control.Monad
+
+import qualified Data.Set as Set
+
+import Elab
+
+addImplicits :: Elab r ()
+addImplicits _ k
+  = let fv = Set.toList (freeIn k)
+        add t v = do
+          x <- lookupType v
+          case x of
+            Just _ -> pure t
+            Nothing -> pure $ Pi v (Set 0) t
+     in foldM add k fv

+ 23 - 1
src/Main.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE RankNTypes, DataKinds #-}
 module Main where
 
 import Types.Context
@@ -11,10 +12,31 @@ import Data.These
 import System.Environment
 import Text.Printf
 
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Reader
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
 import Control.Monad
 
 import Pretty (prettyPrint)
 import Syntax.Pretty ()
+import Syntax
+
+import Elab
+import Elab.Implicits
+
+runElabAndCheck :: Elab [Fresh, Reader Context, Exc TypeError] p -> p
+                -> Context
+                -> Program
+                -> Either TypeError (Context, Maybe (Term, Type))
+runElabAndCheck e p ctx prg
+  = run
+  . runError
+  . flip runReader ctx
+  . flip runFresh' 0
+  $ do (ctx, _) <- checkProgram prg
+       prg' <- local (const ctx) (elabProg e p prg)
+       checkProgram prg'
 
 main :: IO ()
 main = do
@@ -23,7 +45,7 @@ main = do
   case runParser program () x prg of
     Left e -> print e
     Right prog -> do
-      let x = runCheck empty prog
+      let x = runElabAndCheck addImplicits () empty prog
       case x of
         Left (Redefinition v) ->
           printf "Redefinition of %s" (prettyPrint v)