more work on casetree

newt/testcase2.newt

@@ -15,56 +15,54 @@ max Z m = m
 max n Z = n
 max (S k) (S l) = S (max k l)
 
+data List : U -> U where
+  LN : {a : U} -> List a
+  LCons : {a : U} -> a -> List a -> List a
 
 data Vect : Nat -> U -> U where
   Nil : {a : U} -> Vect Z a
   Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a
 
 -- NEXT Need to handle implicits
--- length : {a : U} {n : Nat} -> Vect n a -> Nat
--- length Nil = Z
--- length (Cons x xs) = S (length xs)
+-- I've hacked implicits, but need to figure out indices..
+length : {a : U} {n : Nat} -> Vect n a -> Nat
+length Nil = Z
+length (Cons x xs) = S (length xs)
 
--- data Unit : U where
---   MkUnit : Unit
+data Unit : U where
+  MkUnit : Unit
 
--- foo : Vect (S Z) Unit
--- foo = Cons MkUnit Nil
+-- This should fail (and does!)
+-- bar : Vect (S Z) Unit
+-- bar = (Cons MkUnit (Cons MkUnit Nil))
 
--- -- This should fail (and does!)
--- -- bar : Vect (S Z) Unit
--- -- bar = (Cons MkUnit (Cons MkUnit Nil))
+data Bool : U where
+  True : Bool
+  False : Bool
 
--- data Bool : U where
---   True : Bool
---   False : Bool
-
--- not : Bool -> Bool
--- not = \ v => case v of
---   True => False
---   False => True
+not : Bool -> Bool
+not True = False
+not False = True
 
 
--- not2 : Bool -> Bool
--- not2 = \ v => case v of
---   True => False
---   x => True
+not2 : Bool -> Bool
+not2 True = False
+not2 x = True
+
+-- TEST CASE - remove second clause here and expect error
+and : Bool -> Bool -> Bool
+and True y = y
+and False _ = False
+
+nand : Bool -> Bool -> Bool
+nand x y = not (case x of
+    True => y
+    False => False)
+
+
+-- for stuff like this, we should add Agda () and check for no constructors
+data Void : U where
 
--- and : Bool -> Bool -> Bool
--- and = \ x y => case x of
---   True => y
---   False => False
 
--- -- FIXME - a case is evaluated here, and I don't know why.
-
--- nand : Bool -> Bool -> Bool
--- nand = \ x y => not (case x of
---     True => y
---     False => False)
-
--- -- -- this should be an error.
--- -- foo : Bool -> Bool
-
--- data Void : U where
 
 

src/Lib/CaseTree.idr

@@ -6,6 +6,7 @@ import Data.IORef
 import Data.String
 import Data.Vect
 import Data.List
+import Debug.Trace
 import Lib.Types
 import Lib.TopContext
 -- Will be a circular reference if we have case in terms
@@ -61,6 +62,13 @@ import Lib.Syntax
 -- a function def can let intro happen, so we could have
 -- different lengths of args.
 
+-- We're pulling type from the context, but we'll have it here if we use
+-- Bind more widely
+data Bind = MkBind String Icit Val
+
+Show Bind where
+  show (MkBind str icit x) = "\{str} \{show icit}"
+
 public export
 record Problem where
   constructor MkProb
