primitive erasure implementation, dead code elimination

TODO.md

@@ -2,9 +2,10 @@
 ## TODO
 
 - [ ] add filenames to FC
-- [ ] maybe use backtick for javascript so we don't highlight strings as JS
+- [x] maybe use backtick for javascript so we don't highlight strings as JS
 - [ ] add namespaces
-- [ ] imported files leak info messages everywhere
+- [x] dead code elimination
+- [x] imported files leak info messages everywhere
   - For now, take the start ix for the file and report at end starting there
 - [ ] update node shim to include idris2-playground changes
 - [ ] accepting DCon for another type (skipping case, but should be an error)
@@ -97,9 +98,10 @@
 - [ ] decide what to do for erasure
   - I'm going to try explicit annotation, forall/∀ is erased
   - [x] Parser side
-  - [ ] push down to value/term
+  - [x] push down to value/term
-  - [ ] check quantity
+  - [ ] check quantity!!
-  - [ ] erase in output
+  - [x] erase in output
+  - [ ] remove erased top level arguments
 - [ ] type at point in vscode
 - [ ] repl
 - [ ] LSP

aoc2023/Node.newt

@@ -4,4 +4,4 @@ import Prelude
 
 pfunc fs : JSObject := `require('fs')`
 pfunc getArgs : List String := `arrayToList(String, process.argv)`
-pfunc readFile : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)`
+pfunc readFile uses (fs) : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)`

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -16,7 +16,7 @@
     },
     {
       "name": "keyword.newt",
-      "match": "\\b(data|where|do|class|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
+      "match": "\\b(data|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
     },
     {
       "name": "string.js",

playground/src/monarch.ts

@@ -77,6 +77,7 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
     "ptype",
     "pfunc",
     "if",
+    "uses",
     "then",
     "else",
     "class",

src/Lib/Compile.idr

@@ -4,6 +4,7 @@ module Lib.Compile
 import Lib.Types
 import Lib.Prettier
 import Lib.CompileExp
+import Lib.TopContext
 import Data.String
 import Data.Maybe
 import Data.Nat
@@ -94,6 +95,7 @@ termToJS : JSEnv -> CExp -> Cont e -> JSStmt e
 termToJS env (CBnd k) f = case getAt k env.env of
   (Just e) => f e
   Nothing => ?bad_bounds
+termToJS env CErased f = f JUndefined
 termToJS env (CLam nm t) f =
   let nm' = fresh nm env -- "\{nm}$\{show $ length env}"
       env' = push env (Var nm')
@@ -206,6 +208,8 @@ expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map
 
 expToDoc (LitString str) = jsString str
 expToDoc (LitInt i) = text $ show i
+-- TODO add precedence
+expToDoc (Apply x@(JLam{}) xs) = text "(" ++ expToDoc x ++ ")" ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")"
 expToDoc (Apply x xs) = expToDoc x ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")"
 expToDoc (Var nm) = jsIdent nm
 expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")"
@@ -247,25 +251,64 @@ dcon nm arity =
       obj := ("tag", LitString nm) :: map (\x => (x, Var x)) args
   in stmtToDoc $ JConst nm (JLam args (JReturn (LitObject obj)))
 
+-- use iife to turn stmts into expr
+maybeWrap : JSStmt Return -> JSExp
+maybeWrap (JReturn exp) = exp
+maybeWrap stmt = Apply (JLam [] stmt) []
 
 entryToDoc : TopEntry -> M Doc
 entryToDoc (MkEntry name ty (Fn tm)) = do
-  -- so this has a bunch of lambdas on it now, which we want to consolidate
-  -- and we might need betas? It seems like a mirror of what happens in CExp
   debug "compileFun \{pprint [] tm}"
   ct <- compileFun tm
