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

Record mutual type definitions

Browse Source 
Also add some tests for totality checker
This commit is contained in:
Edwin Brady 2019-06-05 17:28:55 +01:00
parent 95cc48eeb6
commit bf67f5c87c
27 changed files with 258 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/AutoSearch.idr
View File

@ -284,7 +284,7 @@ searchName fc rigc defaults depth def top env target (n, ndef)
let namety : NameType
= case definition ndef of
DCon tag arity => DataCon tag arity
TCon tag arity _ _ _ _ => TyCon tag arity
TCon tag arity _ _ _ _ _ => TyCon tag arity
_ => Func
nty <- nf defs env (embed ty)
(args, appTy) <- mkArgs fc rigc env nty

52
src/Core/Context.idr
View File

@ -236,6 +236,7 @@ data Def : Type where
TCon : (tag : Int) -> (arity : Nat) ->
(parampos : List Nat) -> -- parameters
(detpos : List Nat) -> -- determining arguments
(mutwith : List Name) ->
(datacons : List Name) ->
(typehints : List (Name, Bool)) ->
Def
@ -255,7 +256,7 @@ Show Def where
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 hints)
show (TCon t a ps ds ms cons hints)
= "TyCon " ++ show t ++ " " ++ show a ++ " " ++ show cons
show (ExternDef arity) = "<external def with arith " ++ show arity ++ ">"
show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
@ -275,9 +276,9 @@ TTC Def where
toBuf b (Builtin a)
= throw (InternalError "Trying to serialise a Builtin")
toBuf b (DCon t arity) = do tag 3; toBuf b t; toBuf b arity
toBuf b (TCon t arity parampos detpos datacons _)
toBuf b (TCon t arity parampos detpos ms datacons _)
= do tag 4; toBuf b t; toBuf b arity; toBuf b parampos
toBuf b detpos; toBuf b datacons
toBuf b detpos; toBuf b ms; toBuf b datacons
toBuf b (Hole locs invertible) = do tag 5; toBuf b locs; toBuf b invertible
toBuf b (BySearch c depth def)
= do tag 6; toBuf b c; toBuf b depth; toBuf b def
@ -298,8 +299,9 @@ TTC Def where
3 => do t <- fromBuf r b; a <- fromBuf r b
pure (DCon t a)
4 => do t <- fromBuf r b; a <- fromBuf r b
ps <- fromBuf r b; dets <- fromBuf r b; cs <- fromBuf r b
pure (TCon t a ps dets cs [])
ps <- fromBuf r b; dets <- fromBuf r b;
ms <- fromBuf r b; cs <- fromBuf r b
pure (TCon t a ps dets ms cs [])
5 => do l <- fromBuf r b
i <- fromBuf r b
pure (Hole l i)
@ -511,6 +513,7 @@ public export
record Defs where
constructor MkDefs
gamma : Context GlobalDef
mutData : List Name -- Currently declared but undefined data types
currentNS : List String -- namespace for current definitions
options : Options
toSave : NameMap ()
@ -555,7 +558,7 @@ export
initDefs : Core Defs
initDefs
= do gam <- initCtxt
pure (MkDefs gam ["Main"] defaults empty 100
pure (MkDefs gam [] ["Main"] defaults empty 100
empty empty [] [] 5381 [] [] [] [])
-- Label for context references
@ -910,7 +913,7 @@ getSearchData : {auto c : Ref Ctxt Defs} ->
Core SearchData
getSearchData fc defaults target
= do defs <- get Ctxt
Just (TCon _ _ _ dets cons hs) <- lookupDefExact target (gamma defs)
Just (TCon _ _ _ dets _ cons hs) <- lookupDefExact target (gamma defs)
| _ => throw (UndefinedName fc target)
if defaults
then let defaults = map fst (filter isDefault
@ -930,6 +933,31 @@ getSearchData fc defaults target
direct : (Name, Bool) -> Bool
direct = snd
export
setMutWith : {auto c : Ref Ctxt Defs} ->
FC -> Name -> List Name -> Core ()
setMutWith fc tn tns
= do defs <- get Ctxt
Just g <- lookupCtxtExact tn (gamma defs)
| _ => throw (UndefinedName fc tn)
let TCon t a ps dets _ cons hs = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor"))
updateDef tn (const (Just (TCon t a ps dets tns cons hs)))
export
addMutData : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
addMutData n
= do defs <- get Ctxt
put Ctxt (record { mutData $= (n ::) } defs)
export
dropMutData : {auto c : Ref Ctxt Defs} ->
Name -> Core ()
dropMutData n
= do defs <- get Ctxt
put Ctxt (record { mutData $= filter (/= n) } defs)
export
setDetermining : {auto c : Ref Ctxt Defs} ->
FC -> Name -> List Name -> Core ()
@ -937,10 +965,10 @@ setDetermining fc tyn args
= do defs <- get Ctxt
Just g <- lookupCtxtExact tyn (gamma defs)
| _ => throw (UndefinedName fc tyn)
let TCon t a ps _ cons hs = definition g
let TCon t a ps _ cons ms hs = definition g
| _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor"))
apos <- getPos 0 args (type g)
updateDef tyn (const (Just (TCon t a ps apos cons hs)))
updateDef tyn (const (Just (TCon t a ps apos cons ms hs)))
where
-- Type isn't normalised, but the argument names refer to those given
-- explicitly in the type, so there's no need.
@ -966,9 +994,9 @@ addHintFor fc tyn hintn_in direct
_ => case getNameID hintn_in (gamma defs) of
Nothing => hintn_in
Just idx => Resolved idx
Just (TCon t a ps dets cons hs) <- lookupDefExact tyn (gamma defs)
Just (TCon t a ps dets cons ms hs) <- lookupDefExact tyn (gamma defs)
| _ => throw (GenericMsg fc (show tyn ++ " is not a type constructor"))
updateDef tyn (const (Just (TCon t a ps dets cons ((hintn, direct) :: hs))))
updateDef tyn (const (Just (TCon t a ps dets cons ms ((hintn, direct) :: hs))))
defs <- get Ctxt
put Ctxt (record { saveTypeHints $= ((tyn, hintn, direct) :: )
} defs)
@ -1087,7 +1115,7 @@ addData vars vis (MkData (MkCon dfc tyn arity tycon) datacons)
(TCon tag arity
(paramPos tyn (map type datacons))
(allDet arity)
(map name datacons) [])
[] (map name datacons) [])
(idx, gam') <- addCtxt tyn tydef (gamma defs)
gam'' <- addDataConstructors 0 datacons gam'
put Ctxt (record { gamma = gam'' } defs)

4
src/Core/Coverage.idr
View File

@ -51,7 +51,7 @@ export
isEmpty : Defs -> NF vars -> Core Bool
isEmpty defs (NTCon fc n t a args)
= case !(lookupDefExact n (gamma defs)) of
Just (TCon _ _ _ _ cons _)
Just (TCon _ _ _ _ _ cons _)
=> allM (conflict defs (NTCon fc n t a args)) cons
_ => pure False
isEmpty defs _ = pure False
@ -66,7 +66,7 @@ freeEnv fc (n :: ns) = PVar RigW (Erased fc) :: freeEnv fc ns
getCons : Defs -> NF vars -> Core (List (NF [], Name, Int, Nat))
getCons defs (NTCon _ tn _ _ _)
= case !(lookupDefExact tn (gamma defs)) of
Just (TCon _ _ _ _ cons _) =>
Just (TCon _ _ _ _ _ cons _) =>
do cs' <- traverse addTy cons
pure (mapMaybe id cs')
_ => pure []

17
src/Core/Termination.idr
View File

@ -445,7 +445,7 @@ posArg : Defs -> List Name -> NF [] -> Core Terminating
posArg defs tyns (NTCon _ tc _ _ args)
= let testargs : List (Closure [])
= case !(lookupDefExact tc (gamma defs)) of
Just (TCon _ _ params _ _ _) =>
Just (TCon _ _ params _ _ _ _) =>
dropParams 0 params (map snd args)
_ => map snd args in
if !(anyM (nameIn defs tyns)
@ -502,11 +502,10 @@ calcPositive : {auto c : Ref Ctxt Defs} ->
calcPositive loc n
= do defs <- get Ctxt
case !(lookupDefTyExact n (gamma defs)) of
Just (TCon _ _ _ _ dcons _, ty) =>
Just (TCon _ _ _ _ tns dcons _, ty) =>
case !(totRefsIn defs ty) of
IsTerminating =>
do let tns = []
t <- checkData defs (n :: tns) dcons
do t <- checkData defs (n :: tns) dcons
pure (t , dcons)
bad => pure (bad, dcons)
Just _ => throw (GenericMsg loc (show n ++ " not a data type"))
@ -532,13 +531,17 @@ checkPositive loc n
export
checkTotal : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core Terminating
checkTotal loc n
= do tot <- getTotality loc n
checkTotal loc n_in
= do defs <- get Ctxt
let Just nidx = getNameID n_in (gamma defs)
| Nothing => throw (UndefinedName loc n_in)
let n = Resolved nidx
tot <- getTotality loc n
defs <- get Ctxt
case isTerminating tot of
Unchecked =>
case !(lookupDefExact n (gamma defs)) of
Just (TCon _ _ _ _ _ _)
Just (TCon _ _ _ _ _ _ _)
=> checkPositive loc n
_ => checkTerminating loc n
t => pure t

2
src/TTImp/Elab/Ambiguity.idr
View File

@ -67,7 +67,7 @@ expandAmbigName mode env orig args (IVar fc x) exp
wrapDot : Defs -> EState vars ->
ElabMode -> Name -> List RawImp -> Def -> RawImp -> RawImp
wrapDot _ _ _ _ _ (DCon _ _) tm = tm
wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _) tm = tm
wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _ _) tm = tm
-- Leave primitive applications alone, because they'll be inlined
-- before compiling the case tree
wrapDot defs est (InLHS _) n' [arg] _ tm

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

@ -39,7 +39,7 @@ getNameType rigc env fc x
let nt = case definition def of
PMDef _ _ _ _ => Func
DCon t a => DataCon t a
TCon t a _ _ _ _ => TyCon t a
TCon t a _ _ _ _ _ => TyCon t a
_ => Func
addNameType fc x env (embed (type def))
pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
@ -70,7 +70,7 @@ getVarType rigc nest env fc x
let nt = case definition ndef of
PMDef _ _ _ _ => Func
DCon t a => DataCon t a
TCon t a _ _ _ _ => TyCon t a
TCon t a _ _ _ _ _ => TyCon t a
_ => Func
tm = tmf fc nt
tyenv = useVars (map snd (getArgs tm))
@ -189,8 +189,6 @@ mutual
Just stm =>
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (InternalError "Can't happen: no definition")
logTerm 0 ("Instantiating " ++ show mname) stm
logTerm 0 "Type" (type hdef)
instantiate fc env mname idx hdef locs soln stm
pure True
solveIfUndefined env metavar soln

2
src/TTImp/Elab/Record.idr
View File

@ -37,7 +37,7 @@ toRHS loc (Constr con args)
findConName : Defs -> Name -> Core (Maybe Name)
findConName defs tyn
= case !(lookupDefExact tyn (gamma defs)) of
Just (TCon _ _ _ _ [con] _) => pure (Just con)
Just (TCon _ _ _ _ _ [con] _) => pure (Just con)
_ => pure Nothing
findFields : Defs -> Name -> Core (Maybe (List (String, Maybe Name)))

2
src/TTImp/Interactive/CaseSplit.idr
View File

@ -92,7 +92,7 @@ findCons n lhs
Nothing => pure (SplitFail (CantSplitThis n
("Can't find type of " ++ show n ++ " in LHS")))
Just tyn =>
do Just (TCon _ _ _ _ cons _) <-
do Just (TCon _ _ _ _ _ cons _) <-
lookupDefExact tyn (gamma defs)
| res => pure (SplitFail
(CantSplitThis n

2
src/TTImp/Interactive/ExprSearch.idr
View File

@ -125,7 +125,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
let namety : NameType
= case definition ndef of
DCon tag arity => DataCon tag arity
TCon tag arity _ _ _ _ => TyCon tag arity
TCon tag arity _ _ _ _ _ => TyCon tag arity
_ => Func
log 5 $ "Trying " ++ show (fullname ndef)
nty <- nf defs env (embed ty)

3
src/TTImp/Parser.idr
View File

@ -701,6 +701,9 @@ command
<|> do symbol ":"; exactIdent "missing"
n <- name
pure (Missing n)
<|> do symbol ":"; keyword "total"
n <- name
pure (CheckTotal n)
<|> do symbol ":"; exactIdent "di"
n <- name
pure (DebugInfo n)

39
src/TTImp/ProcessData.idr
View File

@ -114,7 +114,11 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
-- Add the type constructor as a placeholder
tidx <- addDef n (newDef fc n Rig1 vars fullty vis
(TCon 0 arity [] [] [] []))
(TCon 0 arity [] [] [] [] []))
addMutData (Resolved tidx)
defs <- get Ctxt
traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)
case vis of
Private => pure ()
_ => do addHash n
@ -135,16 +139,18 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
-- If n exists, check it's the same type as we have here, and is
-- a data constructor.
-- When looking up, note the data types which were undefined at the
-- point of declaration.
ndefm <- lookupCtxtExact n (gamma defs)
case ndefm of
Nothing => pure ()
Just ndef =>
case definition ndef of
TCon _ _ _ _ _ _ =>
do ok <- convert defs [] fullty (type ndef)
if ok then pure ()
else throw (AlreadyDefined fc n)
_ => throw (AlreadyDefined fc n)
mw <- case ndefm of
Nothing => pure []
Just ndef =>
case definition ndef of
TCon _ _ _ _ mw _ _ =>
do ok <- convert defs [] fullty (type ndef)
if ok then pure mw
else throw (AlreadyDefined fc n)
_ => throw (AlreadyDefined fc n)
logTermNF 5 ("data " ++ show n) [] fullty
@ -154,7 +160,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
-- Add the type constructor as a placeholder while checking
-- data constructors
tidx <- addDef n (newDef fc n Rig1 vars fullty vis
(TCon 0 arity [] [] [] []))
(TCon 0 arity [] [] [] [] []))
case vis of
Private => pure ()
_ => do addHash n
@ -168,11 +174,18 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
let ddef = MkData (MkCon dfc n arity fullty) cons
addData vars vis ddef
-- Type is defined mutually with every data type undefined at the
-- point it was declared, and every data type undefined right now
defs <- get Ctxt
let mutWith = nub (mw ++ mutData defs)
log 3 $ show n ++ " defined in a mutual block with " ++ show mw
setMutWith fc (Resolved tidx) mw
traverse_ (processDataOpt fc (Resolved tidx)) opts
dropMutData (Resolved tidx)
when (not (NoHints `elem` opts)) $
traverse_ (\x => addHintFor fc (Resolved tidx) x True) (map conName cons)
-- TODO: Interface hash
pure ()

17
src/TTImp/ProcessDef.idr
View File

@ -24,8 +24,8 @@ import Data.NameMap
mutual
mismatchNF : Defs -> NF vars -> NF vars -> Core Bool
mismatchNF defs (NTCon _ _ xt _ xargs) (NTCon _ _ yt _ yargs)
= if xt /= yt
mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
= if xn /= yn
then pure True
else anyM (mismatch defs) (zip (map snd xargs) (map snd yargs))
mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
@ -47,9 +47,16 @@ mutual
-- is an impossible case, so return True
export
impossibleOK : Defs -> NF vars -> NF vars -> Core Bool
impossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ tn yt ya yargs)
= anyM (mismatch defs) (zip (map snd xargs) (map snd yargs))
impossibleOK _ _ _ = pure False
impossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
= if xn == yn
then anyM (mismatch defs) (zip (map snd xargs) (map snd yargs))
else pure False
-- If it's a data constructor, any mismatch will do
impossibleOK defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
= if xt /= yt
then pure True
else anyM (mismatch defs) (zip (map snd xargs) (map snd yargs))
impossibleOK defs x y = pure False
-- Given a type checked LHS and its type, return the environment in which we
-- should check the RHS, the LHS and its type in that environment,