@@ -89,7 +97,7 @@ introClause nm (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm,
 findSplit : List Constraint -> Maybe Constraint
 findSplit [] = Nothing
     -- FIXME look up type, ensure it's a constructor
-findSplit (x@(nm, PatCon cnm pats) :: xs) = Just x
+findSplit (x@(nm, PatCon _ cnm pats) :: xs) = Just x
 findSplit (_ :: xs) = findSplit xs
 
 
@@ -119,31 +127,53 @@ 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
-extendPi : Context -> Val -> SnocList Name -> M (Context, Val, List Name)
+extendPi : Context -> Val -> SnocList Bind -> M (Context, Val, List Bind)
+-- NEXT This doesn't work, unsound.
+-- We need all of these vars with icity _and_ to insert implicits in the pattern
+-- extendPi ctx (VPi x str Implicit a b) nms = do
+--     let nm = fresh "pat"
+--     let ctx' = extend ctx nm a
+--     let v = VVar emptyFC (length ctx.env) [<]
+--     tyb <- b $$ v
+--     extendPi ctx' tyb nms
 extendPi ctx (VPi x str icit a b) nms = do
     let nm = fresh "pat"
     let ctx' = extend ctx nm a
     let v = VVar emptyFC (length ctx.env) [<]
     tyb <- b $$ v
-    extendPi ctx' tyb (nms :< nm)
+    extendPi ctx' tyb (nms :< MkBind nm icit a)
 extendPi ctx ty nms = pure (ctx, ty, nms <>> [])
 
 -- filter clause
 
+-- FIXME - I don't think we're properly noticing
+
 
 -- ok, so this is a single constructor, CaseAlt
 -- since we've gotten here, we assume it's possible and we better have at least
 -- one valid clause
 buildCase : Context -> Problem -> String -> (String, Nat, Tm) -> M CaseAlt
-buildCase ctx prob scnm (dcName, arity, ty) = do
+buildCase ctx prob scnm (dcName, _, ty) = do
   vty <- eval [] CBN ty
   (ctx', ty', vars) <- extendPi ctx (vty) [<]
+
+  debug "clauses were \{show prob.clauses} (dcon \{show dcName}) (vars \{show vars})"
   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"
+  debug "    and now \{show clauses}"
+  -- So ideally we'd know which position we're splitting and the surrounding context
+  -- That might be a lot to carry forward (maybe a continuation?) but we could carry
+  -- backwards as a List Missing that we augment as we go up.
+  -- We could even stick a little "throw error" tree in here for the case.
+  -- even going backward, we don't really know where pat$n falls into the expression.
+  -- It would need to keep track of its position. Then fill in the slots (wild vs PCons), or
+  -- wrapping with PCons as we move back up.  E.g. _ (Cons _ (Cons _ _)) _ _ could be missing
+  when (length clauses == 0) $ error ctx.fc "Missing case for \{dcName} splitting \{scnm}"
   tm <- buildTree ctx' (MkProb clauses prob.ty)
-  pure $ CaseCons dcName vars tm
+  pure $ CaseCons dcName (map getName vars) tm
   where
+    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.
     --
@@ -155,24 +185,31 @@ buildCase ctx prob scnm (dcName, arity, ty) = do
     -- If they all fail, we have a coverage issue. (Assuming the constructor is valid)
 
 
-    -- There is a zip here, etc, but are we just re-writing buildTree?
-    -- I suppose vars might be the difference?  There may be something to factor out here
-    -- essentially we're picking apart Pi, binding variables and constraining them to patterns.
-    -- everything we've bound is only used in the PatCon case below.
+    -- we'll want implicit patterns at some point, for now we wildcard implicits because
+    -- we don't have them
+    makeConst : List Bind -> List Pattern -> List (String, Pattern)
+    makeConst [] [] = []
+    -- need M in here to throw.
+    makeConst [] (pat :: pats) = ?extra_patterns
+    --
+    makeConst ((MkBind nm Implicit x) :: xs) [] = (nm, PatWild emptyFC) :: makeConst xs []
+    makeConst ((MkBind nm Explicit x) :: xs) [] = ?extra_binders_2
+    makeConst ((MkBind nm Implicit x) :: xs) (pat :: pats) = (nm, PatWild (getFC pat)) :: makeConst xs (pat :: pats)
+    makeConst ((MkBind nm Explicit x) :: xs) (pat :: pats) = (nm, pat) :: makeConst xs pats
 
-    rewriteCons : List Name -> List Constraint -> List Constraint -> Maybe (List Constraint)
+    rewriteCons : List Bind -> List Constraint -> List Constraint -> Maybe (List Constraint)
     rewriteCons vars [] acc = Just acc
     rewriteCons vars (c@(nm, y) :: xs) acc =
       if nm == scnm
         then case y of
-          PatVar s => Just $ c :: (xs ++ acc)
-          PatWild => Just $ c :: (xs ++ acc)
-          PatCon str ys => if str == dcName
-            then Just $ (zip vars ys) ++ acc
+          PatVar _ s => Just $ c :: (xs ++ acc)
+          PatWild _ => Just $ c :: (xs ++ acc)
+          PatCon _ str ys => if str == dcName
+            then Just $ (makeConst vars ys) ++ acc
             else Nothing
         else rewriteCons vars xs (c :: acc)
 
-    rewriteClause : List Name -> Clause -> Maybe Clause
+    rewriteClause : List Bind -> Clause -> Maybe Clause
     rewriteClause vars (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteCons vars cons []) pats expr
 
 
@@ -193,8 +230,8 @@ lookupName ctx name = go 0 ctx.types
 
 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
+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 [] = []
@@ -208,6 +245,14 @@ checkDone ctx ((x, pat) :: xs) body ty = error emptyFC "stray constraint \{x} /?
 -- 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 Implicit a b)) = do
