diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt index c8ed6c1..cbc9055 100644 --- a/src/Lib/Compile.newt +++ b/src/Lib/Compile.newt @@ -302,7 +302,7 @@ getNames : Tm -> List QName -> List QName getNames (Ref x nm) acc = nm :: acc getNames (Lam x str _ _ t) acc = getNames t acc getNames (App x t u) acc = getNames u $ getNames t acc -getNames (Pi x str icit y t u) acc = getNames u $ getNames t acc +getNames (Pi x str icit y t u) acc = getNames u $ getNames t $ QN primNS "PiType" :: acc getNames (Let x str t u) acc = getNames u $ getNames t acc getNames (LetRec x str _ t u) acc = getNames u $ getNames t acc getNames (Case x t alts) acc = foldl getAltNames acc alts diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 525a8d4..deaa062 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -143,7 +143,7 @@ compileTerm (UU _) = pure $ CRef (QN Nil "U") compileTerm (Pi _ nm icit rig t u) = do t' <- compileTerm t u' <- compileTerm u - pure $ CAppRef (QN Nil "PiType") (t' :: CLam nm u' :: Nil) 0 + pure $ CAppRef (QN primNS "PiType") (t' :: CLam nm u' :: Nil) 0 compileTerm (Case fc t alts) = do t' <- compileTerm t alts' <- for alts $ \case diff --git a/src/Main.newt b/src/Main.newt index 645a3ba..23911b1 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -21,6 +21,7 @@ import Lib.Syntax import Node import Serialize +-- For editors, dump some information about the context (fc, name, type) jsonTopContext : M Json jsonTopContext = do top <- getTop @@ -50,7 +51,6 @@ writeSource fn = do docs <- compile let src = unlines $ ( "\"use strict\";" - :: "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 });" :: "const bouncer = (f,ini) => { let obj = ini; while (obj.tag !== 'return') obj = f(obj); return obj.h0 };" :: Nil) ++ map (render 90 ∘ noAlt) docs @@ -230,6 +230,7 @@ processFile fn = do processDecl primNS (PType emptyFC "Int" Nothing) processDecl primNS (PType emptyFC "String" Nothing) processDecl primNS (PType emptyFC "Char" Nothing) + setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil top <- getTop let modules = updateMap primNS (MkModCtx "" top.defs (MC EmptyMap Nil 0 CheckAll) top.ops) top.modules @@ -241,7 +242,6 @@ processFile fn = do showErrors fn src pure MkUnit - cmdLine : List String -> M (Maybe String × List String) cmdLine Nil = pure (Nothing, Nil) cmdLine ("--top" :: args) = cmdLine args -- handled later