0 | module Core.Termination.Positivity
2 | import Core.Context.Log
4 | import Core.Normalise
7 | import Core.Termination.References
11 | import Libraries.Data.NatSet
15 | isAssertTotal : Ref Ctxt Defs => NHead vars -> Core Bool
16 | isAssertTotal (NRef _ fn_in) =
17 | do fn <- getFullName fn_in
18 | pure (fn == NS builtinNS (UN $
Basic "assert_total"))
19 | isAssertTotal _ = pure False
21 | nameIn : {auto c : Ref Ctxt Defs} ->
22 | Defs -> List Name -> ClosedNF -> Core Bool
23 | nameIn defs tyns (NBind fc x b sc)
24 | = if !(nameIn defs tyns !(evalClosure defs (binderType b)))
26 | else do let nm = Ref fc Bound (MN ("NAMEIN_" ++ show x) 0)
27 | let arg = toClosure defaultOpts Env.empty nm
29 | nameIn defs tyns sc'
30 | nameIn defs tyns (NApp _ nh args)
31 | = do False <- isAssertTotal nh
32 | | True => pure False
33 | anyM (nameIn defs tyns)
34 | !(traverse (evalClosure defs . snd) args)
35 | nameIn defs tyns (NTCon _ n _ args)
38 | else do args' <- traverse (evalClosure defs . snd) args
39 | anyM (nameIn defs tyns) args'
40 | nameIn defs tyns (NDCon _ n _ _ args)
41 | = anyM (nameIn defs tyns)
42 | !(traverse (evalClosure defs . snd) args)
43 | nameIn defs tyns (NDelayed fc lr ty) = nameIn defs tyns ty
44 | nameIn defs tyns (NDelay fc lr ty tm) = nameIn defs tyns !(evalClosure defs tm)
45 | nameIn defs tyns _ = pure False
49 | posArg : {auto c : Ref Ctxt Defs} ->
50 | Defs -> List Name -> ClosedNF -> Core Terminating
52 | posArgs : {auto c : Ref Ctxt Defs} ->
53 | Defs -> List Name -> List ClosedClosure -> Core Terminating
54 | posArgs defs tyn [] = pure IsTerminating
55 | posArgs defs tyn (x :: xs)
56 | = do xNF <- evalClosure defs x
57 | logNF "totality.positivity" 50 "Checking parameter for positivity" Env.empty xNF
58 | IsTerminating <- posArg defs tyn xNF
64 | posArg defs tyns nf@(NTCon loc tc _ args) =
65 | do logNF "totality.positivity" 50 "Found a type constructor" Env.empty nf
66 | testargs <- case !(lookupDefExact tc (gamma defs)) of
67 | Just (TCon _ params _ _ _ _ _) => do
68 | log "totality.positivity" 50 $
69 | unwords [show tc, "has", show (size params), "parameters"]
70 | pure $
NatSet.partition params (map snd args)
71 | _ => throw (GenericMsg loc (show tc ++ " not a data type"))
72 | let (params, indices) = testargs
73 | False <- anyM (nameIn defs tyns) !(traverse (evalClosure defs) indices)
74 | | True => pure (NotTerminating NotStrictlyPositive)
75 | posArgs defs tyns params
77 | posArg defs tyns nf@(NBind fc x (Pi _ _ e ty) sc)
78 | = do logNF "totality.positivity" 50 "Found a Pi-type" Env.empty nf
79 | if !(nameIn defs tyns !(evalClosure defs ty))
80 | then pure (NotTerminating NotStrictlyPositive)
81 | else do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 1)
82 | let arg = toClosure defaultOpts Env.empty nm
84 | posArg defs tyns sc'
85 | posArg defs tyns nf@(NApp fc nh args)
86 | = do False <- isAssertTotal nh
87 | | True => do logNF "totality.positivity" 50 "Trusting an assertion" Env.empty nf
89 | logNF "totality.positivity" 50 "Found an application" Env.empty nf
90 | args <- traverse (evalClosure defs . snd) args
91 | pure $
if !(anyM (nameIn defs tyns) args)
92 | then NotTerminating NotStrictlyPositive
94 | posArg defs tyn (NDelayed fc lr ty) = posArg defs tyn ty
96 | = do logNF "totality.positivity" 50 "Reached the catchall" Env.empty nf
99 | checkPosArgs : {auto c : Ref Ctxt Defs} ->
100 | Defs -> List Name -> ClosedNF -> Core Terminating
101 | checkPosArgs defs tyns (NBind fc x (Pi _ _ e ty) sc)
102 | = case !(posArg defs tyns !(evalClosure defs ty)) of
104 | do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 0)
105 | let arg = toClosure defaultOpts Env.empty nm
106 | checkPosArgs defs tyns !(sc defs arg)
108 | checkPosArgs defs tyns nf
109 | = do logNF "totality.positivity" 50 "Giving up on non-Pi type" Env.empty nf
112 | checkCon : {auto c : Ref Ctxt Defs} ->
113 | Defs -> List Name -> Name -> Core Terminating
114 | checkCon defs tyns cn
115 | = case !(lookupTyExact cn (gamma defs)) of
116 | Nothing => do log "totality.positivity" 20 $
117 | "Couldn't find constructor " ++ show cn
120 | case !(totRefsIn defs ty) of
122 | do tyNF <- nf defs Env.empty ty
123 | logNF "totality.positivity" 20 "Checking the type " Env.empty tyNF
124 | checkPosArgs defs tyns tyNF
127 | checkData : {auto c : Ref Ctxt Defs} ->
128 | Defs -> List Name -> List Name -> Core Terminating
129 | checkData defs tyns [] = pure IsTerminating
130 | checkData defs tyns (c :: cs)
131 | = do log "totality.positivity" 40 $
132 | "Checking positivity of constructor " ++ show c
133 | case !(checkCon defs tyns c) of
134 | IsTerminating => checkData defs tyns cs
137 | blockingAssertTotal : {auto c : Ref Ctxt Defs} -> FC -> Core a -> Core a
138 | blockingAssertTotal loc ma
139 | = do defs <- get Ctxt
140 | let at = NS builtinNS (UN $
Basic "assert_total")
141 | Just _ <- lookupCtxtExact at (gamma defs)
143 | setVisibility loc at Private
145 | setVisibility loc at Public
151 | calcPositive : {auto c : Ref Ctxt Defs} ->
152 | FC -> Name -> Core (Terminating, List Name)
154 | = do defs <- get Ctxt
155 | logC "totality.positivity" 6 $
do pure $
"Calculating positivity: " ++ show !(toFullNames n)
156 | case !(lookupDefTyExact n (gamma defs)) of
157 | Just (TCon _ _ _ _ tns dcons _, ty) =>
158 | let dcons = fromMaybe [] dcons in
159 | case !(totRefsIn defs ty) of
161 | do log "totality.positivity" 30 $
162 | "Now checking constructors of " ++ show !(toFullNames n)
163 | t <- blockingAssertTotal loc $
checkData defs (n :: tns) dcons
165 | bad => pure (bad, dcons)
166 | Just _ => throw (GenericMsg loc (show n ++ " not a data type"))
167 | Nothing => undefinedName loc n