1
src/TTImp/TTImp.idr
View File

@ -301,6 +301,7 @@ data ImpREPL : Type where
ExprSearch : Name -> ImpREPL
GenerateDef : Int -> Name -> ImpREPL
Missing : Name -> ImpREPL
CheckTotal : Name -> ImpREPL
DebugInfo : Name -> ImpREPL
Quit : ImpREPL

11
src/Yaffle/REPL.idr
View File

@ -7,6 +7,7 @@ import Core.Env
import Core.FC
import Core.Metadata
import Core.Normalise
import Core.Termination
import Core.TT
import Core.Unify
import Core.Value
@ -117,6 +118,16 @@ process (Missing n_in)
_ => coreLift $ putStrLn (show fn ++ ": All cases covered"))
(map fst ts)
pure True
process (CheckTotal n)
= do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName emptyFC n)
ts => do traverse_ (\fn =>
do checkTotal emptyFC fn
tot <- getTotality emptyFC fn
coreLift (putStrLn (show fn ++ " is " ++ show tot)))
(map fst ts)
pure True
process (DebugInfo n)
= do defs <- get Ctxt
traverse showInfo !(lookupCtxtName n (gamma defs))

1
tests/Main.idr
View File

@ -18,6 +18,7 @@ ttimpTests
"rewrite001",
"qtt001", "qtt002", "qtt003",
"search001", "search002", "search003", "search004", "search005",
"total001", "total002", "total003",
"with001"]
chdir : String -> IO Bool

