From 4f9c7fa8a9b5bca4ca0fe28515fbb217fb9804ea Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 28 Sep 2024 11:39:17 -0700 Subject: [PATCH] rearrange deck chairs --- TODO.md | 2 - newt.ipkg | 4 +- src/Lib/CompileExp.idr | 2 +- src/Lib/{Check.idr => Elab.idr} | 4 +- src/Lib/{TT.idr => Eval.idr} | 85 +-------------------------------- src/Lib/ProcessDecl.idr | 4 +- src/Lib/Types.idr | 58 ++++++++++++++++++++++ src/Main.idr | 2 +- 8 files changed, 67 insertions(+), 94 deletions(-) rename src/Lib/{Check.idr => Elab.idr} (99%) rename src/Lib/{TT.idr => Eval.idr} (77%) diff --git a/TODO.md b/TODO.md index 67fe578..b6647d7 100644 --- a/TODO.md +++ b/TODO.md @@ -3,8 +3,6 @@ I may be done with `U` - I keep typing `Type`. -TT.idr should be Eval.idr, utilities up front belong elsewhere - - [ ] consider making meta application implicit in term, so its more readable when printed - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people leave that implicit for efficiency. I think it would also make printing more readable. diff --git a/newt.ipkg b/newt.ipkg index 2c57a81..16cd1ec 100644 --- a/newt.ipkg +++ b/newt.ipkg @@ -17,13 +17,13 @@ depends = contrib, base -- modules to install modules = - Lib.Check, + Lib.Elab, Lib.Parser, Lib.Parser.Impl, Lib.Prettier, Lib.ProcessDecl, Lib.Syntax, - Lib.TT, + Lib.Eval, Lib.Token, Lib.TopContext, Lib.Types, diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index d872243..6fcf075 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -8,7 +8,7 @@ import Data.List import Lib.Types -- Name / Tm import Lib.TopContext -import Lib.TT -- lookupMeta +import Lib.Eval -- lookupMeta import Lib.Util public export diff --git a/src/Lib/Check.idr b/src/Lib/Elab.idr similarity index 99% rename from src/Lib/Check.idr rename to src/Lib/Elab.idr index 577e488..a87c9cf 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Elab.idr @@ -1,4 +1,4 @@ -module Lib.Check +module Lib.Elab import Control.Monad.Error.Either import Control.Monad.Error.Interface @@ -10,7 +10,7 @@ import Data.List import Data.Vect import Data.String import Lib.Types -import Lib.TT +import Lib.Eval import Lib.TopContext import Lib.Syntax diff --git a/src/Lib/TT.idr b/src/Lib/Eval.idr similarity index 77% rename from src/Lib/TT.idr rename to src/Lib/Eval.idr index b2e773a..c430172 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/Eval.idr @@ -1,4 +1,4 @@ -module Lib.TT +module Lib.Eval -- For FC import Lib.Parser.Impl @@ -12,89 +12,6 @@ import Data.List import Data.Vect import Data.SortedMap --- Errors cribbed from pi-forall -public export -data ErrorSeg : Type where - DD : Pretty a => a -> ErrorSeg - DS : String -> ErrorSeg - -toDoc : ErrorSeg -> Doc -toDoc (DD x) = pretty x -toDoc (DS str) = text str - -export -error : FC -> String -> M a -error fc msg = throwError $ E fc msg - -export -error' : String -> M a -error' msg = throwError $ E (0,0) msg - --- order does indeed matter on the meta arguments --- because of dependent types (if we want something well-typed back out) - -export -freshMeta : Context -> FC -> Val -> M Tm -freshMeta ctx fc ty = do - mc <- readIORef ctx.metas - putStrLn "INFO at \{show fc}: fresh meta \{show mc.next} : \{show ty}" - writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty ::) } mc - pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds - where - -- hope I got the right order here :) - applyBDs : Nat -> Tm -> Vect k BD -> Tm - applyBDs k t [] = t - -- review the order here - applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k) - applyBDs k t (Defined :: xs) = applyBDs (S k) t xs - - -- makeType : Vect k (String, Val) -> Vect k BD -> Val - -- makeType [] [] = ?makeType_rhs_2 - -- makeType ((nm, ty) :: types) (Defined :: bds) = makeType types bds - -- makeType ((nm, ty) :: types) (Bound :: bds) = VPi emptyFC nm Explicit ty - - -export -lookupMeta : Nat -> M MetaEntry -lookupMeta ix = do - ctx <- get - mc <- readIORef ctx.metas - go mc.metas - where - go : List MetaEntry -> M MetaEntry - go [] = error' "Meta \{show ix} not found" - go (meta@(Unsolved _ k ys _) :: xs) = if k == ix then pure meta else go xs - go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs - -export partial -Show Context where - show ctx = "Context \{show $ map fst $ ctx.types}" - --- TODO Pretty Context - - -||| add a binding to environment -export -extend : Context -> String -> Val -> Context -extend ctx name ty = - { lvl $= S, env $= (VVar emptyFC ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx - --- I guess we define things as values? -export -define : Context -> String -> Val -> Val -> Context -define ctx name val ty = - { lvl $= S, env $= (val ::), types $= ((name,ty) ::), bds $= (Defined ::) } ctx - - --- not used -lookup : Context -> String -> M Val -lookup ctx nm = go ctx.types - where - go : Vect n (String,Val) -> M Val - go [] = error' "Name \{nm} not in scope" - go ((n, ty) :: xs) = if n == nm then pure ty else go xs - - -- Need to wire in the metas... -- if it's top / ctx / IORef, I also need IO... -- if I want errors, I need m anyway. I've already got an error down there. diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index f814904..3455c77 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -2,11 +2,11 @@ module Lib.ProcessDecl import Data.IORef -import Lib.Check +import Lib.Elab import Lib.Parser import Lib.Syntax import Lib.TopContext -import Lib.TT +import Lib.Eval import Lib.Types import Lib.Util diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index d6751f0..8a7a8e8 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -361,6 +361,20 @@ record Context where metas : IORef MetaContext fc : FC + +||| add a binding to environment +export +extend : Context -> String -> Val -> Context +extend ctx name ty = + { lvl $= S, env $= (VVar emptyFC ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx + +-- I guess we define things as values? +export +define : Context -> String -> Val -> Val -> Context +define ctx name val ty = + { lvl $= S, env $= (val ::), types $= ((name,ty) ::), bds $= (Defined ::) } ctx + + export covering Show MetaEntry where @@ -378,6 +392,50 @@ public export M : Type -> Type M = (StateT TopContext (EitherT Impl.Error IO)) +export partial +Show Context where + show ctx = "Context \{show $ map fst $ ctx.types}" + +export +error : FC -> String -> M a +error fc msg = throwError $ E fc msg + +export +error' : String -> M a +error' msg = throwError $ E (0,0) msg + +export +freshMeta : Context -> FC -> Val -> M Tm +freshMeta ctx fc ty = do + mc <- readIORef ctx.metas + putStrLn "INFO at \{show fc}: fresh meta \{show mc.next} : \{show ty}" + writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty ::) } mc + pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds + where + -- hope I got the right order here :) + applyBDs : Nat -> Tm -> Vect k BD -> Tm + applyBDs k t [] = t + -- review the order here + applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k) + applyBDs k t (Defined :: xs) = applyBDs (S k) t xs + + -- makeType : Vect k (String, Val) -> Vect k BD -> Val + -- makeType [] [] = ?makeType_rhs_2 + -- makeType ((nm, ty) :: types) (Defined :: bds) = makeType types bds + -- makeType ((nm, ty) :: types) (Bound :: bds) = VPi emptyFC nm Explicit ty + +export +lookupMeta : Nat -> M MetaEntry +lookupMeta ix = do + ctx <- get + mc <- readIORef ctx.metas + go mc.metas + where + go : List MetaEntry -> M MetaEntry + go [] = error' "Meta \{show ix} not found" + go (meta@(Unsolved _ k ys _) :: xs) = if k == ix then pure meta else go xs + go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs + -- we need more of topcontext later - Maybe switch it up so we're not passing -- around top export diff --git a/src/Main.idr b/src/Main.idr index 8b985b2..af01499 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -8,7 +8,7 @@ import Data.List import Data.String import Data.Vect import Data.IORef --- import Lib.Check +-- import Lib.Elab import Lib.Compile import Lib.Parser -- import Lib.Parser.Impl