]> matita.cs.unibo.it Git - helm.git/blob - components/acic_procedural/cicClassify.ml
unified: some theorems on Lift started
[helm.git] / components / acic_procedural / cicClassify.ml
1 (* Copyright (C) 2003-2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 module C = Cic
27 module R = CicReduction
28 module D = Deannotate
29 module Int = struct
30    type t = int
31    let compare = compare 
32 end
33 module S = Set.Make (Int) 
34
35 type conclusion = (int * int) option
36
37 (* debugging ****************************************************************)
38
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"
42
43 let to_string (classes, rc) =
44    let linearize = String.concat " " (List.map string_of_entry classes) in
45    match rc with
46       | None        -> linearize
47       | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
48
49 let out_table b =
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
54    in
55    Array.iteri map b;
56    prerr_newline ()
57    
58 (****************************************************************************)
59
60 let id x = x
61
62 let rec list_fold_left g map = function
63   | []       -> g
64   | hd :: tl -> map (list_fold_left g map tl) hd
65
66 let get_rels h t = 
67    let rec aux d g = function
68       | C.Sort _
69       | C.Implicit _       -> g
70       | C.Rel i            -> 
71          if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
72       | C.Appl ss          -> list_fold_left g (aux d) ss
73       | C.Const (_, ss)
74       | C.MutInd (_, _, ss)
75       | C.MutConstruct (_, _, _, ss)
76       | C.Var (_, ss)      -> 
77          let map g (_, t) = aux d g t in 
78          list_fold_left g map ss
79       | C.Meta (_, ss)     ->
80          let map g = function 
81             | None   -> g
82             | Some t -> aux d g t
83          in
84          list_fold_left g map ss
85       | C.Cast (t1, t2)    -> aux d (aux d g t2) t1
86       | C.LetIn (_, t1, t2)
87       | C.Lambda (_, t1, t2)
88       | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
89       | C.MutCase (_, _, t1, t2, ss) ->
90          aux d (aux d (list_fold_left g (aux d) ss) t2) t1
91       | C.Fix (_, ss) ->
92          let k = List.length ss in
93          let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
94          list_fold_left g map ss
95       | C.CoFix (_, ss) ->
96          let k = List.length ss in
97          let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
98          list_fold_left g map ss
99    in
100    let g a = a in
101    aux 1 g t S.empty
102
103 let split c t =
104    let add s v c = Some (s, C.Decl v) :: c in
105    let rec aux whd a n c = function
106       | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
107       | v when whd        -> v :: a, n
108       | v                 -> aux true a n c (R.whd ~delta:true c v)
109     in
110     aux false [] 0 c t
111
112 let classify_conclusion = function
113    | C.Rel i                -> Some (i, 0)
114    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
115    | _                      -> None
116
117 let classify c t =
118 try   
119    let vs, h = split c t in
120    let rc = classify_conclusion (List.hd vs) in
121    let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
122    let l, h = List.fold_left map ([], 0) vs in
123    let b = Array.of_list (List.rev l) in
124    let mk_closure b h =
125       let map j = if j < h then S.union (fst b.(j)) else id in 
126       for i = pred h downto 0 do
127          let direct, unused = b.(i) in
128          b.(i) <- S.fold map direct direct, unused 
129       done; b
130    in
131    let b = mk_closure b h in
132    let rec mk_inverse i direct =
133       if S.is_empty direct then () else
134       let j = S.choose direct in
135       if j < h then
136          let unused, inverse = b.(j) in 
137          b.(j) <- unused, S.add i inverse
138        else ();
139        mk_inverse i (S.remove j direct)
140    in
141    let map i (direct, _) = mk_inverse i direct in
142    Array.iteri map b;
143 (*   out_table b; *)
144    List.rev_map snd (List.tl (Array.to_list b)), rc
145 with Invalid_argument _ -> failwith "Classify.classify"
146
147 let overlaps s1 s2 =
148    let predicate x = S.mem x s1 in
149    S.exists predicate s2