33
tests/ttimp/total001/Vect.yaff Normal file
View File

@ -0,0 +1,33 @@
data Bool : Type where
False : Bool
True : Bool
not : Bool -> Bool
not False = True
not True = False
data Nat : Type where
Z : Nat
S : Nat -> Nat
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
data Vect : ? -> Type -> Type where
Nil : Vect Z a
Cons : a -> Vect k a -> Vect (S k) a
data Fin : Nat -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
lookup : Fin n -> Vect n a -> a
lookup FZ (Cons x xs) = x
lookup (FS k) (Cons x xs) = lookup k xs
append : Vect n a -> Vect m a -> Vect (plus n m) a
append xs ys
= case xs of
Nil => ys
Cons z zs => Cons z (append zs ys)

5
tests/ttimp/total001/expected Normal file
View File

@ -0,0 +1,5 @@
Processing as TTImp
Written TTC
Yaffle> Main.lookup is total
Yaffle> Main.append is total
Yaffle> Bye for now!

3
tests/ttimp/total001/input Normal file
View File

@ -0,0 +1,3 @@
:total lookup
:total append
:q

3
tests/ttimp/total001/run Executable file
View File

@ -0,0 +1,3 @@
$1 Vect.yaff < input
rm -rf build

50
tests/ttimp/total002/Total.yaff Normal file
View File

