1 (* ||M|| This file is part of HELM, an Hypertextual, Electronic
2 ||A|| Library of Mathematics, developed at the Computer Science
3 ||T|| Department, University of Bologna, Italy.
5 ||T|| HELM is free software; you can redistribute it and/or
6 ||A|| modify it under the terms of the GNU General Public License
7 \ / version 2 or (at your option) any later version.
8 \ / This software is distributed as is, NO WARRANTY.
9 V_______________________________________________________________ *)
13 (* TODO unify exceptions *)
15 exception WrongUriToInductiveDefinition;;
16 exception Impossible of int;;
17 exception ReferenceToConstant;;
18 exception ReferenceToVariable;;
19 exception ReferenceToCurrentProof;;
20 exception ReferenceToInductiveDefinition;;
24 let debug_print s = if debug then prerr_endline (Lazy.force s)
28 let rec debug_aux t i =
30 let module U = UriManager in
31 CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
34 debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
37 module type Strategy =
41 type config = int * env_term list * NCic.term * stack_term list
43 reduce: (config -> config) ->
44 unwind: (config -> NCic.term) ->
46 val from_stack : stack_term -> config
47 val from_stack_list_for_unwind :
48 unwind: (config -> NCic.term) ->
49 stack_term list -> NCic.term list
50 val from_env : env_term -> config
51 val from_env_for_unwind :
52 unwind: (config -> NCic.term) ->
55 reduce: (config -> config) ->
56 unwind: (config -> NCic.term) ->
57 stack_term -> env_term
59 reduce: (config -> config) ->
60 unwind: (config -> NCic.term) ->
61 int -> env_term list ->
63 val compute_to_stack :
64 reduce: (config -> config) ->
65 unwind: (config -> NCic.term) ->
70 module CallByValueByNameForUnwind' =
72 type config = int * env_term list * NCic.term * stack_term list
73 and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
74 and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
75 let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
76 let from_stack (c,_) = Lazy.force c
77 let from_stack_list_for_unwind ~unwind:_ l =
78 List.map (function (_,c) -> Lazy.force c) l
79 let from_env (c,_) = Lazy.force c
80 let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c
81 let stack_to_env ~reduce:_ ~unwind:_ config = config
82 let compute_to_env ~reduce ~unwind k e t =
83 lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[]))
84 let compute_to_stack ~reduce ~unwind config =
85 lazy (reduce config), lazy (unwind config)
90 (* {{{ module CallByValueByNameForUnwind =
92 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
93 and stack_term = config
94 and env_term = config * config (* cbv, cbn *)
95 and ens_term = config * config (* cbv, cbn *)
99 let from_stack config = config
100 let from_stack_list_for_unwind ~unwind l = List.map unwind l
101 let from_env (c,_) = c
102 let from_ens (c,_) = c
103 let from_env_for_unwind ~unwind (_,c) = unwind c
104 let from_ens_for_unwind ~unwind (_,c) = unwind c
105 let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
106 let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
107 let compute_to_stack ~reduce ~unwind config = config
113 module CallByNameStrategy =
115 type stack_term = Cic.term
116 type env_term = Cic.term
117 type ens_term = Cic.term
118 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
121 let from_stack ~unwind v = v
122 let from_stack_list ~unwind l = l
125 let from_env_for_unwind ~unwind v = v
126 let from_ens_for_unwind ~unwind v = v
127 let stack_to_env ~reduce ~unwind v = v
128 let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
129 let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
133 module CallByNameStrategy =
135 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
136 and stack_term = config
137 and env_term = config
138 and ens_term = config
142 let from_stack config = config
143 let from_stack_list_for_unwind ~unwind l = List.map unwind l
146 let from_env_for_unwind ~unwind c = unwind c
147 let from_ens_for_unwind ~unwind c = unwind c
148 let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
149 let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
150 let compute_to_stack ~reduce ~unwind config = config
154 module CallByValueStrategy =
156 type stack_term = Cic.term
157 type env_term = Cic.term
158 type ens_term = Cic.term
159 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
162 let from_stack ~unwind v = v
163 let from_stack_list ~unwind l = l
166 let from_env_for_unwind ~unwind v = v
167 let from_ens_for_unwind ~unwind v = v
168 let stack_to_env ~reduce ~unwind v = v
169 let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
170 let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
174 module CallByValueStrategyByNameOnConstants =
176 type stack_term = Cic.term
177 type env_term = Cic.term
178 type ens_term = Cic.term
179 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
182 let from_stack ~unwind v = v
183 let from_stack_list ~unwind l = l
186 let from_env_for_unwind ~unwind v = v
187 let from_ens_for_unwind ~unwind v = v
188 let stack_to_env ~reduce ~unwind v = v
189 let compute_to_stack ~reduce ~unwind k e ens =
191 Cic.Const _ as t -> unwind k e ens t
192 | t -> reduce (k,e,ens,t,[])
193 let compute_to_env ~reduce ~unwind k e ens =
195 Cic.Const _ as t -> unwind k e ens t
196 | t -> reduce (k,e,ens,t,[])
200 module LazyCallByValueStrategy =
202 type stack_term = Cic.term lazy_t
203 type env_term = Cic.term lazy_t
204 type ens_term = Cic.term lazy_t
205 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
206 let to_env v = lazy v
207 let to_ens v = lazy v
208 let from_stack ~unwind v = Lazy.force v
209 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
210 let from_env v = Lazy.force v
211 let from_ens v = Lazy.force v
212 let from_env_for_unwind ~unwind v = Lazy.force v
213 let from_ens_for_unwind ~unwind v = Lazy.force v
214 let stack_to_env ~reduce ~unwind v = v
215 let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
216 let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
220 module LazyCallByValueStrategyByNameOnConstants =
222 type stack_term = Cic.term lazy_t
223 type env_term = Cic.term lazy_t
224 type ens_term = Cic.term lazy_t
225 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
226 let to_env v = lazy v
227 let to_ens v = lazy v
228 let from_stack ~unwind v = Lazy.force v
229 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
230 let from_env v = Lazy.force v
231 let from_ens v = Lazy.force v
232 let from_env_for_unwind ~unwind v = Lazy.force v
233 let from_ens_for_unwind ~unwind v = Lazy.force v
234 let stack_to_env ~reduce ~unwind v = v
235 let compute_to_stack ~reduce ~unwind k e ens t =
238 Cic.Const _ as t -> unwind k e ens t
239 | t -> reduce (k,e,ens,t,[]))
240 let compute_to_env ~reduce ~unwind k e ens t =
243 Cic.Const _ as t -> unwind k e ens t
244 | t -> reduce (k,e,ens,t,[]))
248 module LazyCallByNameStrategy =
250 type stack_term = Cic.term lazy_t
251 type env_term = Cic.term lazy_t
252 type ens_term = Cic.term lazy_t
253 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
254 let to_env v = lazy v
255 let to_ens v = lazy v
256 let from_stack ~unwind v = Lazy.force v
257 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
258 let from_env v = Lazy.force v
259 let from_ens v = Lazy.force v
260 let from_env_for_unwind ~unwind v = Lazy.force v
261 let from_ens_for_unwind ~unwind v = Lazy.force v
262 let stack_to_env ~reduce ~unwind v = v
263 let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
264 let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
269 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
272 type stack_term = reduce:bool -> Cic.term
273 type env_term = reduce:bool -> Cic.term
274 type ens_term = reduce:bool -> Cic.term
275 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
277 let value = lazy v in
278 fun ~reduce -> Lazy.force value
280 let value = lazy v in
281 fun ~reduce -> Lazy.force value
282 let from_stack ~unwind v = (v ~reduce:false)
283 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
284 let from_env v = (v ~reduce:true)
285 let from_ens v = (v ~reduce:true)
286 let from_env_for_unwind ~unwind v = (v ~reduce:true)
287 let from_ens_for_unwind ~unwind v = (v ~reduce:true)
288 let stack_to_env ~reduce ~unwind v = v
289 let compute_to_stack ~reduce ~unwind k e ens t =
293 Cic.Const _ as t -> unwind k e ens t
294 | t -> reduce (k,e,ens,t,[])
297 lazy (unwind k e ens t)
300 if reduce then Lazy.force svalue else Lazy.force lvalue
301 let compute_to_env ~reduce ~unwind k e ens t =
305 Cic.Const _ as t -> unwind k e ens t
306 | t -> reduce (k,e,ens,t,[])
309 lazy (unwind k e ens t)
312 if reduce then Lazy.force svalue else Lazy.force lvalue
316 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
318 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
319 and stack_term = config
320 and env_term = config
321 and ens_term = config
323 let to_env config = config
324 let to_ens config = config
325 let from_stack config = config
326 let from_stack_list_for_unwind ~unwind l = List.map unwind l
329 let from_env_for_unwind ~unwind config = unwind config
330 let from_ens_for_unwind ~unwind config = unwind config
331 let stack_to_env ~reduce ~unwind config = reduce config
332 let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
333 let compute_to_stack ~reduce ~unwind config = config
337 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
340 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
341 type env_term = Cic.term
342 type ens_term = Cic.term
343 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
346 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
347 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
350 let from_env_for_unwind ~unwind v = v
351 let from_ens_for_unwind ~unwind v = v
352 let stack_to_env ~reduce ~unwind (k,e,ens,t) =
354 Cic.Const _ as t -> unwind k e ens t
355 | t -> reduce (k,e,ens,t,[])
356 let compute_to_env ~reduce ~unwind k e ens t =
358 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
364 module Reduction(RS : Strategy) =
366 type env = RS.env_term list
367 type stack = RS.stack_term list
368 type config = int * env * NCic.term * stack
370 let rec unwind (k,e,t,s) =
374 NCicSubstitution.psubst ~avoid_beta_redexes:true
375 true 0 (RS.from_env_for_unwind ~unwind) e t
378 else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
381 let list_nth l n = try List.nth l n with Failure _ -> assert false;;
382 let rec replace i s t =
385 | n,he::tl -> he::(replace (n - 1) tl t)
386 | _,_ -> assert false
389 let rec reduce ~delta ?(subst = []) context : config -> config =
390 let rec aux = function
391 | k, e, NCic.Rel n, s when n <= k ->
392 let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
394 | k, _, NCic.Rel n, s as config (* when n > k *) ->
395 (match List.nth context (n - 1 - k) with
396 | (_,NCic.Decl _) -> config
397 | (_,NCic.Def (x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s))
398 | (k, e, NCic.Meta (n,l), s) as config ->
400 let _,_, term,_ = NCicUtils.lookup_subst n subst in
401 aux (k, e, NCicSubstitution.subst_meta l term,s)
402 with NCicUtils.Subst_not_found _ -> config)
403 | (_, _, NCic.Sort _, _) as config -> config
404 | (_, _, NCic.Implicit _, _) -> assert false
405 | (_, _, NCic.Prod _, _) as config -> config
406 | (_, _, NCic.Lambda _, []) as config -> config
407 | (k, e, NCic.Lambda (_,_,t), p::s) ->
408 aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
409 | (k, e, NCic.LetIn (_,_,m,t), s) ->
410 let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
411 aux (k+1, m'::e, t, s)
412 | (_, _, NCic.Appl [], _) -> assert false
413 | (k, e, NCic.Appl (he::tl), s) ->
415 List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
417 aux (k, e, he, tl' @ s)
419 (NReference.Ref (_,_,NReference.Def) as refer), s) as config ->
420 let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
421 if delta >= height then config else aux (0, [], body, s)
422 | (_, _, NCic.Const (NReference.Ref
423 (_,_,NReference.Fix (_,recindex)) as refer),s) as config ->
424 let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in
425 if delta >= height then config else
427 try Some (RS.from_stack (List.nth s recindex))
428 with Failure _ -> None
432 match reduce ~delta:0 ~subst context recparam with
433 | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
435 replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
437 aux (0, [], body, new_s)
439 | (_, _, NCic.Const _, _) as config -> config
440 | (k, e, NCic.Match (_,_,term,pl),s) as config ->
441 let decofix = function
442 | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix _)as refer),s)->
443 let _,_,body,_,_,_ = NCicEnvironment.get_checked_cofix refer in
444 reduce ~delta:0 ~subst context (0,[],body,s)
447 (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
448 | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) ->
449 aux (k, e, List.nth pl (j-1), s)
451 (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') ->
452 let leftno = NCicEnvironment.get_indty_leftno refer in
453 let _,params = HExtlib.split_nth leftno s' in
454 aux (k, e, List.nth pl (j-1), params@s)
460 let whd ?(delta=0) ?(subst=[]) context t =
461 unwind (reduce ~delta ~subst context (0, [], t, []))
468 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
469 senza ridurre la testa
470 module R = Reduction CallByNameStrategy;; OK 56.368s
471 module R = Reduction CallByValueStrategy;; ROTTO
472 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
473 module R = Reduction LazyCallByValueStrategy;; ROTTO
474 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
475 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
477 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
479 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
481 ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
482 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
483 module R = Reduction(CallByValueByNameForUnwind);;
484 module R = Reduction(CallByNameStrategy);;
485 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
486 module RS = CallByValueByNameForUnwind';;
488 module R = Reduction(RS);;
489 module U = UriManager;;
495 let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
496 fun ?(delta=true) ?(subst=[]) context t ->
497 profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
502 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
503 * fallbacks to structural equality *)
504 let (===) x y = Pervasives.compare x y = 0 ;;
508 (* t1, t2 must be well-typed *)
509 let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
510 let heuristic = ref true in
511 let rec aux test_equality_only context t1 t2 =
512 let rec aux2 test_equality_only t1 t2 =
517 | (C.Rel n1, C.Rel n2) -> n1 = n2
519 | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
520 | (C.Sort (C.Type a), C.Sort (C.Type b)) when test_equality_only -> a=b
521 | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
522 | (C.Sort s1, C.Sort s2) -> s1 = s2
524 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
525 aux true context s1 s2 &&
526 aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
527 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
528 aux test_equality_only context s1 s2 && (* sure?! *)
529 aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
531 | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
534 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
535 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
537 (fun (b,ugraph) t1 t2 ->
541 | _,None -> true,ugraph
542 | Some t1',Some t2' ->
543 aux test_equality_only context t1' t2' ugraph
546 ) (true,ugraph) l1 l2
548 if b2 then true,ugraph1 else false,ugraph
551 | C.Meta (n1,l1), _ ->
553 let _,term,_ = NCicUtils.lookup_subst n1 subst in
554 let term' = CicSubstitution.subst_meta l1 term in
555 aux test_equality_only context term' t2 ugraph
556 with CicUtil.Subst_not_found _ -> false,ugraph)
557 | _, C.Meta (n2,l2) ->
559 let _,term,_ = CicUtil.lookup_subst n2 subst in
560 let term' = CicSubstitution.subst_meta l2 term in
561 aux test_equality_only context t1 term' ugraph
562 with CicUtil.Subst_not_found _ -> false,ugraph)
563 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
564 let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
566 aux test_equality_only
567 ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
570 | (C.Appl l1, C.Appl l2) ->
573 (fun x y (b,ugraph) ->
575 aux test_equality_only context x y ugraph
577 false,ugraph) l1 l2 (true,ugraph)
579 Invalid_argument _ -> false,ugraph
581 | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
582 let b' = U.eq uri1 uri2 in
586 (fun (uri1,x) (uri2,y) (b,ugraph) ->
587 if b && U.eq uri1 uri2 then
588 aux test_equality_only context x y ugraph
591 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
593 Invalid_argument _ -> false,ugraph
597 | (C.MutInd (uri1,i1,exp_named_subst1),
598 C.MutInd (uri2,i2,exp_named_subst2)
600 let b' = U.eq uri1 uri2 && i1 = i2 in
604 (fun (uri1,x) (uri2,y) (b,ugraph) ->
605 if b && U.eq uri1 uri2 then
606 aux test_equality_only context x y ugraph
609 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
611 Invalid_argument _ -> false,ugraph
615 | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
616 C.MutConstruct (uri2,i2,j2,exp_named_subst2)
618 let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
622 (fun (uri1,x) (uri2,y) (b,ugraph) ->
623 if b && U.eq uri1 uri2 then
624 aux test_equality_only context x y ugraph
627 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
629 Invalid_argument _ -> false,ugraph
633 | (C.MutCase (uri1,i1,outtype1,term1,pl1),
634 C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
635 let b' = U.eq uri1 uri2 && i1 = i2 in
637 let b'',ugraph''=aux test_equality_only context
638 outtype1 outtype2 ugraph in
640 let b''',ugraph'''= aux test_equality_only context
641 term1 term2 ugraph'' in
643 (fun x y (b,ugraph) ->
645 aux test_equality_only context x y ugraph
648 pl1 pl2 (b''',ugraph''')
653 | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
656 (fun (types,len) (n,_,ty,_) ->
657 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
663 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
664 if b && recindex1 = recindex2 then
665 let b',ugraph' = aux test_equality_only context ty1 ty2
668 aux test_equality_only (tys@context) bo1 bo2 ugraph'
673 fl1 fl2 (true,ugraph)
676 | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
679 (fun (types,len) (n,ty,_) ->
680 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
686 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
688 let b',ugraph' = aux test_equality_only context ty1 ty2
691 aux test_equality_only (tys@context) bo1 bo2 ugraph'
696 fl1 fl2 (true,ugraph)
699 | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
700 | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
701 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
702 | (_,_) -> false,ugraph
706 aux2 test_equality_only t1 t2 ugraph
710 if fst res = true then
714 (*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
715 (* heuristic := false; *)
716 debug t1 [t2] "PREWHD";
717 (*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
719 prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
720 let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
721 let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
722 debug t1' [t2'] "POSTWHD";
724 let rec convert_machines ugraph =
727 | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
728 let (b,ugraph) as res =
729 aux2 test_equality_only
730 (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
738 (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
741 (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
745 Invalid_argument _ -> None
749 | Some problems -> convert_machines ugraph problems
753 convert_machines ugraph
754 [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
755 R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
756 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
758 aux2 test_equality_only t1' t2' ugraph
762 aux false (*c t1 t2 ugraph *)
766 (* {{{ DEBUGGING ONLY
767 let whd ?(delta=true) ?(subst=[]) context t =
768 let res = whd ~delta ~subst context t in
769 let rescsc = CicReductionNaif.whd ~delta ~subst context t in
770 if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
772 debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
774 debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
776 debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
779 let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
787 (*let are_convertible = are_convertible whd*)
789 (* {{{ let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
790 let whd ?(delta=true) ?(subst=[]) context t =
792 whd ~delta ~subst context t
794 profiler_other_whd.HExtlib.profile foo ()
797 (* {{{ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
798 let module C = Cic in
799 let t = whd ~delta ~subst ctx term in
800 let aux = normalize ~delta ~subst in
801 let decl name t = Some (name, C.Decl t) in
804 | C.Var (uri,exp_named_subst) ->
805 C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
807 C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
810 | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
812 let s' = aux ctx s in
813 C.Prod (n, s', aux ((decl n s')::ctx) t)
814 | C.Lambda (n,s,t) ->
815 let s' = aux ctx s in
816 C.Lambda (n, s', aux ((decl n s')::ctx) t)
818 (* the term is already in weak head normal form *)
820 | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
821 | C.Appl [] -> assert false
822 | C.Const (uri,exp_named_subst) ->
823 C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
824 | C.MutInd (uri,typeno,exp_named_subst) ->
825 C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
826 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
827 C.MutConstruct (uri, typeno, consno,
828 List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
829 | C.MutCase (sp,i,outt,t,pl) ->
830 C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
831 (*CSC: to be completed, I suppose *)
835 let normalize ?delta ?subst ctx term =
836 (* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
837 let t = normalize ?delta ?subst ctx term in
838 (* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
842 (* {{{ performs an head beta/cast reduction
843 let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
848 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
849 let he'' = CicSubstitution.subst he' t in
855 Cic.Appl l -> Cic.Appl (l@tl')
856 | _ -> Cic.Appl (he''::tl')
858 head_beta_reduce ~delta ~upto:(upto - 1) he'''
859 | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te
860 | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
862 match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
863 Cic.Constant (_,bo,_,_,_) -> bo
864 | Cic.Variable _ -> raise ReferenceToVariable
865 | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
866 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
871 head_beta_reduce ~upto
872 ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
873 | Cic.Const (uri,ens) as t when delta=true ->
875 match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
876 Cic.Constant (_,bo,_,_,_) -> bo
877 | Cic.Variable _ -> raise ReferenceToVariable
878 | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
879 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
884 head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
889 let are_convertible ?subst ?metasenv context t1 t2 ugraph =
890 let before = Unix.gettimeofday () in
891 let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
892 let after = Unix.gettimeofday () in
893 let diff = after -. before in
896 let nc = List.map (function None -> None | Some (n,_) -> Some n) context in
898 ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
903 (* vim:set foldmethod=marker: *)