-  -- If ct has zero arity and is a compount expression, this fails..
+  let exp = maybeWrap $ termToJS empty ct JReturn
-  let body@(JPlain {}) = termToJS empty ct JPlain
+  pure $ text "const" <+> jsIdent name <+> text "=" <+/> expToDoc exp ++ ";"
-    | js => error (getFC tm) "Not a plain expression: \{render 80 $ stmtToDoc js}"
-  pure (text "const" <+> jsIdent name <+> text "=" <+/> stmtToDoc body)
 entryToDoc (MkEntry name type Axiom) = pure ""
 entryToDoc (MkEntry name type (TCon strs)) = pure $ dcon name (piArity type)
 entryToDoc (MkEntry name type (DCon arity str)) = pure $ dcon name arity
 entryToDoc (MkEntry name type PrimTCon) = pure $ dcon name (piArity type)
-entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src
+entryToDoc (MkEntry name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src
+
+||| This version (call `reverse . snd <$> process "main" ([],[])`) will do dead
+||| code elimination, but the Prelude js primitives are reaching for
+||| stuff like True, False, MkUnit, fs which get eliminated
+process : (List String, List Doc) -> String -> M (List String, List Doc)
+process (done,docs) nm = do
+  let False = nm `elem` done | _ => pure (done,docs)
+  top <- get
+  case TopContext.lookup nm top of
+    Nothing => error emptyFC "\{nm} not in scope"
+    Just entry@(MkEntry name ty (PrimFn src uses)) => do
+      (done,docs) <- foldlM process (nm :: done, docs) uses
+      pure (done, !(entryToDoc entry) :: docs)
+    Just (MkEntry name ty (Fn tm)) => do
+                debug "compileFun \{pprint [] tm}"
+                ct <- compileFun tm
+                -- If ct has zero arity and is a compount expression, this fails..
+                let exp = maybeWrap $ termToJS empty ct JReturn
+                let doc = text "const" <+> jsIdent name <+> text "=" <+/> expToDoc exp ++ ";"
+                (done,docs) <- walkTm tm (nm :: done, docs)
+                pure (done, doc :: docs)
+
+    Just entry => pure (nm :: done, !(entryToDoc entry) :: docs)
+  where
+    walkTm : Tm -> (List String, List Doc) -> M (List String, List Doc)
+    walkAlt : (List String, List Doc) -> CaseAlt -> M (List String, List Doc)
+    walkAlt acc (CaseDefault t) = pure 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 t !(walkTm u acc)
+    walkTm (Pi x str icit y t u) acc = walkTm t !(walkTm u acc)
+    walkTm (Let x str t u) acc = walkTm t !(walkTm u acc)
+    walkTm (LetRec x str t u) acc = walkTm t !(walkTm u acc)
+    walkTm (Case x t alts) acc = foldlM walkAlt acc alts
+    walkTm _ acc = pure acc
 
 export
 compile : M (List Doc)
-compile = do
+-- compile = do
-  top <- get
+--   top <- get
-  traverse entryToDoc top.defs
+--   traverse entryToDoc top.defs
+compile = reverse . snd <$> process ([],[]) "main"

src/Lib/CompileExp.idr

@@ -1,5 +1,5 @@
 ||| First pass of compilation
-||| - work out arities and fully apply functions / constructors
+||| - work out arities and fully apply functions / constructors (currying)
 ||| - expand metas
 ||| I could make names unique (e.q. on lambdas), but I might want that to vary per backend?
 module Lib.CompileExp
@@ -36,41 +36,48 @@ data CExp : Type where
   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.
 export
-getArity : Tm -> Nat
+lamArity : Tm -> Nat
-getArity (Lam _ _ t) = S (getArity t)
+lamArity (Lam _ _ t) = S (lamArity t)
-getArity _ = Z
+lamArity _ = Z
 
 export
 piArity : Tm -> Nat
-piArity (Pi _ _ _ _ b) = S (piArity b)
+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 -> Name -> M Nat
 arityForName fc nm = case lookup nm !get of
   -- let the magic hole through for now (will generate bad JS)
-  Nothing => if nm == "?" then pure 0 else error fc "Name \{show nm} not in scope"
+  Nothing => error fc "Name \{show nm} not in scope"
   (Just (MkEntry name type Axiom)) => pure 0
   (Just (MkEntry name type (TCon strs))) => pure $ piArity type
   (Just (MkEntry name type (DCon k str))) => pure k
-  (Just (MkEntry name type (Fn t))) => pure $ getArity t
+  (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))) => pure $ piArity type
+  (Just (MkEntry name type (PrimFn t uses))) => pure $ piArity type
 
 export
 compileTerm : Tm -> M CExp
 
 -- need to eta out extra args, fill in the rest of the apps
-apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp
+apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp
--- out of args, make one up
+-- out of args, make one up (fix that last arg)
-apply t [] acc (S k) = pure $
+apply t [] acc (S k) ty = pure $
-  CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k)
+  CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k ty)
-apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k
+apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) =  apply t xs (acc :< CErased) k b
-apply t ts acc 0 = go (CApp t (acc <>> [])) ts
+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}"
+apply t ts acc 0 ty = go (CApp t (acc <>> [])) ts
   where
     go : CExp -> List CExp -> M CExp
     -- drop zero arg call
@@ -78,37 +85,60 @@ apply t ts acc 0 = go (CApp t (acc <>> [])) ts
     go t [] = pure t
     go t (arg :: args) = go (CApp t [arg]) args
 
+-- apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp
+-- -- out of args, make one up
+-- apply t [] acc (S k) = pure $
+--   CLam "eta\{show k}" !(apply t [] (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 <>> [])) ts
+--   where
+--     go : CExp -> List CExp -> M CExp
+--     -- drop zero arg call
+--     go (CApp t []) args = go t args
+--     go t [] = pure t
+--     go t (arg :: args) = go (CApp t [arg]) args
+
 compileTerm (Bnd _ k) = pure $ CBnd k
 -- need to eta expand to arity
-compileTerm t@(Ref fc nm _) = apply (CRef nm) [] [<] !(arityForName fc nm)
+compileTerm t@(Ref fc nm _) = do
+  top <- get
+  let Just (MkEntry _ type _) = lookup nm top
+          | Nothing => error fc "Undefined name \{nm}"
+  apply (CRef nm) [] [<] !(arityForName fc nm) type
 
 compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
 compileTerm (Lam _ nm t) = pure $ CLam nm !(compileTerm t)
 compileTerm tm@(App _ _ _) with (funArgs tm)
   _ | (Meta _ k, args) = do
         -- FIXME get arity or zonk?
+        -- let's see if this happens after zonking
+        error (getFC tm) "Lambda in CompileExp"
         -- Maybe we should be storing the Term without the lambdas...
         -- we don't have a lot here, but JS has an "environment" with names and
         -- we can assume fully applied.
-        meta <- lookupMeta k
+        -- meta <- lookupMeta k
-        args' <- traverse compileTerm args
+        -- args' <- traverse compileTerm args
-        -- apply (CRef "Meta\{show k}") args' [<] 0
+        -- -- apply (CRef "Meta\{show k}") args' [<] 0
-        arity <- case meta of
+        -- arity <- case meta of
-                -- maybe throw
+        --         -- maybe throw
-                (Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds
+        --         (Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds
-                (Solved _ j tm) => pure $ getArity !(quote 0 tm)
+        --         (Solved _ j tm) => pure $ lamArity !(quote 0 tm)
-        apply (CRef "Meta\{show k}") args' [<] arity
+        -- apply (CRef "Meta\{show k}") args' [<] arity
   _ | (t@(Ref fc nm _), args) = do
         args' <- traverse compileTerm args
         arity <- arityForName fc nm
-        apply (CRef nm) args' [<] arity
+        top <- get
+        let Just (MkEntry _ type _) = lookup nm top
+          | Nothing => error fc "Undefined name \{nm}"
+        apply (CRef nm) args' [<] arity type
   _ | (t, args) = do
         debug "apply other \{pprint [] t}"
         t' <- compileTerm t
         args' <- traverse compileTerm args
-        apply t' args' [<] 0
+        apply t' args' [<] 0 (U emptyFC)
+        -- error (getFC t) "Don't know how to apply \{showTm t}"
 compileTerm (U _) = pure $ CRef "U"
-compileTerm (Pi _ nm icit t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)]
+compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)]
 compileTerm (Case _ t alts) = do
   t' <- compileTerm t
   alts' <- traverse (\case

src/Lib/Elab.idr

@@ -173,7 +173,7 @@ rename meta ren lvl v = go ren lvl v
             debug "rename: \{show ix} is unsolved"
             catchError {e=Error} (goSpine ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err))
     go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<])))
