1 (* Copyright (C) 2003-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 module CS = CicSubstitution
33 module S = Set.Make (Int)
35 type conclusion = (int * int) option
37 (* debugging ****************************************************************)
39 let string_of_entry inverse =
40 if S.mem 0 inverse then "C" else
41 if S.is_empty inverse then "I" else "P"
43 let to_string (classes, rc) =
44 let linearize = String.concat " " (List.map string_of_entry classes) in
47 | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
50 let map i (_, inverse) =
51 let map i tl = Printf.sprintf "%2u" i :: tl in
52 let iset = String.concat " " (S.fold map inverse []) in
53 Printf.eprintf "%2u|%s\n" i iset
58 (****************************************************************************)
60 let rec list_fold_left g map = function
62 | hd :: tl -> map (list_fold_left g map tl) hd
65 let rec aux d g = function
69 if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
70 | C.Appl ss -> list_fold_left g (aux d) ss
73 | C.MutConstruct (_, _, _, ss)
75 let map g (_, t) = aux d g t in
76 list_fold_left g map ss
82 list_fold_left g map ss
83 | C.Cast (t1, t2) -> aux d (aux d g t2) t1
85 | C.Lambda (_, t1, t2)
86 | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
87 | C.MutCase (_, _, t1, t2, ss) ->
88 aux d (aux d (list_fold_left g (aux d) ss) t2) t1
90 let k = List.length ss in
91 let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
92 list_fold_left g map ss
94 let k = List.length ss in
95 let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
96 list_fold_left g map ss
102 let rec aux a n = function
103 | C.Prod (_, v, t) -> aux (v :: a) (succ n) t
104 | C.Cast (t, v) -> aux a n t
105 | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
110 let classify_conclusion = function
111 | C.Rel i -> Some (i, 0)
112 | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
116 let vs, h = split t in
117 let rc = classify_conclusion (List.hd vs) in
118 let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
119 let l, h = List.fold_left map ([], 0) vs in
120 let b = Array.of_list (List.rev l) in
122 let map j = S.union (fst b.(j)) in
123 for i = pred h downto 0 do
124 let direct, unused = b.(i) in
125 b.(i) <- S.fold map direct direct, unused
128 let b = mk_closure b h in
129 let rec mk_inverse i direct =
130 if S.is_empty direct then () else
131 let j = S.choose direct in
132 let unused, inverse = b.(j) in
133 b.(j) <- unused, S.add i inverse;
134 mk_inverse i (S.remove j direct)
136 let map i (direct, _) = mk_inverse i direct in
139 List.rev_map snd (List.tl (Array.to_list b)), rc
141 let aclassify t = classify (D.deannotate_term t)
144 let predicate x = S.mem x s1 in
145 S.exists predicate s2