add quantity to parser

2024-11-25 21:12:13 -08:00
parent da1cbd2ce6
commit 07cbeec6cc
7 changed files with 76 additions and 50 deletions
--- a/TODO.md
+++ b/TODO.md
@@ -2,6 +2,7 @@
 ## TODO

 - [ ] add filenames to FC
+- [ ] maybe use backtick for javascript so we don't highlight strings as JS
 - [ ] add namespaces
 - [ ] imported files leak info messages everywhere
  - For now, take the start ix for the file and report at end starting there
@@ -94,6 +95,11 @@
 - [ ] detect extra clauses in case statements
 - [ ] add test framework
 - [ ] decide what to do for erasure
+  - I'm going to try explicit annotation, forall/∀ is erased
+  - [x] Parser side
+  - [ ] push down to value/term
+  - [ ] check quantity
+  - [ ] erase in output
 - [ ] type at point in vscode
 - [ ] repl
 - [ ] LSP
--- a/port/Prelude.newt
+++ b/port/Prelude.newt
@@ -207,11 +207,11 @@ pfunc listToArray : {a : U} -> List a -> Array a := "
 }
 "

-pfunc alen : {a : U} -> Array a -> Int := "(a,arr) => arr.length"
-pfunc aget : {a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]"
-pfunc aempty : {a : U} -> Unit -> Array a := "() => []"
+pfunc alen : {0 a : U} -> Array a -> Int := "(a,arr) => arr.length"
+pfunc aget : {0 a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]"
+pfunc aempty : {0 a : U} -> Unit -> Array a := "() => []"

-pfunc arrayToList : {a} → Array a → List a := "(a,arr) => {
+pfunc arrayToList : {0 a} → Array a → List a := "(a,arr) => {
  let rval = Nil(a)
  for (let i = arr.length - 1;i >= 0; i--) {
    rval = _$3A$3A_(a, arr[i], rval)
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -906,10 +906,10 @@ undo : List DoStmt -> M Raw
 undo [] = error emptyFC "do block must end in expression"
 undo ((DoExpr fc tm) :: Nil) = pure tm
 -- TODO decide if we want to use >> or just >>=
-undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc "_" Explicit !(undo xs)) Explicit
+undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) !(undo xs)) Explicit
 -- undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>_") tm Explicit) !(undo xs) Explicit
 undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs
-undo ((DoArrow fc nm tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc nm Explicit !(undo xs)) Explicit
+undo ((DoArrow fc nm tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc nm Explicit Many) !(undo xs)) Explicit

 check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
  (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty
@@ -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 nm icit tm), ty@(VPi fc' nm' icit' a b)) => do
+  (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' a b)) => do
          debug "icits \{nm} \{show icit} \{nm'} \{show icit'}"
          if icit == icit' then do
              let var = VVar fc (length ctx.env) [<]
@@ -949,7 +949,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
              pure $ Lam fc nm' sc
            else
              error fc "Icity issue checking \{show t} at \{show ty}"
-  (t@(RLam fc nm icit tm), ty) =>
+  (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
@@ -1032,10 +1032,9 @@ infer ctx (RApp fc t u icit) = do
  pure (App fc t u, !(b $$ !(eval ctx.env CBN u)))

 infer ctx (RU fc) = pure (U fc, VU fc) -- YOLO
-infer ctx (RPi fc nm icit ty ty2) = do
+infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do
  ty' <- check ctx ty (VU fc)
  vty' <- eval ctx.env CBN ty'
-  let nm := fromMaybe "_" nm
  ty2' <- check (extend ctx nm vty') ty2 (VU fc)
  pure (Pi fc nm icit ty' ty2', (VU fc))
 infer ctx (RLet fc nm ty v sc) = do
@@ -1053,7 +1052,7 @@ infer ctx (RAnn fc tm rty) = do
  tm <- check ctx tm vty
  pure (tm, vty)

-infer ctx (RLam fc nm icit tm) = do
+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
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -172,8 +172,8 @@ letExpr = do
      t <- typeExpr
      pure (name,fc,t)

-pLetArg : Parser (Icit, String, Maybe Raw)
-pLetArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
+pLamArg : Parser (Icit, String, Maybe Raw)
+pLamArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
       <|> (Auto,,) <$> dbraces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
       <|> (Explicit,,) <$> parens (ident <|> uident) <*> optional (sym ":" >> typeExpr)
       <|> (Explicit,,Nothing) <$> (ident <|> uident)
@@ -183,11 +183,12 @@ pLetArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> ty
 export
 lamExpr : Parser Raw
 lamExpr = do
+  pos <- getPos
  keyword "\\" <|> keyword "λ"
-  args <- some $ withPos pLetArg
+  args <- some $ withPos pLamArg
  keyword "=>"
  scope <- typeExpr
-  pure $ foldr (\(fc, icit, name, ty), sc => RLam fc name icit sc) scope args
+  pure $ foldr (\(fc, icit, name, ty), sc => RLam pos (BI fc name icit Many) sc) scope args


 -- Idris just has a term on the LHS and sorts it out later..
@@ -262,23 +263,28 @@ term =  caseExpr
 varname : Parser String
 varname = (ident <|> uident <|> keyword "_" *> pure "_")

+quantity : Parser Quant
+quantity = fromMaybe Many <$> optional (Zero <$ keyword "0")
+
 ebind : Parser Telescope
 ebind = do
  -- don't commit until we see the ":"
  sym "("
+  quant <- quantity
  names <- try (some (withPos varname) <* sym ":")
  ty <- typeExpr
  sym ")"
-  pure $ map (\(pos, name) => (pos, name, Explicit, ty)) names
+  pure $ map (\(pos, name) => (BI pos name Explicit quant, ty)) names

 ibind : Parser Telescope
 ibind = do
  -- I've gone back and forth on this, but I think {m a b} is more useful than {Nat}
  sym "{"
+  quant <- quantity
  names <- (some (withPos varname))
  ty <- optional (sym ":" *> typeExpr)
  sym "}"
-  pure $ map (\(pos,name) => (pos, name, Implicit, fromMaybe (RImplicit pos) ty)) names
+  pure $ map (\(pos,name) => (BI pos name Implicit quant, fromMaybe (RImplicit pos) ty)) names

 abind : Parser Telescope
 abind = do
@@ -288,8 +294,8 @@ abind = do
  ty <- typeExpr
  sym "}}"
  case name of
-    Just (pos,name) => pure [(pos, name, Auto, ty)]
-    Nothing => pure [(getFC ty, "_", Auto, ty)]
+    Just (pos,name) => pure [(BI pos name Auto Many, ty)]
+    Nothing => pure [(BI (getFC ty) "_" Auto Many, ty)]

 arrow : Parser Unit
 arrow = sym "->" <|> sym "→"
@@ -302,17 +308,17 @@ forAll = do
  all <- some (withPos varname)
  keyword "."
  scope <- typeExpr
-  pure $ foldr (\ (fc, n), sc => RPi fc (Just n) Implicit (RImplicit fc) sc) scope all
+  pure $ foldr (\ (fc, n), sc => RPi fc (BI fc n Implicit Zero) (RImplicit fc) sc) scope all

 binders : Parser Raw
 binders = do
  binds <- many (abind <|> ibind <|> ebind)
  arrow
  scope <- typeExpr
-  pure $ foldr (uncurry mkBind) scope (join binds)
+  pure $ foldr mkBind scope (join binds)
  where
-    mkBind : FC -> (String, Icit, Raw) -> Raw -> Raw
-    mkBind fc (name, icit, ty) scope = RPi fc (Just name) icit ty scope
+    mkBind : (BindInfo, Raw) -> Raw -> Raw
+    mkBind (info, ty) scope = RPi (getFC info) info ty scope

 typeExpr
  = binders
@@ -324,7 +330,7 @@ typeExpr
        case scope of
          Nothing      => pure exp
          -- consider Maybe String to represent missing
-          (Just scope) => pure $ RPi fc Nothing Explicit exp scope
+          (Just scope) => pure $ RPi fc (BI fc "_" Explicit Many) exp scope


 -- And top level stuff
@@ -411,7 +417,7 @@ parseData = do
 nakedBind : Parser Telescope
 nakedBind = do
  names <- some (withPos varname)
-  pure $ map (\(pos,name) => (pos, name, Explicit,  RImplicit pos)) names
+  pure $ map (\(pos,name) => (BI pos name Explicit Many, RImplicit pos)) names

 export
 parseClass : Parser Decl
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -244,9 +244,9 @@ processDecl (Class classFC nm tele decls) = do
  -- We'll need names for the telescope
  let dcName = "Mk\{nm}"
  let tcType = teleToPi tele (RU classFC)
-  let tail = foldl (\ acc, (fc, nm, icit, _) => RApp fc acc (RVar fc nm) icit) (RVar classFC nm) tele
+  let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar classFC nm) tele
  let dcType = teleToPi impTele $
-    foldr (\(fc, nm, ty), acc =>  RPi fc (Just nm) Explicit ty acc  ) tail fields
+    foldr (\(fc, nm, ty), acc =>  RPi fc (BI fc nm Explicit Many) ty acc  ) tail fields

  putStrLn "tcon type \{pretty tcType}"
  putStrLn "dcon type \{pretty dcType}"
@@ -255,9 +255,9 @@ processDecl (Class classFC nm tele decls) = do
  putStrLn $ render 90 $ pretty decl
  processDecl decl
  for_ fields $ \ (fc,name,ty) => do
-      let funType = teleToPi impTele $ RPi fc Nothing Auto tail ty
+      let funType = teleToPi impTele $ RPi fc (BI fc "_" Auto Many) tail ty
      let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar classFC dcName) fields
-      let lhs = foldl (\acc, (fc', nm, _, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
+      let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
      let lhs = RApp classFC lhs autoPat Auto
      let decl = Def fc name [(lhs, (RVar fc name))]

@@ -274,11 +274,11 @@ processDecl (Class classFC nm tele decls) = do
    getSigs (_:: xs) = getSigs xs

    impTele : Telescope
-    impTele = map (\(fc, nm, _, ty) => (fc, nm, Implicit, ty)) tele
+    impTele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit quant, ty)) tele

    teleToPi : Telescope -> Raw -> Raw
    teleToPi [] end = end
-    teleToPi ((fc, nm, icit, ty) :: tele) end = RPi fc (Just nm) icit ty (teleToPi tele end)
+    teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end)

 processDecl (Instance instfc ty decls) = do
  let decls = collectDecl decls
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -9,9 +9,6 @@ import Lib.Types
 public export
 data Raw : Type where