+  let l = length ctx.env
+  let nm = fresh "pat"
+  let ctx' = extend ctx nm a
+  -- type of the rest
+  -- clauses <- traverse (introClause nm) prob.clauses
+  vb <- b $$ VVar fc l [<]
+  Lam fc nm <$> buildTree ctx' ({ ty := vb } prob)
 buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit a b)) = do
   let l = length ctx.env
   let nm = fresh "pat"

src/Lib/Parser.idr

@@ -53,13 +53,13 @@ optional pa = Just <$> pa <|> pure Nothing
 
 stringLit : Parser Raw
 stringLit = do
-  fc <- getFC
+  fc <- getPos
   t <- token StringKind
   pure $ RLit fc (LString (cast t))
 
 intLit : Parser Raw
 intLit = do
-  fc <- getFC
+  fc <- getPos
   t <- token Number
   pure $ RLit fc (LInt (cast t))
 
@@ -73,12 +73,12 @@ export term : (Parser Raw)
 
 -- the inside of Raw
 atom : Parser Raw
-atom = RU <$> getFC <* keyword "U"
-    <|> RVar <$> getFC <*> ident
-    <|> RVar <$> getFC <*> uident
+atom = RU <$> getPos <* keyword "U"
+    <|> RVar <$> getPos <*> ident
+    <|> RVar <$> getPos <*> uident
     <|> lit
-    <|> RImplicit <$> getFC <* keyword "_"
-    <|> RHole <$> getFC <* keyword "?"
+    <|> RImplicit <$> getPos <* keyword "_"
+    <|> RHole <$> getPos <* keyword "?"
     <|> parens typeExpr
 
 -- Argument to a Spine
@@ -100,7 +100,7 @@ parseApp : Parser Raw
 parseApp = do
   hd <- atom
   rest <- many pArg
-  fc <- getFC
+  fc <- getPos
   pure $ foldl (\a, (c,b) => RApp fc a b c) hd rest
 
 parseOp : Parser Raw
@@ -109,7 +109,7 @@ parseOp = parseApp >>= go 0
     go : Int -> Raw -> Parser Raw
     go prec left =
       do
-        fc <- getFC
+        fc <- getPos
         op <- token Oper
         let Just (p,fix) = lookup op operators
          | Nothing => fail "expected operator"
@@ -127,12 +127,12 @@ letExpr = do
   alts <- startBlock $ someSame $ letAssign
   keyword' "in"
   scope <- typeExpr
-  fc <- getFC
+  fc <- getPos
   pure $ foldl (\ acc, (n,fc,v) => RLet fc n (RImplicit fc) v acc) scope alts
   where
     letAssign : Parser (Name,FC,Raw)
     letAssign = do
-      fc <- getFC
+      fc <- getPos
       name <- ident
       -- TODO type assertion
       keyword "="
@@ -154,7 +154,7 @@ lamExpr = do
   args <- some pLetArg
   keyword "=>"
   scope <- typeExpr
-  fc <- getFC
+  fc <- getPos
   pure $ foldr (\(icit, name, ty), sc => RLam fc name icit sc) scope args
 
 
@@ -168,12 +168,12 @@ lamExpr = do
 pPattern' : Parser Pattern
 pPattern : Parser Pattern
 pPattern
-   = PatWild <$ keyword "_"
-  <|> PatVar <$> ident
-  <|> PatCon <$> uident <*> pure []
+   = PatWild <$ keyword "_" <*> getPos
+  <|> PatVar <$> getPos <*> ident
+  <|> PatCon <$> getPos <*> uident <*> pure []
   <|> parens pPattern'
 
-pPattern'  = PatCon <$> uident <*> many pPattern <|> pPattern
+pPattern'  = PatCon <$> getPos <*> uident <*> many pPattern <|> pPattern
 
 caseAlt : Parser RCaseAlt
 caseAlt = do
@@ -191,7 +191,7 @@ caseExpr = do
   sc <- term
   keyword "of"
   alts <- startBlock $ someSame $ caseAlt
