@@ -103,7 +103,7 @@ processDecl : List String -> Decl -> M Unit
processDecl ns ( PMixFix _ _ _ _) = pure MkUnit
processDecl ns ( PMixFix _ _ _ _) = pure MkUnit
processDecl ns ( TypeSig fc names tm) = do
processDecl ns ( TypeSig fc names tm) = do
putStrLn " ----- "
log 1 $ \ _ = > " ----- "
top <- get
top <- get
mc <- readIORef top.metaCtx
mc <- readIORef top.metaCtx
@@ -114,7 +114,7 @@ processDecl ns (TypeSig fc names tm) = do
pure MkUnit
pure MkUnit
ty <- check ( mkCtx fc) tm ( VU fc)
ty <- check ( mkCtx fc) tm ( VU fc)
ty <- zonk top 0 Nil ty
ty <- zonk top 0 Nil ty
putStrLn " TypeSig \ { u n words names} : \ { r ender 90 $ pprint Nil ty} "
log 1 $ \ _ = > " TypeSig \ { u n words names} : \ { r ender 90 $ pprint Nil ty} "
ignore $ for names $ \nm = > setDef ( QN ns nm) fc ty Axiom
ignore $ for names $ \nm = > setDef ( QN ns nm) fc ty Axiom
processDecl ns ( PType fc nm ty) = do
processDecl ns ( PType fc nm ty) = do
@@ -126,7 +126,7 @@ processDecl ns (PFunc fc nm used ty src) = do
top <- get
top <- get
ty <- check ( mkCtx fc) ty ( VU fc)
ty <- check ( mkCtx fc) ty ( VU fc)
ty' <- nf Nil ty
ty' <- nf Nil ty
putStrLn " pfunc \ { n m} : \ { r ender 90 $ pprint Nil ty'} = \ { s h o w s r c} "
log 1 $ \ _ = > " pfunc \ { n m} : \ { r ender 90 $ pprint Nil ty'} = \ { s h o w s r c} "
-- TODO wire through fc?
-- TODO wire through fc?
for used $ \ name = > case lookupRaw name top of
for used $ \ name = > case lookupRaw name top of
Nothing = > error fc " \ { n ame} not in scope "
Nothing = > error fc " \ { n ame} not in scope "
@@ -134,8 +134,8 @@ processDecl ns (PFunc fc nm used ty src) = do
setDef ( QN ns nm) fc ty' ( PrimFn src used)
setDef ( QN ns nm) fc ty' ( PrimFn src used)
processDecl ns ( Def fc nm clauses) = do
processDecl ns ( Def fc nm clauses) = do
putStrLn " ----- "
log 1 $ \ _ = > " ----- "
putStrLn " Def \ { s h o w n m} "
log 1 $ \ _ = > " Def \ { s h o w n m} "
top <- get
top <- get
mc <- readIORef top.metaCtx
mc <- readIORef top.metaCtx
let ( Just entry) = lookupRaw nm top
let ( Just entry) = lookupRaw nm top
@@ -143,7 +143,7 @@ processDecl ns (Def fc nm clauses) = do
let ( MkEntry fc name ty Axiom) = entry
let ( MkEntry fc name ty Axiom) = entry
| _ = > throwError $ E fc " \ { n m} already defined at \ { s h o w e n try.fc} "
| _ = > throwError $ E fc " \ { n m} already defined at \ { s h o w e n try.fc} "
putStrLn " check \ { n m} at \ { r ender 90 $ pprint Nil ty} "
log 1 $ \ _ = > " check \ { n m} at \ { r ender 90 $ pprint Nil ty} "
vty <- eval Nil CBN ty
vty <- eval Nil CBN ty
debug $ \ _ = > " \ { n m} vty is \ { s h o w v ty} "
debug $ \ _ = > " \ { n m} vty is \ { s h o w v ty} "
@@ -151,7 +151,7 @@ processDecl ns (Def fc nm clauses) = do
-- I can take LHS apart syntactically or elaborate it with an infer
-- I can take LHS apart syntactically or elaborate it with an infer
clauses' <- traverse makeClause clauses
clauses' <- traverse makeClause clauses
tm <- buildTree ( mkCtx fc) ( MkProb clauses' vty)
tm <- buildTree ( mkCtx fc) ( MkProb clauses' vty)
-- putStrLn "Ok \{render 90 $ pprint Nil tm}"
-- log 1 $ \ _ => "Ok \{render 90 $ pprint Nil tm}"
mc <- readIORef top.metaCtx
mc <- readIORef top.metaCtx
solveAutos
solveAutos
@@ -160,21 +160,21 @@ processDecl ns (Def fc nm clauses) = do
-- Day1.newt is a test case
-- Day1.newt is a test case
-- tm' <- nf Nil tm
-- tm' <- nf Nil tm
tm' <- zonk top 0 Nil tm
tm' <- zonk top 0 Nil tm
when top.verbose $ \ _ = > putStrLn " NF \ n \ { r ender 80 $ pprint Nil tm'} "
debug $ \ _ = > " NF \ n \ { r ender 80 $ pprint Nil tm'} "
-- TODO we want to keep both versions, but this is checking in addition to erasing
-- TODO we want to keep both versions, but this is checking in addition to erasing
-- currently CompileExp is also doing erasure.
-- currently CompileExp is also doing erasure.
-- TODO we need erasure info on the lambdas or to fake up an appropriate environment
-- TODO we need erasure info on the lambdas or to fake up an appropriate environment
-- and erase inside. Currently the checking is imprecise
-- and erase inside. Currently the checking is imprecise
tm'' <- erase Nil tm' Nil
tm'' <- erase Nil tm' Nil
when top.verbose $ \ _ = > putStrLn " ERASED \ n \ { r ender 80 $ pprint Nil tm'} "
debug $ \ _ = > " ERASED \ n \ { r ender 80 $ pprint Nil tm'} "
debug $ \ _ = > " Add def \ { n m} \ { r ender 90 $ pprint Nil tm'} : \ { r ender 90 $ pprint Nil ty} "
debug $ \ _ = > " Add def \ { n m} \ { r ender 90 $ pprint Nil tm'} : \ { r ender 90 $ pprint Nil ty} "
updateDef ( QN ns nm) fc ty ( Fn tm')
updateDef ( QN ns nm) fc ty ( Fn tm')
processDecl ns ( DCheck fc tm ty) = do
processDecl ns ( DCheck fc tm ty) = do
putStrLn " ----- DCheck "
log 1 $ \ _ = > " ----- DCheck "
top <- get
top <- get
putStrLn " INFO at \ { s h o w f c}: check \ { s h o w t m} at \ { s h o w t y} "
info fc " check \ { s h o w t m} at \ { s h o w t y} "
ty' <- check ( mkCtx fc) ty ( VU fc)
ty' <- check ( mkCtx fc) ty ( VU fc)
putStrLn " got type \ { r ender 90 $ pprint Nil ty'} "
putStrLn " got type \ { r ender 90 $ pprint Nil ty'} "
vty <- eval Nil CBN ty'
vty <- eval Nil CBN ty'
@@ -189,8 +189,8 @@ processDecl ns (Class classFC nm tele decls) = do
-- REVIEW maybe we can leverage Record for this
-- REVIEW maybe we can leverage Record for this
-- a couple of catches, we don't want the dotted accessors and
-- a couple of catches, we don't want the dotted accessors and
-- the self argument should be an auto-implicit
-- the self argument should be an auto-implicit
putStrLn " ----- "
log 1 $ \ _ = > " ----- "
putStrLn " Class \ { n m} "
log 1 $ \ _ = > " Class \ { n m} "
let fields = getSigs decls
let fields = getSigs decls
-- We'll need names for the telescope
-- We'll need names for the telescope
let dcName = " Mk \ { n m} "
let dcName = " Mk \ { n m} "
@@ -198,11 +198,11 @@ processDecl ns (Class classFC nm tele decls) = do
let tail = foldl mkApp ( RVar classFC nm) tele
let tail = foldl mkApp ( RVar classFC nm) tele
let dcType = teleToPi ( impTele tele) $ foldr mkPi tail fields
let dcType = teleToPi ( impTele tele) $ foldr mkPi tail fields
putStrLn " tcon type \ { r ender 90 $ pretty tcType} "
log 1 $ \ _ = > " tcon type \ { r ender 90 $ pretty tcType} "
putStrLn " dcon type \ { r ender 90 $ pretty dcType} "
log 1 $ \ _ = > " dcon type \ { r ender 90 $ pretty dcType} "
let decl = Data classFC nm tcType ( TypeSig classFC ( dcName : : Nil) dcType : : Nil)
let decl = Data classFC nm tcType ( TypeSig classFC ( dcName : : Nil) dcType : : Nil)
putStrLn " Decl: "
log 1 $ \ _ = > " Decl: "
putStrLn $ render 90 $ pretty decl
log 1 $ \ _ = > render 90 $ pretty decl
processDecl ns decl
processDecl ns decl
ignore $ for fields $ \case
ignore $ for fields $ \case
( fc,name,ty) = > do
( fc,name,ty) = > do
@@ -212,8 +212,8 @@ processDecl ns (Class classFC nm tele decls) = do
let lhs = RApp classFC lhs autoPat Auto
let lhs = RApp classFC lhs autoPat Auto
let decl = Def fc name ( ( lhs, ( RVar fc name) ) : : Nil)
let decl = Def fc name ( ( lhs, ( RVar fc name) ) : : Nil)
putStrLn " \ { n ame} : \ { r ender 90 $ pretty funType} "
log 1 $ \ _ = > " \ { n ame} : \ { r ender 90 $ pretty funType} "
putStrLn " \ { r ender 90 $ pretty decl} "
log 1 $ \ _ = > " \ { r ender 90 $ pretty decl} "
processDecl ns $ TypeSig fc ( name : : Nil) funType
processDecl ns $ TypeSig fc ( name : : Nil) funType
processDecl ns decl
processDecl ns decl
where
where
@@ -234,8 +234,8 @@ processDecl ns (Class classFC nm tele decls) = do
-- TODO - these are big, break them out into individual functions
-- TODO - these are big, break them out into individual functions
processDecl ns ( Instance instfc ty decls) = do
processDecl ns ( Instance instfc ty decls) = do
putStrLn " ----- "
log 1 $ \ _ = > " ----- "
putStrLn " Instance \ { r ender 90 $ pretty ty} "
log 1 $ \ _ = > " Instance \ { r ender 90 $ pretty ty} "
top <- get
top <- get
let tyFC = getFC ty
let tyFC = getFC ty
@@ -296,9 +296,9 @@ processDecl ns (Instance instfc ty decls) = do
setDef ( QN ns nm') fc ty' Axiom
setDef ( QN ns nm') fc ty' Axiom
let decl = ( Def fc nm' xs)
let decl = ( Def fc nm' xs)
putStrLn " *** "
log 1 $ \ _ = > " *** "
putStrLn " « \ { n m'}» : \ { r ender 90 $ pprint Nil ty'} "
log 1 $ \ _ = > " « \ { n m'}» : \ { r ender 90 $ pprint Nil ty'} "
putStrLn $ render 80 $ pretty decl
log 1 $ \ _ = > render 80 $ pretty decl
pure $ Just decl
pure $ Just decl
_ = > pure Nothing
_ = > pure Nothing
@@ -308,9 +308,9 @@ processDecl ns (Instance instfc ty decls) = do
processDecl ns decl
processDecl ns decl
let ( QN _ con') = con
let ( QN _ con') = con
let decl = Def instfc instname ( ( RVar instfc instname, mkRHS instname conTele ( RVar instfc con') ) : : Nil)
let decl = Def instfc instname ( ( RVar instfc instname, mkRHS instname conTele ( RVar instfc con') ) : : Nil)
putStrLn " SIGDECL "
log 1 $ \ _ = > " SIGDECL "
putStrLn " \ { r ender 90 $ pretty sigDecl} "
log 1 $ \ _ = > " \ { r ender 90 $ pretty sigDecl} "
putStrLn $ render 80 $ pretty decl
log 1 $ \ _ = > render 80 $ pretty decl
processDecl ns decl
processDecl ns decl
where
where
-- try to extract types of individual fields from the typeclass dcon
-- try to extract types of individual fields from the typeclass dcon
@@ -346,8 +346,8 @@ processDecl ns (ShortData fc lhs sigs) = do
let ty = foldr mkPi (RU fc) args
let ty = foldr mkPi (RU fc) args
cons <- traverse (mkDecl args Nil) sigs
cons <- traverse (mkDecl args Nil) sigs
let dataDecl = Data fc nm ty cons
let dataDecl = Data fc nm ty cons
putStrLn " SHORTDATA"
log 1 $ \ _ = > " SHORTDATA"
putStrLn " \ { r ender 90 $ pretty dataDecl} "
log 1 $ \ _ = > " \ { r ender 90 $ pretty dataDecl} "
processDecl ns dataDecl
processDecl ns dataDecl
where
where
mkPi : FC × Name → Raw → Raw
mkPi : FC × Name → Raw → Raw
@@ -371,8 +371,8 @@ processDecl ns (ShortData fc lhs sigs) = do
mkDecl args acc tm = error ( getFC tm) " Expected contructor application, got: \ { s h o w t m} "
mkDecl args acc tm = error ( getFC tm) " Expected contructor application, got: \ { s h o w t m} "
processDecl ns ( Data fc nm ty cons) = do
processDecl ns ( Data fc nm ty cons) = do
putStrLn " ----- "
log 1 $ \ _ = > " ----- "
putStrLn " Data \ { n m} "
log 1 $ \ _ = > " Data \ { n m} "
top <- get
top <- get
mc <- readIORef top.metaCtx
mc <- readIORef top.metaCtx
tyty <- check ( mkCtx fc) ty ( VU fc)
tyty <- check ( mkCtx fc) ty ( VU fc)
@@ -403,7 +403,7 @@ processDecl ns (Data fc nm ty cons) = do
setDef ( QN ns nm') fc dty ( DCon ( getArity dty) hn)
setDef ( QN ns nm') fc dty ( DCon ( getArity dty) hn)
pure $ map ( QN ns) names
pure $ map ( QN ns) names
decl = > throwError $ E ( getFC decl) " expected constructor declaration "
decl = > throwError $ E ( getFC decl) " expected constructor declaration "
putStrLn " setDef \ { n m} TCon \ { s h o w $ j o i n cnames} "
log 1 $ \ _ = > " setDef \ { n m} TCon \ { s h o w $ j o i n cnames} "
updateDef ( QN ns nm) fc tyty ( TCon ( join cnames) )
updateDef ( QN ns nm) fc tyty ( TCon ( join cnames) )
where
where
binderName : Binder → Name
binderName : Binder → Name
@@ -415,8 +415,8 @@ processDecl ns (Data fc nm ty cons) = do
checkDeclType _ = error fc " data type doesn't return U "
checkDeclType _ = error fc " data type doesn't return U "
processDecl ns ( Record recordFC nm tele cname decls) = do
processDecl ns ( Record recordFC nm tele cname decls) = do
putStrLn " ----- "
log 1 $ \ _ = > " ----- "
putStrLn " Record "
log 1 $ \ _ = > " Record "
let fields = getSigs decls
let fields = getSigs decls
let dcName = fromMaybe " Mk \ { s h o w n m} " cname
let dcName = fromMaybe " Mk \ { s h o w n m} " cname
let tcType = teleToPi tele ( RU recordFC)
let tcType = teleToPi tele ( RU recordFC)
@@ -425,11 +425,11 @@ processDecl ns (Record recordFC nm tele cname decls) = do
let dcType = teleToPi ( impTele tele) $
let dcType = teleToPi ( impTele tele) $
foldr ( \ x acc = > case the ( FC × String × Raw) x of ( fc, nm, ty) = > RPi fc ( BI fc nm Explicit Many) ty acc ) tail fields
foldr ( \ x acc = > case the ( FC × String × Raw) x of ( fc, nm, ty) = > RPi fc ( BI fc nm Explicit Many) ty acc ) tail fields
putStrLn " tcon type \ { r ender 90 $ pretty tcType} "
log 1 $ \ _ = > " tcon type \ { r ender 90 $ pretty tcType} "
putStrLn " dcon type \ { r ender 90 $ pretty dcType} "
log 1 $ \ _ = > " dcon type \ { r ender 90 $ pretty dcType} "
let decl = Data recordFC nm tcType ( TypeSig recordFC ( dcName : : Nil) dcType : : Nil)
let decl = Data recordFC nm tcType ( TypeSig recordFC ( dcName : : Nil) dcType : : Nil)
putStrLn " Decl: "
log 1 $ \ _ = > " Decl: "
putStrLn $ render 90 $ pretty decl
log 1 $ \ _ = > render 90 $ pretty decl
processDecl ns decl
processDecl ns decl
ignore $ for fields $ \case
ignore $ for fields $ \case
( fc,name,ty) = > do
( fc,name,ty) = > do
@@ -442,8 +442,8 @@ processDecl ns (Record recordFC nm tele cname decls) = do
-- let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
-- let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
-- let lhs = RApp recordFC lhs autoPat Explicit
-- let lhs = RApp recordFC lhs autoPat Explicit
-- let decl = Def fc name [(lhs, (RVar fc name))]
-- let decl = Def fc name [(lhs, (RVar fc name))]
-- putStrLn "\{name} : \{render 90 $ pretty funType}"
-- log 1 $ \ _ => "\{name} : \{render 90 $ pretty funType}"
-- putStrLn "\{render 90 $ pretty decl}"
-- log 1 $ \ _ => "\{render 90 $ pretty decl}"
-- processDecl ns $ TypeSig fc (name :: Nil) funType
-- processDecl ns $ TypeSig fc (name :: Nil) funType
-- processDecl ns decl
-- processDecl ns decl
@@ -452,7 +452,7 @@ processDecl ns (Record recordFC nm tele cname decls) = do
let lhs = foldl ( \acc x = > case the ( BindInfo × Raw) x of ( BI fc' nm icit quant, _) = > RApp fc' acc ( RVar fc' nm) Implicit) ( RVar fc pname) tele
let lhs = foldl ( \acc x = > case the ( BindInfo × Raw) x of ( BI fc' nm icit quant, _) = > RApp fc' acc ( RVar fc' nm) Implicit) ( RVar fc pname) tele
let lhs = RApp recordFC lhs autoPat Explicit
let lhs = RApp recordFC lhs autoPat Explicit
let pdecl = Def fc pname ( ( lhs, ( RVar fc name) ) : : Nil)
let pdecl = Def fc pname ( ( lhs, ( RVar fc name) ) : : Nil)
putStrLn " \ { p n ame} : \ { r ender 90 $ pretty funType} "
log 1 $ \ _ = > " \ { p n ame} : \ { r ender 90 $ pretty funType} "
putStrLn " \ { r ender 90 $ pretty pdecl} "
log 1 $ \ _ = > " \ { r ender 90 $ pretty pdecl} "
processDecl ns $ TypeSig fc ( pname : : Nil) funType
processDecl ns $ TypeSig fc ( pname : : Nil) funType
processDecl ns pdecl
processDecl ns pdecl