case builder starting to work

src/Lib/CaseTree.idr

@@ -2,11 +2,13 @@
 ||| Follow §5.2 in Jesper Cockx paper Elaborating Dependent (co)pattern matching
 module Lib.CaseTree
 
+import Data.IORef
 import Data.String
 import Data.Vect
 import Data.List
 import Lib.Types
 import Lib.TopContext
+-- Will be a circular reference if we have case in terms
 import Lib.Check
 import Lib.TT
 import Lib.Syntax
@@ -42,23 +44,6 @@ import Lib.Syntax
 -- The pvars point to bound variables _or_ full expressions (Val) of a dcon applied to bound vars
 -- (e.g. S k). Perhaps something like `let` or a specific `pvar` binder?
 
-0 Constraint : Type
-Constraint = (String, Pattern)
-
-record Clause where
-  constructor MkClause
-  fc : FC
-  -- I'm including the type of the left, so we can check pats and get the list of possibilities
-  -- But maybe rethink what happens on the left.
-  -- It's a VVar k or possibly a pattern.
-  -- a pattern either is zipped out, dropped (non-match) or is assigned to rhs
-  -- if we can do all three then we can have a VVar here.
-  cons : List Constraint
-  pats : List Pattern
-  -- We'll need some context to typecheck this
-  -- it has names from Pats, which will need types in the env
-  expr : Raw
-
 -- when we INTRO, we pop a pat from pats and a type from ty
 -- add to gamma
 -- add a constraint to each clause binding the var t to the pat
@@ -69,8 +54,14 @@ record Clause where
 -- turn matches into subst
 -- see if we're good (no pats, no constraints)
 
--- Do I want Val or Tm here?
+-- a case statement doesn't have pats, intro has been done
+-- already, and we have a pile of clauses referencing a
+-- name in the context.
 
+-- a function def can let intro happen, so we could have
+-- different lengths of args.
+
+public export
 record Problem where
   constructor MkProb
   clauses : List Clause
@@ -84,6 +75,7 @@ fresh : {auto ctx : Context} -> String -> String
 fresh base = base ++ "$" ++ show (length ctx.env)
 
 -- The result is a casetree, but it's in Tm
+export
 buildTree : Context -> Problem -> M Tm
 
 introClause : String -> Clause -> M Clause
@@ -96,9 +88,8 @@ introClause nm (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm,
 -- this may dot into a dependent.
 findSplit : List Constraint -> Maybe Constraint
 findSplit [] = Nothing
-findSplit (x@(nm, PatCon{}) :: xs) =
     -- FIXME look up type, ensure it's a constructor
-    Just x
+findSplit (x@(nm, PatCon cnm pats) :: xs) = Just x
 findSplit (_ :: xs) = findSplit xs
 
 
@@ -110,15 +101,21 @@ findSplit (_ :: xs) = findSplit xs
 
 -- TODO, we may need to filter these for the situation.
 getConstructors : Context -> Val -> M (List (String, Nat, Tm))
-getConstructors ctx (VRef fc nm (TCon names) sc) = traverse lookupDCon names
+getConstructors ctx (VRef fc nm _ sc) = do
+  names <- lookupTCon nm
+  traverse lookupDCon names
   where
+    lookupTCon : String -> M (List String)
+    lookupTCon str = case lookup nm !get of
+        (Just (MkEntry name type (TCon names))) => pure names
+        _ => error fc "Not a type constructor \{nm}"
     lookupDCon : String -> M (String, Nat, Tm)
     lookupDCon nm = do
       case lookup nm !get of
         (Just (MkEntry name type (DCon k str))) => pure (name, k, type)
         Just _ => error fc "Internal Error: \{nm} is not a DCon"
         Nothing => error fc "Internal Error: DCon \{nm} not found"
-getConstructors ctx tm = error (getValFC tm) "Not a type constructor"
+getConstructors ctx tm = error (getValFC tm) "Not a type constructor \{show tm}"
 
 -- Extend environment with fresh variables from a pi-type
 -- return context, remaining type, and list of names
@@ -142,8 +139,9 @@ buildCase ctx prob scnm (dcName, arity, ty) = do
   vty <- eval [] CBN ty
   (ctx', ty', vars) <- extendPi ctx (vty) [<]
   let clauses = mapMaybe (rewriteClause vars) prob.clauses
+  debug "clauses were \{show prob.clauses} and now \{show clauses}"
   when (length clauses == 0) $ error emptyFC "No valid clauses / missing case / FIXME FC and some details"
-  tm <- buildTree ctx' (MkProb clauses ty')
+  tm <- buildTree ctx' (MkProb clauses prob.ty)
   pure $ CaseCons dcName vars tm
   where
     -- for each clause in prob, find nm on LHS of some constraint, and