@ -0,0 +1,50 @@
data Bool : Type where
False : Bool
True : Bool
not : Bool -> Bool
not False = True
not True = False
data Nat : Type where
Z : Nat
S : Nat -> Nat
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
ack : Nat -> Nat -> Nat
ack Z n = S n
ack (S k) Z = ack k (S Z)
ack (S j) (S k) = ack j (ack (S j) k)
foo : Nat -> Nat
foo Z = Z
foo (S Z) = (S Z)
foo (S (S k)) = foo (S k)
foo' : Nat -> Nat
foo' Z = Z
foo' (S Z) = (S Z)
foo' (S p@(S k)) = foo' p
data Bin : Type where
EPS : Bin
C0 : Bin -> Bin
C1 : Bin -> Bin
foom : Bin -> Nat
foom EPS = Z
foom (C0 EPS) = Z
foom (C0 (C1 x)) = S (foom (C1 x))
foom (C0 (C0 x)) = foom (C0 x)
foom (C1 x) = S (foom x)
pfoom : Bin -> Nat
pfoom EPS = Z
pfoom (C0 EPS) = Z
pfoom (C0 (C1 x)) = S (pfoom (C0 x))
pfoom (C0 (C0 x)) = pfoom (C0 x)
pfoom (C1 x) = S (foom x)

