1 exception CicReductionInternalError;;
2 exception WrongUriToInductiveDefinition;;
6 let rec debug_aux t i =
8 let module U = UriManager in
9 CicPp.ppobj (C.Variable ("DEBUG", None,
10 C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
11 C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
12 C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
13 C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
14 C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
15 C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
16 C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
17 C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
18 C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
33 print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
38 exception Impossible of int;;
39 exception ReferenceToDefinition;;
40 exception ReferenceToAxiom;;
41 exception ReferenceToVariable;;
42 exception ReferenceToCurrentProof;;
43 exception ReferenceToInductiveDefinition;;
45 (* takes a well-typed term *)
49 let module S = CicSubstitution in
51 C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
52 | C.Var _ as t -> if l = [] then t else C.Appl (t::l)
53 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
54 | C.Sort _ as t -> t (* l should be empty *)
55 | C.Implicit as t -> t
56 | C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
57 | C.Prod _ as t -> t (* l should be empty *)
58 | C.Lambda (name,s,t) as t' ->
61 | he::tl -> whdaux tl (S.subst he t)
62 (* when name is Anonimous the substitution should be superfluous *)
64 | C.Appl (he::tl) -> whdaux (tl@l) he
65 | C.Appl [] -> raise (Impossible 1)
66 | C.Const (uri,cookingsno) as t ->
67 (match CicCache.get_cooked_obj uri cookingsno with
68 C.Definition (_,body,_,_) -> whdaux l body
69 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
70 (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *)
71 | C.Variable _ -> if l = [] then t else C.Appl (t::l)
72 | C.CurrentProof (_,_,body,_) -> whdaux l body
73 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
75 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
76 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
77 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
78 | C.MutCase (mutind,cookingsno,i,_,term,pl) as t ->
81 C.CoFix (i,fl) as t ->
82 let (_,_,body) = List.nth fl i in
84 let counter = ref (List.length fl) in
86 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
91 | C.Appl (C.CoFix (i,fl) :: tl) ->
92 let (_,_,body) = List.nth fl i in
94 let counter = ref (List.length fl) in
96 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
103 (match decofix (whdaux [] term) with
104 C.MutConstruct (_,_,_,j) -> whdaux l (List.nth pl (j-1))
105 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
106 let (arity, r, num_ingredients) =
107 match CicCache.get_obj mutind with
108 C.InductiveDefinition (tl,ingredients,r) ->
109 let (_,_,arity,_) = List.nth tl i
110 and num_ingredients =
113 if k < cookingsno then i + List.length l else i
116 (arity,r,num_ingredients)
117 | _ -> raise WrongUriToInductiveDefinition
120 let num_to_eat = r + num_ingredients in
124 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
125 | _ -> raise (Impossible 5)
127 eat_first (num_to_eat,tl)
129 whdaux (ts@l) (List.nth pl (j-1))
130 | C.Abst _| C.Cast _ | C.Implicit ->
131 raise (Impossible 2) (* we don't trust our whd ;-) *)
134 | C.Fix (i,fl) as t ->
135 let (_,recindex,_,body) = List.nth fl i in
138 Some (List.nth l recindex)
144 (match whdaux [] recparam with
146 | C.Appl ((C.MutConstruct _)::_) ->
148 let counter = ref (List.length fl) in
150 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
154 (* Possible optimization: substituting whd recparam in l *)
156 | _ -> if l = [] then t else C.Appl (t::l)
158 | None -> if l = [] then t else C.Appl (t::l)
160 | C.CoFix (i,fl) as t ->
162 let (_,_,body) = List.nth fl i in
164 let counter = ref (List.length fl) in
166 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
172 if l = [] then t else C.Appl (t::l)
177 (* t1, t2 must be well-typed *)
178 let are_convertible t1 t2 =
179 let module U = UriManager in
181 debug t1 [t2] "PREWHD";
182 (* this trivial euristic cuts down the total time of about five times ;-) *)
183 (* this because most of the time t1 and t2 are "sintactically" the same *)
188 let module C = Cic in
191 debug t1' [t2'] "POSTWHD";
192 (*if !fdebug = 0 then ignore(Unix.system "read" );*)
194 (C.Rel n1, C.Rel n2) -> n1 = n2
195 | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
196 | (C.Meta n1, C.Meta n2) -> n1 = n2
197 | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
198 | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
199 aux s1 s2 && aux t1 t2
200 | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
201 aux s1 s2 && aux t1 t2
202 | (C.Appl l1, C.Appl l2) ->
204 List.fold_right2 (fun x y b -> aux x y && b) l1 l2 true
206 Invalid_argument _ -> false
208 | (C.Const (uri1,_), C.Const (uri2,_)) ->
209 (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *)
210 (*CSC: mentre sono delirante, quindi ... *)
211 (* WARNING: it is really important that the two cookingsno are not *)
212 (* checked for equality. This allows not to cook an object with no *)
213 (* ingredients only to update the cookingsno. E.g: if a term t has *)
214 (* a reference to a term t1 which does not depend on any variable *)
215 (* and t1 depends on a term t2 (that can't depend on any variable *)
216 (* because of t1), then t1 cooked at every level could be the same *)
217 (* as t1 cooked at level 0. Doing so, t2 will be extended in t *)
218 (* with cookingsno 0 and not 2. But this will not cause any trouble*)
219 (* if here we don't check that the two cookingsno are equal. *)
221 | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) ->
222 (* WARNIG: see the previous warning *)
223 U.eq uri1 uri2 && i1 = i2
224 | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) ->
225 (* WARNIG: see the previous warning *)
226 U.eq uri1 uri2 && i1 = i2 && j1 = j2
227 | (C.MutCase (uri1,_,i1,outtype1,term1,pl1),
228 C.MutCase (uri2,_,i2,outtype2,term2,pl2)) ->
229 (* WARNIG: see the previous warning *)
230 (* aux outtype1 outtype2 should be true if aux pl1 pl2 *)
231 U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 &&
233 List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true
234 | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
237 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
238 b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2)
240 | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
243 (fun (_,ty1,bo1) (_,ty2,bo2) b ->
244 b && aux ty1 ty2 && aux bo1 bo2)
246 | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
247 | (C.Implicit, _) | (_, C.Implicit) ->
248 raise (Impossible 3) (* we don't trust our whd ;-) *)