diff --git a/src/Core/CaseTree.idr b/src/Core/CaseTree.idr index 97fcc64..353fff8 100644 --- a/src/Core/CaseTree.idr +++ b/src/Core/CaseTree.idr @@ -5,10 +5,10 @@ import Core.TT mutual public export data CaseTree : List Name -> Type where - Switch : {name : _} -> - (idx : Nat) -> IsVar name idx vars -> - (scTy : Term vars) -> List (CaseAlt vars) -> - CaseTree vars + Case : {name : _} -> + (idx : Nat) -> IsVar name idx vars -> + (scTy : Term vars) -> List (CaseAlt vars) -> + CaseTree vars STerm : Term vars -> CaseTree vars Unmatched : (msg : String) -> CaseTree vars Impossible : CaseTree vars @@ -34,6 +34,26 @@ data Pat : List Name -> Type where FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars PUnmatchable : FC -> Term vars -> Pat vars +mutual + export + Show (CaseTree vars) where + show (Case {name} idx prf ty alts) + = "case " ++ show name ++ " : " ++ show ty ++ " of { " ++ + showSep " | " (assert_total (map show alts)) ++ " }" + show (STerm tm) = show tm + show (Unmatched msg) = "Error: " ++ show msg + show Impossible = "Impossible" + + export + Show (CaseAlt vars) where + show (ConCase n tag args sc) + = show n ++ " " ++ showSep " " (map show args) ++ " => " ++ + show sc + show (ConstCase c sc) + = show c ++ " => " ++ show sc + show (DefaultCase sc) + = "_ => " ++ show sc + mkPat' : List (Pat vars) -> Term vars -> Term vars -> Pat vars mkPat' [] orig (Local fc c idx p) = PLoc fc idx p mkPat' args orig (Ref fc (DataCon t a) n) = PCon fc n t a args @@ -56,9 +76,9 @@ mkPat tm = mkPat' [] tm tm mutual insertCaseNames : (ns : List Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ (ns ++ inner)) - insertCaseNames {inner} {outer} ns (Switch idx prf scTy alts) + insertCaseNames {inner} {outer} ns (Case idx prf scTy alts) = let (_ ** prf') = insertVarNames {outer} {inner} {ns} _ prf in - Switch _ prf' (insertNames {outer} ns scTy) + Case _ prf' (insertNames {outer} ns scTy) (map (insertCaseAltNames {outer} {inner} ns) alts) insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x) insertCaseNames ns (Unmatched msg) = Unmatched msg @@ -80,9 +100,9 @@ mutual export thinTree : (n : Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ n :: inner) -thinTree n (Switch idx prf scTy alts) +thinTree n (Case idx prf scTy alts) = let (_ ** prf') = insertVar {n} _ prf in - Switch _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts) + Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts) thinTree n (STerm tm) = STerm (thin n tm) thinTree n (Unmatched msg) = Unmatched msg thinTree n Impossible = Impossible diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 316f86d..5eecbb7 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1,5 +1,6 @@ module Core.Context +import Core.CaseTree import public Core.Core import Core.Env import public Core.Name @@ -176,7 +177,14 @@ lookupCtxtName n ctxt public export data Def : Type where None : Def -- Not yet defined - Fn : ClosedTerm -> Def -- Ordinary function definition + PMDef : (args : List Name) -> + (treeCT : CaseTree args) -> + (treeRT : CaseTree args) -> + (pats : List (vs ** (Env Term vs, Term vs, Term vs))) -> + -- original checked patterns (LHS/RHS) with the names in + -- the environment. Used for display purposes, and for helping + -- find size changes in termination checking + Def -- Ordinary function definition DCon : (tag : Int) -> (arity : Nat) -> Def -- data constructor TCon : (tag : Int) -> (arity : Nat) -> (parampos : List Nat) -> -- parameters @@ -192,7 +200,8 @@ data Def : Type where export Show Def where show None = "undefined" - show (Fn tm) = show tm + show (PMDef args ct rt pats) + = show args ++ "; " ++ show ct show (DCon t a) = "DataCon " ++ show t ++ " " ++ show a show (TCon t a ps ds cons) = "TyCon " ++ show t ++ " " ++ show a ++ " " ++ show cons @@ -203,7 +212,8 @@ Show Def where export TTC Def where toBuf b None = tag 0 - toBuf b (Fn x) = do tag 1; toBuf b x + toBuf b (PMDef args ct rt pats) + = do tag 1; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats toBuf b (DCon t arity) = do tag 2; toBuf b t; toBuf b arity toBuf b (TCon t arity parampos detpos datacons) = do tag 3; toBuf b t; toBuf b arity; toBuf b parampos @@ -215,8 +225,11 @@ TTC Def where fromBuf r b = case !getTag of 0 => pure None - 1 => do x <- fromBuf r b - pure (Fn x) + 1 => do args <- fromBuf r b + ct <- fromBuf r b + rt <- fromBuf r b + pats <- fromBuf r b + pure (PMDef args ct rt pats) 2 => do t <- fromBuf r b; a <- fromBuf r b pure (DCon t a) 3 => do t <- fromBuf r b; a <- fromBuf r b diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr index 832753e..997bb33 100644 --- a/src/Core/Hash.idr +++ b/src/Core/Hash.idr @@ -142,7 +142,7 @@ mutual export Hashable (CaseTree vars) where - hashWithSalt h (Switch idx x scTy xs) + hashWithSalt h (Case idx x scTy xs) = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs hashWithSalt h (STerm x) = h `hashWithSalt` 1 `hashWithSalt` x diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 56eef90..63bd7ec 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -1,5 +1,6 @@ module Core.Normalise +import Core.CaseTree import Core.Context import Core.Core import Core.Env @@ -131,24 +132,140 @@ parameters (defs : Defs, opts : EvalOpts) evalRef env locs meta fc nt n stk def = do Just res <- lookupCtxtExact n (gamma defs) | Nothing => pure def - evalDef env locs meta (definition res) (flags res) stk def + evalDef env locs meta fc (definition res) (flags res) stk def + + getCaseBound : List (AppInfo, Closure free) -> + (args : List Name) -> + LocalEnv free vars -> + Maybe (LocalEnv free (args ++ vars)) + getCaseBound [] [] loc = Just loc + getCaseBound [] (x :: xs) loc = Nothing -- mismatched arg length + getCaseBound (arg :: args) [] loc = Nothing -- mismatched arg length + getCaseBound (arg :: args) (n :: ns) loc + = do loc' <- getCaseBound args ns loc + pure (snd arg :: loc') + + evalConAlt : Env Term free -> + LocalEnv free (more ++ vars) -> FC -> + Stack free -> + (args : List Name) -> + List (AppInfo, Closure free) -> + CaseTree (args ++ more) -> + (default : Core (NF free)) -> + Core (NF free) + evalConAlt {more} {vars} env loc fc stk args args' sc def + = maybe def (\bound => + let loc' : LocalEnv _ ((args ++ more) ++ vars) + = rewrite sym (appendAssociative args more vars) in + bound in + evalTree env loc' fc stk sc def) + (getCaseBound args' args loc) + + tryAlt : Env Term free -> + LocalEnv free (more ++ vars) -> FC -> + Stack free -> NF free -> CaseAlt more -> + (default : Core (NF free)) -> Core (NF free) + -- Ordinary constructor matching + tryAlt {more} {vars} env loc fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc) def + = if tag == tag' + then evalConAlt env loc fc stk args args' sc def + else def + -- Type constructor matching, in typecase + tryAlt {more} {vars} env loc fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc) def + = if nm == nm' + then evalConAlt env loc fc stk args args' sc def + else def + -- Primitive type matching, in typecase + tryAlt env loc fc stk (NPrimVal _ c) (ConCase (UN x) tag [] sc) def + = if show c == x + then evalTree env loc fc stk sc def + else def + -- Type of type matching, in typecase + tryAlt env loc fc stk (NType _) (ConCase (UN "Type") tag [] sc) def + = evalTree env loc fc stk sc def + -- Arrow matching, in typecase + tryAlt {more} {vars} + env loc fc stk (NBind pfc x (Pi r e aty) scty) (ConCase (UN "->") tag [s,t] sc) def + = evalConAlt {more} {vars} env loc fc stk [s,t] + [(explApp Nothing, MkNFClosure aty), + (explApp Nothing, MkNFClosure (NBind pfc x (Lam r e aty) scty))] + sc def + -- Constant matching + tryAlt env loc fc stk (NPrimVal _ c') (ConstCase c sc) def + = if c == c' then evalTree env loc fc stk sc def + else def + -- Default case matches against any *concrete* value + tryAlt env loc fc stk val (DefaultCase sc) def + = if concrete val + then evalTree env loc fc stk sc def + else def + where + concrete : NF free -> Bool + concrete (NDCon _ _ _ _ _) = True + concrete (NTCon _ _ _ _ _) = True + concrete (NPrimVal _ _) = True + concrete (NBind _ _ _ _) = True + concrete (NType _) = True + concrete _ = False + tryAlt _ _ _ _ _ _ def = def + + findAlt : Env Term free -> + LocalEnv free (args ++ vars) -> FC -> + Stack free -> NF free -> List (CaseAlt args) -> + (default : Core (NF free)) -> Core (NF free) + findAlt env loc fc stk val [] def = def + findAlt env loc fc stk val (x :: xs) def + = tryAlt env loc fc stk val x (findAlt env loc fc stk val xs def) + + evalTree : {vars : _} -> + Env Term free -> LocalEnv free (args ++ vars) -> FC -> + Stack free -> CaseTree args -> + (default : Core (NF free)) -> Core (NF free) + evalTree {args} {vars} {free} env loc fc stk (Case idx x _ alts) def + = do let x' : IsVar _ _ ((args ++ vars) ++ free) + = rewrite sym (appendAssociative args vars free) in + varExtend x + xval <- evalLocal env loc fc Nothing idx x' [] + findAlt env loc fc stk xval alts def + evalTree {args} {vars} {free} env loc fc stk (STerm tm) def + = do let tm' : Term ((args ++ vars) ++ free) + = rewrite sym (appendAssociative args vars free) in + embed tm + case fuel opts of + Nothing => eval env loc tm' stk + Just Z => def + Just (S k) => + do let opts' = record { fuel = Just k } opts + evalWithOpts defs opts' env loc tm' stk + evalTree env loc fc stk _ def = def + + extendFromStack : (args : List Name) -> + LocalEnv free vars -> Stack free -> + Maybe (LocalEnv free (args ++ vars), Stack free) + extendFromStack [] loc stk = Just (loc, stk) + extendFromStack (n :: ns) loc [] = Nothing + extendFromStack (n :: ns) loc (arg :: args) + = do (loc', stk') <- extendFromStack ns loc args + pure (snd arg :: loc', stk') evalDef : {vars : _} -> Env Term free -> LocalEnv free vars -> - (isMeta : Bool) -> + (isMeta : Bool) -> FC -> Def -> List DefFlag -> Stack free -> (def : Lazy (NF free)) -> Core (NF free) - evalDef {vars} env locs meta (Fn tm) flags stk def + evalDef {vars} env locs meta fc (PMDef args tree _ _) flags stk def -- If evaluating the definition fails (e.g. due to a case being -- stuck) return the default = if meta || not (holesOnly opts) || (tcInline opts && elem TCInline flags) - then catch (eval env locs (embed tm) stk) - (\err => pure def) + then case extendFromStack args locs stk of + Nothing => pure def + Just (locs', stk') => + evalTree env locs' fc stk' tree (pure def) else pure def -- All other cases, use the default value, which is already applied to -- the stack - evalDef env locs _ _ _ stk def = pure def + evalDef env locs _ _ _ _ stk def = pure def -- Make sure implicit argument order is right... 'vars' is used so we'll -- write it explicitly, but it does appear after the parameters in 'eval'! diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index eb53020..8c5bae0 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -309,7 +309,7 @@ TTC (Pat vars) where mutual export TTC (CaseTree vars) where - toBuf b (Switch {name} idx x scTy xs) + toBuf b (Case {name} idx x scTy xs) = do tag 0; toBuf b name; toBuf b idx; toBuf b scTy; toBuf b xs toBuf b (STerm x) = do tag 1; toBuf b x @@ -321,7 +321,7 @@ mutual = case !getTag of 0 => do name <- fromBuf r b; idx <- fromBuf r b scTy <- fromBuf r b; xs <- fromBuf r b - pure (Switch {name} idx (mkPrf idx) scTy xs) + pure (Case {name} idx (mkPrf idx) scTy xs) 1 => do x <- fromBuf r b pure (STerm x) 2 => do msg <- fromBuf r b diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 7e019a6..59e6f22 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -1,5 +1,6 @@ module Core.Unify +import Core.CaseTree import Core.Context import Core.Core import Core.Env @@ -244,7 +245,7 @@ instantiate {newvars} loc env mname mref mdef locs otm tm logTerm 6 "Definition" rhs noteUpdate mref addDef (Resolved mref) - (record { definition = Fn rhs } mdef) + (record { definition = PMDef [] (STerm rhs) (STerm rhs) [] } mdef) removeHole mref where updateLoc : List (Var vs) -> IsVar name v vs' -> @@ -646,7 +647,7 @@ retryGuess mode smode (hid, (loc, hname)) -- All constraints resolved, so turn into a -- proper definition and remove it from the -- hole list - [] => do let gdef = record { definition = Fn tm } def + [] => do let gdef = record { definition = PMDef [] (STerm tm) (STerm tm) [] } def noteUpdate hid addDef (Resolved hid) gdef removeGuess hid diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index dca9478..45c6bf8 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -1,5 +1,6 @@ module TTImp.Elab.App +import Core.CaseTree import Core.Context import Core.Core import Core.Env @@ -31,7 +32,7 @@ getNameType rigc env fc x expected | [] => throw (UndefinedName fc x) | ns => throw (AmbiguousName fc (map fst ns)) let nt = case definition def of - Fn _ => Func + PMDef _ _ _ _ => Func DCon t a => DataCon t a TCon t a _ _ _ => TyCon t a _ => Func