-    go ren lvl (VPi fc n icit ty tm) = pure (Pi fc n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC 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 (U fc)
     -- for now, we don't do solutions with case in them.
     go ren lvl (VCase fc sc alts) = error fc "Case in solution"
@@ -278,7 +278,7 @@ unify env mode t u = do
         else solve env k sp (VMeta fc' k' sp') >> pure neutral
     unify' t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral
     unify' (VMeta fc i sp) t' = solve env i sp t' >> pure neutral
-    unify' (VPi fc _ _ a b) (VPi fc' _ _ a' b') = do
+    unify' (VPi fc _ _ _ a b) (VPi fc' _ _ _ a' b') = do
       let fresh = VVar fc (length env) [<]
       [| unify env mode a a' <+> unify (fresh :: env) mode !(b $$ fresh) !(b' $$ fresh) |]
 
@@ -378,14 +378,14 @@ unifyCatch fc ctx ty' ty = do
 insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
   case !(forceMeta ty) of
-    VPi fc x Auto a b => do
+    VPi fc x Auto rig a b => do
       -- FIXME mark meta as auto, maybe try to solve here?
       m <- freshMeta ctx (getFC tm) a AutoSolve
       debug "INSERT Auto \{pprint (names ctx) m} : \{show a}"
       debug "TM \{pprint (names ctx) tm}"
       mv <- eval ctx.env CBN m
       insert ctx (App (getFC tm) tm m) !(b $$ mv)
-    VPi fc x Implicit a b => do
+    VPi fc x Implicit rig a b => do
       m <- freshMeta ctx (getFC tm) a Normal
       debug "INSERT \{pprint (names ctx) m} : \{show a}"
       debug "TM \{pprint (names ctx) tm}"
@@ -482,7 +482,7 @@ getConstructors ctx scfc tm = error scfc "Can't split - not VRef: \{!(pprint ctx
 -- 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 a b) nms sc = do
+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) [<]
@@ -499,7 +499,7 @@ substVal k v tm = go tm
     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 a b) = VPi fc nm icit (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
@@ -850,7 +850,7 @@ buildLitCases ctx prob fc scnm scty = do
 -- This process is similar to extendPi, but we need to stop
 -- if one clause is short on patterns.
 buildTree ctx (MkProb [] ty) = error emptyFC "no clauses"
-buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit a b)) = do
+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
@@ -934,7 +934,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
   -- rendered in ProcessDecl
   (RHole fc, ty) => freshMeta ctx fc ty User
 
