fixes to pattern matching and codegen, J example works now

README.md

@@ -33,6 +33,13 @@ I have `Let` in the core language. Partly because I'd like this to make it into
 
 I've got no idea what I'm doing here. I worked off of Jesper Cockx "Elaborating Dependent (Co)pattern Matching", leaving out codata for now.
 
+For the dependent thing, I've change unify to return `VVar` constraints. I think this is an error typechecking on
+RHS (meta solutions are handled separately). On the LHS, I'm rewriting the environment to turn the var from a bind
+to a define. Unification has been tweaked to look up `VVar` in environment. Bind will hand back the same `VVar`.
+
+Some of this I could probably do with subst, but the RHS is `Raw`, it takes typechecking to turn it into a clean `Tm`,
+and I need this information for the typechecking.
+
 ## Issues
 
 - I need to do some erasure of values unused at runtime

TODO.md

@@ -1,17 +1,20 @@
 
 ## TODO
 
-- [ ] there is some zero argument application in generated code
+- [x] there is some zero argument application in generated code
-  - possibly the fancy "apply arity then curry the rest" bit
 - [x] get equality.newt to work
+  - [x] broken again because I added J, probably need to constrain scrutinee to value
 - [x] inline metas.  Maybe zonk after TC/elab
 - [x] implicit patterns
-- [ ] pair syntax
+- [ ] pair syntax (should this be a comma operator)
 - [ ] list syntax
 - [ ] operators
 - [ ] import
-- [ ] add {{ }} and solving autos
+- [ ] add {{ }} and solving autos (or maybe just `auto` keyword)
   - considering various solutions.  Perhaps marking the data type as solvable, if we had types on metas.
+  - keep as implicit and mark auto, behavior overlaps a lot with implicit
+  - but we might want to solve right away when creating the implicit
+  - later we might need postpone
 - [ ] do blocks
 - [ ] some solution for `+` (classes? ambiguity?)
 - [ ] show compiler failure in the editor (exit code != 0)

src/Lib/Check.idr

@@ -260,6 +260,7 @@ fresh base = base ++ "$" ++ show (length ctx.env)
 export
 buildTree : Context -> Problem -> M Tm
 
+-- Updates a clause for INTRO
 introClause : String -> Icit -> Clause -> M Clause
 introClause nm icit (MkClause fc cons (pat :: pats) expr) =
   if icit == getIcit pat then pure $ MkClause fc ((nm, pat) :: cons) pats expr
@@ -305,15 +306,16 @@ getConstructors ctx (VRef fc nm _ _) = do
 getConstructors ctx tm = error (getValFC tm) "Not a type constructor \{show tm}"
 
 -- Extend environment with fresh variables from a pi-type
+-- the pi-type here is the telescope of a constructor
 -- return context, remaining type, and list of names
-extendPi : Context -> Val -> SnocList Bind -> M (Context, Val, List Bind)
+extendPi : Context -> Val -> SnocList Bind -> SnocList Val -> M (Context, Val, List Bind, SnocList Val)
-extendPi ctx (VPi x str icit a b) nms = do
+extendPi ctx (VPi x str icit a b) nms sc = do
     let nm = fresh str -- "pat"
     let ctx' = extend ctx nm a
     let v = VVar emptyFC (length ctx.env) [<]
     tyb <- b $$ v
-    extendPi ctx' tyb (nms :< MkBind nm icit a)
+    extendPi ctx' tyb (nms :< MkBind nm icit a) (sc :< VVar x (length ctx.env) [<])
-extendPi ctx ty nms = pure (ctx, ty, nms <>> [])
+extendPi ctx ty nms sc = pure (ctx, ty, nms <>> [], sc)
 
 -- turn vars into lets for forced values.
 -- Maybe we need to do more? revist the paper.
@@ -332,10 +334,10 @@ updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus`
 -- since we've gotten here, we assume it's possible and we better have at least
 -- one valid clause
 buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M CaseAlt
-buildCase ctx prob scnm scty (dcName, _, ty) = do
+buildCase ctx prob scnm scty (dcName, arity, ty) = do
   debug "CASE \{scnm} \{dcName} \{pprint (names ctx) ty}"
   vty <- eval [] CBN ty
-  (ctx', ty', vars) <- extendPi ctx (vty) [<]
+  (ctx', ty', vars, sc) <- extendPi ctx (vty) [<] [<]
 
   -- what is the goal?
   -- we have something here that informs what happens in the casealt, possibly tweaking
@@ -358,14 +360,21 @@ buildCase ctx prob scnm scty (dcName, _, ty) = do
   debug "unify dcon dom with scrut"
   res <- unify ctx' (length ctx'.env) ty' scty
   --res <- unify ctx' (length ctx.env) ty' scty
+
+  let Just x = findIndex ((==scnm) . fst) ctx'.types
+    | Nothing => error ctx.fc "\{scnm} not is scope?"
+  let lvl = ((length ctx'.env) `minus` (cast x)) `minus` 1
+  let scon : (Nat, Val) = (lvl, VRef ctx.fc dcName (DCon arity dcName) sc)
+
   debug "scty \{show scty}"
   debug "UNIFY results \{show res.constraints}"
   debug "before types: \{show ctx'.types}"
   debug "before env: \{show ctx'.env}"
+  debug "SC CONSTRAINT: \{show scon}"
 
   -- So we go and stuff stuff into the environment, which I guess gets it into the RHS,
   -- but doesn't touch goal...
-  ctx' <- updateContext ctx' res.constraints
+  ctx' <- updateContext ctx' (scon :: res.constraints)
   debug "context types: \{show ctx'.types}"
   debug "context env: \{show ctx'.env}"
   -- This doesn't really update existing val... including types in the context.

src/Lib/CompileExp.idr

@@ -70,7 +70,8 @@ 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
-    go (CApp t []) [] = pure t
+    -- drop zero arg call
+    go (CApp t []) args = go t args
     go t [] = pure t
     go t (arg :: args) = go (CApp t [arg]) args
 
@@ -117,12 +118,12 @@ compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u)
 
 export
 compileFun : Tm -> M CExp
-compileFun tm = go tm []
+compileFun tm = go tm [<]
   where
-    go : Tm -> List String -> M CExp
+    go : Tm -> SnocList String -> M CExp
-    go (Lam _ nm t) acc = go t (nm :: acc)
+    go (Lam _ nm t) acc = go t (acc :< nm)
-    go tm [] = compileTerm tm
+    go tm [<] = compileTerm tm
-    go tm args = pure $ CFun (reverse args) !(compileTerm tm)
+    go tm args = pure $ CFun (args <>> []) !(compileTerm tm)
 
 
 

tests/black/equality.newt

@@ -10,3 +10,15 @@ sym Refl = Refl
 
 trans : {A : U} {x y z : A} -> Eq x y -> Eq y z -> Eq x z
 trans Refl Refl = Refl
+
+coerce : {A B : U} -> Eq A B -> A -> B
+coerce Refl a = a
+
+J : {A : U} ->
+    {C : (x y : A) -> Eq x y -> U} ->
+    (c : (x : _) -> C x x Refl) ->
+    (x y : A) ->
+    (p : Eq x y) ->
+    C x y p
+-- this was failing until I constrained scrutinee to the constructor + args
+J c x y Refl = c x