@@ -167,10 +165,10 @@ buildCase ctx prob scnm (dcName, arity, ty) = do
     rewriteCons vars (c@(nm, y) :: xs) acc =
       if nm == scnm
         then case y of
-          (PatVar s) => Just $ c :: (xs ++ acc)
+          PatVar s => Just $ c :: (xs ++ acc)
           PatWild => Just $ c :: (xs ++ acc)
-          (PatCon str ys) => if str == dcName
-            then Just $ acc ++ (zip vars ys)
+          PatCon str ys => if str == dcName
+            then Just $ (zip vars ys) ++ acc
             else Nothing
         else rewriteCons vars xs (c :: acc)
 
@@ -187,6 +185,28 @@ lookupName ctx name = go 0 ctx.types
     -- 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 (S ix) xs
 
+-- FIXME need to check done here...
+      -- If all of the constraints are assignments, fixup context and type check
+      -- else bail:
+
+      -- error fc "Stuck, no splits \{show constraints}"
+
+checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm
+checkDone ctx [] body ty = check ctx body ty
+checkDone ctx ((x, PatWild) :: xs) body ty = checkDone ctx xs body ty
+checkDone ctx ((nm, (PatVar nm')) :: xs) body ty = checkDone ({ types $= rename } ctx) xs body ty
+  where
+    rename : Vect n (String, Val) -> Vect n (String, Val)
+    rename [] = []
+    rename ((name, ty) :: xs) =
+      if name == nm
+        then (nm', ty) :: xs
+        else (name, ty) :: rename xs
+
+checkDone ctx ((x, pat) :: xs) body ty = error emptyFC "stray constraint \{x} /? \{show pat}"
+
+-- 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
   let l = length ctx.env
@@ -203,30 +223,16 @@ buildTree ctx prob@(MkProb ((MkClause fc [] [] expr) :: cs) ty) = check ctx expr
 -- 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
-buildTree ctx prob@(MkProb ((MkClause fc xs [] expr) :: cs) ty) = do
-
-  -- REVIEW There is a extendPi here.
-
-  -- We don't need ty here if we're happy with Val...
-  let Just (scnm, _) := findSplit xs | _ => error fc "Stuck, no splits"
+buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
+  debug "buildTree \{show constraints} \{show expr}"
+  let Just (scnm, pat) := findSplit constraints
+    | _ => checkDone ctx constraints expr ty
 
+  debug "split on \{scnm} because \{show pat}"
   let Just (sctm, ty') := lookupName ctx scnm
     | _ => error fc "Internal Error: can't find \{scnm} in environment"
 
-  -- get constructors, for each of them run the problem, build Case result
-  cons <- getConstructors ctx ty' -- probably need pi-types too for recursion
-  -- we have a case tree for each dcon, from a recursive call, collect into `Case`
+  cons <- getConstructors ctx ty'
   alts <- traverse (buildCase ctx prob scnm) cons
 
-  -- Maybe `scnm` should be something other than a name? Index is not stable,
-  -- we're working with term at the moment, so Val isn't great.
-  -- But this is elab and we do name -> Bnd in `infer`, so why not.
-
   pure $ Case fc sctm alts
-
-
-
-
-
--- A telescope is a list of binders, right? I've been leaving things as pi types to be explicit
-

src/Lib/Check.idr

@@ -181,8 +181,8 @@ infer : Context -> Raw  -> M  (Tm, Val)
 export
 check : Context -> Raw -> Val  -> M  Tm
 
--- FIXME we need to switch to FC
 
+-- This is the old case checking that expected a user-supplied case tree
 checkAlt : Val -> Context -> Val -> RCaseAlt -> M CaseAlt
 checkAlt scty ctx ty (MkAlt ptm body) = do
   -- we have a pattern term and a body
@@ -270,7 +270,16 @@ checkAlt scty ctx ty (MkAlt ptm body) = do
 
 
 check ctx tm ty = case (tm, !(forceType ty)) of
+  -- previous code
+  -- (RCase fc rsc alts, ty) => do
+  --   (sc, scty) <- infer ctx rsc
+  --   let (VRef fc nm (TCon cnames) sp) = scty
+  --     | _ => error fc "expected TCon for scrutinee type, got: \{show scty}"
+  --   debug "constructor names \{show cnames}"
+  --   alts' <- for alts $ checkAlt scty ctx ty
+  --   pure $ Case emptyFC sc alts'
   (RCase fc rsc alts, ty) => do
+    -- scrutinee must infer.  We will probably want to `let` it too.
     (sc, scty) <- infer ctx rsc
     let (VRef fc nm (TCon cnames) sp) = scty
       | _ => error fc "expected TCon for scrutinee type, got: \{show scty}"

src/Lib/Parser.idr

@@ -28,8 +28,11 @@ import Data.Maybe
 -- exercises.  There is some fill in the parser stuff that may show
 -- the future.
 
+
 ident = token Ident
 
+uident = token UIdent
+
 parens : Parser a -> Parser a
 parens pa = do
   sym "("
@@ -72,6 +75,7 @@ export term : (Parser Raw)
 atom : Parser Raw
 atom = RU <$> getFC <* keyword "U"
     <|> RVar <$> getFC <*> ident
+    <|> RVar <$> getFC <*> uident
     <|> lit
     <|> RImplicit <$> getFC <* keyword "_"
     <|> RHole <$> getFC <* keyword "?"
@@ -153,11 +157,23 @@ lamExpr = do
   fc <- getFC
   pure $ foldr (\(icit, name, ty), sc => RLam fc name icit sc) scope args
 
+
+-- Idris just has a term on the LHS and sorts it out later..
+-- This allows some eval, like n + 2 -> S (S n), and expands to more complexity
+-- like dotting
+
+-- We may need to look up names at some point to see if they're constructors.
+
+-- so, we can do the capital letter thing here or push that bit down and collect single/double
+pPattern' : Parser Pattern
 pPattern : Parser Pattern
 pPattern
    = PatWild <$ keyword "_"
   <|> PatVar <$> ident
+  <|> PatCon <$> uident <*> pure []
+  <|> parens pPattern'
 
+pPattern'  = PatCon <$> uident <*> many pPattern <|> pPattern
 
 caseAlt : Parser RCaseAlt
 caseAlt = do
@@ -235,20 +251,27 @@ typeExpr = binders
 
 export
 parseSig : Parser Decl
-parseSig = TypeSig <$> getFC <*> ident <* keyword ":" <*> mustWork typeExpr
+parseSig = TypeSig <$> getFC <*> (ident <|> uident) <* keyword ":" <*> mustWork typeExpr
 
 parseImport : Parser Decl
-parseImport = DImport <$> getFC <* keyword "import" <* commit <*> ident
+parseImport = DImport <$> getFC <* keyword "import" <* commit <*> uident
 
 -- Do we do pattern stuff now? or just name = lambda?
 
 export
 parseDef : Parser Decl
-parseDef = Def <$> getFC <*> ident <* keyword "=" <*> mustWork typeExpr
+parseDef = do
+  fc <- getFC
+  nm <- ident
+  pats <- many pPattern
+  keyword "="
+  body <- mustWork typeExpr
+  -- these get collected later
+  pure $ Def nm [MkClause fc [] pats body]
 
 export
 parsePType : Parser Decl
-parsePType = PType <$> getFC <* keyword "ptype" <*> ident
+parsePType = PType <$> getFC <* keyword "ptype" <*> uident
 
 parsePFunc : Parser Decl
 parsePFunc = do
@@ -260,15 +283,13 @@ parsePFunc = do
   keyword ":="
   src <- mustWork (cast <$> token StringKind)
   pure $ PFunc fc nm ty src
-  -- PFunc <$> getFC <* keyword "pfunc" <*> mustWork ident <* keyword ":" <*> mustWork typeExpr <* keyword ":=" <*> (cast <$> token StringKind)
-
 
 export
 parseData : Parser Decl
 parseData = do
   fc <- getFC
   keyword "data"
-  name <- ident
+  name <- uident
   keyword ":"
   ty <- typeExpr
   keyword "where"
@@ -290,7 +311,7 @@ export
 parseMod : Parser Module
 parseMod = do
   keyword "module"
-  name <- ident
+  name <- uident
   -- probably should be manySame, and we want to start with col -1
   -- if we enforce blocks indent more than parent
   decls <- startBlock $ manySame $ parseDecl

src/Lib/ProcessDecl.idr

@@ -2,6 +2,7 @@ module Lib.ProcessDecl
 
 import Data.IORef
 
+import Lib.CaseTree
 import Lib.Check
 import Lib.Parser
 import Lib.Syntax
@@ -16,6 +17,17 @@ getArity (Pi x str icit t u) = S (getArity u)
 getArity _ = Z
 
 -- Can metas live in context for now?
+-- We'll have to be able to add them, which might put gamma in a ref
+
+-- collect Defs into List Decl, special type, or add Defs to Decl?
+
+export
+collectDecl : List Decl -> List Decl
+collectDecl [] = []
+collectDecl ((Def nm cl) :: rest@(Def nm' cl' :: xs)) =
+  if nm == nm' then collectDecl (Def nm (cl ++ cl') :: xs)
+  else (Def nm cl :: collectDecl rest)
+collectDecl (x :: xs) = x :: collectDecl xs
 
 export
 processDecl : Decl -> M ()
@@ -40,7 +52,9 @@ processDecl (PFunc fc nm ty src) = do
   putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}"
   modify $ setDef nm ty' (PrimFn src)
 
-processDecl (Def fc nm raw) = do
+processDecl (Def nm clauses) = do
+  -- FIXME - I guess we need one on Def, too, or pull off of first clause
+  let fc = emptyFC
   putStrLn "-----"
   putStrLn "def \{show nm}"
   ctx <- get
@@ -48,10 +62,17 @@ processDecl (Def fc nm raw) = do
     | Nothing => throwError $ E fc "skip def \{nm} without Decl"
   let (MkEntry name ty Axiom) := entry
     | _ => throwError $ E fc "\{nm} already defined"
-  putStrLn "check \{nm} = \{show raw} at \{pprint [] ty}"
+
+  -- and we pass to the case tree stuff now
+  -- maybe fix up the clauses to match?
+  -- Also we need to distinguish DCon/var
+
+  putStrLn "check \{nm} ... at \{pprint [] ty}"
   vty <- eval empty CBN ty
   putStrLn "vty is \{show vty}"
-  tm <- check (mkCtx ctx.metas) raw vty
+
+  tm <- buildTree (mkCtx ctx.metas) (MkProb clauses vty)
+  -- tm <- check (mkCtx ctx.metas) body vty
   putStrLn "Ok \{pprint [] tm}"
 
   mc <- readIORef ctx.metas
@@ -65,7 +86,6 @@ processDecl (Def fc nm raw) = do
   modify $ setDef nm ty (Fn tm)
 
 processDecl (DCheck fc tm ty) = do
-
   top <- get
   putStrLn "check \{show tm} at \{show ty}"
   ty' <- check (mkCtx top.metas) tm (VU fc)
@@ -114,6 +134,7 @@ processDecl (Data fc nm ty cons) = do
   -- Maybe a pi -> binders function
   -- TODO we're putting in axioms, we need constructors
   -- for each constructor, check and add
+  putStrLn "setDef \{nm}  TCon \{show cnames}"
   modify $ setDef nm tyty (TCon cnames)
   pure ()
   where

src/Lib/Syntax.idr

@@ -12,14 +12,36 @@ data Raw : Type where
 public export
 data RigCount = Rig0 | RigW
 
+
+
 public export
 data Pattern
   = PatVar Name
   | PatCon Name (List Pattern)
   | PatWild
+  -- Not handling this yet, but we need to be able to work with numbers and strings...
   -- | PatLit Literal
 
 -- %runElab deriveShow `{Pattern}
+public export
+Constraint : Type
+Constraint = (String, Pattern)
+
+public export
+record Clause where
+  constructor MkClause
+  fc : FC
+  -- I'm including the type of the left, so we can check pats and get the list of possibilities
+  -- But maybe rethink what happens on the left.
+  -- It's a VVar k or possibly a pattern.
+  -- a pattern either is zipped out, dropped (non-match) or is assigned to rhs
+  -- if we can do all three then we can have a VVar here.
+  cons : List Constraint
+  pats : List Pattern
+  -- We'll need some context to typecheck this
+  -- it has names from Pats, which will need types in the env
+  expr : Raw
+
 
 -- could be a pair, but I suspect stuff will be added?
 public export
@@ -64,7 +86,7 @@ data Decl : Type where
 
 data Decl
   = TypeSig FC Name Raw
-  | Def FC Name Raw
+  | Def Name (List Clause)
   | DImport FC Name
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
@@ -94,10 +116,16 @@ implementation Show Raw
 export
 implementation Show Decl
 
+export Show Pattern
+
+export covering
+Show Clause where
+  show (MkClause fc cons pats expr) = show (fc, cons, pats, expr)
+
 covering
 Show Decl where
   show (TypeSig _ str x) = foo ["TypeSig", show str, show x]
-  show (Def _ str x) = foo ["Def", show str, show x]
+  show (Def str clauses) = foo ["Def", show str, show clauses]
   show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys]
   show (DImport _ str) = foo ["DImport", show str]
   show (DCheck _ x y) = foo ["DCheck", show x, show y]
@@ -138,6 +166,12 @@ Show Raw where
   show (RParseError _ str) = foo [ "ParseError", "str"]
   show (RU _) = "U"
 
+export
+Pretty Pattern where
+  pretty (PatVar nm) = text nm
+  pretty (PatCon nm args) = text nm <+> spread (map pretty args)
+  pretty PatWild = "_"
+
 export
 Pretty Raw where
   pretty = asDoc 0
@@ -181,7 +215,10 @@ Pretty Module where
       where
         doDecl : Decl -> Doc
         doDecl (TypeSig _ nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
-        doDecl (Def _ nm tm) = text nm <+> text "=" <+> nest 2 (pretty tm)
+        doDecl (Def nm clauses) = spread $ map doClause clauses
+          where
+            doClause : Clause -> Doc
+            doClause (MkClause fc _ pats body) = text nm <+> spread (map pretty pats) <+> text "=" <+> nest 2 (pretty body)
         doDecl (DImport _ nm) = text "import" <+> text nm ++ line
         -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
         doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))

src/Lib/Token.idr

@@ -7,6 +7,7 @@ import public Text.Lexer
 public export
 data Kind
   = Ident
+  | UIdent
   | Keyword
   | Oper
   | Number
@@ -24,6 +25,7 @@ data Kind
 export
 Show Kind where
   show Ident   = "Ident"
+  show UIdent   = "UIdent"
   show Keyword = "Keyword"
   show Oper    = "Oper"
   show Number  = "Number"
@@ -39,6 +41,7 @@ Show Kind where
 export
 Eq Kind where
   Ident   == Ident = True
+  UIdent  == UIdent = True
   Keyword == Keyword = True
   Oper    == Oper = True
   Number  == Number = True

src/Lib/Tokenizer.idr

@@ -13,6 +13,9 @@ specialOps = ["->", ":", "=>", ":="]
 checkKW : String -> Token Kind
 checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
 
+checkUKW : String -> Token Kind
+checkUKW s = if elem s keywords then Tok Keyword s else Tok UIdent s
+
 isOpChar : Char -> Bool
 isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
 
@@ -42,7 +45,8 @@ unquote str = case unpack str of
 
 rawTokens : Tokenizer (Token Kind)
 rawTokens
-   =  match (alpha <+> many identMore) checkKW
+   =  match (lower <+> many identMore) checkKW
+  <|> match (upper <+> many identMore) checkUKW
   <|> match (some digit) (Tok Number)
   <|> match (is '#' <+> many alpha) (Tok Pragma)
   <|> match (quo <+> manyUntil quo ((esc any <+> any) <|> any) <+> opt quo) (Tok StringKind . unquote)