-  (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' a b)) => do
+  (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) [<]
@@ -952,7 +952,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
   (t@(RLam _ (BI fc nm icit quant) tm), ty) =>
             error fc "Expected pi type, got \{!(prvalCtx ty)}"
 
-  (tm, ty@(VPi fc nm' Implicit a b)) => do
+  (tm, ty@(VPi fc nm' Implicit rig a b)) => do
     let names = toList $ map fst ctx.types
     debug "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} "
     let var = VVar fc (length ctx.env) [<]
@@ -980,8 +980,8 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
       -- Kovacs doesn't insert on tm = Implicit Lam, we don't have Plicity in Lam
       -- so I'll check the inferred type for an implicit pi
       -- This seems wrong, the ty' is what insert runs on, so we're just short circuiting here
-      (tm'@(Lam{}), ty'@(VPi _ _ Implicit _ _)) => do debug "CheckMe 1"; pure (tm', ty')
+      (tm'@(Lam{}), ty'@(VPi _ _ Implicit rig _ _)) => do debug "CheckMe 1"; pure (tm', ty')
-      (tm'@(Lam{}), ty'@(VPi _ _ Auto _ _)) => do debug "CheckMe 2"; pure (tm', ty')
+      (tm'@(Lam{}), ty'@(VPi _ _ Auto rig _ _)) => do debug "CheckMe 2"; pure (tm', ty')
       (tm', ty') => do
         debug "RUN INSERT ON \{pprint names tm'} at \{show ty'}"
         insert ctx tm' ty'
@@ -1016,7 +1016,7 @@ infer ctx (RApp fc t u icit) = do
         pure (Auto, t, tty)
 
   (a,b) <- case !(forceMeta tty) of
-    (VPi fc str icit' a b) => if icit' == icit then pure (a,b)
+    (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
@@ -1025,7 +1025,8 @@ infer ctx (RApp fc t u icit) = do
       debug "unify PI for \{show tty}"
       a <- eval ctx.env CBN !(freshMeta ctx fc (VU emptyFC) Normal)
       b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal
-      unifyCatch fc ctx tty (VPi fc ":ins" icit a b)
+      -- 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
@@ -1036,7 +1037,7 @@ 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 ty' 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'
@@ -1057,8 +1058,7 @@ infer ctx (RLam _ (BI fc nm icit quant) tm) = do
   let ctx' = extend ctx nm a
   (tm', b) <- infer ctx' tm
   debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}"
-  pure $ (Lam fc nm tm', VPi fc nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
+  pure $ (Lam fc nm tm', VPi fc nm icit quant a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
-  -- error {ctx} [DS "can't infer lambda"]
 
 infer ctx (RImplicit fc) = do
   ty <- freshMeta ctx fc (VU emptyFC) Normal

src/Lib/Eval.idr

@@ -150,7 +150,7 @@ eval env mode (Meta fc i) =
         (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<]
         (Solved _ k t) => pure $ t
 eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
-eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
+eval env mode (Pi fc x icit rig a b) = pure $ VPi fc x icit rig !(eval env mode a) (MkClosure env b)
 eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) !(eval (VVar fc (length env) [<] :: env) mode u)
 eval env mode (LetRec fc nm t u) = pure $ VLetRec fc nm !(eval (VVar fc (length env) [<] :: env) mode t) !(eval (VVar fc (length env) [<] :: env) mode u)
 -- Here, we assume env has everything. We push levels onto it during type checking.
@@ -186,7 +186,7 @@ quote l (VMeta fc i sp) =
         (Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp
         (Solved _ k t) => quote l !(vappSpine t sp)
 quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<]))
-quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
+quote l (VPi fc x icit rig a b) = pure $ Pi fc x icit rig !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
 quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) u)
 quote l (VLetRec fc nm t u) = pure $ LetRec fc nm !(quote (S l) t) !(quote (S l) u)
 quote l (VU fc) = pure (U fc)
@@ -260,7 +260,7 @@ zonk top l env t = case t of
   (Meta fc k) => zonkApp top l env t []
   (Lam fc nm u) => Lam fc nm <$> (zonk top (S l) (VVar fc l [<] :: env) u)
   (App fc t u) => zonkApp top l env t [!(zonk top l env u)]
-  (Pi fc nm icit a b) => Pi fc nm icit <$> zonk top l env a <*> zonkBind top l env b
+  (Pi fc nm icit rig a b) => Pi fc nm icit rig <$> zonk top l env a <*> zonkBind top l env b
   (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u
   (LetRec fc nm t u) => LetRec fc nm <$> zonkBind top l env t <*> zonkBind top l env u
   (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts

src/Lib/Parser.idr

@@ -396,11 +396,12 @@ parsePFunc = do
   fc <- getPos
   keyword "pfunc"
   nm <- ident
+  uses <- optional (keyword "uses" >> parens (many $ uident <|> ident <|> token MixFix))
   keyword ":"
   ty <- typeExpr
   keyword ":="
   src <- cast <$> token JSLit
-  pure $ PFunc fc nm ty src
+  pure $ PFunc fc nm (fromMaybe [] uses) ty src
 
 export
 parseData : Parser Decl

src/Lib/ProcessDecl.idr

@@ -18,8 +18,8 @@ import Lib.Util
 -- 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 t u) = False
+isCandidate ty (Pi fc nm Explicit rig t u) = False
-isCandidate ty (Pi fc nm icit t u) = isCandidate ty u
+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
@@ -73,8 +73,9 @@ contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
           writeIORef top.metas mc
           go xs)
 
+-- FIXME - decide if we want to count Zero here
 getArity : Tm -> Nat
-getArity (Pi x str icit t u) = S (getArity u)
+getArity (Pi x str icit rig t u) = S (getArity u)
 -- Ref or App (of type constructor) are valid
 getArity _ = Z
 
@@ -181,12 +182,16 @@ processDecl (PType fc nm ty) = do
   ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc)
   setDef nm fc ty' PrimTCon
 
-processDecl (PFunc fc nm ty src) = do
+processDecl (PFunc fc nm uses ty src) = do
   top <- get
   ty <- check (mkCtx fc) ty (VU fc)
   ty' <- nf [] ty
   putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}"
-  setDef nm fc ty' (PrimFn src)
+  -- TODO wire through fc?
+  for_ uses $ \ name => case lookup name top of
+    Nothing => error fc "\{name} not in scope"
+    _ => pure ()
+  setDef nm fc ty' (PrimFn src uses)
 
 processDecl (Def fc nm clauses) = do
   putStrLn "-----"
@@ -274,7 +279,7 @@ processDecl (Class classFC nm tele decls) = do
     getSigs (_:: xs) = getSigs xs
 
     impTele : Telescope
-    impTele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit quant, ty)) tele
+    impTele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tele
 
     teleToPi : Telescope -> Raw -> Raw
     teleToPi [] end = end
