*)
module C = Cic
-module CS = CicSubstitution
+module R = CicReduction
module D = Deannotate
module Int = struct
type t = int
(****************************************************************************)
+let id x = x
+
let rec list_fold_left g map = function
| [] -> g
| hd :: tl -> map (list_fold_left g map tl) hd
let g a = a in
aux 1 g t S.empty
-let split t =
- let rec aux a n = function
- | C.Prod (_, v, t) -> aux (v :: a) (succ n) t
- | C.Cast (t, v) -> aux a n t
- | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
- | v -> v :: a, n
+let split c t =
+ let add s v c = Some (s, C.Decl v) :: c in
+ let rec aux whd a n c = function
+ | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
+ | v when whd -> v :: a, n
+ | v -> aux true a n c (R.whd ~delta:true c v)
in
- aux [] 0 t
+ aux false [] 0 c t
let classify_conclusion = function
| C.Rel i -> Some (i, 0)
| C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
| _ -> None
-let classify t =
- let vs, h = split t in
+let classify c t =
+try
+ let vs, h = split c t in
let rc = classify_conclusion (List.hd vs) in
let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
let l, h = List.fold_left map ([], 0) vs in
let b = Array.of_list (List.rev l) in
let mk_closure b h =
- let map j = S.union (fst b.(j)) in
+ let map j = if j < h then S.union (fst b.(j)) else id in
for i = pred h downto 0 do
let direct, unused = b.(i) in
b.(i) <- S.fold map direct direct, unused
let rec mk_inverse i direct =
if S.is_empty direct then () else
let j = S.choose direct in
- let unused, inverse = b.(j) in
- b.(j) <- unused, S.add i inverse;
- mk_inverse i (S.remove j direct)
+ if j < h then
+ let unused, inverse = b.(j) in
+ b.(j) <- unused, S.add i inverse
+ else ();
+ mk_inverse i (S.remove j direct)
in
let map i (direct, _) = mk_inverse i direct in
Array.iteri map b;
(* out_table b; *)
List.rev_map snd (List.tl (Array.to_list b)), rc
-
-let aclassify t = classify (D.deannotate_term t)
+with Invalid_argument _ -> failwith "Classify.classify"
let overlaps s1 s2 =
let predicate x = S.mem x s1 in