-  pure $ RCase !(getFC) sc alts
+  pure $ RCase !(getPos) sc alts
 
 -- This hits an idris codegen bug if parseOp is last and Lazy
 term =  caseExpr
@@ -215,9 +215,9 @@ ibind = do
   mustWork $ do
     names <- some ident
     ty <- optional (sym ":" >> typeExpr)
-    pos <- getFC
+    pos <- getPos
     sym "}"
-    -- getFC is a hack here, I would like to position at the name...
+    -- getPos is a hack here, I would like to position at the name...
     pure $ map (\name => (name, Implicit, fromMaybe (RImplicit pos) ty)) names
 
 arrow : Parser Unit
@@ -230,7 +230,7 @@ binders = do
   arrow
   commit
   scope <- typeExpr
-  fc <- getFC
+  fc <- getPos
   pure $ foldr (mkBind fc) scope (join binds)
   where
     mkBind : FC -> (String, Icit, Raw) -> Raw -> Raw
@@ -243,7 +243,7 @@ typeExpr = binders
         case scope of
           Nothing      => pure exp
           -- consider Maybe String to represent missing
-          (Just scope) => pure $ RPi !(getFC) Nothing Explicit exp scope
+          (Just scope) => pure $ RPi !(getPos) Nothing Explicit exp scope
 
 
 -- And top level stuff
@@ -251,31 +251,31 @@ typeExpr = binders
 
 export
 parseSig : Parser Decl
-parseSig = TypeSig <$> getFC <*> (ident <|> uident) <* keyword ":" <*> mustWork typeExpr
+parseSig = TypeSig <$> getPos <*> (ident <|> uident) <* keyword ":" <*> mustWork typeExpr
 
 parseImport : Parser Decl
-parseImport = DImport <$> getFC <* keyword "import" <* commit <*> uident
+parseImport = DImport <$> getPos <* keyword "import" <* commit <*> uident
 
 -- Do we do pattern stuff now? or just name = lambda?
 
 export
 parseDef : Parser Decl
 parseDef = do
-  fc <- getFC
+  fc <- getPos
   nm <- ident
   pats <- many pPattern
   keyword "="
   body <- mustWork typeExpr
   -- these get collected later
-  pure $ Def nm [MkClause fc [] pats body]
+  pure $ Def fc nm [MkClause fc [] pats body]
 
 export
 parsePType : Parser Decl
-parsePType = PType <$> getFC <* keyword "ptype" <*> uident
+parsePType = PType <$> getPos <* keyword "ptype" <*> uident
 
 parsePFunc : Parser Decl
 parsePFunc = do
-  fc <- getFC
+  fc <- getPos
   keyword "pfunc"
   nm <- ident
   keyword ":"
@@ -287,7 +287,7 @@ parsePFunc = do
 export
 parseData : Parser Decl
 parseData = do
-  fc <- getFC
+  fc <- getPos
   keyword "data"
   name <- uident
   keyword ":"
@@ -301,7 +301,7 @@ parseData = do
 -- Not sure what I want here.
 -- I can't get a Tm without a type, and then we're covered by the other stuff
 parseNorm : Parser Decl
-parseNorm = DCheck <$> getFC <* keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
+parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
 
 export
 parseDecl : Parser Decl

src/Lib/Parser/Impl.idr

@@ -24,6 +24,10 @@ public export
 FC : Type
 FC = (Int,Int)
 
+public export
+interface HasFC a where
+  getFC : a -> FC
+
 %name FC fc
 
 export
@@ -159,8 +163,8 @@ mutual
 
 -- withIndentationBlock - sets the col
 export
-getFC : Parser FC
-getFC = P $ \toks,com, (l,c) => case toks of
+getPos : Parser FC
+getPos = P $ \toks,com, (l,c) => case toks of
   [] => OK emptyFC toks com
   (t :: ts) => OK (start t) toks com
 

src/Lib/ProcessDecl.idr