@@ -309,7 +314,7 @@ processDecl (Instance instfc ty decls) = do
     | _ => error tyFC "\{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 a b) <- eval [] CBN dcty
+  vdcty@(VPi _ nm icit rig a b) <- eval [] CBN dcty
     | x => error (getFC x) "dcty not Pi"
   debug "dcty \{pprint [] dcty}"
   let (_,args) = funArgs codomain
@@ -322,8 +327,8 @@ processDecl (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 ty) => do
+     (MkBind fc nm Explicit rig ty) => do
-       let ty' = foldr (\(MkBind fc nm' icit ty'), acc => Pi fc nm' icit ty' acc) ty tele
+       let ty' = foldr (\(MkBind 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
        setDef nm' fc ty' Axiom
@@ -353,10 +358,10 @@ processDecl (Instance instfc ty decls) = do
     -- 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 ty sc) env bnds = do
+    getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do
-      bnd <- MkBind fc nm Explicit <$> quote (length env) ty
+      bnd <- MkBind fc nm Explicit rig <$> quote (length env) ty
       getFields !(sc $$ VVar fc (length env) [<]) env (bnd :: bnds)
-    getFields tm@(VPi fc nm _ ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env 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
 
     tenv : Nat -> Env
@@ -364,13 +369,13 @@ processDecl (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 ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit)
+    mkRHS instName (MkBind 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
 
     apply : Val -> List Val -> M Val
     apply x [] = pure x
-    apply (VPi fc nm icit a b) (x :: xs) = apply !(b $$ x) xs
+    apply (VPi fc nm icit rig a b) (x :: xs) = apply !(b $$ x) xs
     apply x (y :: xs) = error instfc "expected pi type \{show x}"
 
 processDecl (Data fc nm ty cons) = do
@@ -395,7 +400,7 @@ processDecl (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 (\(MkBind _ nm _ _ _) => nm) tele
           let (Ref _ hn _, args) := funArgs codomain
             | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}"
           when (hn /= nm) $
@@ -411,5 +416,5 @@ processDecl (Data fc nm ty cons) = do
   where
     checkDeclType : Tm -> M ()
     checkDeclType (U _) = pure ()
-    checkDeclType (Pi _ str icit t u) = checkDeclType u
+    checkDeclType (Pi _ str icit rig t u) = checkDeclType u
     checkDeclType _ = error fc "data type doesn't return U"

src/Lib/Syntax.idr

@@ -120,7 +120,7 @@ data Decl
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
   | PType FC Name (Maybe Raw)
-  | PFunc FC Name Raw String
+  | PFunc FC Name (List String) Raw String
   | PMixFix FC (List Name) Nat Fixity
   | Class FC Name Telescope (List Decl)
   | Instance FC Raw (List Decl)
@@ -132,7 +132,7 @@ HasFC Decl where
   getFC (DCheck x tm tm1) = x
   getFC (Data x str tm xs) = x
   getFC (PType x str mtm) = x
-  getFC (PFunc x str tm str1) = x
+  getFC (PFunc x str _ tm str1) = x
   getFC (PMixFix x strs k y) = x
   getFC (Class x str xs ys) = x
   getFC (Instance x tm xs) = x
@@ -176,7 +176,7 @@ Show Decl where
   show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys]
   show (DCheck _ x y) = foo ["DCheck", show x, show y]
   show (PType _ name ty) = foo ["PType", name, show ty]
-  show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src]
+  show (PFunc _ nm uses ty src) = foo ["PFunc", nm, show uses, show ty, show src]
   show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
   show (Class _ nm tele decls) = foo ["Class",  nm, "...", show $ map show decls]
   show (Instance _ nm decls) = foo ["Instance",  show nm, show $ map show decls]
