edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 12:54:28 +03:00
Code Issues Projects Releases Wiki Activity

Replace 'Fn' with 'PMDef'

Browse Source 
Pattern matching clauses rather than just simple terms
This commit is contained in:
Edwin Brady 2019-04-19 21:50:23 +01:00
parent cd958bd304
commit 82ac86bde0
7 changed files with 177 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
src/Core/CaseTree.idr
View File

@ -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

23
src/Core/Context.idr
View File

@ -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

2
src/Core/Hash.idr
View File

@ -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

129
src/Core/Normalise.idr
View File

@ -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'!

4
src/Core/TTC.idr
View File

@ -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

5
src/Core/Unify.idr
View File

@ -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

3
src/TTImp/Elab/App.idr
View File

@ -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