From 13dd77345ce77b2d1eb8b7d57cea3cb4e8dec8d3 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 7 Aug 2024 21:49:35 -0700 Subject: [PATCH] Process pattern in correct order --- newt/testcase.newt | 37 ++++++++++++++++++++--- src/Lib/Check.idr | 66 +++++++++++++++++++++++------------------- src/Lib/Compile.idr | 19 +++++++----- src/Lib/TopContext.idr | 1 + src/Lib/Types.idr | 13 +++++++-- 5 files changed, 92 insertions(+), 44 deletions(-) diff --git a/newt/testcase.newt b/newt/testcase.newt index 21d7b25..4c6a082 100644 --- a/newt/testcase.newt +++ b/newt/testcase.newt @@ -1,7 +1,5 @@ module Scratch - - data Nat : U where Z : Nat S : Nat -> Nat @@ -16,8 +14,39 @@ plus = \ n m => case n of S k => S (plus k m) -- So this isn't working at the moment, I think I need --- to replace the n with S ?k +-- to replace the n with S k +-- +-- this is working kinda, but `length {a}` xs doesn't, so we +-- don't know the a's are the same +-- +-- I think "unify" scty with the end of the constructor type +-- But it's going to be something like +-- Vect (S k) a' =?= Vect n a length : {a : U} {n : Nat} -> Vect n a -> Nat length = \ v => case v of Nil => Z - Cons {a} {n'} x xs => S (length {a} xs) + Cons x xs => S (length xs) + +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)) + +data Bool : U where + True : Bool + False : Bool + +not : Bool -> Bool +not = \ v => case v of + True => False + False => True + +data Void : U where + +falseElim : {A : U} -> Void -> A +falseElim = \ v => case v of diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 8962eb9..cc7a383 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -133,13 +133,13 @@ parameters (ctx: Context) -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. _ => error emptyFC "unify failed \{show t'} =?= \{show u'} \n env is \{show ctx.env} \{show $ map fst ctx.types}" -unifyCatch : Context -> Val -> Val -> M () -unifyCatch ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do +unifyCatch : FC -> Context -> Val -> Val -> M () +unifyCatch fc ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do let names = toList $ map fst ctx.types a <- quote ctx.lvl ty' b <- quote ctx.lvl ty let msg = "\n failed to unify \{pprint names a}\n with \{pprint names b}\n " <+> str - throwError (E x msg) + throwError (E fc msg) insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val) insert ctx tm ty = do @@ -180,7 +180,7 @@ checkAlt scty ctx ty (MkAlt ptm body) = do -- 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}" + 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 @@ -193,50 +193,56 @@ checkAlt scty ctx ty (MkAlt ptm body) = do -- I suspect I'll rewrite this a few times vdcty <- eval [] CBN dcty debug "go \{show vdcty} \{show ptm}" - alttm <- go vdcty ptm ctx + alttm <- go vdcty args ctx debug "GOT \{pprint (names ctx) alttm}" -- package up the results into something. -- REVIEW args, also probably want the tag not the name. - pure $ CaseCons con args alttm + pure $ CaseCons con (map (snd . snd) args) alttm where + argsFC : List (FC, Icit, String) -> FC + argsFC [] = emptyFC + argsFC ((fc,_) :: xs) = fc - go : Val -> Raw -> Context -> M Tm + go : Val -> List (FC, Icit, String) -> Context -> M Tm -- FIXME icit - go (VPi fc str Explicit a b) (RApp _ t (RVar _ nm) Explicit) ctx = do - debug "*** \{nm} : \{show a}" + -- 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) t ctx' - go (VPi fc str Implicit a b) (RApp _ t (RVar _ nm) Implicit) ctx = do - debug "*** \{nm} : \{show a}" - let var = VVar emptyFC (length ctx.env) [<] - let ctx' = extend ctx nm a - Lam emptyFC nm <$> go !(b $$ var) t ctx' - go (VPi fc str Implicit a b) t ctx = do - let var = VVar emptyFC (length ctx.env) [<] + Lam emptyFC nm <$> go !(b $$ var) rest ctx' + go (VPi fc 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 emptyFC "_" <$> go !(b $$ var) t ctx' + Lam fc' "_" <$> go !(b $$ var) args ctx' -- same deal with _ for name - go (VPi fc str icit x y) (RApp _ t (RImplicit _) icit') ctx = ?rhs_19 - go (VPi fc str icit x y) tm ctx = error emptyFC "Can't use \{show tm} as pattern" + go (VPi fc str Explicit a b) ((fc', Implicit, nm) :: rest) ctx = do + error fc' "Implicit/Explicit mismatch \{show str} \{show nm}" + go (VPi fc str icit x y) [] ctx = error emptyFC "Not enough arguments" -- nameless variable - go ctype (RImplicit _) ctx = ?rhs_2 - go ctype (RVar _ nm) ctx = do - debug "*** end" + go ctype [] ctx = do + debug "*** end \{show ctype}" check ctx body ty -- pure ctx -- this should be our constructor. -- This happens if we run out of runway (more args and no pi) - go ctype tm ctx = error (getFC tm) "unhandled in go \{show ctype} \{show tm}" - - getArgs : Raw -> List String -> M (String, List String) + -- 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 _ nm) icit) acc = getArgs t (nm :: acc) - getArgs (RApp _ t (RHole _) icit) acc = getArgs t ("_" :: acc) - getArgs tm _ = error emptyFC "Patterns must be constructor and vars, got \{show tm}" + 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}" check ctx tm ty = case (tm, !(forceType ty)) of @@ -300,7 +306,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of insert ctx tm' ty' debug "INFER \{show tm} to (\{pprint names tm'} : \{show ty'}) expect \{show ty}" - unifyCatch ctx ty' ty + unifyCatch (getFC tm) ctx ty' ty pure tm' infer ctx (RVar fc nm) = go 0 ctx.types diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 1294c88..5e5955e 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -12,15 +12,20 @@ data JSExp : Type where data JSStmt : Type where +-- Need to sort out + + + compile : Nat -> Tm -> Doc -- Oh, we don't have local names... -compile l (Bnd k) = text "_\{show k}" +compile l (Bnd _ k) = text "_\{show k}" -- this is tied to Bnd -- And we probably want `{...}` with statements... -compile l (Lam str t) = text "(_\{show l}) => " <+> compile (S l) t -compile l (Ref str mt) = text str -compile l (App t u) = compile l t <+> "(" <+> compile l u <+> ")" +compile l (Lam _ str t) = text "(_\{show l}) => " <+> compile (S l) t +compile l (Ref _ str mt) = text str +compile l (App _ t u) = compile l t <+> "(" <+> compile l u <+> ")" -compile l U = "undefined" -compile l (Pi str icit t u) = "undefined" -compile l (Meta k) = text "ZONKME \{show k}" +compile l (U _) = "undefined" +compile l (Pi _ str icit t u) = "undefined" +compile l (Meta _ k) = text "ZONKME \{show k}" +compile l (Case fc tm alts) = ?rhs_8 diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index 97b32bc..57e5934 100644 --- a/src/Lib/TopContext.idr +++ b/src/Lib/TopContext.idr @@ -17,6 +17,7 @@ lookup nm top = go top.defs -- Maybe pretty print? export +covering Show TopContext where show (MkTop defs metas _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 2caab08..05655e0 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -80,11 +80,16 @@ getFC (U fc) = fc getFC (Pi fc str icit t u) = fc getFC (Case fc t xs) = fc +covering +Show Tm +covering Show CaseAlt where - show alt = "FIXME" + show (CaseDefault tm) = "_ => \{show tm}" + show (CaseCons nm args tm) = "\{nm} \{unwords args} => \{show tm}" -- public export +covering Show Tm where show (Bnd _ k) = "(Bnd \{show k})" show (Ref _ str _) = "(Ref \{show str})" @@ -92,8 +97,8 @@ Show Tm where show (App _ t u) = "(\{show t} \{show u})" show (Meta _ i) = "(Meta \{show i})" show (U _) = "U" - show (Pi _ str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})" - show (Pi _ str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})" + show (Pi _ str Explicit t u) = "(Pi (\{str} : \{show t}) => \{show u})" + show (Pi _ str Implicit t u) = "(Pi {\{str} : \{show t}} => \{show u})" show (Case _ sc alts) = "(Case \{show sc} \{show alts})" -- I can't really show val because it's HOAS... @@ -265,6 +270,7 @@ public export data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm public export +covering Show Def where show Axiom = "axiom" show (TCon strs) = "TCon \{show strs}" @@ -282,6 +288,7 @@ record TopEntry where -- FIXME snoc export +covering Show TopEntry where show (MkEntry name type def) = "\{name} : \{show type} := \{show def}"