-public export
-data RigCount = Rig0 | RigW
-
 public export
 data Pattern
  = PatVar FC Icit Name
@@ -69,10 +66,10 @@ data DoStmt : Type where
 data Decl : Type
 data Raw : Type where
  RVar : (fc : FC) -> (nm : Name) -> Raw
-  RLam : (fc : FC) -> (nm : String) -> (icit : Icit) -> (ty : Raw) -> Raw
+  RLam : (fc : FC) -> BindInfo -> (ty : Raw) -> Raw
  RApp : (fc : FC) -> (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw
  RU   : (fc : FC) -> Raw
-  RPi  : (fc : FC) -> (nm : Maybe Name) -> (icit : Icit) -> (ty : Raw) -> (sc : Raw) -> Raw
+  RPi  : (fc : FC) -> BindInfo -> (ty : Raw) -> (sc : Raw) -> Raw
  RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw
  RAnn : (fc : FC) -> (tm : Raw) -> (ty : Raw) -> Raw
  RLit : (fc : FC) -> Literal -> Raw
@@ -89,10 +86,10 @@ data Raw : Type where
 export
 HasFC Raw where
  getFC (RVar fc nm) = fc
-  getFC (RLam fc nm icit ty) = fc
+  getFC (RLam fc _ ty) = fc
  getFC (RApp fc t u icit) = fc
  getFC (RU fc) = fc
-  getFC (RPi fc nm icit ty sc) = fc
+  getFC (RPi fc _ ty sc) = fc
  getFC (RLet fc nm ty v sc) = fc
  getFC (RAnn fc tm ty) = fc
  getFC (RLit fc y) = fc
@@ -114,12 +111,12 @@ data Import = MkImport FC Name

 public export
 Telescope : Type
-Telescope = (List (FC, String, Icit, Raw))
+Telescope = List (BindInfo, Raw)

 public export
 data Decl
  = TypeSig FC (List Name) Raw
-  | Def FC Name (List (Raw,Raw)) -- (List Clause)
+  | Def FC Name (List (Raw, Raw)) -- (List Clause)
  | DCheck FC Raw Raw
  | Data FC Name Raw (List Decl)
  | PType FC Name (Maybe Raw)
@@ -188,10 +185,6 @@ export covering
 Show Module where
  show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]

