From 6b1eef86a70c1d0552030741ccbb278298d7354d Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 4 Jan 2025 09:26:33 -0800 Subject: [PATCH] Newt in Newt compiles (but does not run) --- done/Data/List1.newt | 17 + done/Data/SortedMap.newt | 3 + done/Lib/Compile.newt | 361 +++++++++ done/Lib/CompileExp.newt | 170 +++++ done/Lib/Elab.newt | 1508 +++++++++++++++++++++++++++++++++++++ done/Lib/Eval.newt | 5 + done/Lib/Parser.newt | 18 +- done/Lib/ProcessDecl.newt | 471 ++++++++++++ done/Lib/Types.newt | 31 +- done/Lib/Util.newt | 6 +- done/Main.newt | 234 ++++++ done/Node.newt | 34 + done/Test/Parser.newt | 26 + newt/Prelude.newt | 44 +- newt/SortedMap.newt | 3 + scripts/translate.sh | 2 +- src/Lib/Compile.idr | 28 +- src/Lib/Elab.idr | 81 +- src/Lib/Eval.idr | 1 + src/Lib/ProcessDecl.idr | 12 +- src/Lib/Util.idr | 6 +- 21 files changed, 2970 insertions(+), 91 deletions(-) create mode 100644 done/Lib/Compile.newt create mode 100644 done/Lib/CompileExp.newt create mode 100644 done/Lib/Elab.newt create mode 100644 done/Lib/ProcessDecl.newt create mode 100644 done/Main.newt create mode 100644 done/Node.newt create mode 100644 done/Test/Parser.newt diff --git a/done/Data/List1.newt b/done/Data/List1.newt index 1d2c573..a42ab28 100644 --- a/done/Data/List1.newt +++ b/done/Data/List1.newt @@ -8,3 +8,20 @@ record List1 a where constructor _:::_ head1 : a tail1 : List a + +split1 : String → String → List1 String +split1 str by = case split str by of + Nil => str ::: Nil + x :: xs => x ::: xs + +unsnoc : ∀ a. List1 a → List a × a +unsnoc {a} (x ::: xs) = go x xs + where + go : a → List a → List a × a + go x Nil = (Nil, x) + go x (y :: ys) = let (as, a) = go y ys in (x :: as, a) + +splitFileName : String → String × String +splitFileName fn = case split1 fn "." of + part ::: Nil => (part, "") + xs => mapFst (joinBy ".") $ unsnoc xs diff --git a/done/Data/SortedMap.newt b/done/Data/SortedMap.newt index ea477b3..f076698 100644 --- a/done/Data/SortedMap.newt +++ b/done/Data/SortedMap.newt @@ -200,3 +200,6 @@ foldMap f m Nil = m foldMap f m ((a,b) :: xs) = case lookupMap a m of Nothing => foldMap f (updateMap a b m) xs Just (_, b') => foldMap f (updateMap a (f b' b) m) xs + +listValues : ∀ k v. SortedMap k v → List v +listValues sm = map snd $ toList sm diff --git a/done/Lib/Compile.newt b/done/Lib/Compile.newt new file mode 100644 index 0000000..a046ba1 --- /dev/null +++ b/done/Lib/Compile.newt @@ -0,0 +1,361 @@ +-- TODO Audit how much "outside" stuff could pile up in the continuation. +module Lib.Compile + +import Lib.Types +import Lib.Prettier +import Lib.CompileExp +import Lib.TopContext +import Data.String +import Data.Maybe +import Data.Int + +data StKind = Plain | Return | Assign String + +JSStmt : StKind -> U +JSExp : U + +data JAlt : U where + JConAlt : ∀ e. String -> JSStmt e -> JAlt + JDefAlt : ∀ e. JSStmt e -> JAlt + JLitAlt : ∀ e. JSExp -> JSStmt e -> JAlt + +data JSExp : U where + LitArray : List JSExp -> JSExp + LitObject : List (String × JSExp) -> JSExp + LitString : String -> JSExp + LitInt : Int -> JSExp + Apply : JSExp -> List JSExp -> JSExp + Var : String -> JSExp + JLam : List String -> JSStmt Return -> JSExp + JUndefined : JSExp + Index : JSExp -> JSExp -> JSExp + Dot : JSExp -> String -> JSExp + +data JSStmt : StKind -> U where + -- Maybe make this a snoc... + JSnoc : ∀ a. JSStmt Plain -> JSStmt a -> JSStmt a + JPlain : JSExp -> JSStmt Plain + JConst : (nm : String) -> JSExp -> JSStmt Plain + JReturn : JSExp -> JSStmt Return + JLet : (nm : String) -> JSStmt (Assign nm) -> JSStmt Plain -- need somebody to assign + JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm) + -- TODO - switch to Int tags + -- FIXME add e to JAlt (or just drop it?) + JCase : ∀ a. JSExp -> List JAlt -> JSStmt a + -- throw can't be used + JError : ∀ a. String -> JSStmt a + +Cont : StKind → U +Cont e = JSExp -> JSStmt e + +-- JSEnv contains `Var` for binders or `Dot` for destructured data. It +-- used to translate binders +record JSEnv where + constructor MkEnv + jsenv : List JSExp + depth : Int + +-- this was like this, are we not using depth? +push : JSEnv -> JSExp -> JSEnv +push (MkEnv env depth) exp = MkEnv (exp :: env) depth + +emptyJSEnv : JSEnv +emptyJSEnv = MkEnv Nil 0 + +litToJS : Literal -> JSExp +litToJS (LString str) = LitString str +litToJS (LChar c) = LitString $ pack (c :: Nil) +litToJS (LInt i) = LitInt i + +-- Stuff nm.h1, nm.h2, ... into environment +-- TODO consider JSExp instead of nm, so we can have $foo.h1 instead of assigning a sc. +mkEnv : String -> Int -> JSEnv -> List String -> JSEnv +mkEnv nm k env Nil = env +mkEnv nm k env (x :: xs) = mkEnv nm (1 + k) (push env (Dot (Var nm) "h\{show k}")) xs + +envNames : Env -> List String + +-- given a name, find a similar one that doesn't shadow in Env +freshName : String -> JSEnv -> String +freshName nm env = if free env.jsenv nm then nm else go nm 1 + where + free : List JSExp -> String -> Bool + free Nil nm = True + free (Var n :: xs) nm = if n == nm then False else free xs nm + free (_ :: xs) nm = free xs nm + + go : String -> Int -> String + go nm k = let nm' = "\{nm}\{show k}" in if free env.jsenv nm' then nm' else go nm (1 + k) + +freshName' : String -> JSEnv -> (String × JSEnv) +freshName' nm env = + let nm' = freshName nm env -- "\{nm}$\{show $ length env}" + env' = push env (Var nm') + in (nm', env') + +freshNames : List String -> JSEnv -> (List String × JSEnv) +freshNames nms env = go nms env Lin + where + go : List Name -> JSEnv -> SnocList Name -> (List String × JSEnv) + go Nil env acc = (acc <>> Nil, env) + go (n :: ns) env acc = + let (n', env') = freshName' n env + in go ns env' (acc :< n') + +-- This is inspired by A-normalization, look into the continuation monad +-- There is an index on JSStmt, adopted from Stefan Hoeck's code. +-- +-- Here we turn a Term into a statement (which may be a sequence of statements), there +-- is a continuation, which turns the final JSExpr into a JSStmt, and the function returns +-- a JSStmt, wrapping recursive calls in JSnoc if necessary. +termToJS : ∀ e. JSEnv -> CExp -> Cont e -> JSStmt e +termToJS env (CBnd k) f = case getAt (cast k) env.jsenv of + (Just e) => f e + Nothing => fatalError "Bad bounds" +termToJS env CErased f = f JUndefined +termToJS env (CLam nm t) f = + let (nm',env') = freshName' nm env -- "\{nm}$\{show $ length env}" + in f $ JLam (nm' :: Nil) (termToJS env' t JReturn) +termToJS env (CFun nms t) f = + let (nms', env') = freshNames nms env + in f $ JLam nms' (termToJS env' t JReturn) +termToJS env (CRef nm) f = f $ Var nm +termToJS env (CMeta k) f = f $ LitString "META \{show k}" +termToJS env (CLit lit) f = f (litToJS lit) +-- if it's a var, just use the original +termToJS env (CLet nm (CBnd k) u) f = case getAt (cast k) env.jsenv of + Just e => termToJS (push env e) u f + Nothing => fatalError "bad bounds" +termToJS env (CLet nm t u) f = + let nm' = freshName nm env + env' = push env (Var nm') + -- If it's a simple term, use const + in case termToJS env t (JAssign nm') of + (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) + t' => JSnoc (JLet nm' t') (termToJS env' u f) +termToJS env (CLetRec nm t u) f = + let nm' = freshName nm env + env' = push env (Var nm') + -- If it's a simple term, use const + in case termToJS env' t (JAssign nm') of + (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) + t' => JSnoc (JLet nm' t') (termToJS env' u f) + +termToJS env (CApp t args etas) f = termToJS env t (\ t' => (argsToJS t' args Lin f)) -- (f (Apply t' args')))) + where + etaExpand : JSEnv -> Nat -> SnocList JSExp -> JSExp -> JSExp + etaExpand env Z args tm = Apply tm (args <>> Nil) + etaExpand env (S etas) args tm = + let nm' = freshName "eta" env + env' = push env (Var nm') + in JLam (nm' :: Nil) $ JReturn $ etaExpand (push env (Var nm')) etas (args :< Var nm') tm + + argsToJS : ∀ e. JSExp -> List CExp -> SnocList JSExp -> (JSExp -> JSStmt e) -> JSStmt e + argsToJS tm Nil acc k = k (etaExpand env (cast etas) acc tm) + -- k (acc <>> Nil) + argsToJS tm (x :: xs) acc k = termToJS env x (\ x' => argsToJS tm xs (acc :< x') k) + + +termToJS {e} env (CCase t alts) f = + -- need to assign the scrutinee to a variable (unless it is a var already?) + -- and add (Bnd -> JSExpr map) + -- TODO default case, let's drop the extra field. + + termToJS env t $ \case + (Var nm) => maybeCaseStmt env nm alts + t' => do + -- TODO refactor nm to be a JSExp with Var{} or Dot{} + -- FIXME sc$ seemed to shadow something else, lets get this straightened out + -- we need freshName names that are not in env (i.e. do not play in debruijn) + let nm = "_sc$\{show env.depth}" + let env' = MkEnv env.jsenv (1 + env.depth) + JSnoc (JConst nm t') (maybeCaseStmt env' nm alts) + + where + termToJSAlt : JSEnv -> String -> CAlt -> JAlt + termToJSAlt env nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f) + -- intentionally reusing scrutinee name here + termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (env) u f) + termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f) + + maybeCaseStmt : JSEnv -> String -> List CAlt -> JSStmt e + -- If there is a single alt, assume it matched + maybeCaseStmt env nm ((CConAlt _ args u) :: Nil) = (termToJS (mkEnv nm 0 env args) u f) + maybeCaseStmt env nm alts@(CLitAlt _ _ :: _) = + (JCase (Var nm) (map (termToJSAlt env nm) alts)) + maybeCaseStmt env nm alts = + (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts)) + +jsKeywords : List String +jsKeywords = ( + "break" :: "case" :: "catch" :: "continue" :: "debugger" :: "default" :: "delete" :: "do" :: "else" :: + "finally" :: "for" :: "function" :: "if" :: "in" :: "instanceof" :: "new" :: "return" :: "switch" :: + "this" :: "throw" :: "try" :: "typeof" :: "var" :: "void" :: "while" :: "with" :: + "class" :: "const" :: "enum" :: "export" :: "extends" :: "import" :: "super" :: + "implements" :: "class" :: "let" :: "package" :: "private" :: "protected" :: "public" :: + "static" :: "yield" :: + "null" :: "true" :: "false" :: + -- might not be a big issue with namespaces on names now. + "String" :: "Number" :: "Array" :: "BigInt" :: Nil) + + +-- escape identifiers for js +jsIdent : String -> Doc +jsIdent id = if elem id jsKeywords then text ("$" ++ id) else text $ pack $ fix (unpack id) + where + fix : List Char -> List Char + fix Nil = Nil + fix (x :: xs) = + if isAlphaNum x || x == '_' then + x :: fix xs + -- make qualified names more readable + else if x == '.' then '_' :: fix xs + else if x == '$' then + '$' :: '$' :: fix xs + else + '$' :: (toHex (cast x)) ++ fix xs + +stmtToDoc : ∀ e. JSStmt e -> Doc + + +expToDoc : JSExp -> Doc +expToDoc (LitArray xs) = fatalError "TODO - LitArray to doc" +expToDoc (LitObject xs) = text "{" <+> folddoc (\ a e => a ++ text ", " <+/> e) (map entry xs) <+> text "}" + where + entry : (String × JSExp) -> Doc + -- TODO quote if needed + entry (nm, exp) = jsIdent nm ++ text ":" <+> expToDoc exp + +expToDoc (LitString str) = text $ quoteString str +expToDoc (LitInt i) = text $ show i +-- TODO add precedence +expToDoc (Apply x@(JLam _ _) xs) = text "(" ++ expToDoc x ++ text ")" ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")" +expToDoc (Apply x xs) = expToDoc x ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")" +expToDoc (Var nm) = jsIdent nm +expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> text "(" ++ expToDoc exp ++ text ")" +expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> bracket "{" (stmtToDoc body) "}" +expToDoc JUndefined = text "undefined" +expToDoc (Index obj ix) = expToDoc obj ++ text "(" ++ expToDoc ix ++ text " :: Nil)" +expToDoc (Dot obj nm) = expToDoc obj ++ text "." ++ jsIdent nm + +caseBody : ∀ e. JSStmt e -> Doc +caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt) +-- caseBody {e = Return} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt) +caseBody {e} stmt@(JCase _ _) = nest 2 (line ++ stmtToDoc stmt text "break;") +caseBody stmt = line ++ text "{" ++ nest 2 (line ++ stmtToDoc stmt text "break;") text "}" + +altToDoc : JAlt -> Doc +altToDoc (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ text ":" ++ caseBody stmt +altToDoc (JDefAlt stmt) = text "default" ++ text ":" ++ caseBody stmt +altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ text ":" ++ caseBody stmt + +stmtToDoc (JSnoc x y) = stmtToDoc x stmtToDoc y +stmtToDoc (JPlain x) = expToDoc x ++ text ";" +-- I might not need these split yet. +stmtToDoc (JLet nm body) = text "let" <+> jsIdent nm ++ text ";" stmtToDoc body +stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";" +stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";") +stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";" +stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ text ");" +stmtToDoc (JCase sc alts) = + text "switch (" ++ expToDoc sc ++ text ")" <+> bracket "{" (stack $ map altToDoc alts) "}" + +mkArgs : Nat -> List String -> List String +mkArgs Z acc = acc +mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc) + +dcon : QName -> Nat -> Doc +dcon qn@(QN ns nm) Z = stmtToDoc $ JConst (show qn) $ LitObject (("tag", LitString nm) :: Nil) +dcon qn@(QN ns nm) arity = + let args = mkArgs arity Nil + obj = ("tag", LitString nm) :: map (\x => (x, Var x)) args + in stmtToDoc $ JConst (show qn) (JLam args (JReturn (LitObject obj))) + +-- use iife to turn stmts into expr +maybeWrap : JSStmt Return -> JSExp +maybeWrap (JReturn exp) = exp +maybeWrap stmt = Apply (JLam Nil stmt) Nil + +entryToDoc : TopEntry -> M Doc +entryToDoc (MkEntry _ name ty (Fn tm)) = do + debug $ \ _ => "compileFun \{render 90 $ pprint Nil tm}" + ct <- compileFun tm + let exp = maybeWrap $ termToJS emptyJSEnv ct JReturn + pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";" +entryToDoc (MkEntry _ name type Axiom) = pure $ text "" +entryToDoc (MkEntry _ name type (TCon strs)) = pure $ dcon name (piArity type) +entryToDoc (MkEntry _ name type (DCon arity str)) = pure $ dcon name (cast arity) +entryToDoc (MkEntry _ name type PrimTCon) = pure $ dcon name (piArity type) +entryToDoc (MkEntry _ name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent (show name) <+> text "=" <+> text src + + +process : (List QName × List Doc) -> QName -> M (List QName × List Doc) +walkTm : Tm -> (List QName × List Doc) -> M (List QName × List Doc) +walkAlt : (List QName × List Doc) -> CaseAlt -> M (List QName × List Doc) + +walkAlt acc (CaseDefault t) = walkTm t acc +walkAlt acc (CaseCons name args t) = walkTm t acc +walkAlt acc (CaseLit lit t) = walkTm t acc + + +walkTm (Ref x nm y) acc = process acc nm +walkTm (Lam x str _ _ t) acc = walkTm t acc +walkTm (App x t u) acc = walkTm u acc >>= walkTm t +walkTm (Pi x str icit y t u) acc = walkTm u acc >>= walkTm t +walkTm (Let x str t u) acc = walkTm u acc >>= walkTm t +walkTm (LetRec x str _ t u) acc = walkTm u acc >>= walkTm t +walkTm (Case x t alts) acc = foldlM walkAlt acc alts +walkTm _ acc = pure acc + +-- This version (call `reverse ∘ snd <$> process "main" (Nil × Nil)`) will do dead +-- code elimination, but the Prelude js primitives are reaching for +-- stuff like True, False, MkUnit, fs which get eliminated +process (done,docs) nm = do + let (False) = elem nm done | _ => pure (done,docs) + top <- get + case lookup nm top of + Nothing => error emptyFC "\{show nm} not in scope" + Just entry@(MkEntry _ name ty (PrimFn src used)) => do + (done,docs) <- foldlM assign (nm :: done, docs) used + edoc <- entryToDoc entry + pure (done, edoc :: docs) + Just (MkEntry _ name ty (Fn tm)) => do + debug $ \ _ => "compileFun \{render 90 $ pprint Nil tm}" + ct <- compileFun tm + -- If ct has zero arity and is a compount expression, this fails.. + let exp = maybeWrap $ termToJS emptyJSEnv ct JReturn + let doc = text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";" + (done,docs) <- walkTm tm (nm :: done, docs) + pure (done, doc :: docs) + Just entry => do + edoc <- entryToDoc entry + pure (nm :: done, edoc :: docs) + where + assign : (List QName × List Doc) -> String -> M (List QName × List Doc) + assign (done, docs) nm = do + top <- get + case lookupRaw nm top of + Nothing => pure (done, docs) + (Just (MkEntry fc name type def)) => do + let tag = QN Nil nm + let (False) = elem tag done | _ => pure (done,docs) + (done,docs) <- process (done, docs) name + let doc = text "const" <+> jsIdent nm <+> text "=" <+> jsIdent (show name) ++ text ";" + pure (tag :: done, doc :: docs) + + + + +compile : M (List Doc) +compile = do + top <- get + case lookupRaw "main" top of + Just (MkEntry fc name type def) => do + tmp <- snd <$> process (Nil, Nil) name + let exec = stmtToDoc $ JPlain $ Apply (Var $ show name) Nil + pure $ reverse (exec :: tmp) + -- If there is no main, compile everything for the benefit of the playground + Nothing => do + top <- get + traverse entryToDoc $ map snd $ toList top.defs + diff --git a/done/Lib/CompileExp.newt b/done/Lib/CompileExp.newt new file mode 100644 index 0000000..0283008 --- /dev/null +++ b/done/Lib/CompileExp.newt @@ -0,0 +1,170 @@ +-- First pass of compilation +-- - work out arities and fully apply functions / constructors (currying) +-- currying is problemmatic because we need to insert lambdas (η-expand) and +-- it breaks all of the de Bruijn indices +-- - expand metas (this is happening earlier) +-- - erase stuff (there is another copy that essentially does the same thing) +-- I could make names unique (e.q. on lambdas), but I might want that to vary per backend? +module Lib.CompileExp + +import Data.List + +import Lib.Types -- Name / Tm +import Lib.TopContext +import Lib.Prettier +import Lib.Util + + +CExp : U + + +data CAlt : U where + CConAlt : String -> List String -> CExp -> CAlt + -- REVIEW keep var name? + CDefAlt : CExp -> CAlt + -- literal + CLitAlt : Literal -> CExp -> CAlt + +data CExp : U where + CBnd : Int -> CExp + CLam : Name -> CExp -> CExp + CFun : List Name -> CExp -> CExp + -- REVIEW This feels like a hack, but if we put CLam here, the + -- deBruijn gets messed up in code gen + CApp : CExp -> List CExp -> Int -> CExp + -- TODO make DCon/TCon app separate so we can specialize + -- U / Pi are compiled to type constructors + CCase : CExp -> List CAlt -> CExp + CRef : Name -> CExp + CMeta : Int -> CExp + CLit : Literal -> CExp + CLet : Name -> CExp -> CExp -> CExp + CLetRec : Name -> CExp -> CExp -> CExp + CErased : CExp + +-- I'm counting Lam in the term for arity. This matches what I need in +-- code gen. + +lamArity : Tm -> Nat +lamArity (Lam _ _ _ _ t) = S (lamArity t) +lamArity _ = Z + + +piArity : Tm -> Nat +piArity (Pi _ _ _ quant _ b) = S (piArity b) +piArity _ = Z + +-- This is how much we want to curry at top level +-- leading lambda Arity is used for function defs and metas +-- TODO - figure out how this will work with erasure +arityForName : FC -> QName -> M Nat +arityForName fc nm = do + top <- get + case lookup nm top of + -- let the magic hole through for now (will generate bad JS) + Nothing => error fc "Name \{show nm} not in scope" + (Just (MkEntry _ name type Axiom)) => pure Z + (Just (MkEntry _ name type (TCon strs))) => pure $ piArity type + (Just (MkEntry _ name type (DCon k str))) => pure $ cast k + (Just (MkEntry _ name type (Fn t))) => pure $ lamArity t + (Just (MkEntry _ name type (PrimTCon))) => pure $ piArity type + -- Assuming a primitive can't return a function + (Just (MkEntry _ name type (PrimFn t used))) => pure $ piArity type + + +compileTerm : Tm -> M CExp + +-- need to eta out extra args, fill in the rest of the apps +apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp +-- out of args, make one up (fix that last arg) +apply t Nil acc (S k) ty = pure $ CApp t (acc <>> Nil) (1 + cast k) + -- inserting Clam, index wrong? + -- CLam "eta\{show k}" !(apply t Nil (acc :< CBnd k) k ty) +apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) = apply t xs (acc :< CErased) k b +apply t (x :: xs) acc (S k) (Pi y str icit Many a b) = apply t xs (acc :< x) k b +-- see if there is anything we have to handle here +apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}. Overapplied function that escaped type checking?" +-- once we hit zero, we fold the rest +apply t ts acc Z ty = go (CApp t (acc <>> Nil) 0) ts + where + go : CExp -> List CExp -> M CExp + -- drop zero arg call + go (CApp t Nil 0) args = go t args + go t Nil = pure t + go t (arg :: args) = go (CApp t (arg :: Nil) 0) args + +-- apply : CExp -> List CExp -> SnocList CExp -> Int -> M CExp +-- -- out of args, make one up +-- apply t Nil acc (S k) = pure $ +-- CLam "eta\{show k}" !(apply t Nil (acc :< CBnd k) k) +-- apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k +-- apply t ts acc 0 = go (CApp t (acc <>> Nil)) ts +-- where +-- go : CExp -> List CExp -> M CExp +-- -- drop zero arg call +-- go (CApp t Nil) args = go t args +-- go t Nil = pure t +-- go t (arg :: args) = go (CApp t (arg :: Nil)) args + +compileTerm (Bnd _ k) = pure $ CBnd k +-- need to eta expand to arity +compileTerm t@(Ref fc nm _) = do + top <- get + let (Just (MkEntry _ _ type _)) = lookup nm top + | Nothing => error fc "Undefined name \{show nm}" + arity <- arityForName fc nm + apply (CRef (show nm)) Nil Lin arity type + +compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME +compileTerm (Lam _ nm _ _ t) = CLam nm <$> compileTerm t +compileTerm tm@(App _ _ _) = case funArgs tm of + (Meta _ k, args) => do + -- this will be undefined, should only happen for use metas + pure $ CApp (CRef "Meta\{show k}") Nil 0 + (t@(Ref fc nm _), args) => do + args' <- traverse compileTerm args + arity <- arityForName fc nm + top <- get + let (Just (MkEntry _ _ type _)) = lookup nm top + | Nothing => error fc "Undefined name \{show nm}" + apply (CRef (show nm)) args' Lin arity type + (t, args) => do + debug $ \ _ => "apply other \{render 90 $ pprint Nil t}" + t' <- compileTerm t + args' <- traverse compileTerm args + apply t' args' Lin Z (UU emptyFC) + -- error (getFC t) "Don't know how to apply \{showTm t}" +compileTerm (UU _) = pure $ CRef "U" +compileTerm (Pi _ nm icit rig t u) = do + t' <- compileTerm t + u' <- compileTerm u + pure $ CApp (CRef "PiType") (t' :: u' :: Nil) 0 +compileTerm (Case _ t alts) = do + t' <- compileTerm t + alts' <- for alts $ \case + CaseDefault tm => CDefAlt <$> compileTerm tm + -- we use the base name for the tag, some primitives assume this + CaseCons (QN ns nm) args tm => CConAlt nm args <$> compileTerm tm + CaseLit lit tm => CLitAlt lit <$> compileTerm tm + pure $ CCase t' alts' +compileTerm (Lit _ lit) = pure $ CLit lit +compileTerm (Let _ nm t u) = do + t' <- compileTerm t + u' <- compileTerm u + pure $ CLet nm t' u' +compileTerm (LetRec _ nm _ t u) = do + t' <- compileTerm t + u' <- compileTerm u + pure $ CLetRec nm t' u' +compileTerm (Erased _) = pure CErased + + +compileFun : Tm -> M CExp +compileFun tm = go tm Lin + where + go : Tm -> SnocList String -> M CExp + go (Lam _ nm _ _ t) acc = go t (acc :< nm) + go tm Lin = compileTerm tm + go tm args = CFun (args <>> Nil) <$> compileTerm tm + + diff --git a/done/Lib/Elab.newt b/done/Lib/Elab.newt new file mode 100644 index 0000000..8e99bc8 --- /dev/null +++ b/done/Lib/Elab.newt @@ -0,0 +1,1508 @@ +module Lib.Elab + +import Lib.Parser.Impl +import Lib.Prettier +import Data.List +import Data.String +import Data.IORef +import Lib.Types +import Lib.Eval +import Lib.TopContext +import Lib.Syntax + + +vprint : Context -> Val -> M String +vprint ctx v = do + tm <- quote (length' ctx.env) v + pure $ render 90 $ pprint (names ctx) tm + + +-- collectDecl collects multiple Def for one function into one + +collectDecl : List Decl -> List Decl +collectDecl Nil = Nil +collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) = + if nm == nm' then collectDecl (Def fc nm (cl ++ cl') :: xs) + else (Def fc nm cl :: collectDecl rest) +collectDecl (x :: xs) = x :: collectDecl xs + +rpprint : List String → Tm → String +rpprint names tm = render 90 $ pprint names tm + +-- renaming +-- dom gamma ren +data Pden = PR Int Int (List Int) + +showCtx : Context -> M String +showCtx ctx = + unlines ∘ reverse <$> go (names ctx) 0 (reverse $ zip ctx.env ctx.types) Nil + where + isVar : Int -> Val -> Bool + isVar k (VVar _ k' Lin) = k == k' + isVar _ _ = False + + go : List String -> Int -> List (Val × String × Val) -> List String -> M (List String) + go _ _ Nil acc = pure acc + go names k ((v, n, ty) :: xs) acc = if isVar k v + -- TODO - use Doc and add <+/> as appropriate to printing + then do + tty <- quote ctx.lvl ty + go names (1 + k) xs (" \{n} : \{rpprint names tty}" :: acc) + else do + tm <- quote ctx.lvl v + tty <- quote ctx.lvl ty + go names (1 + k) xs (" \{n} = \{rpprint names tm} : \{rpprint names tty}" :: acc) + +dumpCtx : Context -> M String +dumpCtx ctx = do + let names = (map fst ctx.types) + -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. + env <- for (zip ctx.env ctx.types) $ \case + (v, n, ty) => do + sty <- vprint ctx ty + sv <- vprint ctx v + pure " \{n} : \{sty} = \{sv}" + let msg = unlines (reverse env) -- ++ " -----------\n" ++ " goal \{rpprint names ty'}" + pure msg + + + +-- return Bnd and type for name + +lookupName : Context -> String -> Maybe (Tm × Val) +lookupName ctx name = go 0 ctx.types + where + go : Int -> List (String × Val) -> Maybe (Tm × Val) + go ix Nil = Nothing + -- FIXME - we should stuff a Binder of some sort into "types" + go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (1 + ix) xs + + +lookupDef : Context -> String -> Maybe Val +lookupDef ctx name = go 0 ctx.types ctx.env + where + go : Int -> List (String × Val) -> List Val -> Maybe Val + go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs + go ix _ _ = Nothing + + +-- IORef for metas needs IO + +forceMeta : Val -> M Val +forceMeta (VMeta fc ix sp) = do + meta <- lookupMeta ix + case meta of + (Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp) + (Solved _ k t) => vappSpine t sp >>= forceMeta +forceMeta x = pure x + + +record UnifyResult where + constructor MkResult + -- wild guess here - lhs is a VVar + constraints : List (Int × Val) + +instance Semigroup UnifyResult where + (MkResult cs) <+> (MkResult cs') = MkResult (cs ++ cs') + +instance Monoid UnifyResult where + neutral = MkResult Nil + +data UnifyMode = UNormal | UPattern + + + +check : Context -> Raw -> Val -> M Tm + + +unifyCatch : FC -> Context -> Val -> Val -> M Unit + +-- Check that the arguments are not explicit and the type constructor in codomain matches +-- Later we will build a table of codomain type, and maybe make the user tag the candidates +-- like Idris does with %hint +isCandidate : Val -> Tm -> Bool +isCandidate ty (Pi fc nm Explicit rig t u) = False +isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u +isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm' +isCandidate ty (App fc t u) = isCandidate ty t +isCandidate _ _ = False + +-- This is a crude first pass + +findMatches : Context -> Val -> List TopEntry -> M (List String) +findMatches ctx ty Nil = pure Nil +findMatches ctx ty ((MkEntry _ name type def) :: xs) = do + let (True) = isCandidate ty type | False => findMatches ctx ty xs + top <- get + -- let ctx = mkCtx (getFC ty) + -- FIXME we're restoring state, but the INFO logs have already been emitted + -- Also redo this whole thing to run during elab, recheck constraints, etc. + mc <- readIORef top.metaCtx + catchError(do + -- TODO sort out the FC here + let fc = getFC ty + debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}" + -- This check is solving metas, so we save mc below in case we want this solution + -- tm <- check (mkCtx fc) (RVar fc name) ty + -- FIXME RVar should optionally have qualified names + let (QN ns nm) = name + tm <- check ctx (RVar fc nm) ty + debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}" + writeIORef top.metaCtx mc + (_::_ nm) <$> findMatches ctx ty xs) + (\ err => do + debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}" + writeIORef top.metaCtx mc + findMatches ctx ty xs) + + +contextMatches : Context -> Val -> M (List (Tm × Val)) +contextMatches ctx ty = go (zip ctx.env ctx.types) + where + go : List (Val × String × Val) -> M (List (Tm × Val)) + go Nil = pure Nil + go ((tm, nm, vty) :: xs) = do + type <- quote ctx.lvl vty + let (True) = isCandidate ty type | False => go xs + top <- get + mc <- readIORef top.metaCtx + catchError(do + debug $ \ _ => "TRY context \{nm} : \{rpprint (names ctx) type} for \{show ty}" + unifyCatch (getFC ty) ctx ty vty + mc' <- readIORef top.metaCtx + writeIORef top.metaCtx mc + tm <- quote ctx.lvl tm + (_::_ (tm, vty)) <$> go xs) + (\ err => do + debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}" + writeIORef top.metaCtx mc + go xs) + + +getArity : Tm -> Int +getArity (Pi x str icit rig t u) = 1 + getArity u +-- Ref or App (of type constructor) are valid +getArity _ = 0 + +-- Can metas live in context for now? +-- We'll have to be able to add them, which might put gamma in a ref + + + +-- Makes the arg for `solve` when we solve an auto +makeSpine : Int -> List BD -> SnocList Val +makeSpine k Nil = Lin +makeSpine k (Defined :: xs) = makeSpine (k - 1) xs +makeSpine k (Bound :: xs) = makeSpine (k - 1) xs :< VVar emptyFC (k - 1) Lin + + +solve : Env -> (k : Int) -> SnocList Val -> Val -> M Unit + + + +trySolveAuto : MetaEntry -> M Bool +trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do + debug $ \ _ => "TRYAUTO solving \{show k} : \{show ty}" + -- fill in solved metas in type + x <- quote ctx.lvl ty + ty <- eval ctx.env CBN x + debug $ \ _ => "AUTO ---> \{show ty}" + -- we want the context here too. + top <- get + Nil <- contextMatches ctx ty + | ((tm, vty) :: Nil) => do + unifyCatch (getFC ty) ctx ty vty + val <- eval ctx.env CBN tm + debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}" + let sp = makeSpine ctx.lvl ctx.bds + solve ctx.env k sp val + pure True + | res => do + debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}" + pure False + (nm :: Nil) <- findMatches ctx ty $ map snd $ toList top.defs + | res => do + debug $ \ _ => "FAILED to solve \{show ty}, matches: \{show res}" + pure False + tm <- check ctx (RVar fc nm) ty + val <- eval ctx.env CBN tm + debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}" + let sp = makeSpine ctx.lvl ctx.bds + solve ctx.env k sp val + pure True +trySolveAuto _ = pure False + +-- export +-- solveAutos : Int -> List MetaEntry -> M Unit +-- solveAutos mstart Nil = pure MkUnit +-- solveAutos mstart (entry :: es) = do +-- res <- trySolveAuto entry +-- -- idris is inlining this and blowing stack? +-- if res +-- then do +-- top <- get +-- mc <- readIORef top.metaCtx +-- let mlen = length mc.metas `minus` mstart +-- solveAutos mstart (take mlen mc.metas) +-- else +-- solveAutos mstart es + + +-- Called from ProcessDecl, this was popping the stack, the tail call optimization doesn't +-- handle the traversal of the entire meta list. I've turned the restart into a trampoline +-- and filtered it down to unsolved autos. + +solveAutos : Int -> M Unit +solveAutos mstart = do + top <- get + mc <- readIORef top.metaCtx + let mlen = length' mc.metas - mstart + res <- run $ filter isAuto (take (cast mlen) mc.metas) + if res then solveAutos mstart else pure MkUnit + where + isAuto : MetaEntry -> Bool + isAuto (Unsolved fc k ctx x AutoSolve xs) = True + isAuto _ = False + + run : List MetaEntry -> M Bool + run Nil = pure False + run (e :: es) = do + res <- trySolveAuto e + if res then pure True else run es + +-- We need to switch to SortedMap here + +updateMeta : Int -> (MetaEntry -> M MetaEntry) -> M Unit +updateMeta ix f = do + top <- get + mc <- readIORef top.metaCtx + metas <- go mc.metas + writeIORef top.metaCtx $ MC metas mc.next + where + go : List MetaEntry -> M (List MetaEntry) + go Nil = error' "Meta \{show ix} not found" + go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs + go (x@((Solved _ k y)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs + + +checkAutos : Int -> List MetaEntry -> M Unit +checkAutos ix Nil = pure MkUnit +checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do + ty' <- quote ctx.lvl ty + when (usesMeta ty') $ \ _ => ignore $ trySolveAuto entry + checkAutos ix rest + where + usesMeta : Tm -> Bool + usesMeta (App _ (Meta _ k) u) = if k == ix then True else usesMeta u + usesMeta (App _ _ u) = usesMeta u + usesMeta _ = False +checkAutos ix (_ :: rest) = checkAutos ix rest + + + +addConstraint : Env -> Int -> SnocList Val -> Val -> M Unit +addConstraint env ix sp tm = do + updateMeta ix $ \case + (Unsolved pos k a b c cons) => do + debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}" + pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons)) + (Solved _ k tm) => error' "Meta \{show k} already solved (addConstraint :: Nil)" + top <- get + mc <- readIORef top.metaCtx + checkAutos ix mc.metas + -- this loops too + -- solveAutos 0 mc.metas + pure MkUnit + + +-- return renaming, the position is the new VVar +invert : Int -> SnocList Val -> M (List Int) +invert lvl sp = go sp Nil + where + go : SnocList Val -> List Int -> M (List Int) + go Lin acc = pure $ reverse acc + go (xs :< VVar fc k Lin) acc = do + if elem k acc + then do + debug $ \ _ => "\{show k} \{show acc}" + -- when does this happen? + error fc "non-linear pattern: \{show sp}" + else go xs (k :: acc) + go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}" + + +-- REVIEW why am I converting to Tm? +-- we have to "lift" the renaming when we go under a lambda +-- I think that essentially means our domain ix are one bigger, since we're looking at lvl +-- in the codomain, so maybe we can just keep that value + +rename : Int -> List Int -> Int -> Val -> M Tm + +renameSpine : Int -> List Int -> Int -> Tm -> SnocList Val -> M Tm +renameSpine meta ren lvl tm Lin = pure tm +renameSpine meta ren lvl tm (xs :< x) = do + xtm <- rename meta ren lvl x + xs' <- renameSpine meta ren lvl tm xs + pure $ App emptyFC xs' xtm + +rename meta ren lvl (VVar fc k sp) = case findIndex' (_==_ k) ren of + Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" + Just x => renameSpine meta ren lvl (Bnd fc x) sp +rename meta ren lvl (VRef fc nm def sp) = renameSpine meta ren lvl (Ref fc nm def) sp +rename meta ren lvl (VMeta fc ix sp) = do + -- So sometimes we have an unsolved meta in here which reference vars out of scope. + debug $ \ _ => "rename Meta \{show ix} spine \{show sp}" + if ix == meta + -- REVIEW is this the right fc? + then error fc "meta occurs check" + else do + meta' <- lookupMeta ix + case meta' of + Solved fc _ val => do + debug $ \ _ => "rename: \{show ix} is solved" + val' <- vappSpine val sp + rename meta ren lvl val' + _ => do + debug $ \ _ => "rename: \{show ix} is unsolved" + catchError (renameSpine meta ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) +rename meta ren lvl (VLam fc n icit rig t) = do + tapp <- t $$ VVar fc lvl Lin + scope <- rename meta (lvl :: ren) (1 + lvl) tapp + pure (Lam fc n icit rig scope) +rename meta ren lvl (VPi fc n icit rig ty tm) = do + ty' <- rename meta ren lvl ty + tmapp <- tm $$ VVar emptyFC lvl Lin + scope' <- rename meta (lvl :: ren) (1 + lvl) tmapp + pure (Pi fc n icit rig ty' scope') +rename meta ren lvl (VU fc) = pure (UU fc) +rename meta ren lvl (VErased fc) = pure (Erased fc) +-- for now, we don't do solutions with case in them. +rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution" +rename meta ren lvl (VLit fc lit) = pure (Lit fc lit) +rename meta ren lvl (VLet fc name val body) = do + val' <- rename meta ren lvl val + body' <- rename meta (lvl :: ren) (1 + lvl) body + pure $ Let fc name val' body' +-- these probably shouldn't show up in solutions... +rename meta ren lvl (VLetRec fc name ty val body) = do + ty' <- rename meta ren lvl ty + val' <- rename meta (lvl :: ren) (1 + lvl) val + body' <- rename meta (lvl :: ren) (1 + lvl) body + pure $ LetRec fc name ty' val' body' + +lams : Nat -> List String -> Tm -> Tm +lams Z _ tm = tm +-- REVIEW do we want a better FC, icity?, rig? +lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm) +lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm) + + +unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult + +.boundNames : Context -> List String +ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst ctx.types) + +solve env m sp t = do + meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m + | _ => error (getFC t) "Meta \{show m} already solved! (solve :: Nil)" + debug $ \ _ => "SOLVE \{show m} \{show kind} lvl \{show $ length' env} sp \{show sp} is \{show t}" + let size = length $ filter (\x => x == Bound) ctx_.bds + debug $ \ _ => "\{show m} size is \{show size} sps \{show $ snoclen sp}" + let (True) = snoclen sp == size + | _ => do + let l = length' env + debug $ \ _ => "meta \{show m} (\{show ix}) applied to \{show $ snoclen sp} args instead of \{show size}" + debug $ \ _ => "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}" + addConstraint env m sp t + let l = length' env + debug $ \ _ => "meta \{show meta}" + ren <- invert l sp + -- force unlet + hack <- quote l t + t <- eval env CBN hack + catchError (do + tm <- rename m ren l t + + let tm = lams (snoclen sp) (reverse ctx_.boundNames) tm + top <- get + soln <- eval Nil CBN tm + + updateMeta m $ \case + (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln + (Solved _ k x) => error' "Meta \{show ix} already solved! (solve2 :: Nil)" + for cons $ \case + MkMc fc env sp rhs => do + val <- vappSpine soln sp + debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}" + unify env UNormal val rhs + mc <- readIORef top.metaCtx + -- stack ... + -- checkAutos ix mc.metas + pure MkUnit + ) + + (\case + Postpone fc ix msg => do + -- let someone else solve this and then check again. + debug $ \ _ => "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}" + addConstraint env m sp t + -- I get legit errors after stuffing in solution + -- report for now, tests aren't hitting this branch + err => throwError err + -- debug $ \ _ => "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}" + -- debug $ \ _ => "because \{showError "" err}" + -- addConstraint env m sp t + ) + +unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult +unifySpine env mode False _ _ = error emptyFC "unify failed at head" -- unreachable now +unifySpine env mode True Lin Lin = pure (MkResult Nil) +unifySpine env mode True (xs :< x) (ys :< y) = + -- I had idiom brackets here, technically fairly easy to desugar, but not adding at this time + _<+>_ <$> unify env mode x y <*> unifySpine env mode True xs ys +unifySpine env mode True _ _ = error emptyFC "meta spine length mismatch" + + +unify env mode t u = do + debug $ \ _ => "Unify lvl \{show $ length env}" + debug $ \ _ => " \{show t}" + debug $ \ _ => " =?= \{show u}" + t' <- forceMeta t >>= unlet env + u' <- forceMeta u >>= unlet env + debug $ \ _ => "forced \{show t'}" + debug $ \ _ => " =?= \{show u'}" + debug $ \ _ => "env \{show env}" + -- debug $ \ _ => "types \{show $ ctx.types}" + let l = length' env + -- On the LHS, variable matching is yields constraints/substitutions + -- We want this to happen before VRefs are expanded, and mixing mode + -- into the case tree explodes it further. + case mode of + UPattern => unifyPattern t' u' + UNormal => unifyMeta t' u' + + -- The case tree is still big here. It's hard for idris to sort + -- What we really want is what I wrote - handle meta, handle lam, handle var, etc + + where + -- The case tree here was huge, so I split it into stages + -- newt will have similar issues because it doesn't emit a default case + + unifyRest : Val -> Val -> M UnifyResult + unifyRest (VPi fc _ _ _ a b) (VPi fc' _ _ _ a' b') = do + let fresh = VVar fc (length' env) Lin + xb <- b $$ fresh + xb' <- b' $$ fresh + _<+>_ <$> unify env mode a a' <*> unify (fresh :: env) mode xb xb' + + unifyRest (VU _) (VU _) = pure neutral + -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. + unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" + + unifyRef : Val -> Val -> M UnifyResult + unifyRef t'@(VRef fc k def sp) u'@(VRef fc' k' def' sp') = + -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y + do + -- catchError(unifySpine env mode (k == k') sp sp') $ \ err => do + Nothing <- tryEval env t' + | Just v => do + debug $ \ _ => "tryEval \{show t'} to \{show v}" + unify env mode v u' + Nothing <- tryEval env u' + | Just v => unify env mode t' v + if k == k' + then unifySpine env mode (k == k') sp sp' + else error fc "vref mismatch \{show t'} \{show u'}" + + -- Lennart.newt cursed type references itself + -- We _could_ look up the ref, eval against Nil and vappSpine... + unifyRef t u@(VRef fc' k' def sp') = do + debug $ \ _ => "expand \{show t} =?= %ref \{show k'}" + top <- get + case lookup k' top of + Just (MkEntry _ name ty (Fn tm)) => do + vtm <- eval Nil CBN tm + appvtm <- vappSpine vtm sp' + unify env mode t appvtm + _ => error fc' "unify failed \{show t} =?= \{show u} (no Fn :: Nil)\n env is \{show env}" + + unifyRef t@(VRef fc k def sp) u = do + debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}" + top <- get + case lookup k top of + Just (MkEntry _ name ty (Fn tm)) => do + vtm <- eval Nil CBN tm + tmsp <- vappSpine vtm sp + unify env mode tmsp u + _ => error fc "unify failed \{show t} (no Fn :: Nil) =?= \{show u}\n env is \{show env}" + unifyRef t u = unifyRest t u + + unifyVar : Val -> Val -> M UnifyResult + unifyVar t'@(VVar fc k sp) u'@(VVar fc' k' sp') = + if k == k' then unifySpine env mode (k == k') sp sp' + else error fc "Failed to unify \{show t'} and \{show u'}" + + unifyVar t'@(VVar fc k Lin) u = do + vu <- tryEval env u + case vu of + Just v => unify env mode t' v + Nothing => error fc "Failed to unify \{show t'} and \{show u}" + + unifyVar t u'@(VVar fc k Lin) = do + vt <- tryEval env t + case vt of + Just v => unify env mode v u' + Nothing => error fc "Failed to unify \{show t} and \{show u'}" + unifyVar t u = unifyRef t u + + unifyLam : Val -> Val -> M UnifyResult + unifyLam (VLam fc _ _ _ t) (VLam _ _ _ _ t') = do + let fresh = VVar fc (length' env) Lin + vappt <- t $$ fresh + vappt' <- t' $$ fresh + unify (fresh :: env) mode vappt vappt' + unifyLam t (VLam fc' _ _ _ t') = do + debug $ \ _ => "ETA \{show t}" + let fresh = VVar fc' (length' env) Lin + vappt <- vapp t fresh + vappt' <- t' $$ fresh + unify (fresh :: env) mode vappt vappt' + unifyLam (VLam fc _ _ _ t) t' = do + debug $ \ _ => "ETA' \{show t'}" + let fresh = VVar fc (length' env) Lin + appt <- t $$ fresh + vappt' <- vapp t' fresh + unify (fresh :: env) mode appt vappt' + unifyLam t u = unifyVar t u + + unifyMeta : Val -> Val -> M UnifyResult + -- flex/flex + unifyMeta (VMeta fc k sp) (VMeta fc' k' sp') = + if k == k' then unifySpine env mode (k == k') sp sp' + -- TODO, might want to try the other way, too. + else if snoclen sp < snoclen sp' + then solve env k' sp' (VMeta fc k sp) >> pure neutral + else solve env k sp (VMeta fc' k' sp') >> pure neutral + unifyMeta t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral + unifyMeta (VMeta fc i sp) t' = solve env i sp t' >> pure neutral + unifyMeta t v = unifyLam t v + + unifyPattern : Val -> Val -> M UnifyResult + unifyPattern t'@(VVar fc k sp) u'@(VVar fc' k' sp') = + if k == k' then unifySpine env mode (k == k') sp sp' + else case (sp, sp') of + (Lin,Lin) => if k < k' + then pure $ MkResult ((k, u') :: Nil) + else pure $ MkResult ((k', t') :: Nil) + _ => error fc "Failed to unify \{show t'} and \{show u'}" + + unifyPattern (VVar fc k Lin) u = pure $ MkResult((k, u) :: Nil) + unifyPattern t (VVar fc k Lin) = pure $ MkResult ((k, t) :: Nil) + unifyPattern t u = unifyMeta t u + + +unifyCatch fc ctx ty' ty = do + res <- catchError (unify ctx.env UNormal ty' ty) $ \err => do + let names = map fst ctx.types + debug $ \ _ => "fail \{show ty'} \{show ty}" + a <- quote ctx.lvl ty' + b <- quote ctx.lvl ty + let msg = "unification failure: \{errorMsg err}\n failed to unify \{rpprint names a}\n with \{rpprint names b}\n " + throwError (E fc msg) + case res of + MkResult Nil => pure MkUnit + cs => do + -- probably want a unification mode that throws instead of returning constraints + -- TODO need a normalizeHoles, maybe on quote? + debug $ \ _ => "fail with constraints \{show cs.constraints}" + a <- quote ctx.lvl ty' + b <- quote ctx.lvl ty + let names = map fst ctx.types + let msg = "unification failure\n failed to unify \{rpprint names a}\n with \{rpprint names b}" + let msg = msg ++ "\nconstraints \{show cs.constraints}" + throwError (E fc msg) + -- error fc "Unification yields constraints \{show cs.constraints}" + + +freshMeta : Context -> FC -> Val -> MetaKind -> M Tm +freshMeta ctx fc ty kind = do + top <- get + mc <- readIORef top.metaCtx + debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" + let newmeta = Unsolved fc mc.next ctx ty kind Nil + writeIORef top.metaCtx $ MC (newmeta :: mc.metas) (1 + mc.next) + -- infinite loop - keeps trying Ord a => Ord (a \x a) + -- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta + pure $ applyBDs 0 (Meta fc mc.next) ctx.bds + where + -- hope I got the right order here :) + applyBDs : Int -> Tm -> List BD -> Tm + applyBDs k t Nil = t + -- review the order here + applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k) + applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs + +insert : (ctx : Context) -> Tm -> Val -> M (Tm × Val) +insert ctx tm ty = do + ty' <- forceMeta ty + case ty' of + VPi fc x Auto rig a b => do + m <- freshMeta ctx (getFC tm) a AutoSolve + debug $ \ _ => "INSERT Auto \{rpprint (names ctx) m} : \{show a}" + debug $ \ _ => "TM \{rpprint (names ctx) tm}" + mv <- eval ctx.env CBN m + bapp <- b $$ mv + insert ctx (App (getFC tm) tm m) bapp + VPi fc x Implicit rig a b => do + m <- freshMeta ctx (getFC tm) a Normal + debug $ \ _ => "INSERT \{rpprint (names ctx) m} : \{show a}" + debug $ \ _ => "TM \{rpprint (names ctx) tm}" + mv <- eval ctx.env CBN m + bapp <- b $$ mv + insert ctx (App (getFC tm) tm m) bapp + va => pure (tm, va) + +primType : FC -> QName -> M Val +primType fc nm = do + top <- get + case lookup nm top of + Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name PrimTCon Lin + _ => error fc "Primitive type \{show nm} not in scope" + + +infer : Context -> Raw -> M (Tm × Val) + + +data Bind = MkBind String Icit Val + +instance Show Bind where + show (MkBind str icit x) = "\{str} \{show icit}" + + +---------------- Case builder + + +record Problem where + constructor MkProb + clauses : List Clause + -- I think a pi-type representing the pattern args -> goal, so we're checking + -- We might pull out the pattern abstraction to a separate step and drop pats from clauses. + ty : Val + +-- Might have to move this if Check reaches back in... +-- this is kinda sketchy, we can't use it twice at the same depth with the same name. +fresh : {{ctx : Context}} -> String -> String +fresh {{ctx}} base = base ++ "$" ++ show (length' ctx.env) + +-- The result is a casetree, but it's in Tm + +buildTree : Context -> Problem -> M Tm + +-- Updates a clause for INTRO +introClause : String -> Icit -> Clause -> M Clause +introClause nm icit (MkClause fc cons (pat :: pats) expr) = + if icit == getIcit pat then pure $ MkClause fc ((nm, pat) :: cons) pats expr + else if icit == Implicit then pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) (pat :: pats) expr + else if icit == Auto then pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) (pat :: pats) expr + else error fc "Explicit arg and \{show $ getIcit pat} pattern \{show nm} \{show pat}" +-- handle implicts at end? +introClause nm Implicit (MkClause fc cons Nil expr) = pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) Nil expr +introClause nm Auto (MkClause fc cons Nil expr) = pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) Nil expr +introClause nm icit (MkClause fc cons Nil expr) = error fc "Clause size doesn't match" + +-- A split candidate looks like x /? Con ... +-- we need a type here. I pulled if off of the +-- pi-type, but do we need metas solved or dependents split? +-- this may dot into a dependent. +findSplit : List Constraint -> Maybe Constraint +findSplit Nil = Nothing + -- FIXME look up type, ensure it's a constructor +findSplit (x@(nm, PatCon _ _ _ _ _) :: xs) = Just x +findSplit (x@(nm, PatLit _ val) :: xs) = Just x +findSplit (x :: xs) = findSplit xs + + +-- *************** +-- right, I think we rewrite the names in the context before running raw and we're good to go? +-- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was? + +-- we could pass into build case and use it for (x /? y) + +-- TODO, we may need to filter these against the type to rule out +-- impossible cases +getConstructors : Context -> FC -> Val -> M (List (QName × Int × Tm)) +getConstructors ctx scfc (VRef fc nm _ _) = do + names <- lookupTCon nm + traverse lookupDCon names + where + lookupTCon : QName -> M (List QName) + lookupTCon str = do + top <- get + case lookup nm top of + (Just (MkEntry _ name type (TCon names))) => pure names + _ => error scfc "Not a type constructor \{show nm}" + lookupDCon : QName -> M (QName × Int × Tm) + lookupDCon nm = do + top <- get + case lookup nm top of + (Just (MkEntry _ name type (DCon k str))) => pure (name, k, type) + Just _ => error fc "Internal Error: \{show nm} is not a DCon" + Nothing => error fc "Internal Error: DCon \{show nm} not found" +getConstructors ctx scfc tm = do + tms <- vprint ctx tm + error scfc "Can't split - not VRef: \{tms}" + +-- Extend environment with fresh variables from a pi-type +-- the pi-type here is the telescope of a constructor +-- return context, remaining type, and list of names +extendPi : Context -> Val -> SnocList Bind -> SnocList Val -> M (Context × Val × List Bind × SnocList Val) +extendPi ctx (VPi x str icit rig a b) nms sc = do + let nm = fresh str -- "pat" + let ctx' = extend ctx nm a + let v = VVar emptyFC (length' ctx.env) Lin + tyb <- b $$ v + extendPi ctx' tyb (nms :< MkBind nm icit a) (sc :< VVar x (length' ctx.env) Lin) +extendPi ctx ty nms sc = pure (ctx, ty, nms <>> Nil, sc) + +-- turn vars into lets for forced values. +-- substitute inside values +-- FIXME we're not going under closures at the moment. +substVal : Int -> Val -> Val -> Val +substVal k v tm = go tm + where + go : Val -> Val + go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp)) + go (VLet fc nm a b) = VLet fc nm (go a) b + go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b + go (VMeta fc ix sp) = VMeta fc ix (map go sp) + go (VRef fc nm y sp) = VRef fc nm y (map go sp) + go tm = tm + -- FIXME - do I need a Val closure like idris? + -- or env in unify... + -- or quote back + -- go (VLam fc nm sc) = VLam fc nm sc + -- go (VCase x sc xs) = ?rhs_2 + -- go (VU x) = ?rhs_7 + -- go (VLit x y) = ?rhs_8 + + +-- need to turn k into a ground value + +-- TODO rework this to do something better. We've got constraints, and +-- and may need to do proper unification if it's already defined to a value +-- below we're handling the case if it's defined to another var, but not +-- checking for loops. +updateContext : Context -> List (Int × Val) -> M Context +updateContext ctx Nil = pure ctx +updateContext ctx ((k, val) :: cs) = + let ix = cast $ lvl2ix (length' ctx.env) k in + case getAt ix ctx.env of + (Just (VVar _ k' Lin)) => + if k' /= k + then updateContext ctx ((k',val) :: cs) + else + let ctx' = MkCtx ctx.lvl (map (substVal k val) ctx.env) ctx.types (replaceV ix Defined ctx.bds) ctx.ctxFC + in updateContext ctx' cs + (Just val') => do + -- This is fine for Z =?= Z but for other stuff, we probably have to match + info (getFC val) "need to unify \{show val} and \{show val'} or something" + updateContext ctx cs + Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext" + + -- + -- updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs + where + replace : Nat -> Val -> List Val -> List Val + replace k x Nil = Nil + replace Z x (y :: xs) = x :: xs + replace (S k) x (y :: xs) = y :: replace k x xs + + replaceV : ∀ a. Nat -> a -> List a -> List a + replaceV k x Nil = Nil + replaceV Z x (y :: xs) = x :: xs + replaceV (S k) x (y :: xs) = y :: replaceV k x xs + +-- ok, so this is a single constructor, CaseAlt +-- return Nothing if dcon doesn't unify with scrut +buildCase : Context -> Problem -> String -> Val -> (QName × Int × Tm) -> M (Maybe CaseAlt) +buildCase ctx prob scnm scty (dcName, arity, ty) = do + debug $ \ _ => "CASE \{scnm} match \{show dcName} ty \{rpprint (names ctx) ty}" + vty <- eval Nil CBN ty + (ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin + + -- TODO I think we need to figure out what is dotted, maybe + -- the environment manipulation below is sufficient bookkeeping + -- or maybe it's a bad approach. + + -- At some point, I'll take a break and review more papers and code, + -- now that I know some of the questions I'm trying to answer. + + -- We get unification constraints from matching the data constructors + -- codomain with the scrutinee type + debug $ \ _ => "unify dcon cod with scrut\n \{show ty'}\n \{show scty}" + Just res <- catchError(Just <$> unify ctx'.env UPattern ty' scty) + (\err => do + debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}" + pure Nothing) + | _ => pure Nothing + + -- if the value is already constrained to a different constructor, return Nothing + debug $ \ _ => "scrut \{scnm} constrained to \{show $ lookupDef ctx scnm}" + let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}" + + case lookupDef ctx scnm of + Just val@(VRef fc nm y sp) => + if nm /= dcName + then do + debug $ \ _ => "SKIP \{show dcName} because \{scnm} forced to \{show val}" + pure Nothing + else do + debug $ \ _ => "case \{show dcName} dotted \{show val}" + when (length vars /= snoclen sp) $ \ _ => error emptyFC "\{show $ length vars} vars /= \{show $ snoclen sp}" + + -- TODO - I think we need to define the context vars to sp via updateContext + + let lvl = length' ctx'.env - length' vars + let scons = constrainSpine lvl (sp <>> Nil) -- REVIEW is this the right order? + ctx' <- updateContext ctx' scons + + debug $ \ _ => "(dcon \{show dcName} ty \{show ty'} scty \{show scty}" + debug $ \ _ => "(dcon \{show dcName}) (vars \{show vars}) clauses were" + for prob.clauses $ (\x => debug $ \ _ => " \{show x}") + clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses + debug $ \ _ => "and now:" + for clauses $ (\x => debug $ \ _ => " \{show x}") + when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show dcName} splitting \{scnm}" + tm <- buildTree ctx' (MkProb clauses prob.ty) + pure $ Just $ CaseCons dcName (map getName vars) tm + + _ => do + (Right res) <- tryError (unify ctx'.env UPattern ty' scty) + | Left err => do + debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}" + pure Nothing + + -- Constrain the scrutinee's variable to be dcon applied to args + let (Just x) = findIndex' ((_==_ scnm) ∘ fst) ctx'.types + | Nothing => error ctx.ctxFC "\{scnm} not is scope?" + let lvl = lvl2ix (length' ctx'.env) x + let scon = (lvl, VRef ctx.ctxFC dcName (DCon arity dcName) sc) + + debug $ \ _ => "scty \{show scty}" + debug $ \ _ => "UNIFY results \{show res.constraints}" + debug $ \ _ => "before types: \{show ctx'.types}" + debug $ \ _ => "before env: \{show ctx'.env}" + debug $ \ _ => "SC CONSTRAINT: \{show scon}" + + -- push the constraints into the environment by turning bind into define + -- Is this kosher? It might be a problem if we've already got metas over + -- this stuff, because it intends to ignore defines. + ctx' <- updateContext ctx' (scon :: res.constraints) + + debug $ \ _ => "context types: \{show ctx'.types}" + debug $ \ _ => "context env: \{show ctx'.env}" + + -- What if all of the pattern vars are defined to meta + + debug $ \ _ => "(dcon \{show dcName} ty \{show ty'} scty \{show scty}" + debug $ \ _ => "(dcon \{show dcName}) (vars \{show vars}) clauses were" + for prob.clauses $ (\x => debug $ \ _ => " \{show x}") + clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses + debug $ \ _ => "and now:" + for clauses $ (\x => debug $ \ _ => " \{show x}") + when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show dcName} splitting \{scnm}" + tm <- buildTree ctx' (MkProb clauses prob.ty) + pure $ Just $ CaseCons dcName (map getName vars) tm + where + constrainSpine : Int -> List Val -> List (Int × Val) + constrainSpine lvl Nil = Nil + constrainSpine lvl (v :: vs) = (lvl, v) :: constrainSpine (1 + lvl) vs + + getName : Bind -> String + getName (MkBind nm _ _) = nm + + -- for each clause in prob, find nm on LHS of some constraint, and + -- "replace" with the constructor and vars. + -- + -- This will be: + -- x /? y can probably just leave this + -- x /? D a b c split into three x /? a, y /? b, z /? c + -- x /? E a b drop this clause + -- We get a list of clauses back (a Problem) and then solve that + -- If they all fail, we have a coverage issue. (Assuming the constructor is valid) + + makeConstr : List Bind -> List Pattern -> M (List (String × Pattern)) + makeConstr Nil Nil = pure $ Nil + -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$> + makeConstr Nil (pat :: pats) = error ctx.ctxFC "too many patterns" + makeConstr ((MkBind nm Implicit x) :: xs) Nil = do + rest <- makeConstr xs Nil + pure $ (nm, PatWild emptyFC Implicit) :: rest + makeConstr ((MkBind nm Auto x) :: xs) Nil = do + rest <- makeConstr xs Nil + pure $ (nm, PatWild emptyFC Auto) :: rest + -- FIXME need a proper error, but requires wiring M three levels down + makeConstr ((MkBind nm Explicit x) :: xs) Nil = error ctx.ctxFC "not enough patterns" + makeConstr ((MkBind nm Explicit x) :: xs) (pat :: pats) = + if getIcit pat == Explicit + then do + rest <- makeConstr xs pats + pure $ (nm, pat) :: rest + else error ctx.ctxFC "mismatch between Explicit and \{show $ getIcit pat}" + makeConstr ((MkBind nm icit x) :: xs) (pat :: pats) = + if getIcit pat /= icit -- Implicit/Explicit Implicit/Auto, etc + then do + rest <- makeConstr xs (pat :: pats) + pure $ (nm, PatWild (getFC pat) icit) :: rest + else do + rest <- makeConstr xs pats + pure $ (nm, pat) :: rest + + -- replace constraint with constraints on parameters, or nothing if non-matching clause + rewriteConstraint : QName -> List Bind -> List Constraint -> List Constraint -> M (Maybe (List Constraint)) + rewriteConstraint sctynm vars Nil acc = pure $ Just acc + rewriteConstraint sctynm vars (c@(nm, y) :: xs) acc = + if nm == scnm + then case y of + PatVar _ _ s => pure $ Just $ c :: (xs ++ acc) + PatWild _ _ => pure $ Just $ c :: (xs ++ acc) + -- FIXME why don't we hit this (when user puts 'x' for Just 'x') + PatLit fc lit => error fc "Literal \{show lit} in constructor split" + PatCon fc icit nm ys as => if nm == dcName + then case as of + Nothing => do + rest <- makeConstr vars ys + pure $ Just $ rest ++ xs ++ acc + -- putting this in constraints causes it to be renamed scnm -> nm' when we check body. + Just nm' => do + rest <- makeConstr vars ys + pure $ Just $ (scnm, (PatVar fc icit nm')) :: rest ++ xs ++ acc + else do + -- TODO can we check this when we make the PatCon? + top <- get + case lookup nm top of + (Just (MkEntry _ name type (DCon k tcname))) => + if (tcname /= sctynm) + then error fc "Constructor is \{show tcname} expected \{show sctynm}" + else pure Nothing + Just _ => error fc "Internal Error: \{show nm} is not a DCon" + Nothing => error fc "Internal Error: DCon \{show nm} not found" + else rewriteConstraint sctynm vars xs (c :: acc) + + rewriteClause : QName -> List Bind -> Clause -> M (Maybe Clause) + rewriteClause sctynm vars (MkClause fc cons pats expr) = do + Just cons <- rewriteConstraint sctynm vars cons Nil | _ => pure Nothing + pure $ Just $ MkClause fc cons pats expr + + +splitArgs : Raw -> List (Raw × Icit) -> (Raw × List (Raw × Icit)) +splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args) +splitArgs tm args = (tm, args) + + +mkPat : TopContext -> (Raw × Icit) -> M Pattern +mkPat top (RAs fc as tm, icit) = do + pat <- mkPat top (tm, icit) + case pat of + (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as) + (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}" + t => error fc "Can't put as on non-constructor \{show tm}" +mkPat top (tm, icit) = do + case splitArgs tm Nil of + ((RVar fc nm), b) => case lookupRaw nm top of + (Just (MkEntry _ name type (DCon k str))) => do + -- TODO check arity, also figure out why we need reverse + bpat <- traverse (mkPat top) b + pure $ PatCon fc icit name bpat Nothing + -- This fires when a global is shadowed by a pattern var + -- Just _ => error (getFC tm) "\{show nm} is not a data constructor" + _ => case b of + Nil => pure $ PatVar fc icit nm + _ => error (getFC tm) "patvar applied to args" + ((RImplicit fc), Nil) => pure $ PatWild fc icit + ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments" + ((RLit fc lit), Nil) => pure $ PatLit fc lit + ((RLit fc y), b) => error fc "lit cannot be applied to arguments" + (a,b) => error (getFC a) "expected pat var or constructor, got \{show a}" + + + +makeClause : TopContext -> (Raw × Raw) -> M Clause +makeClause top (lhs, rhs) = do + let (nm, args) = splitArgs lhs Nil + pats <- traverse (mkPat top) args + pure $ MkClause (getFC lhs) Nil pats rhs + + + +-- we'll want both check and infer, we're augmenting a context +-- so probably a continuation: +-- Context -> List Decl -> (Context -> M a) -> M a +checkWhere : Context -> List Decl -> Raw -> Val -> M Tm +checkWhere ctx decls body ty = do + -- we're going to be very proscriptive here + let (TypeSig sigFC (name :: Nil) rawtype :: decls) = decls + | x :: _ => error (getFC x) "expected type signature" + | _ => check ctx body ty + funTy <- check ctx rawtype (VU sigFC) + debug $ \ _ => "where clause \{name} : \{rpprint (names ctx) funTy}" + let (Def defFC name' clauses :: decls') = decls + | x :: _ => error (getFC x) "expected function definition" + | _ => error sigFC "expected function definition after this signature" + unless (name == name') $ \ _ => error defFC "Expected def for \{name}" + -- REVIEW is this right, cribbed from my top level code + top <- get + clauses' <- traverse (makeClause top) clauses + vty <- eval ctx.env CBN funTy + debug $ \ _ => "\{name} vty is \{show vty}" + let ctx' = extend ctx name vty + + -- if I lift, I need to namespace it, add args, and add args when + -- calling locally + -- context could hold a Name -> Val (not Tm because levels) to help with that + -- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...) + -- But I'll attempt letrec first + tm <- buildTree (withPos ctx' defFC) (MkProb clauses' vty) + vtm <- eval ctx'.env CBN tm + -- Should we run the rest with the definition in place? + -- I'm wondering if switching from bind to define will mess with metas + -- let ctx' = define ctx name vtm vty + ty' <- checkWhere ctx' decls' body ty + pure $ LetRec sigFC name funTy tm ty' + + +checkDone : Context -> List (String × Pattern) -> Raw -> Val -> M Tm +checkDone ctx Nil body ty = do + debug $ \ _ => "DONE-> check body \{show body} at \{show ty}" + -- TODO better dump context function + debugM $ showCtx ctx + -- Hack to try to get Combinatory working + -- we're trying to subst in solutions here. + env' <- for ctx.env $ \ val => do + ty <- quote (length' ctx.env) val + -- This is not getting vars under lambdas + eval ctx.env CBV ty + types' <- for ctx.types $ \case + (nm,ty) => do + nty <- quote (length' env') ty + ty' <- eval env' CBV nty + pure (nm, ty') + let ctx = MkCtx ctx.lvl env' types' ctx.bds ctx.ctxFC + debug $ \ _ => "AFTER" + debugM $ showCtx ctx + -- I'm running an eval here to run case statements that are + -- unblocked by lets in the env. (Tree.newt:cmp) + -- The case eval code only works in the Tm -> Val case at the moment. + -- we don't have anything like `vapp` for case + ty <- quote (length' ctx.env) ty + ty <- eval ctx.env CBN ty + + debug $ \ _ => "check at \{show ty}" + got <- check ctx body ty + debug $ \ _ => "DONE<- got \{rpprint (names ctx) got}" + pure got +checkDone ctx ((x, PatWild _ _) :: xs) body ty = checkDone ctx xs body ty +checkDone ctx ((nm, (PatVar _ _ nm')) :: xs) body ty = + let ctx = MkCtx ctx.lvl ctx.env (rename ctx.types) ctx.bds ctx.ctxFC in + checkDone ctx xs body ty + where + rename : List (String × Val) -> List (String × Val) + rename Nil = Nil + rename ((name, ty) :: xs) = + if name == nm + then (nm', ty) :: xs + else (name, ty) :: rename xs + +checkDone ctx ((x, pat) :: xs) body ty = error (getFC pat) "stray constraint \{x} /? \{show pat}" + +-- need to run constructors, then run default + +-- wild/var can come before 'x' so we need a list first +getLits : String -> List Clause -> List Literal +getLits nm Nil = Nil +getLits nm ((MkClause fc cons pats expr) :: cs) = case find ((_==_ nm) ∘ fst) cons of + Just (_, (PatLit _ lit)) => lit :: getLits nm cs + _ => getLits nm cs + + +-- then build a lit case for each of those + +buildLitCase : Context -> Problem -> FC -> String -> Val -> Literal -> M CaseAlt +buildLitCase ctx prob fc scnm scty lit = do + + -- Constrain the scrutinee's variable to be lit value + let (Just ix) = findIndex' ((_==_ scnm) ∘ fst) ctx.types + | Nothing => error ctx.ctxFC "\{scnm} not is scope?" + let lvl = lvl2ix (length' ctx.env) ix + let scon = (lvl, VLit fc lit) + ctx' <- updateContext ctx (scon :: Nil) + let clauses = mapMaybe rewriteClause prob.clauses + + when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show lit} splitting \{scnm}" + tm <- buildTree ctx' (MkProb clauses prob.ty) + pure $ CaseLit lit tm + + where + -- FIXME - thread in M for errors + -- replace constraint with constraints on parameters, or nothing if non-matching clause + rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint) + rewriteConstraint Nil acc = Just acc + rewriteConstraint (c@(nm, y) :: xs) acc = + if nm == scnm + then case y of + PatVar _ _ s => Just $ c :: (xs ++ acc) + PatWild _ _ => Just $ c :: (xs ++ acc) + PatLit fc lit' => if lit' == lit then Just $ (xs ++ acc) else Nothing + PatCon _ _ str ys as => Nothing -- error matching lit against constructor + else rewriteConstraint xs (c :: acc) + + rewriteClause : Clause -> Maybe Clause + rewriteClause (MkClause fc cons pats expr) = do + cons <- rewriteConstraint cons Nil + pure $ MkClause fc cons pats expr + + + +buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt) +buildLitCases ctx prob fc scnm scty = do + let lits = nub $ getLits scnm prob.clauses + alts <- traverse (buildLitCase ctx prob fc scnm scty) lits + -- TODO build default case + -- run getLits + -- buildLitCase for each + + let defclauses = filter isDefault prob.clauses + when (length' defclauses == 0) $ \ _ => error fc "no default for literal slot on \{show scnm}" + tm <- buildTree ctx (MkProb defclauses prob.ty) + + pure $ alts ++ ( CaseDefault tm :: Nil) + where + isDefault : Clause -> Bool + isDefault cl = case find ((_==_ scnm) ∘ fst) cl.cons of + Just (_, (PatVar _ _ _)) => True + Just (_, (PatWild _ _)) => True + Nothing => True + _ => False + +-- TODO - figure out if these need to be in Prelude or have a special namespace +-- If we lookupRaw "String", we could get different answers in different contexts. +-- maybe Hardwire this one +stringType intType charType : QName +stringType = QN ("Prim" :: Nil) "String" +intType = QN ("Prim" :: Nil) "Int" +charType = QN ("Prim" :: Nil) "Char" + +litTyName : Literal -> QName +litTyName (LString str) = stringType +litTyName (LInt i) = intType +litTyName (LChar c) = charType + +renameContext : String -> String -> Context -> Context +renameContext from to ctx = MkCtx ctx.lvl ctx.env (go ctx.types) ctx.bds ctx.ctxFC + where + go : List (String × Val) -> List (String × Val) + go Nil = Nil + go ((a,b) :: types) = if a == from then (to,b) :: types else (a,b) :: go types + +-- This process is similar to extendPi, but we need to stop +-- if one clause is short on patterns. +buildTree ctx (MkProb Nil ty) = error emptyFC "no clauses" +buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit rig a b)) = do + let l = length' ctx.env + let nm = fresh str -- "pat" + let ctx' = extend ctx nm a + -- type of the rest + clauses <- traverse (introClause nm icit) prob.clauses + -- REVIEW fc from a pat? + vb <- b $$ VVar fc l Lin + Lam fc nm icit rig <$> buildTree ctx' (MkProb clauses vb) +buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) = + error fc "Extra pattern variables \{show pats}" +-- need to find some name we can split in (x :: xs) +-- so LHS of constraint is name (or VVar - if we do Val) +-- then run the split +-- some of this is copied into check +buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do + debug $ \ _ => "buildTree \{show constraints} \{show expr}" + let (Just (scnm, pat)) = findSplit constraints + | _ => do + debug $ \ _ => "checkDone \{show constraints}" + checkDone ctx constraints expr ty + + debug $ \ _ => "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}" + let (Just (sctm, scty)) = lookupName ctx scnm + | _ => error fc "Internal Error: can't find \{scnm} in environment" + + -- REVIEW We probably need to know this is a VRef before we decide to split on this slot.. + scty' <- unlet ctx.env scty >>= forceType ctx.env + -- TODO attempting to pick up Autos that could have been solved immediately + -- If we try on creation, we're looping at the moment, because of the possibility + -- of Ord a -> Ord b -> Ord (a \x b). Need to cut earlier when solving or switch to + -- Idris method... + scty' <- case scty' of + (VMeta fc1 ix sp) => do + meta <- lookupMeta ix + case meta of + (Solved _ k t) => forceType ctx.env scty' + (Unsolved _ k xs _ _ _) => do + top <- get + mc <- readIORef top.metaCtx + ignore $ solveAutos 0 + forceType ctx.env scty' + + _ => pure scty' + + case pat of + PatCon fc _ _ _ as => do + -- expand vars that may be solved, eval top level functions + debug $ \ _ => "EXP \{show scty} -> \{show scty'}" + -- this is per the paper, but it would be nice to coalesce + -- default cases + cons <- getConstructors ctx (getFC pat) scty' + debug $ \ _ => "CONS \{show $ map fst cons}" + alts <- traverse (buildCase ctx prob scnm scty') cons + debug $ \ _ => "GOTALTS \{show alts}" + when (length' (mapMaybe id alts) == 0) $ \ _ => error (fc) "no alts for \{show scty'}" + pure $ Case fc sctm (mapMaybe id alts) + PatLit fc v => do + let tyname = litTyName v + case scty' of + (VRef fc1 nm x sp) => when (nm /= tyname) $ \ _ => error fc "expected \{show scty} and got \{show tyname}" + _ => error fc "expected \{show scty} and got \{show tyname}" + -- need to run through all of the PatLits in this slot and then find a fallback + -- walk the list of patterns, stop if we hit a PatVar / PatWild, fail if we don't + alts <- buildLitCases ctx prob fc scnm scty + pure $ Case fc sctm alts + pat => error (getFC pat) "Internal error - tried to split on \{show pat}" + +showDef : Context -> List String -> Int -> Val -> M String +showDef ctx names n v@(VVar _ n' Lin) = if n == n' + then pure "" + else do + -- REVIEW - was using names, is it ok to pull from the context? + vv <- vprint ctx v + pure "= \{vv}" +showDef ctx names n v = do + vv <- vprint ctx v + pure "= \{vv}" + -- pure "= \{rpprint names !(quote ctx.lvl v)}" + +-- desugar do +undo : FC -> List DoStmt -> M Raw +undo prev Nil = error prev "do block must end in expression" +undo prev ((DoExpr fc tm) :: Nil) = pure tm +-- TODO decide if we want to use >> or just >>= +undo prev ((DoExpr fc tm) :: xs) = do + xs' <- undo fc xs + pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit +undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs +undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do + top <- get + case lookupRaw nm top of + Just _ => do + let nm = "$sc" + xs' <- undo fc xs + rest <- pure $ RCase fc (RVar fc nm) (MkAlt left xs' :: Nil) + pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit) + (RLam fc (BI fc nm Explicit Many) rest) Explicit + Nothing => do + xs' <- undo fc xs + pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit) + (RLam fc (BI fc' nm Explicit Many) xs') Explicit +undo prev ((DoArrow fc left right alts) :: xs) = do + let nm = "$sc" + xs' <- undo fc xs + rest <- pure $ RCase fc (RVar fc nm) (MkAlt left xs' :: alts) + pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit) + (RLam fc (BI fc nm Explicit Many) rest) Explicit + +check ctx tm ty = do + ty' <- forceType ctx.env ty + case (tm, ty') of + (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty + (RIf fc a b c, ty) => + let tm' = RCase fc a ( MkAlt (RVar (getFC b) "True") b :: MkAlt (RVar (getFC c) "False") c :: Nil) in + check ctx tm' ty + (RDo fc stmts, ty) => do + stmts' <- undo fc stmts + check ctx stmts' ty + (RCase fc rsc alts, ty) => do + (sc, scty) <- infer ctx rsc + scty <- forceMeta scty + debug $ \ _ => "SCTM \{rpprint (names ctx) sc}" + debug $ \ _ => "SCTY \{show scty}" + + let scnm = fresh "sc" + top <- get + clauses <- for alts $ \case + (MkAlt pat rawRHS) => do + pat' <- mkPat top (pat, Explicit) + pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS + -- buildCase expects scrutinee to be a name in the context, so we need to let it. + -- if it's a Bnd and not shadowed we could skip the let, but that's messy. + let ctx' = extend ctx scnm scty + tree <- buildTree ctx' $ MkProb clauses ty + pure $ Let fc scnm sc tree + + -- rendered in ProcessDecl + (RHole fc, ty) => freshMeta ctx fc ty User + + (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' rig a b)) => do + debug $ \ _ => "icits \{nm} \{show icit} \{nm'} \{show icit'}" + if icit == icit' then do + let var = VVar fc (length' ctx.env) Lin + let ctx' = extend ctx nm a + bapp <- b $$ var + tm' <- check ctx' tm bapp + pure $ Lam fc nm icit rig tm' + else if icit' /= Explicit then do + let var = VVar fc (length' ctx.env) Lin + ty' <- b $$ var + -- use nm' here if we want them automatically in scope + sc <- check (extend ctx nm' a) t ty' + pure $ Lam fc nm' icit rig sc + else + error fc "Icity issue checking \{show t} at \{show ty}" + (t@(RLam _ (BI fc nm icit quant) tm), ty) => do + pty <- prvalCtx ty + error fc "Expected pi type, got \{pty}" + + + (RLet fc nm ty v sc, rty) => do + ty' <- check ctx ty (VU emptyFC) + vty <- eval ctx.env CBN ty' + v' <- check ctx v vty + vv <- eval ctx.env CBN v' + let ctx' = define ctx nm vv vty + sc' <- check ctx' sc rty + pure $ Let fc nm v' sc' + + (RImplicit fc, ty) => freshMeta ctx fc ty Normal + + (tm, ty@(VPi fc nm' Implicit rig a b)) => do + let names = map fst ctx.types + debug $ \ _ => "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} " + let var = VVar fc (length' ctx.env) Lin + ty' <- b $$ var + debugM $ do + pty' <- prvalCtx {{(extend ctx nm' a)}} ty' + pure "XXX ty' is \{pty'}" + sc <- check (extend ctx nm' a) tm ty' + pure $ Lam (getFC tm) nm' Implicit rig sc + + (tm, ty@(VPi fc nm' Auto rig a b)) => do + let names = map fst ctx.types + debug $ \ _ => "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} " + let var = VVar fc (length' ctx.env) Lin + ty' <- b $$ var + debugM $ do + pty' <- prvalCtx {{(extend ctx nm' a)}} ty' + pure "XXX ty' is \{pty'}" + sc <- check (extend ctx nm' a) tm ty' + pure $ Lam (getFC tm) nm' Auto rig sc + + (tm,ty) => do + (tm', ty') <- infer ctx tm + (tm', ty') <- insert ctx tm' ty' + + let names = map fst ctx.types + debug $ \ _ => "INFER \{show tm} to (\{rpprint names tm'} : \{show ty'}) expect \{show ty}" + unifyCatch (getFC tm) ctx ty' ty + pure tm' + +infer ctx (RVar fc nm) = go 0 ctx.types + where + go : Int -> List (String × Val) -> M (Tm × Val) + go i Nil = do + top <- get + case lookupRaw nm top of + Just (MkEntry _ name ty def) => do + debug $ \ _ => "lookup \{show name} as \{show def}" + vty <- eval Nil CBN ty + pure (Ref fc name def, vty) + Nothing => error fc "\{show nm} not in scope" + go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty) + else go (i + 1) xs +-- FIXME tightens up output but hardcodes a name +-- infer ctx (RApp fc (RVar _ "_$_") u icit) = infer ctx u +infer ctx (RApp fc t u icit) = do + -- If the app is explicit, add any necessary metas + (icit, t, tty) <- case the Icit icit of + Explicit => do + (t, tty) <- infer ctx t + (t, tty) <- insert ctx t tty + pure (Explicit, t, tty) + Implicit => do + (t, tty) <- infer ctx t + pure (Implicit, t, tty) + Auto => do + (t, tty) <- infer ctx t + pure (Auto, t, tty) + + (a,b) <- do + tty' <- forceMeta tty + case tty' of + (VPi fc' str icit' rig a b) => if icit' == icit then pure (a,b) + else error fc "IcitMismatch \{show icit} \{show icit'}" + + -- If it's not a VPi, try to unify it with a VPi + -- TODO test case to cover this. + tty => do + debug $ \ _ => "unify PI for \{show tty}" + a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN + b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal + -- FIXME - I had to guess Many here. What are the side effects? + unifyCatch fc ctx tty (VPi fc ":ins" icit Many a b) + pure (a,b) + + u <- check ctx u a + u' <- eval ctx.env CBN u + bappu <- b $$ u' + pure (App fc t u, bappu) + +infer ctx (RU fc) = pure (UU fc, VU fc) -- YOLO +infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do + ty' <- check ctx ty (VU fc) + vty' <- eval ctx.env CBN ty' + ty2' <- check (extend ctx nm vty') ty2 (VU fc) + pure (Pi fc nm icit quant ty' ty2', (VU fc)) +infer ctx (RLet fc nm ty v sc) = do + ty' <- check ctx ty (VU emptyFC) + vty <- eval ctx.env CBN ty' + v' <- check ctx v vty + vv <- eval ctx.env CBN v' + let ctx' = define ctx nm vv vty + (sc',scty) <- infer ctx' sc + pure $ (Let fc nm v' sc', scty) + +infer ctx (RAnn fc tm rty) = do + ty <- check ctx rty (VU fc) + vty <- eval ctx.env CBN ty + tm <- check ctx tm vty + pure (tm, vty) + +infer ctx (RLam _ (BI fc nm icit quant) tm) = do + a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN + let ctx' = extend ctx nm a + (tm', b) <- infer ctx' tm + debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}" + tyb <- quote (1 + ctx.lvl) b + pure $ (Lam fc nm icit quant tm', VPi fc nm icit quant a (MkClosure ctx.env tyb)) + +infer ctx (RImplicit fc) = do + ty <- freshMeta ctx fc (VU emptyFC) Normal + vty <- eval ctx.env CBN ty + tm <- freshMeta ctx fc vty Normal + pure (tm, vty) + +infer ctx (RLit fc (LString str)) = do + ty <- primType fc stringType + pure (Lit fc (LString str), ty) +infer ctx (RLit fc (LInt i)) = do + ty <- primType fc intType + pure (Lit fc (LInt i), ty) +infer ctx (RLit fc (LChar c)) = do + ty <- primType fc charType + pure (Lit fc (LChar c), ty) +infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns" +infer ctx tm = error (getFC tm) "Implement infer \{show tm}" diff --git a/done/Lib/Eval.newt b/done/Lib/Eval.newt index 129f244..30395fb 100644 --- a/done/Lib/Eval.newt +++ b/done/Lib/Eval.newt @@ -79,6 +79,11 @@ tryEval env (VRef fc k _ sp) = do val <- vappSpine vtm sp case val of VCase _ _ _ => pure Nothing + -- For now? There is a spot in Compile.newt that has + -- two applications of fresh that is getting unfolded even + -- though it has the same head and spine. Possibly because it's + -- coming out of a let and is instantly applied + VLetRec _ _ _ _ _ => pure Nothing v => pure $ Just v) (\ _ => pure Nothing) _ => pure Nothing diff --git a/done/Lib/Parser.newt b/done/Lib/Parser.newt index 2679891..3542d83 100644 --- a/done/Lib/Parser.newt +++ b/done/Lib/Parser.newt @@ -654,14 +654,14 @@ parseMod = do pure $ MkModule name imports decls -data ReplCmd = - Def Decl - | Norm Raw -- or just name? - | Check Raw +-- data ReplCmd = +-- Def Decl +-- | Norm Raw -- or just name? +-- | Check Raw --- Eventually I'd like immediate actions in the file, like lean, but I --- also want to REPL to work and we can do that first. -parseRepl : Parser ReplCmd -parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr - <|> Check <$ keyword "#check" <*> typeExpr +-- -- Eventually I'd like immediate actions in the file, like lean, but I +-- -- also want to REPL to work and we can do that first. +-- parseRepl : Parser ReplCmd +-- parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr +-- <|> Check <$ keyword "#check" <*> typeExpr diff --git a/done/Lib/ProcessDecl.newt b/done/Lib/ProcessDecl.newt new file mode 100644 index 0000000..0885c2c --- /dev/null +++ b/done/Lib/ProcessDecl.newt @@ -0,0 +1,471 @@ +module Lib.ProcessDecl + +import Data.IORef +import Data.String +import Data.Vect +import Data.List +import Data.Maybe + +import Lib.Elab +import Lib.Parser +import Lib.Syntax +import Lib.TopContext +import Lib.Eval +import Lib.Types +import Lib.Util +import Lib.Erasure + +dumpEnv : Context -> M String +dumpEnv ctx = + unlines ∘ reverse <$> go (names ctx) 0 (reverse $ zip ctx.env ctx.types) Nil + where + isVar : Int -> Val -> Bool + isVar k (VVar _ k' Lin) = k == k' + isVar _ _ = False + + go : List String -> Int -> List (Val × String × Val) -> List String -> M (List String) + go _ _ Nil acc = pure acc + go names k ((v, n, ty) :: xs) acc = if isVar k v + -- TODO - use Doc and add <+/> as appropriate to printing + then do + ty' <- quote ctx.lvl ty + go names (1 + k) xs (" \{n} : \{render 90 $ pprint names ty'}":: acc) + else do + v' <- quote ctx.lvl v + ty' <- quote ctx.lvl ty + go names (1 + k) xs (" \{n} = \{render 90 $ pprint names v'} : \{render 90 $ pprint names ty'}":: acc) + + +logMetas : Int -> M Unit +logMetas mstart = do + -- FIXME, now this isn't logged for Sig / Data. + top <- get + mc <- readIORef {M} top.metaCtx + let mlen = cast {Int} {Nat} $ length' mc.metas - mstart + ignore $ for (reverse $ take mlen mc.metas) $ \case + (Solved fc k soln) => do + -- TODO put a flag on this, vscode is getting overwhelmed and + -- dropping errors + --info fc "solve \{show k} as \{render 90 $ pprint Nil !(quote 0 soln)}" + pure MkUnit + (Unsolved fc k ctx ty User cons) => do + ty' <- quote ctx.lvl ty + let names = map fst ctx.types + env <- dumpEnv ctx + let msg = "\{env} -----------\n \{render 90 $ pprint names ty'}" + info fc "User Hole\n\{msg}" + + (Unsolved fc k ctx ty kind cons) => do + ty' <- forceMeta ty + tm <- quote ctx.lvl ty' + -- Now that we're collecting errors, maybe we simply check at the end + -- TODO - log constraints? + -- FIXME in Combinatory, the val doesn't match environment? + let msg = "Unsolved meta \{show k} \{show kind} type \{render 90 $ pprint (names ctx) tm} \{show $ length' cons} constraints" + msgs <- for cons $ \case + (MkMc fc env sp val) => do + pure " * (m\{show k} (\{unwords $ map show $ sp <>> Nil}) =?= \{show val}" + sols <- case kind of + AutoSolve => do + x <- quote ctx.lvl ty + ty <- eval ctx.env CBN x + debug $ \ _ => "AUTO ---> \{show ty}" + -- we want the context here too. + top <- get + -- matches <- case !(contextMatches ctx ty) of + -- Nil => findMatches ctx ty $ toList top.defs + -- xs => pure xs + matches <- findMatches ctx ty $ map snd $ toList top.defs + -- TODO try putting mc into TopContext for to see if it gives better terms + pure $ (" \{show $ length' matches} Solutions: \{show matches}" :: Nil) + -- pure $ " \{show $ length' matches} Solutions:" :: map ((" " ++) ∘ interpolate ∘ pprint (names ctx) ∘ fst) matches + + _ => pure Nil + info fc $ unlines ((msg :: Nil) ++ msgs ++ sols) + -- addError $ E fc $ unlines ((msg :: Nil) ++ msgs ++ sols) + + +-- Used for Class and Record +getSigs : List Decl -> List (FC × String × Raw) +getSigs Nil = Nil +getSigs ((TypeSig _ Nil _) :: xs) = getSigs xs +getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs +getSigs (_ :: xs) = getSigs xs + +teleToPi : Telescope -> Raw -> Raw +teleToPi Nil end = end +teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end) + +impTele : Telescope -> Telescope +impTele tele = map foo tele + where + foo : BindInfo × Raw → BindInfo × Raw + foo (BI fc nm _ _ , ty) = (BI fc nm Implicit Zero, ty) + + + +processDecl : List String -> Decl -> M Unit + +-- REVIEW I supposed I could have updated top here instead of the dance with the parser... +processDecl ns (PMixFix _ _ _ _) = pure MkUnit + +processDecl ns (TypeSig fc names tm) = do + putStrLn "-----" + + top <- get + mc <- readIORef top.metaCtx + -- let mstart = length' mc.metas + for names $ \nm => do + let (Nothing) = lookupRaw nm top + | Just entry => error fc "\{show nm} is already defined at \{show entry.fc}" + pure MkUnit + ty <- check (mkCtx fc) tm (VU fc) + ty <- zonk top 0 Nil ty + putStrLn "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}" + for_ names $ \nm => setDef (QN ns nm) fc ty Axiom + -- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here + -- logMetas mstart + +processDecl ns (PType fc nm ty) = do + top <- get + ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc) + setDef (QN ns nm) fc ty' PrimTCon + +processDecl ns (PFunc fc nm used ty src) = do + top <- get + ty <- check (mkCtx fc) ty (VU fc) + ty' <- nf Nil ty + putStrLn "pfunc \{nm} : \{render 90 $ pprint Nil ty'} = \{show src}" + -- TODO wire through fc? + for used $ \ name => case lookupRaw name top of + Nothing => error fc "\{name} not in scope" + _ => pure MkUnit + setDef (QN ns nm) fc ty' (PrimFn src used) + +processDecl ns (Def fc nm claused) = do + putStrLn "-----" + putStrLn "Def \{show nm}" + top <- get + mc <- readIORef top.metaCtx + let mstart = length' mc.metas + let (Just entry) = lookupRaw nm top + | Nothing => throwError $ E fc "No declaration for \{nm}" + let (MkEntry fc name ty Axiom) = entry + | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}" + + putStrLn "check \{nm} at \{render 90 $ pprint Nil ty}" + vty <- eval Nil CBN ty + + debug $ \ _ => "\{nm} vty is \{show vty}" + + + -- I can take LHS apart syntactically or elaborate it with an infer + claused' <- traverse (makeClause top) claused + tm <- buildTree (mkCtx fc) (MkProb claused' vty) + -- putStrLn "Ok \{render 90 $ pprint Nil tm}" + + mc <- readIORef top.metaCtx + let mlen = length' mc.metas - mstart + solveAutos mstart + -- TODO - make nf that expands all metas and drop zonk + -- Day1.newt is a test case + -- tm' <- nf Nil tm + tm' <- zonk top 0 Nil tm + when top.verbose $ \ _ => putStrLn "NF\n\{render 80 $ pprint Nil tm'}" + -- TODO we want to keep both versions, but this is checking in addition to erasing + -- currently CompileExp is also doing erasure. + -- TODO we need erasure info on the lambdas or to fake up an appropriate environment + -- and erase inside. Currently the checking is imprecise + tm'' <- erase Nil tm' Nil + when top.verbose $ \ _ => putStrLn "ERASED\n\{render 80 $ pprint Nil tm'}" + debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm'} : \{render 90 $ pprint Nil ty}" + updateDef (QN ns nm) fc ty (Fn tm') + -- logMetas mstart + +processDecl ns (DCheck fc tm ty) = do + putStrLn "----- DCheck" + top <- get + + putStrLn "INFO at \{show fc}: check \{show tm} at \{show ty}" + ty' <- check (mkCtx fc) ty (VU fc) + putStrLn " got type \{render 90 $ pprint Nil ty'}" + vty <- eval Nil CBN ty' + res <- check (mkCtx fc) tm vty + putStrLn " got \{render 90 $ pprint Nil res}" + norm <- nf Nil res + putStrLn " NF \{render 90 $ pprint Nil norm}" + norm <- nfv Nil res + putStrLn " NFV \{render 90 $ pprint Nil norm}" + +processDecl ns (Class classFC nm tele decls) = do + -- REVIEW maybe we can leverage Record for this + -- a couple of catches, we don't want the dotted accessors and + -- the self argument should be an auto-implicit + putStrLn "-----" + putStrLn "Class \{nm}" + let fields = getSigs decls + -- We'll need names for the telescope + let dcName = "Mk\{nm}" + let tcType = teleToPi tele (RU classFC) + let tail = foldl mkApp (RVar classFC nm) tele + let dcType = teleToPi (impTele tele) $ foldr mkPi tail fields + + putStrLn "tcon type \{render 90 $ pretty tcType}" + putStrLn "dcon type \{render 90 $ pretty dcType}" + let decl = Data classFC nm tcType (TypeSig classFC (dcName :: Nil) dcType :: Nil) + putStrLn "Decl:" + putStrLn $ render 90 $ pretty decl + processDecl ns decl + ignore $ for fields $ \case + (fc,name,ty) => do + let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Auto Many) tail ty + let autoPat = foldl mkAutoApp (RVar classFC dcName) fields + let lhs = makeLHS (RVar fc name) tele + let lhs = RApp classFC lhs autoPat Auto + let decl = Def fc name ((lhs, (RVar fc name)) :: Nil) + + putStrLn "\{name} : \{render 90 $ pretty funType}" + putStrLn "\{render 90 $ pretty decl}" + processDecl ns $ TypeSig fc (name :: Nil) funType + processDecl ns decl + where + makeLHS : Raw → Telescope → Raw + makeLHS acc ((BI fc' nm icit quant, _) :: tele) = RApp fc' (makeLHS acc tele) (RVar fc' nm) Implicit + makeLHS acc Nil = acc + + -- TODO probably should just do the fold ourselves then. + mkAutoApp : Raw → FC × String × Raw → Raw + mkAutoApp acc (fc, nm, ty) = RApp fc acc (RVar fc nm) Explicit + + mkPi : FC × String × Raw → Raw → Raw + mkPi (fc, nm, ty) acc = RPi fc (BI fc nm Explicit Many) ty acc + + mkApp : Raw → BindInfo × Raw → Raw + mkApp acc (BI fc nm icit _, _) = RApp fc acc (RVar fc nm) icit + +-- TODO - these are big, break them out into individual functions +processDecl ns (Instance instfc ty decls) = do + + putStrLn "-----" + putStrLn "Instance \{render 90 $ pretty ty}" + top <- get + let tyFC = getFC ty + + vty <- check (mkCtx instfc) ty (VU instfc) + -- Here `tele` holds arguments to the instance + let (codomain, tele) = splitTele vty + -- env represents the environment of those arguments + let env = tenv (length tele) + debug $ \ _ => "codomain \{render 90 $ pprint Nil codomain}" + debug $ \ _ => "tele is \{show tele}" + + -- ok so we need a name, a hack for now. + -- Maybe we need to ask the user (e.g. `instance someName : Monad Foo where`) + -- or use "Monad\{show $ length' defs}" + let instname = interpolate $ pprint Nil codomain + let sigDecl = TypeSig instfc (instname :: Nil) ty + -- This needs to be declared before processing the defs, but the defs need to be + -- declared before this - side effect is that a duplicate def is noted at the first + -- member + case lookupRaw instname top of + Just _ => pure MkUnit -- TODO check that the types match + Nothing => processDecl ns sigDecl + + let (Just decls) = collectDecl <$> decls + | _ => do + debug $ \ _ => "Forward declaration \{show sigDecl}" + + let (Ref _ tconName _, args) = funArgs codomain + | (tm, _) => error tyFC "\{render 90 $ pprint Nil codomain} doesn't appear to be a TCon application" + let (Just (MkEntry _ name type (TCon cons))) = lookup tconName top + | _ => error tyFC "\{show tconName} is not a type constructor" + let (con :: Nil) = cons + | _ => error tyFC "\{show tconName} has multiple constructors \{show cons}" + let (Just (MkEntry _ _ dcty (DCon _ _))) = lookup con top + | _ => error tyFC "can't find constructor \{show con}" + vdcty@(VPi _ nm icit rig a b) <- eval Nil CBN dcty + | x => error (getFC x) "dcty not Pi" + debug $ \ _ => "dcty \{render 90 $ pprint Nil dcty}" + let (_,args) = funArgs codomain + + debug $ \ _ => "traverse \{show $ map showTm args}" + -- This is a little painful because we're reverse engineering the + -- individual types back out from the composite type + args' <- traverse (eval env CBN) args + debug $ \ _ => "args' is \{show args'}" + appty <- apply vdcty args' + conTele <- getFields appty env Nil + -- declare individual functions, collect their defs + defs <- for conTele $ \case + (MkBinder fc nm Explicit rig ty) => do + let ty' = foldr (\ x acc => case the Binder x of (MkBinder fc nm' icit rig ty') => Pi fc nm' icit rig ty' acc) ty tele + let nm' = "\{instname},\{nm}" + -- we're working with a Tm, so we define directly instead of processDecl + let (Just (Def fc name xs)) = find (\x => case the Decl x of + (Def y name xs) => name == nm + _ => False) decls + | _ => error instfc "no definition for \{nm}" + + setDef (QN ns nm') fc ty' Axiom + let decl = (Def fc nm' xs) + putStrLn "***" + putStrLn "«\{nm'}» : \{render 90 $ pprint Nil ty'}" + putStrLn $ render 80 $ pretty decl + pure $ Just decl + _ => pure Nothing + + for (mapMaybe id defs) $ \decl => do + -- debug because already printed above, but nice to have it near processing + debug $ \ _ => render 80 $ pretty decl + processDecl ns decl + let (QN _ con') = con + let decl = Def instfc instname ((RVar instfc instname, mkRHS instname conTele (RVar instfc con')) :: Nil) + putStrLn "SIGDECL" + putStrLn "\{render 90 $ pretty sigDecl}" + putStrLn $ render 80 $ pretty decl + processDecl ns decl + where + -- try to extract types of individual fields from the typeclass dcon + -- We're assuming they don't depend on each other. + getFields : Val -> Env -> List Binder -> M (List Binder) + getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do + bnd <- MkBinder fc nm Explicit rig <$> quote (length' env) ty + appsc <- sc $$ VVar fc (length' env) Lin + getFields appsc env (bnd :: bnds) + getFields tm@(VPi fc nm _ rig ty sc) env bnds = do + appsc <- sc $$ VVar fc (length' env) Lin + getFields appsc env bnds + getFields tm xs bnds = pure $ reverse bnds + + tenv : Nat -> Env + tenv Z = Nil + tenv (S k) = (VVar emptyFC (cast k) Lin :: tenv k) + + mkRHS : String -> List Binder -> Raw -> Raw + mkRHS instName (MkBinder fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit) + mkRHS instName (b :: bs) tm = mkRHS instName bs tm + mkRHS instName Nil tm = tm + + apply : Val -> List Val -> M Val + apply x Nil = pure x + apply (VPi fc nm icit rig a b) (x :: xs) = do + bx <- b $$ x + apply bx xs + apply x (y :: xs) = error instfc "expected pi type \{show x}" + +processDecl ns (ShortData fc lhs sigs) = do + (nm,args) <- getArgs lhs Nil + let ty = foldr mkPi (RU fc) args + cons <- traverse (mkDecl args Nil) sigs + let dataDecl = Data fc nm ty cons + putStrLn "SHORTDATA" + putStrLn "\{render 90 $ pretty dataDecl}" + processDecl ns dataDecl + where + mkPi : FC × Name → Raw → Raw + mkPi (fc,n) a = RPi fc (BI fc n Explicit Zero) (RU fc) a + + getArgs : Raw -> List (FC × String) -> M (String × List (FC × String)) + getArgs (RVar fc1 nm) acc = pure (nm, acc) + getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc) + getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}" + + mkDecl : List (FC × Name) -> List Raw -> Raw -> M Decl + mkDecl args acc (RVar fc' name) = do + let base = foldr (\ ty acc => RPi (getFC ty) (BI (getFC ty) "_" Explicit Many) ty acc) lhs acc + let ty = foldr mkPi base args + pure $ TypeSig fc' (name :: Nil) ty + where + mkPi : FC × String → Raw → Raw + mkPi (fc,nm) acc = RPi fc (BI fc nm Implicit Zero) (RU fc) acc + + mkDecl args acc (RApp fc' t u icit) = mkDecl args (u :: acc) t + mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}" + +processDecl ns (Data fc nm ty cons) = do + putStrLn "-----" + putStrLn "Data \{nm}" + top <- get + mc <- readIORef top.metaCtx + tyty <- check (mkCtx fc) ty (VU fc) + case lookupRaw nm top of + Just (MkEntry _ name type Axiom) => do + tyty' <- eval Nil CBN tyty + type' <- eval Nil CBN type + unifyCatch fc (mkCtx fc) tyty' type' + Just (MkEntry _ name type _) => error fc "\{show nm} already declared" + Nothing => setDef (QN ns nm) fc tyty Axiom + cnames <- for cons $ \x => case x of + (TypeSig fc names tm) => do + debug $ \ _ => "check dcon \{show names} \{show tm}" + dty <- check (mkCtx fc) tm (VU fc) + debug $ \ _ => "dty \{show names} is \{render 90 $ pprint Nil dty}" + + -- We only check that codomain used the right type constructor + -- We know it's in U because it's part of a checked Pi type + let (codomain, tele) = splitTele dty + -- for printing + let tnames = reverse $ map binderName tele + let (Ref _ hn _, args) = funArgs codomain + | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}" + when (hn /= QN ns nm) $ \ _ => + error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}" + + for names $ \ nm' => do + setDef (QN ns nm') fc dty (DCon (getArity dty) hn) + pure $ map (QN ns) names + decl => throwError $ E (getFC decl) "expected constructor declaration" + putStrLn "setDef \{nm} TCon \{show $ join cnames}" + updateDef (QN ns nm) fc tyty (TCon (join cnames)) + -- logMetas mstart + where + binderName : Binder → Name + binderName (MkBinder _ nm _ _ _) = nm + + checkDeclType : Tm -> M Unit + checkDeclType (UU _) = pure MkUnit + checkDeclType (Pi _ str icit rig t u) = checkDeclType u + checkDeclType _ = error fc "data type doesn't return U" + +processDecl ns (Record recordFC nm tele cname decls) = do + putStrLn "-----" + putStrLn "Record" + let fields = getSigs decls + let dcName = fromMaybe "Mk\{show nm}" cname + let tcType = teleToPi tele (RU recordFC) + -- REVIEW - I probably want to stick the telescope in front of the fields + let tail = foldl (\ acc bi => case the (BindInfo × Raw) bi of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) 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 + + putStrLn "tcon type \{render 90 $ pretty tcType}" + putStrLn "dcon type \{render 90 $ pretty dcType}" + let decl = Data recordFC nm tcType (TypeSig recordFC (dcName :: Nil) dcType :: Nil) + putStrLn "Decl:" + putStrLn $ render 90 $ pretty decl + processDecl ns decl + for_ fields $ \case + (fc,name,ty) => do + -- TODO dependency isn't handled yet + -- we'll need to replace stuff like `len` with `len self`. + let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Explicit Many) tail ty + let autoPat = foldl (\acc x => case the (FC × String × Raw) x of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields + + -- `fieldName` - consider dropping to keep namespace clean + -- 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 decl = Def fc name [(lhs, (RVar fc name))] + -- putStrLn "\{name} : \{render 90 $ pretty funType}" + -- putStrLn "\{render 90 $ pretty decl}" + -- processDecl ns $ TypeSig fc (name :: Nil) funType + -- processDecl ns decl + + -- `.fieldName` + let pname = "." ++ name + 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 pdecl = Def fc pname ((lhs, (RVar fc name)) :: Nil) + putStrLn "\{pname} : \{render 90 $ pretty funType}" + putStrLn "\{render 90 $ pretty pdecl}" + processDecl ns $ TypeSig fc (pname :: Nil) funType + processDecl ns pdecl diff --git a/done/Lib/Types.newt b/done/Lib/Types.newt index 316612a..54a1581 100644 --- a/done/Lib/Types.newt +++ b/done/Lib/Types.newt @@ -146,6 +146,9 @@ showCaseAlt (CaseDefault tm) = "_ => \{show tm}" showCaseAlt (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}" showCaseAlt (CaseLit lit tm) = "\{show lit} => \{show tm}" +instance Show CaseAlt where + show = showCaseAlt + showTm : Tm -> String showTm = show @@ -488,20 +491,20 @@ error fc msg = throwError $ E fc msg error' : ∀ a. String -> M a error' msg = throwError $ E emptyFC msg -freshMeta : Context -> FC -> Val -> MetaKind -> M Tm -freshMeta ctx fc ty kind = do - top <- get - mc <- readIORef top.metaCtx - debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" - writeIORef top.metaCtx $ MC (Unsolved fc mc.next ctx ty kind Nil :: mc.metas) (1 + mc.next) - pure $ applyBDs 0 (Meta fc mc.next) ctx.bds - where - -- hope I got the right order here :) - applyBDs : Int -> Tm -> List BD -> Tm - applyBDs k t Nil = t - -- review the order here - applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k) - applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs +-- freshMeta : Context -> FC -> Val -> MetaKind -> M Tm +-- freshMeta ctx fc ty kind = do +-- top <- get +-- mc <- readIORef top.metaCtx +-- debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" +-- writeIORef top.metaCtx $ MC (Unsolved fc mc.next ctx ty kind Nil :: mc.metas) (1 + mc.next) +-- pure $ applyBDs 0 (Meta fc mc.next) ctx.bds +-- where +-- -- hope I got the right order here :) +-- applyBDs : Int -> Tm -> List BD -> Tm +-- applyBDs k t Nil = t +-- -- review the order here +-- applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k) +-- applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs lookupMeta : Int -> M MetaEntry lookupMeta ix = do diff --git a/done/Lib/Util.newt b/done/Lib/Util.newt index e3de96b..51ffc22 100644 --- a/done/Lib/Util.newt +++ b/done/Lib/Util.newt @@ -11,16 +11,16 @@ funArgs tm = go tm Nil go t args = (t, args) data Binder : U where - MkBind : FC -> String -> Icit -> Quant -> Tm -> Binder + MkBinder : FC -> String -> Icit -> Quant -> Tm -> Binder -- I don't have a show for terms without a name list instance Show Binder where - show (MkBind _ nm icit quant t) = "(\{show quant}\{nm} \{show icit} : ... :: Nil)" + show (MkBinder _ nm icit quant t) = "(\{show quant}\{nm} \{show icit} : ... :: Nil)" splitTele : Tm -> (Tm × List Binder) splitTele = go Nil where go : List Binder -> Tm -> (Tm × List Binder) - go ts (Pi fc nm icit quant t u) = go (MkBind fc nm icit quant t :: ts) u + go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u go ts tm = (tm, reverse ts) diff --git a/done/Main.newt b/done/Main.newt new file mode 100644 index 0000000..0d1ba52 --- /dev/null +++ b/done/Main.newt @@ -0,0 +1,234 @@ +module Main + +import Data.List +import Data.List1 +import Data.String +import Data.Vect +import Data.IORef +import Lib.Common +import Lib.Compile +import Lib.Parser +import Lib.Elab +import Lib.Parser.Impl +import Lib.Prettier +import Lib.ProcessDecl +import Lib.Token +import Lib.Tokenizer +import Lib.TopContext +import Lib.Types +import Lib.Syntax +import Lib.Syntax +import Node +-- import System +-- import System.Directory +-- import System.File +-- import System.Path +-- import Data.Buffer + +jsonTopContext : M Json +jsonTopContext = do + top <- get + pure $ JsonObj (("context", JsonArray (map jsonDef $ listValues top.defs)) :: Nil) + where + jsonDef : TopEntry -> Json + -- There is no FC here... + jsonDef (MkEntry fc (QN ns name) type def) = JsonObj + ( ("fc", toJson fc) + :: ("name", toJson name) + :: ("type", toJson (render 80 $ pprint Nil type) ) + :: Nil) + +dumpContext : TopContext -> M Unit +dumpContext top = do + putStrLn "Context:" + go $ listValues top.defs + putStrLn "---" + where + go : List TopEntry -> M Unit + go Nil = pure MkUnit + go (x :: xs) = putStrLn " \{show x}" >> go xs + +writeSource : String -> M Unit +writeSource fn = do + docs <- compile + let src = unlines $ + ( "\"use strict\";" + :: "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" + :: Nil) + ++ map (render 90) docs + (Right _) <- liftIO {M} $ writeFile fn src + | Left err => exitFailure (show err) + -- (Right _) <- chmodRaw fn 493 | Left err => exitFailure (show err) + pure MkUnit + + +parseDecls : String -> Operators -> TokenList -> SnocList Decl -> M (List Decl × Operators) +parseDecls fn ops Nil acc = pure (acc <>> Nil, ops) +parseDecls fn ops toks@(first :: _) acc = + case partialParse fn (sameLevel parseDecl) ops toks of + Left (err, toks) => do + putStrLn $ showError "" err + addError err + parseDecls fn ops (recover toks) acc + Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl) + where + recover : TokenList -> TokenList + recover Nil = Nil + -- skip to top token, but make sure there is progress + recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds + then (tok :: toks) + else recover toks + +-- New style loader, one def at a time +processModule : FC -> String -> List String -> QName -> M String +processModule importFC base stk qn@(QN ns nm) = do + top <- get + -- TODO make top.loaded a List QName + let name = joinBy "." (snoc ns nm) + let (False) = elem name top.loaded | _ => pure "" + modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors (name :: top.loaded)top.ops) + let fn = (joinBy "/" (base :: ns)) ++ "/" ++ nm ++ ".newt" + (Right src) <- liftIO {M} $ readFile fn + | Left err => exitFailure "ERROR at \{show importFC}: error reading \{fn}: \{show err}" + let (Right toks) = tokenise fn src + | Left err => exitFailure (showError src err) + + let (Right ((nameFC, modName), ops, toks)) = partialParse fn parseModHeader top.ops toks + | Left (err, toks) => exitFailure (showError src err) + + putStrLn "module \{modName}" + let ns = split modName "." + let (path, modName') = unsnoc $ split1 modName "." + -- let bparts = split base "/" + let (True) = qn == QN path modName' + | _ => exitFailure "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}" + + let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks + | Left (err, toks) => exitFailure (showError src err) + + for_ imports $ \case + MkImport fc name' => do + let (a,b) = unsnoc $ split1 name' "." + let qname = QN a b + -- we could use `fc` if it had a filename in it + when (elem name' stk) $ \ _ => error emptyFC "import loop \{show name} -> \{show name'}" + + processModule fc base (name :: stk) qname + + top <- get + mc <- readIORef top.metaCtx + -- REVIEW suppressing unsolved and solved metas from previous files + -- I may want to know about (or exitFailure early on) unsolved + let mstart = length mc.metas + -- let Right (decls, ops, toks) = partialParse fn (manySame parseDecl) top.ops toks + -- | Left (err, toks) => exitFailure (showError src err) + (decls, ops) <- parseDecls fn top.ops toks Lin + modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors top.loaded ops) + putStrLn "process Decls" + + traverse (tryProcessDecl ns) (collectDecl decls) + + -- we don't want implict errors from half-processed functions + -- but suppress them all on error for simplicity. + errors <- readIORef top.errors + if stk == Nil then logMetas (cast mstart) else pure MkUnit + pure src + where + + -- parseDecls : + -- tryParseDecl : + tryProcessDecl : List String -> Decl -> M Unit + tryProcessDecl ns decl = do + Left err <- tryError $ processDecl ns decl | _ => pure MkUnit + addError err + + +baseDir : SnocList String -> SnocList String -> Either String String +baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil) +baseDir (dirs :< d) (ns :< n) = if d == n + then baseDir dirs ns + else Left "module path doesn't match directory" +baseDir Lin _ = Left "module path doesn't match directory" + + +processFile : String -> M Unit +processFile fn = do + putStrLn "*** Process \{fn}" + let parts = split1 fn "/" + let (dirs,file) = unsnoc parts + let dir = if dirs == Nil then "." else joinBy "/" dirs + let (name, ext) = splitFileName file + putStrLn "\{show dir} \{show name} \{show ext}" + (Right src) <- liftIO {M} $ readFile fn + | Left err => error (MkFC fn (0,0)) "error reading \{fn}: \{show err}" + let (Right toks) = tokenise fn src + | Left err => throwError err + let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader EmptyMap toks + | Left (err,toks) => throwError err + let ns = split modName "." + let (path, modName') = unsnoc $ split1 modName "." + + -- Any case splits after this point causes it to loop, no idea why + + -- let (True) = modName' == name + -- | False => throwError $ E (MkFC fn (0,0)) "module name \{modName'} doesn't match \{name}" + -- let (Right base) = baseDir (Lin <>< dirs) (Lin <>< path) + -- | Left err => pure MkUnit -- exitFailure "ERROR at \{show nameFC}: \{err}" + -- let base = if base == "" then "." else base + + -- declare internal primitives + processDecl ("Prim" :: Nil) (PType emptyFC "Int" Nothing) + processDecl ("Prim" :: Nil) (PType emptyFC "String" Nothing) + processDecl ("Prim" :: Nil) (PType emptyFC "Char" Nothing) + let base = "port" -- FIXME + src <- processModule emptyFC base Nil (QN path modName') + top <- get + -- -- dumpContext top + + -- (Nil) <- liftIO {M} $ readIORef top.errors + -- | errors => do + -- for_ errors $ \err => + -- putStrLn (showError src err) + -- exitFailure "Compile failed" + pure MkUnit + + +cmdLine : List String -> M (Maybe String × List String) +cmdLine Nil = pure (Nothing, Nil) +cmdLine ("--top" :: args) = cmdLine args -- handled later +cmdLine ("-v" :: args) = do + modify (\ top => MkTop top.defs top.metaCtx True top.errors top.loaded top.ops) + cmdLine args +cmdLine ("-o" :: fn :: args) = do + (out, files) <- cmdLine args + pure ((out <|> Just fn), files) + +cmdLine (fn :: args) = do + let (True) = isSuffixOf ".newt" fn + | _ => error emptyFC "Bad argument \{show fn}" + (out, files) <- cmdLine args + pure $ (out, fn :: files) + +main' : M Unit +main' = do + let (arg0 :: args) = getArgs + | _ => error emptyFC "error reading args" + (out, files) <- cmdLine args + traverse_ processFile files + + when (elem "--top" args) $ \ _ => do + json <- jsonTopContext + putStrLn "TOP:\{renderJson json}" + + case out of + Nothing => pure MkUnit + Just name => writeSource name + + +main : IO Unit +main = do + -- we'll need to reset for each file, etc. + ctx <- emptyTop + (Right _) <- .runM main' ctx + | Left err => exitFailure "ERROR at \{show $ getFC err}: \{errorMsg err}" + putStrLn "done" diff --git a/done/Node.newt b/done/Node.newt new file mode 100644 index 0000000..1577e9c --- /dev/null +++ b/done/Node.newt @@ -0,0 +1,34 @@ +module Node + +import Prelude + +pfunc fs : JSObject := `require('fs')` +pfunc getArgs : List String := `arrayToList(String, process.argv.slice(1))` +pfunc readFile uses (fs MkIORes Left Right) : (fn : String) -> IO (Either String String) := `(fn) => (w) => { + let result + try { + let content = fs.readFileSync(fn, 'utf8') + result = Right(undefined, undefined, content) + } catch (e) { + let err = ""+e + result = Left(undefined, undefined, e) + } + return MkIORes(undefined, result, w) +}` + +-- I wonder if I should automatically `uses` the constructors in the types +pfunc writeFile uses (fs MkIORes MkUnit) : String → String → IO (Either String Unit) := `(fn, content) => { + let result + try { + fs.writeFileSync(fn, content, 'utf8') + result = Right(undefined, undefined, MkUnit) + } catch (e) { + let err = ""+e + result = Left(undefined, undefined, e) + } + return MkIORes(undefined, result, w) +}` + +-- maybe System.exit or something, like the original putStrLn msg >> exitFailure +pfunc exitFailure : ∀ a. String → a := `(_, msg) => { throw new Error(msg) }` + diff --git a/done/Test/Parser.newt b/done/Test/Parser.newt new file mode 100644 index 0000000..e218a37 --- /dev/null +++ b/done/Test/Parser.newt @@ -0,0 +1,26 @@ +module Test.Parser + +import Prelude +import Lib.Parser +import Lib.Tokenizer +import Node + + + +main : IO Unit +main = do + let fn = "port/Lib/Parser.newt" + (Right text) <- readFile fn + | Left msg => putStrLn $ "ERROR: " ++ msg + let (Right toks) = tokenise fn text + | Left (E fc msg) => putStrLn msg + | _ => putStrLn "postpone error" + -- debugLog toks + + let (OK a toks com ops) = runP parseMod toks False EmptyMap (MkFC fn (0,0)) + | fail => debugLog fail + putStrLn "Module" + debugLog $ a + let (MkModule name imports decls) = a + let lines = map (render 90 ∘ pretty) decls + putStrLn $ joinBy "\n" lines diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 7b34b9f..6c7c715 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -9,7 +9,7 @@ the _ a = a const : ∀ a b. a → b → a const a b = a - +data Unit = MkUnit data Bool = True | False not : Bool → Bool @@ -185,9 +185,16 @@ instance Traversable List where traverse f Nil = return Nil traverse f (x :: xs) = return _::_ <*> f x <*> traverse f xs + +traverse_ : ∀ t f a b. {{Traversable t}} {{Applicative f}} → (a → f b) → t a → f Unit +traverse_ f xs = return (const MkUnit) <*> traverse f xs + for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b) for stuff fun = traverse fun stuff +for_ : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f Unit +for_ stuff fun = return (const MkUnit) <*> traverse fun stuff + instance Applicative Maybe where return a = Just a Nothing <*> _ = Nothing @@ -259,7 +266,7 @@ instance Eq String where instance Eq Char where a == b = jsEq a b -data Unit = MkUnit + ptype Array : U → U pfunc listToArray : {a : U} -> List a -> Array a := ` @@ -749,6 +756,10 @@ ordNub {a} {{ordA}} xs = go $ qsort _<_ xs go (a :: b :: xs) = if a == b then go (a :: xs) else a :: go (b :: xs) go t = t +nub : ∀ a. {{Eq a}} → List a → List a +nub Nil = Nil +nub (x :: xs) = if elem x xs then nub xs else x :: nub xs + ite : ∀ a. Bool → a → a → a ite c t e = if c then t else e @@ -809,6 +820,9 @@ force f = f MkUnit when : ∀ f. {{Applicative f}} → Bool → Lazy (f Unit) → f Unit when b fa = if b then force fa else return MkUnit +unless : ∀ f. {{Applicative f}} → Bool → Lazy (f Unit) → f Unit +unless b fa = when (not b) fa + instance ∀ a. {{Ord a}} → Ord (List a) where compare Nil Nil = EQ compare Nil ys = LT @@ -838,6 +852,12 @@ isDigit _ = False isUpper : Char → Bool isUpper c = let o = ord c in 64 < o && o < 91 +isAlphaNum : Char → Bool +isAlphaNum c = let o = ord c in + 64 < o && o < 91 || + 47 < o && o < 58 || + 96 < o && o < 123 + ignore : ∀ f a. {{Functor f}} → f a → f Unit ignore = map (const MkUnit) @@ -849,6 +869,7 @@ instance ∀ a. {{Show a}} → Show (Maybe a) where -- TODO pfunc isPrefixOf uses (True False): String → String → Bool := `(pfx, s) => s.startsWith(pfx) ? True : False` +pfunc isSuffixOf uses (True False): String → String → Bool := `(pfx, s) => s.endsWith(pfx) ? True : False` pfunc strIndex : String → Int → Char := `(s, ix) => s[ix]` @@ -861,3 +882,22 @@ getAt' i xs = getAt (cast i) xs length' : ∀ a. List a → Int length' Nil = 0 length' (x :: xs) = 1 + length' xs + +unlines : List String → String +unlines lines = joinBy "\n" lines + +-- TODO inherit Semigroup +class Monoid a where + neutral : a + +findIndex' : ∀ a. (a → Bool) → List a → Maybe Int +findIndex' {a} pred xs = go xs 0 + where + go : List a → Int → Maybe Int + go Nil ix = Nothing + go (x :: xs) ix = if pred x then Just ix else go xs (ix + 1) + +pfunc fatalError : ∀ a. String → a := `(_, msg) => { throw new Error(msg) }` + +foldlM : ∀ m a e. {{Monad m}} → (a → e → m a) → a → List e → m a +foldlM f a xs = foldl (\ ma b => ma >>= flip f b) (pure a) xs diff --git a/newt/SortedMap.newt b/newt/SortedMap.newt index 7bfd17a..9a65b1b 100644 --- a/newt/SortedMap.newt +++ b/newt/SortedMap.newt @@ -198,3 +198,6 @@ foldMap f m Nil = m foldMap f m ((a,b) :: xs) = case lookupMap a m of Nothing => foldMap f (updateMap a b m) xs Just (_, b') => foldMap f (updateMap a (f b' b) m) xs + +listValues : ∀ k v. SortedMap k v → List v +listValues sm = map snd $ toList sm diff --git a/scripts/translate.sh b/scripts/translate.sh index daf1c3a..d942c88 100755 --- a/scripts/translate.sh +++ b/scripts/translate.sh @@ -18,7 +18,7 @@ find src -type f -name '*.idr' | while read -r file; do s/\binterface\b/class/g; s/import public/import/g; s/\[\]/Nil/g; - s{\[([^<].*?)\]}{"(" . (join " ::", split /,/, $1) . " :: Nil)"}ge; + s{\[([^<|][^()]*?)\]}{"(" . (join " ::", split /,/, $1) . " :: Nil)"}ge; s/\bsym\b/symbol/g; s/^export//g; s/^\s*covering//g; diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 9d0d093..ed67b04 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -74,8 +74,8 @@ mkEnv nm k env (x :: xs) = mkEnv nm (S k) (push env (Dot (Var nm) "h\{show k}")) envNames : Env -> List String ||| given a name, find a similar one that doesn't shadow in Env -fresh : String -> JSEnv -> String -fresh nm env = if free env.env nm then nm else go nm 1 +freshName : String -> JSEnv -> String +freshName nm env = if free env.env nm then nm else go nm 1 where free : List JSExp -> String -> Bool free [] nm = True @@ -85,9 +85,9 @@ fresh nm env = if free env.env nm then nm else go nm 1 go : String -> Nat -> String go nm k = let nm' = "\{nm}\{show k}" in if free env.env nm' then nm' else go nm (S k) -fresh' : String -> JSEnv -> (String, JSEnv) -fresh' nm env = - let nm' = fresh nm env -- "\{nm}$\{show $ length env}" +freshName' : String -> JSEnv -> (String, JSEnv) +freshName' nm env = + let nm' = freshName nm env -- "\{nm}$\{show $ length env}" env' = push env (Var nm') in (nm', env') @@ -97,7 +97,7 @@ freshNames nms env = go nms env [<] go : List Name -> JSEnv -> SnocList Name -> (List String, JSEnv) go Nil env acc = (acc <>> Nil, env) go (n :: ns) env acc = - let (n', env') = fresh' n env + let (n', env') = freshName' n env in go ns env' (acc :< n') -- This is inspired by A-normalization, look into the continuation monad @@ -112,7 +112,7 @@ termToJS env (CBnd k) f = case getAt k env.env of Nothing => ?bad_bounds termToJS env CErased f = f JUndefined termToJS env (CLam nm t) f = - let (nm',env') = fresh' nm env -- "\{nm}$\{show $ length env}" + let (nm',env') = freshName' nm env -- "\{nm}$\{show $ length env}" in f $ JLam [nm'] (termToJS env' t JReturn) termToJS env (CFun nms t) f = let (nms', env') = freshNames nms env @@ -125,14 +125,14 @@ termToJS env (CLet nm (CBnd k) u) f = case getAt k env.env of Just e => termToJS (push env e) u f Nothing => ?bad_bounds2 termToJS env (CLet nm t u) f = - let nm' = fresh nm env + let nm' = freshName nm env env' = push env (Var nm') -- If it's a simple term, use const in case termToJS env t (JAssign nm') of (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) t' => JSnoc (JLet nm' t') (termToJS env' u f) termToJS env (CLetRec nm t u) f = - let nm' = fresh nm env + let nm' = freshName nm env env' = push env (Var nm') -- If it's a simple term, use const in case termToJS env' t (JAssign nm') of @@ -144,7 +144,7 @@ termToJS env (CApp t args etas) f = termToJS env t (\ t' => (argsToJS t' args [< etaExpand : JSEnv -> Nat -> SnocList JSExp -> JSExp -> JSExp etaExpand env Z args tm = Apply tm (args <>> []) etaExpand env (S etas) args tm = - let nm' = fresh "eta" env + let nm' = freshName "eta" env env' = push env (Var nm') in JLam [nm'] $ JReturn $ etaExpand (push env (Var nm')) etas (args :< Var nm') tm @@ -164,7 +164,7 @@ termToJS env (CCase t alts) f = t' => do -- TODO refactor nm to be a JSExp with Var{} or Dot{} -- FIXME sc$ seemed to shadow something else, lets get this straightened out - -- we need fresh names that are not in env (i.e. do not play in debruijn) + -- we need freshName names that are not in env (i.e. do not play in debruijn) let nm = "_sc$\{show env.depth}" let env' = { depth $= S } env JSnoc (JConst nm t') (maybeCaseStmt env' nm alts) @@ -184,8 +184,8 @@ termToJS env (CCase t alts) f = maybeCaseStmt env nm alts = (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts)) -keywords : List String -keywords = [ +jsKeywords : List String +jsKeywords = [ "break", "case", "catch", "continue", "debugger", "default", "delete", "do", "else", "finally", "for", "function", "if", "in", "instanceof", "new", "return", "switch", "this", "throw", "try", "typeof", "var", "void", "while", "with", @@ -199,7 +199,7 @@ keywords = [ ||| escape identifiers for js jsIdent : String -> Doc -jsIdent id = if elem id keywords then text ("$" ++ id) else text $ pack $ fix (unpack id) +jsIdent id = if elem id jsKeywords then text ("$" ++ id) else text $ pack $ fix (unpack id) where fix : List Char -> List Char fix [] = [] diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index fd24b7b..5611b4b 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -320,45 +320,48 @@ invert lvl sp = go sp [] -- we have to "lift" the renaming when we go under a lambda -- I think that essentially means our domain ix are one bigger, since we're looking at lvl -- in the codomain, so maybe we can just keep that value -rename : Nat -> List Nat -> Nat -> Val -> M Tm -rename meta ren lvl v = go ren lvl v - where - go : List Nat -> Nat -> Val -> M Tm - goSpine : List Nat -> Nat -> Tm -> SnocList Val -> M Tm - goSpine ren lvl tm [<] = pure tm - goSpine ren lvl tm (xs :< x) = do - xtm <- go ren lvl x - pure $ App emptyFC !(goSpine ren lvl tm xs) xtm - go ren lvl (VVar fc k sp) = case findIndex (== k) ren of - Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" - Just x => goSpine ren lvl (Bnd fc $ cast x) sp - go ren lvl (VRef fc nm def sp) = goSpine ren lvl (Ref fc nm def) sp - go ren lvl (VMeta fc ix sp) = do - -- So sometimes we have an unsolved meta in here which reference vars out of scope. - debug "rename Meta \{show ix} spine \{show sp}" - if ix == meta - -- REVIEW is this the right fc? - then error fc "meta occurs check" - else case !(lookupMeta ix) of - Solved fc _ val => do - debug "rename: \{show ix} is solved" - go ren lvl !(vappSpine val sp) - _ => do - debug "rename: \{show ix} is unsolved" - catchError (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) - go ren lvl (VLam fc n icit rig t) = pure (Lam fc n icit rig !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<]))) - go ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) - go ren lvl (VU fc) = pure (UU fc) - go ren lvl (VErased fc) = pure (Erased fc) - -- for now, we don't do solutions with case in them. - go ren lvl (VCase fc sc alts) = error fc "Case in solution" - go ren lvl (VLit fc lit) = pure (Lit fc lit) - go ren lvl (VLet fc name val body) = - pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) body) - -- these probably shouldn't show up in solutions... - go ren lvl (VLetRec fc name ty val body) = - pure $ LetRec fc name !(go ren lvl ty) !(go (lvl :: ren) (S lvl) val) !(go (lvl :: ren) (S lvl) body) + +rename : Nat -> List Nat -> Nat -> Val -> M Tm + +renameSpine : Nat -> List Nat -> Nat -> Tm -> SnocList Val -> M Tm +renameSpine meta ren lvl tm [<] = pure tm +renameSpine meta ren lvl tm (xs :< x) = do + xtm <- rename meta ren lvl x + pure $ App emptyFC !(renameSpine meta ren lvl tm xs) xtm + + + + +rename meta ren lvl (VVar fc k sp) = case findIndex (== k) ren of + Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" + Just x => renameSpine meta ren lvl (Bnd fc $ cast x) sp +rename meta ren lvl (VRef fc nm def sp) = renameSpine meta ren lvl (Ref fc nm def) sp +rename meta ren lvl (VMeta fc ix sp) = do + -- So sometimes we have an unsolved meta in here which reference vars out of scope. + debug "rename Meta \{show ix} spine \{show sp}" + if ix == meta + -- REVIEW is this the right fc? + then error fc "meta occurs check" + else case !(lookupMeta ix) of + Solved fc _ val => do + debug "rename: \{show ix} is solved" + rename meta ren lvl !(vappSpine val sp) + _ => do + debug "rename: \{show ix} is unsolved" + catchError (renameSpine meta ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) +rename meta ren lvl (VLam fc n icit rig t) = pure (Lam fc n icit rig !(rename meta (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<]))) +rename meta ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(rename meta ren lvl ty) !(rename meta (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) +rename meta ren lvl (VU fc) = pure (UU fc) +rename meta ren lvl (VErased fc) = pure (Erased fc) +-- for now, we don't do solutions with case in them. +rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution" +rename meta ren lvl (VLit fc lit) = pure (Lit fc lit) +rename meta ren lvl (VLet fc name val body) = + pure $ Let fc name !(rename meta ren lvl val) !(rename meta (lvl :: ren) (S lvl) body) +-- these probably shouldn't show up in solutions... +rename meta ren lvl (VLetRec fc name ty val body) = + pure $ LetRec fc name !(rename meta ren lvl ty) !(rename meta (lvl :: ren) (S lvl) val) !(rename meta (lvl :: ren) (S lvl) body) lams : Nat -> List String -> Tm -> Tm lams 0 _ tm = tm @@ -564,7 +567,7 @@ unifyCatch fc ctx ty' ty = do a <- quote ctx.lvl ty' b <- quote ctx.lvl ty let names = toList $ map fst ctx.types - let msg = "unification failure\n failed to unify \{pprint names a}\n with \{pprint names b}" + let msg = "xxunification failure\n failed to unify \{pprint names a}\n with \{pprint names b}" let msg = msg ++ "\nconstraints \{show cs.constraints}" throwError (E fc msg) -- error fc "Unification yields constraints \{show cs.constraints}" diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 61cfc0b..deb1b0f 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -79,6 +79,7 @@ tryEval env (VRef fc k _ sp) = do val <- vappSpine vtm sp case val of VCase _ _ _ => pure Nothing + VLetRec _ _ _ _ _ => pure Nothing v => pure $ Just v) (\ _ => pure Nothing) _ => pure Nothing diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 4701c2d..87e09d3 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -83,7 +83,7 @@ getSigs : List Decl -> List (FC, String, Raw) getSigs [] = [] getSigs ((TypeSig _ [] _) :: xs) = getSigs xs getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs -getSigs (_:: xs) = getSigs xs +getSigs (_ :: xs) = getSigs xs teleToPi : Telescope -> Raw -> Raw teleToPi [] end = end @@ -272,8 +272,8 @@ processDecl ns (Instance instfc ty decls) = do conTele <- getFields !(apply vdcty args') env [] -- declare individual functions, collect their defs defs <- for conTele $ \case - (MkBind fc nm Explicit rig ty) => do - let ty' = foldr (\(MkBind fc nm' icit rig ty'), acc => Pi fc nm' icit rig ty' acc) ty tele + (MkBinder fc nm Explicit rig ty) => do + let ty' = foldr (\(MkBinder fc nm' icit rig ty'), acc => Pi fc nm' icit rig ty' acc) ty tele let nm' = "\{instname},\{nm}" -- we're working with a Tm, so we define directly instead of processDecl let Just (Def fc name xs) = find (\case (Def y name xs) => name == nm; _ => False) decls @@ -302,7 +302,7 @@ processDecl ns (Instance instfc ty decls) = do -- We're assuming they don't depend on each other. getFields : Val -> Env -> List Binder -> M (List Binder) getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do - bnd <- MkBind fc nm Explicit rig <$> quote (length env) ty + bnd <- MkBinder fc nm Explicit rig <$> quote (length env) ty getFields !(sc $$ VVar fc (length env) [<]) env (bnd :: bnds) getFields tm@(VPi fc nm _ rig ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env bnds getFields tm xs bnds = pure $ reverse bnds @@ -312,7 +312,7 @@ processDecl ns (Instance instfc ty decls) = do tenv (S k) = (VVar emptyFC k [<] :: tenv k) mkRHS : String -> List Binder -> Raw -> Raw - mkRHS instName (MkBind fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit) + mkRHS instName (MkBinder fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit) mkRHS instName (b :: bs) tm = mkRHS instName bs tm mkRHS instName [] tm = tm @@ -364,7 +364,7 @@ processDecl ns (Data fc nm ty cons) = do -- We know it's in U because it's part of a checked Pi type let (codomain, tele) = splitTele dty -- for printing - let tnames = reverse $ map (\(MkBind _ nm _ _ _) => nm) tele + let tnames = reverse $ map (\(MkBinder _ nm _ _ _) => nm) tele let (Ref _ hn _, args) := funArgs codomain | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}" when (hn /= QN ns nm) $ diff --git a/src/Lib/Util.idr b/src/Lib/Util.idr index 2afd882..e246b8b 100644 --- a/src/Lib/Util.idr +++ b/src/Lib/Util.idr @@ -12,17 +12,17 @@ funArgs tm = go tm [] public export data Binder : Type where - MkBind : FC -> String -> Icit -> Quant -> Tm -> Binder + MkBinder : FC -> String -> Icit -> Quant -> Tm -> Binder -- I don't have a show for terms without a name list export Show Binder where - show (MkBind _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]" + show (MkBinder _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]" export splitTele : Tm -> (Tm, List Binder) splitTele = go [] where go : List Binder -> Tm -> (Tm, List Binder) - go ts (Pi fc nm icit quant t u) = go (MkBind fc nm icit quant t :: ts) u + go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u go ts tm = (tm, reverse ts)