@@ -278,7 +278,8 @@ Pretty Decl where
   pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map pretty xs))
   pretty (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
   pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
-  pretty (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
+  pretty (PFunc _ nm [] ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
+  pretty (PFunc _ nm uses ty src) = "pfunc" <+> text nm <+> "uses" <+> spread (map text uses) <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
   pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
   pretty (Class _ _ _ _) = text "TODO pretty Class"
   pretty (Instance _ _ _) = text "TODO pretty Instance"

src/Lib/Types.idr

@@ -50,9 +50,15 @@ data Quant = Zero | Many
 
 public export
 Show Quant where
-  show Zero = "0"
+  show Zero = "0 "
   show Many = ""
 
+Eq Quant where
+  Zero == Zero = True
+  Many == Many = True
+  _ == _ = False
+
+-- We could make this polymorphic and use for environment...
 public export
 data BindInfo : Type where
   BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo
@@ -114,7 +120,7 @@ data Tm : Type where
   Lam : FC -> Name -> Tm -> Tm
   App : FC -> Tm -> Tm -> Tm
   U   : FC -> Tm
-  Pi  : FC -> Name -> Icit -> Tm -> Tm -> Tm
+  Pi  : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm
   Case : FC -> Tm -> List CaseAlt -> Tm
   -- need type?
   Let : FC -> Name -> Tm -> Tm -> Tm
@@ -132,7 +138,7 @@ HasFC Tm where
   getFC (Lam fc str t) = fc
   getFC (App fc t u) = fc
   getFC (U fc) = fc
-  getFC (Pi fc str icit t u) = fc
+  getFC (Pi fc str icit quant t u) = fc
   getFC (Case fc t xs) = fc
   getFC (Lit fc _) = fc
   getFC (Let fc _ _ _) = fc
@@ -156,9 +162,9 @@ Show Tm where
   show (Meta _ i) = "(Meta \{show i})"
   show (Lit _ l) = "(Lit \{show l})"
   show (U _) = "U"
-  show (Pi _ str Explicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
+  show (Pi _ str Explicit rig t u) = "(Pi (\{show rig} \{str} : \{show t}) => \{show u})"
-  show (Pi _ str Implicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
+  show (Pi _ str Implicit rig t u) = "(Pi {\{show rig} \{str} : \{show t}} => \{show u})"
-  show (Pi _ str Auto t u) = "(Pi {{\{str} : \{show t}}} => \{show u})"
+  show (Pi _ str Auto rig t u) = "(Pi {{\{show rig} \{str} : \{show t}}} => \{show u})"
   show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
   show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})"
   show (LetRec _ nm t u) = "(LetRec \{nm} \{show t} \{show u})"
@@ -186,7 +192,7 @@ Eq (Tm) where
   (Lam _ n t) == Lam _ n' t' = t == t'
   (App _ t u) == App _ t' u' = t == t' && u == u'
   (U _) == (U _) = True
-  (Pi _ n icit t u) == (Pi _ n' icit' t' u') = icit == icit' && t == t' && u == u'
+  (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u'
   _ == _ = False
 
 
@@ -223,14 +229,14 @@ pprint names tm = go 0 names tm
     go p names (Lam _ nm t) = parens 0 p $ nest 2 $ text "\\ \{nm} =>" <+/> go 0 (nm :: names) t
     go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u
     go p names (U _) = "U"
-    go p names (Pi _ nm Auto t u) = parens 0 p $
+    go p names (Pi _ nm Auto rig t u) = parens 0 p $
-      text "{{" <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u
+      text "{{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u
-    go p names (Pi _ nm Implicit t u) = parens 0 p $
+    go p names (Pi _ nm Implicit rig t u) = parens 0 p $
-      text "{" <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u
+      text "{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u
-    go p names (Pi _ "_" Explicit t u) =
+    go p names (Pi _ "_" Explicit Many t u) =
       parens 0 p $ go 1 names t <+> "->" <+> go 0 ("_" :: names) u
-    go p names (Pi _ nm Explicit t u) = parens 0 p $
+    go p names (Pi _ nm Explicit rig t u) = parens 0 p $
-      text "(" ++ text nm <+> ":" <+> go 0 names t ++ ")" <+> "->" <+> go 0 (nm :: names) u
+      text "(" ++  text (show rig) <+> text nm <+> ":" <+> go 0 names t ++ ")" <+> "->" <+> go 0 (nm :: names) u
     -- FIXME - probably way wrong on the names here.  There is implicit binding going on
     go p names (Case _ sc alts) = parens 0 p $ text "case" <+> go 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (goAlt 0 names) alts)))
     go p names (Lit _ lit) = text (show lit)
@@ -266,7 +272,7 @@ data Val : Type where
   -- we'll need to look this up in ctx with IO
   VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val
   VLam : FC -> Name -> Closure -> Val
-  VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val
+  VPi : FC -> Name -> Icit -> Quant -> (a : Lazy Val) -> (b : Closure) -> Val
   VLet : FC -> Name -> Val -> Val -> Val
   VLetRec : FC -> Name -> Val -> Val -> Val
   VU : FC -> Val
@@ -279,7 +285,7 @@ getValFC (VRef fc _ _ _) = fc
 getValFC (VCase fc _ _) = fc
 getValFC (VMeta fc _ _) = fc
 getValFC (VLam fc _ _) = fc
-getValFC (VPi fc _ _ a b) = fc
+getValFC (VPi fc _ _ _ a b) = fc
 getValFC (VU fc) = fc
 getValFC (VLit fc _) = fc
 getValFC (VLet fc _ _ _) = fc
@@ -299,8 +305,8 @@ Show Val where
   show (VRef _ nm _ sp) = "(\{nm} \{unwords $ map show (sp <>> [])})"
   show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ length sp} sp])"
   show (VLam _ str x) = "(%lam \{str} \{show x})"