-Show RigCount where
-  show Rig0 = "Rig0"
-  show RigW = "RigW"
-
 export
 Show Pattern where
  show (PatVar _ icit str) = foo ["PatVar", show icit, show str]
@@ -203,6 +196,9 @@ covering
 Show RCaseAlt where
  show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]

+Show BindInfo where
+  show (BI _ name icit quant) = foo ["BI", show name, show icit, show quant]
+
 covering
 Show Raw where
  show (RImplicit _) = "_"
@@ -211,9 +207,9 @@ Show Raw where
  show (RAnn _ t ty) = foo [ "RAnn", show t, show ty]
  show (RLit _ x) = foo [ "RLit", show x]
  show (RLet _ x ty v scope) = foo [ "Let", show x, " : ", show ty, " = ", show v, " in ", show scope]
-  show (RPi _ str x y z) = foo [ "Pi", show str, show x, show y, show z]
+  show (RPi _ bi y z) = foo [ "Pi", show bi, show y, show z]
  show (RApp _ x y z) = foo [ "App", show x, show y, show z]
-  show (RLam _ x i y) = foo [ "Lam", show x, show i, show y]
+  show (RLam _ bi y) = foo [ "Lam", show bi, show y]
  show (RCase _ x xs) = foo [ "Case", show x, show xs]
  show (RDo _ stmts) = foo [ "DO", "FIXME"]
  show (RU _) = "U"
@@ -240,6 +236,8 @@ export
 Pretty Raw where
  pretty = asDoc 0
    where
+    bindDoc : BindInfo -> Doc
+    bindDoc (BI _ nm icit quant) = ?rhs_0
    wrap : Icit -> Doc -> Doc
    wrap Explicit x = text "(" ++ x ++ text ")"
    wrap Implicit x = text "{" ++ x ++ text "}"
@@ -250,15 +248,15 @@ Pretty Raw where

    asDoc : Nat -> Raw -> Doc
    asDoc p (RVar _ str) = text str
-    asDoc p (RLam _ str icit x) = par p 0 $ text "\\" ++ wrap icit (text str) <+> text "=>" <+> asDoc 0 x
+    asDoc p (RLam _ (BI _ nm icit q) x) = par p 0 $ text "\\" ++ wrap icit (text nm) <+> text "=>" <+> asDoc 0 x
    -- This needs precedence and operators...
    asDoc p (RApp _ x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y
    asDoc p (RApp _ x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}"
    asDoc p (RApp _ x y Auto) = par p 2 $ asDoc 2 x <+> text "{{" ++ asDoc 0 y ++ text "}}"
    asDoc p (RU _) = text "U"
-    asDoc p (RPi _ Nothing Explicit ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
-    asDoc p (RPi _ nm icit ty scope) =
-      par p 1 $ wrap icit (text (fromMaybe "_" nm) <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope
+    asDoc p (RPi _ (BI _ "_" Explicit Many) ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
+    asDoc p (RPi _ (BI _ nm icit quant) ty scope) =
+      par p 1 $ wrap icit (text "_" <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope
    asDoc p (RLet _ x v ty scope) =
      par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty
          <+> text "=" <+> asDoc p v
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -45,6 +45,23 @@ Show BD where
  show Bound = "bnd"
  show Defined = "def"

+public export
+data Quant = Zero | Many
+
+public export
+Show Quant where
+  show Zero = "0"
+  show Many = ""
+
+public export
+data BindInfo : Type where
+  BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo
+
+%name BindInfo bi
+
+public export
+HasFC BindInfo where
+  getFC (BI fc _ _ _) = fc

 -- do we just admit string names for these and let the prim functions
 -- sort it out?