diff --git a/newt.ipkg b/newt.ipkg index 7e0a24c..2c57a81 100644 --- a/newt.ipkg +++ b/newt.ipkg @@ -17,7 +17,6 @@ depends = contrib, base -- modules to install modules = - Lib.CaseTree, Lib.Check, Lib.Parser, Lib.Parser.Impl, diff --git a/newt/Zoo1.newt b/newt/Zoo1.newt index d75ef0a..b0e0e42 100644 --- a/newt/Zoo1.newt +++ b/newt/Zoo1.newt @@ -59,15 +59,13 @@ cApp : Closure -> Val -> Val -- If I put Closure instead of MkClosure, it reports missing case, fix that (should be bad constructor or something) cApp (MkClosure env t) u = eval (Define env u) t +hole : Val + eval env (Var x) = case lookup env x of -- case doesn't use the new code. We've got a wildcard here that -- is forced to {Val}, but we don't have forcing/dotting -- I guess we see what Jesper says about dotting Just x => x - -eval env (App t u) = - let tv = eval env t - tu = eval env u - in ? - + Nothing => VVar x +eval env _ = hole diff --git a/src/Lib/CaseTree.idr b/src/Lib/CaseTree.idr deleted file mode 100644 index 0263c08..0000000 --- a/src/Lib/CaseTree.idr +++ /dev/null @@ -1,348 +0,0 @@ -||| Builds a case tree from clauses. -||| 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 Debug.Trace -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 - - --- ok, so new idea: - --- we make a meta for each patvar --- then "solve" the meta when we match stuff up. --- a meta is something we can change - --- but the solutions vary per branch. n is S k in one branch and Z in another. --- and metas are essentially global. - --- NEXT So on LHS, I think we need to collect constraints pat$0 = Val and change --- the entry in the environment to a let? - --- Except I think the let might reference something not bound yet? For RHS (a raw), we --- can shadow. For expected type, we might have to mess with the Val? - --- On RHS I don't think unification can assign a value to a name. - --- exempli gratia --- fromMaybe : Maybe Nat -> Nat --- fromMaybe (Just x) = x --- ^- currently --- fromMaybe Nothing = Z - - --- LHSProblem --- List of [ E ] qbar --> rhs --- E is bag of constraints: --- { w_k /? p_k : A_k | k = 1 ... l } --- qbar copatterns - - --- Case Tree is Σ;Γ ⊢ P | f qbar := Q : C ⤳ Σ' --- rules fig 10 refined version of fig 7, so well type. --- I guess fig 7 will tell us how to typecheck results if we want to skip --- to casetree or verify - --- Agda or Lean would look more like the paper here... - --- I may need defs/lets in the environment - --- Simplified guess at type --- We'll want to add dotted values and push this out --- where the parser can see it - --- I've got a janky typescript POC without types. - --- add FC to Pattern for errors? - --- on the left we have either a bound variable or a constructor applied to bound variables --- on the right we have a pattern --- Raw will refer to variables in pattern, so we either need to subst into Raw, which sounds painful --- or get the variables into scope in a way that the Raw can use them --- 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? - --- 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 --- wrap the result of buildTree with a lambda - --- intro all the things --- split all the things --- turn matches into subst --- see if we're good (no pats, no constraints) - --- 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. - --- 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 - clauses : List Clause - -- I think a pi-type representing the pattern args -> goal, so we're checking - -- We might pull out the pattern abstraction to a separate step and drop pats from clauses. - ty : Val - --- Might have to move this if Check reaches back in... - -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 -> Icit -> Clause -> M Clause --- I don't think this makes a difference? -introClause nm Implicit (MkClause fc cons pats expr) = pure $ MkClause fc ((nm, PatWild fc) :: cons) pats expr -introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't match" -introClause nm icit (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm, pat) :: cons) pats expr - --- A split candidate looks like x /? Con ... --- we need a type here. I pulled if off of the --- pi-type, but do we need metas solved or dependents split? --- this may dot into a dependent. -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 (_ :: xs) = findSplit xs - - --- *************** --- right, I think we rewrite the names in the context before running raw and we're good to go? --- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was? - --- we could pass into build case and use it for (x /? y) - --- TODO, we may need to filter these for the situation. -getConstructors : Context -> Val -> M (List (String, Nat, Tm)) -getConstructors ctx (VRef fc nm _ _) = 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 \{show tm}" - --- Extend environment with fresh variables from a pi-type --- return context, remaining type, and list of names -extendPi : Context -> Val -> SnocList Bind -> M (Context, Val, List Bind) -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 :< MkBind nm icit a) -extendPi ctx ty nms = pure (ctx, ty, nms <>> []) - --- filter clause - --- FIXME - I don't think we're properly noticing - -updateContext : Context -> List (Nat, Val) -> M Context -updateContext ctx [] = pure ctx -updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in - pure $ {env $= makeLet ix} ctx - where - makeLet : Nat -> Env -> Env - makeLet _ [] = ?nothing_to_update - makeLet 0 ((VVar fc j [<]) :: xs) = val :: xs - makeLet 0 (_ :: xs) = ?not_a_var - makeLet (S k) (x :: xs) = x :: makeLet k xs - --- 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 -> Val -> (String, Nat, Tm) -> M CaseAlt -buildCase ctx prob scnm scty (dcName, _, ty) = do - debug "CASE \{scnm} \{dcName} \{pprint (names ctx) ty}" - vty <- eval [] CBN ty - (ctx', ty', vars) <- extendPi ctx (vty) [<] - - -- what is the goal? - -- we have something here that informs what happens in the casealt, possibly tweaking - -- context or goal - -- e.g. we get to end of Just {a} x and goal is Maybe Val, we want `let a = Val` in context. - -- likewise if the constructor says `Foo String` and goal is `Foo x` we know x is String in this branch. - - -- we need unify to hand constraints back... - -- we may need to walk through the case alt constraint and discharge or drop things? - - -- should I somehow make those holes? It would be nice to not make the user dot it. - -- And we don't _need_ a solution, just if it's unified against - - -- I think I'm going down a different road than Idris.. - - - -- do this or see how other people manage? - -- this puts the failure on the LHS - -- unifying these should say say VVar 1 is Nat. - -- ERROR at (23, 0): unify failed (%var 1 [< ]) =?= (%ref Nat [< ]) [no Fn] - res <- unify ctx' (length ctx.env) ty' scty - debug "scty \{show scty}" - debug "UNIFY results \{show res.constraints}" - debug "before types: \{show ctx'.types}" - debug "before env: \{show ctx'.env}" - - -- 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 - debug "context types: \{show ctx'.types}" - debug "context env: \{show ctx'.env}" - -- This doesn't really update existing val... including types in the context. - - -- What if all of the pattern vars are defined to meta - - debug "(dcon \{show dcName} ty \{show ty'} scty \{show scty}" - debug "(dcon \{show dcName}) (vars \{show vars}) clauses were" - for_ prob.clauses $ (\x => debug " \{show x}") - let clauses = mapMaybe (rewriteClause vars) prob.clauses - debug "and now:" - for_ clauses $ (\x => debug " \{show x}") - -- 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 (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. - -- - -- This will be: - -- x /? y can probably just leave this - -- x /? D a b c split into three x /? a, y /? b, z /? c - -- x /? E a b drop this clause - -- We get a list of clauses back (a Problem) and then solve that - -- If they all fail, we have a coverage issue. (Assuming the constructor is valid) - - - -- 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 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 $ (makeConst vars ys) ++ xs ++ acc - else Nothing - else rewriteCons vars xs (c :: acc) - - rewriteClause : List Bind -> Clause -> Maybe Clause - rewriteClause vars (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteCons vars cons []) pats expr - - - -lookupName : Context -> String -> Maybe (Tm, Val) -lookupName ctx name = go 0 ctx.types - where - go : Nat -> Vect n (String, Val) -> Maybe (Tm, Val) - go ix [] = Nothing - -- 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 = do - debug "DONE-> check body \{show body} at \{show ty}" - debug "\{show ctx.env}" - debug "\{show ctx.types}" - got <- check ctx body ty - debug "DONE<- got \{pprint (names ctx) got}" - pure got -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 - let nm = fresh "pat" - let ctx' = extend ctx nm a - -- type of the rest - clauses <- traverse (introClause nm icit) prob.clauses - -- REVIEW fc from a pat? - vb <- b $$ VVar fc l [<] - Lam fc nm <$> buildTree ctx' ({ clauses := clauses, ty := vb } prob) -buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) = - error fc "Extra pattern variables \{show pats}" -buildTree ctx prob@(MkProb ((MkClause fc [] [] expr) :: cs) ty) = check (withPos ctx fc) expr ty --- 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 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, scty) := lookupName ctx scnm - | _ => error fc "Internal Error: can't find \{scnm} in environment" - - cons <- getConstructors ctx scty - alts <- traverse (buildCase ctx prob scnm scty) cons - - pure $ Case fc sctm alts diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 5127715..7d19856 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -200,16 +200,16 @@ insert ctx tm ty = do insert ctx (App emptyFC tm m) !(b $$ mv) va => pure (tm, va) -lookupName : Context -> Raw -> M (Maybe (Tm, Val)) -lookupName ctx (RVar fc nm) = go 0 ctx.types - where - go : Nat -> Vect n (String, Val) -> M (Maybe (Tm, Val)) - go i [] = case lookup nm !(get) of - Just (MkEntry name ty def) => pure $ Just (Ref fc nm def, !(eval [] CBN ty)) - Nothing => pure Nothing - go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd fc i, ty) - else go (i + 1) xs -lookupName ctx _ = pure Nothing +-- lookupName : Context -> Raw -> M (Maybe (Tm, Val)) +-- lookupName ctx (RVar fc nm) = go 0 ctx.types +-- where +-- go : Nat -> Vect n (String, Val) -> M (Maybe (Tm, Val)) +-- go i [] = case lookup nm !(get) of +-- Just (MkEntry name ty def) => pure $ Just (Ref fc nm def, !(eval [] CBN ty)) +-- Nothing => pure Nothing +-- go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd fc i, ty) +-- else go (i + 1) xs +-- lookupName ctx _ = pure Nothing primType : FC -> String -> M Val @@ -225,110 +225,284 @@ export check : Context -> Raw -> Val -> M Tm --- 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 - (con, args) <- getArgs ptm [] - debug "ALT con \{con} args \{show args}" - let Just (MkEntry _ dcty (DCon arity _)) = lookup con !(get) - | Nothing => do - -- check body with con bound at scty against ty - let ctx' = extend ctx con scty - body' <- check ctx' body ty - pure $ CaseDefault body' - | _ => error emptyFC "expected datacon, got \{con}" - -- arity is wrong, but we actually need the type anyway - -- in fact arity is for later (eval?) and we need to do implicits first - debug "arity is \{show arity} dcty \{pprint [] dcty} con \{show con} pats \{show args}" - -- and then we run the names against the type - -- get all that into a context and run the body - -- So, how does this work? - -- The constructor has arguments - -- they may or may not be bound to names. - -- their types may depend on nameless arguments - -- the RHS is a function of some or all of this +data Bind = MkBind String Icit Val - -- I suspect I'll rewrite this a few times - vdcty <- eval [] CBN dcty - debug "go \{show vdcty} \{show ptm}" - alttm <- go vdcty args ctx - debug "GOT \{pprint (names ctx) alttm}" +Show Bind where + show (MkBind str icit x) = "\{str} \{show icit}" - -- package up the results into something. - -- REVIEW args, also probably want the tag not the name. - pure $ CaseCons con (map (snd . snd) args) alttm +public export +record Problem where + constructor MkProb + clauses : List Clause + -- I think a pi-type representing the pattern args -> goal, so we're checking + -- We might pull out the pattern abstraction to a separate step and drop pats from clauses. + ty : Val +-- Might have to move this if Check reaches back in... + +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 -> Icit -> Clause -> M Clause +-- I don't think this makes a difference? +introClause nm Implicit (MkClause fc cons pats expr) = pure $ MkClause fc ((nm, PatWild fc) :: cons) pats expr +introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't match" +introClause nm icit (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm, pat) :: cons) pats expr + +-- A split candidate looks like x /? Con ... +-- we need a type here. I pulled if off of the +-- pi-type, but do we need metas solved or dependents split? +-- this may dot into a dependent. +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 (_ :: xs) = findSplit xs + + +-- *************** +-- right, I think we rewrite the names in the context before running raw and we're good to go? +-- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was? + +-- we could pass into build case and use it for (x /? y) + +-- TODO, we may need to filter these for the situation. +getConstructors : Context -> Val -> M (List (String, Nat, Tm)) +getConstructors ctx (VRef fc nm _ _) = do + names <- lookupTCon nm + traverse lookupDCon names where - argsFC : List (FC, Icit, String) -> FC - argsFC [] = emptyFC - argsFC ((fc,_) :: xs) = fc + 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 \{show tm}" - go : Val -> List (FC, Icit, String) -> Context -> M Tm - -- FIXME icit - -- backwards? - go (VPi fc str Explicit a b) ((fc', Explicit, nm) :: rest) ctx = do - debug "*** \{nm} : \{show a} Explicit \{str}" - let var = VVar fc' (length ctx.env) [<] - let ctx' = extend ctx nm a - Lam fc' nm <$> go !(b $$ var) rest ctx' - go (VPi fc str Implicit a b) ((fc', Implicit, nm) :: rest) ctx = do - debug "*** \{nm} : \{show a} Implicit \{str}" - let var = VVar emptyFC (length ctx.env) [<] - let ctx' = extend ctx nm a - Lam emptyFC nm <$> go !(b $$ var) rest ctx' +-- Extend environment with fresh variables from a pi-type +-- return context, remaining type, and list of names +extendPi : Context -> Val -> SnocList Bind -> M (Context, Val, List Bind) +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 :< MkBind nm icit a) +extendPi ctx ty nms = pure (ctx, ty, nms <>> []) - go (VPi _ str Implicit a b) args ctx = do - debug "*** insert \{str}" - let fc' = argsFC args - let var = VVar fc' (length ctx.env) [<] - let ctx' = extend ctx "_" a - Lam fc' "_" <$> go !(b $$ var) args ctx' - -- same deal with _ for name - go (VPi fc str Explicit a b) ((fc', Implicit, nm) :: rest) ctx = do - error fc' "Implicit/Explicit mismatch \{show str} at \{show nm}" - go (VPi fc str icit x y) [] ctx = error emptyFC "Not enough arguments" +-- filter clause - -- nameless variable - go ctype [] ctx = do - debug "*** end \{show ctype}" - -- FIXME FIXME - I think I should be unifying ctype against scty and learning stuff from it - -- like n = S k. - -- debug "Unifying constructor" - -- unifyCatch emptyFC ctx ctype scty - -- my first example has issues with Vect Z 0 =?= +-- FIXME - I don't think we're properly noticing - check ctx body ty - -- This happens if we run out of runway (more args and no pi) - -- go ctype tm ctx = error (getF "unhandled in checkAlt.go type: \{show ctype} term: \{show tm}" - go ctype args ctx = error (argsFC args) "Extra args" - getArgs : Raw -> List (FC,Icit, String) -> M (String, List (FC,Icit, String)) - getArgs (RVar _ nm) acc = pure (nm, acc) - -- TODO implicits - getArgs (RApp _ t (RVar fc nm) icit) acc = getArgs t ((fc,icit,nm) :: acc) - getArgs (RApp _ t (RHole fc) icit) acc = getArgs t ((fc,icit,"_") :: acc) - getArgs tm _ = error (getFC tm) "Patterns must be constructor and vars, got \{show tm}" +updateContext : Context -> List (Nat, Val) -> M Context +updateContext ctx [] = pure ctx +updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in + pure $ {env $= makeLet ix} ctx + where + makeLet : Nat -> Env -> Env + makeLet _ [] = ?nothing_to_update + makeLet 0 ((VVar fc j [<]) :: xs) = val :: xs + makeLet 0 (_ :: xs) = ?not_a_var + makeLet (S k) (x :: xs) = x :: makeLet k xs + +-- 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 -> Val -> (String, Nat, Tm) -> M CaseAlt +buildCase ctx prob scnm scty (dcName, _, ty) = do + debug "CASE \{scnm} \{dcName} \{pprint (names ctx) ty}" + vty <- eval [] CBN ty + (ctx', ty', vars) <- extendPi ctx (vty) [<] + + -- what is the goal? + -- we have something here that informs what happens in the casealt, possibly tweaking + -- context or goal + -- e.g. we get to end of Just {a} x and goal is Maybe Val, we want `let a = Val` in context. + -- likewise if the constructor says `Foo String` and goal is `Foo x` we know x is String in this branch. + + -- we need unify to hand constraints back... + -- we may need to walk through the case alt constraint and discharge or drop things? + + -- should I somehow make those holes? It would be nice to not make the user dot it. + -- And we don't _need_ a solution, just if it's unified against + + -- I think I'm going down a different road than Idris.. + + + -- do this or see how other people manage? + -- this puts the failure on the LHS + -- unifying these should say say VVar 1 is Nat. + -- ERROR at (23, 0): unify failed (%var 1 [< ]) =?= (%ref Nat [< ]) [no Fn] + res <- unify ctx' (length ctx.env) ty' scty + debug "scty \{show scty}" + debug "UNIFY results \{show res.constraints}" + debug "before types: \{show ctx'.types}" + debug "before env: \{show ctx'.env}" + + -- 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 + debug "context types: \{show ctx'.types}" + debug "context env: \{show ctx'.env}" + -- This doesn't really update existing val... including types in the context. + + -- What if all of the pattern vars are defined to meta + + debug "(dcon \{show dcName} ty \{show ty'} scty \{show scty}" + debug "(dcon \{show dcName}) (vars \{show vars}) clauses were" + for_ prob.clauses $ (\x => debug " \{show x}") + let clauses = mapMaybe (rewriteClause vars) prob.clauses + debug "and now:" + for_ clauses $ (\x => debug " \{show x}") + -- 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 (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. + -- + -- This will be: + -- x /? y can probably just leave this + -- x /? D a b c split into three x /? a, y /? b, z /? c + -- x /? E a b drop this clause + -- We get a list of clauses back (a Problem) and then solve that + -- If they all fail, we have a coverage issue. (Assuming the constructor is valid) + + + -- 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 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 $ (makeConst vars ys) ++ xs ++ acc + else Nothing + else rewriteCons vars xs (c :: acc) + + rewriteClause : List Bind -> Clause -> Maybe Clause + rewriteClause vars (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteCons vars cons []) pats expr + + + +lookupName : Context -> String -> Maybe (Tm, Val) +lookupName ctx name = go 0 ctx.types + where + go : Nat -> Vect n (String, Val) -> Maybe (Tm, Val) + go ix [] = Nothing + -- 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 = do + debug "DONE-> check body \{show body} at \{show ty}" + debug "\{show ctx.env}" + debug "\{show ctx.types}" + got <- check ctx body ty + debug "DONE<- got \{pprint (names ctx) got}" + pure got +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 + let nm = fresh "pat" + let ctx' = extend ctx nm a + -- type of the rest + clauses <- traverse (introClause nm icit) prob.clauses + -- REVIEW fc from a pat? + vb <- b $$ VVar fc l [<] + Lam fc nm <$> buildTree ctx' ({ clauses := clauses, ty := vb } prob) +buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) = + error fc "Extra pattern variables \{show pats}" +buildTree ctx prob@(MkProb ((MkClause fc [] [] expr) :: cs) ty) = check (withPos ctx fc) expr ty +-- 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 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, scty) := lookupName ctx scnm + | _ => error fc "Internal Error: can't find \{scnm} in environment" + + cons <- getConstructors ctx scty + alts <- traverse (buildCase ctx prob scnm scty) cons + + pure $ Case fc sctm alts 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. + -- We've got a beta redex or need to do something... + -- Maybe we can let the scrutinee and jump into the middle? (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' + + let scnm = fresh "sc" + -- FIXME FC + let clauses = map (\(MkAlt pat rawRHS) =>MkClause fc [(scnm, pat)] [] rawRHS ) alts + let ctx' = extend ctx scnm scty + cons <- getConstructors ctx' scty + alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons + + pure $ Case fc sc alts + + -- buildTree ctx (MkProb{}) + -- ?hole -- Document a hole, pretend it's implemented (RHole fc, ty) => do ty' <- quote ctx.lvl ty diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index a94ecaa..6d109c8 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -1,4 +1,6 @@ -- TODO I think I'm missing the bit where a case might need to be assigned to a variable. +-- E.g. case statement whose result is passed to complex expression should assign a variable +-- then the stuff happens. We'd need to know more about the callback for that. -- TODO And then get primitives and a way to declare extern functions. That may get us -- to utility module Lib.Compile diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index bf3b79d..4f0b1ec 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -177,7 +177,8 @@ pPattern' = PatCon <$> getPos <*> uident <*> many pPattern <|> pPattern caseAlt : Parser RCaseAlt caseAlt = do - pat <- parseOp -- pPattern -- term and sort it out later? + -- pat <- parseOp -- pPattern -- term and sort it out later? + pat <- pPattern' keyword "=>" commit t <- term diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index c9b0c0d..9e53cca 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -2,7 +2,6 @@ module Lib.ProcessDecl import Data.IORef -import Lib.CaseTree import Lib.Check import Lib.Parser import Lib.Syntax diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 8514ff8..e0b04d3 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -50,7 +50,7 @@ record Clause where -- could be a pair, but I suspect stuff will be added? public export -data RCaseAlt = MkAlt Raw Raw +data RCaseAlt = MkAlt Pattern Raw data Raw : Type where RVar : FC -> (nm : Name) -> Raw diff --git a/test/src/Main.idr b/test/src/Main.idr index 5b995e5..27aab4c 100644 --- a/test/src/Main.idr +++ b/test/src/Main.idr @@ -6,7 +6,6 @@ import Lib.Types import Lib.ProcessDecl import Lib.TopContext import Lib.Syntax -import Lib.CaseTree testCase : M () testCase = do