@@ -24,9 +24,9 @@ getArity _ = Z
 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 ((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
 
 export
@@ -52,9 +52,7 @@ processDecl (PFunc fc nm ty src) = do
   putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}"
   modify $ setDef nm ty' (PrimFn src)
 
-processDecl (Def nm clauses) = do
-  -- FIXME - I guess we need one on Def, too, or pull off of first clause
-  let fc = emptyFC
+processDecl (Def fc nm clauses) = do
   putStrLn "-----"
   putStrLn "def \{show nm}"
   ctx <- get
@@ -71,7 +69,7 @@ processDecl (Def nm clauses) = do
   vty <- eval empty CBN ty
   putStrLn "vty is \{show vty}"
 
-  tm <- buildTree (mkCtx ctx.metas) (MkProb clauses vty)
+  tm <- buildTree ({ fc := fc} $ mkCtx ctx.metas) (MkProb clauses vty)
   -- tm <- check (mkCtx ctx.metas) body vty
   putStrLn "Ok \{pprint [] tm}"
 

src/Lib/Syntax.idr

@@ -16,12 +16,18 @@ data RigCount = Rig0 | RigW
 
 public export
 data Pattern
-  = PatVar Name
-  | PatCon Name (List Pattern)
-  | PatWild
+  = PatVar FC Name
+  | PatCon FC Name (List Pattern)
+  | PatWild FC
   -- Not handling this yet, but we need to be able to work with numbers and strings...
   -- | PatLit Literal
 
+export
+HasFC Pattern where
+  getFC (PatVar fc str) = fc
+  getFC (PatCon fc str xs) = fc
+  getFC (PatWild fc) = fc
+
 -- %runElab deriveShow `{Pattern}
 public export
 Constraint : Type
@@ -65,7 +71,7 @@ data Raw : Type where
 %name Raw tm
 
 export
-getFC : Raw -> FC
+HasFC Raw where
   getFC (RVar fc nm) = fc
   getFC (RLam fc nm icit ty) = fc
   getFC (RApp fc t u icit) = fc
@@ -86,7 +92,7 @@ data Decl : Type where
 
 data Decl
   = TypeSig FC Name Raw
-  | Def Name (List Clause)
+  | Def FC Name (List Clause)
   | DImport FC Name
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
@@ -125,7 +131,7 @@ Show Clause where
 covering
 Show Decl where
   show (TypeSig _ str x) = foo ["TypeSig", show str, show x]
-  show (Def str clauses) = foo ["Def", show str, show clauses]
+  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]
@@ -142,9 +148,9 @@ Show RigCount where
 
 export
 Show Pattern where
-  show (PatVar str) = foo ["PatVar", show str]
-  show (PatCon str xs) = foo ["PatCon", show str, assert_total $ show xs]
-  show PatWild = "PatWild"
+  show (PatVar _ str) = foo ["PatVar", show str]
+  show (PatCon _ str xs) = foo ["PatCon", show str, assert_total $ show xs]
+  show (PatWild _) = "PatWild"
   -- show (PatLit x) = foo ["PatLit" , show x]
 
 covering
@@ -168,9 +174,11 @@ Show Raw where
 
 export
 Pretty Pattern where
-  pretty (PatVar nm) = text nm
-  pretty (PatCon nm args) = text nm <+> spread (map pretty args)
-  pretty PatWild = "_"
+  pretty (PatVar _ nm) = text nm
+  pretty (PatCon _ nm args) = text nm <+> spread (map pretty args)
+  pretty (PatWild _)= "_"
+
+
 
 export
 Pretty Raw where
@@ -215,7 +223,7 @@ Pretty Module where
       where
         doDecl : Decl -> Doc
         doDecl (TypeSig _ nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
-        doDecl (Def nm clauses) = spread $ map doClause clauses
+        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)

src/Lib/Types.idr

@@ -89,7 +89,7 @@ data Tm : Type where
 %name Tm t, u, v
 
 export
-getFC : Tm -> FC
+HasFC Tm where
   getFC (Bnd fc k) = fc
   getFC (Ref fc str x) = fc
   getFC (Meta fc k) = fc
@@ -365,7 +365,7 @@ record Context where
   -- We only need this here if we don't pass TopContext
   -- top : TopContext
   metas : IORef MetaContext
-
+  fc : FC
 
 export
 names : Context -> List String
@@ -379,7 +379,7 @@ M = (StateT TopContext (EitherT Impl.Error IO))
 -- around top
 export
 mkCtx : IORef MetaContext -> Context
-mkCtx metas = MkCtx 0 [] [] [] metas
+mkCtx metas = MkCtx 0 [] [] [] metas emptyFC
 
 ||| Force argument and print if verbose is true
 export