-  show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
+  show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show  x}}. \{show  y})"
-  show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"
+  show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show  x}). \{show  y})"
   show (VCase fc sc alts) = "(%case \{show sc} ...)"
   show (VU _) = "U"
   show (VLit _ lit) = show lit
@@ -375,7 +381,8 @@ record MetaContext where
 
 
 public export
-data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm | PrimTCon | PrimFn String
+data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm | PrimTCon
+         | PrimFn String (List String)
 
 public export
 covering
@@ -385,7 +392,7 @@ Show Def where
   show (DCon k tyname) = "DCon \{show k} \{show tyname}"
   show (Fn t) = "Fn \{show t}"
   show (PrimTCon) = "PrimTCon"
-  show (PrimFn src) = "PrimFn \{show src}"
+  show (PrimFn src uses) = "PrimFn \{show src} \{show uses}"
 
 ||| entry in the top level context
 public export

src/Lib/Util.idr

@@ -13,12 +13,12 @@ funArgs tm = go tm []
 
 public export
 data Binder : Type where
-  MkBind : FC -> String -> Icit -> Tm -> Binder
+  MkBind : 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 t) = "[\{nm} \{show icit} : ...]"
+  show (MkBind _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]"
 
 data Foo : Type -> Type where
   MkFoo : Nat -> Foo a
@@ -28,5 +28,5 @@ splitTele : Tm -> (Tm, List Binder)
 splitTele = go []
   where
     go : List Binder -> Tm -> (Tm, List Binder)
-    go ts (Pi fc nm icit t u) = go (MkBind fc nm icit t :: ts) u
+    go ts (Pi fc nm icit quant t u) = go (MkBind fc nm icit quant t :: ts) u
     go ts tm = (tm, reverse ts)