9
tests/ttimp/total002/expected Normal file
View File

@ -0,0 +1,9 @@
Processing as TTImp
Written TTC
Yaffle> Main.Nat is total
Yaffle> Main.ack is total
Yaffle> Main.foo is total
Yaffle> Main.foo' is total
Yaffle> Main.foom is total
Yaffle> Main.pfoom is not terminating due to recursive path $resolved158 -> Main.pfoom -> Main.pfoom
Yaffle> Bye for now!

7
tests/ttimp/total002/input Normal file
View File

@ -0,0 +1,7 @@
:total Nat
:total ack
:total foo
:total foo'
:total foom
:total pfoom
:q

3
tests/ttimp/total002/run Executable file
View File

@ -0,0 +1,3 @@
$1 Total.yaff < input
rm -rf build

15
tests/ttimp/total003/Bad.yaff Normal file
View File

@ -0,0 +1,15 @@
data Bad : Type where
MkBad : (Bad -> Int) -> Int -> Bad
MkBad' : Int -> Bad
foo : Bad -> Int
foo (MkBad f i) = f (MkBad' i)
foo (MkBad' x) = x
foo2 : Bad -> Int
foo2 b = case b of
MkBad f i => f (MkBad' i)
MkBad' x => x
data T : Type -> Type where
MkT : T (T a) -> T a

8
tests/ttimp/total003/expected Normal file
View File

@ -0,0 +1,8 @@
Processing as TTImp
Written TTC
Yaffle> Main.Bad is not strictly positive
Yaffle> Main.MkBad is not strictly positive
Yaffle> Main.MkBad' is not strictly positive
Yaffle> Main.foo is not terminating due to calls to $resolved71, $resolved72
Yaffle> Main.T is not strictly positive
Yaffle> Bye for now!

6
tests/ttimp/total003/input Normal file
View File

@ -0,0 +1,6 @@
:total Bad
:total MkBad
:total MkBad'
:total foo
:total T
:q

3
tests/ttimp/total003/run Executable file
View File

@ -0,0 +1,3 @@
$1 Bad.yaff < input
rm -rf build