2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 (* TODO unify exceptions *)
16 module type Strategy =
20 type config = int * env_term list * NCic.term * stack_term list
22 reduce: (config -> config) ->
23 unwind: (config -> NCic.term) ->
25 val from_stack : stack_term -> config
26 val from_stack_list_for_unwind :
27 unwind: (config -> NCic.term) ->
28 stack_term list -> NCic.term list
29 val from_env : env_term -> config
30 val from_env_for_unwind :
31 unwind: (config -> NCic.term) ->
34 reduce: (config -> config) ->
35 unwind: (config -> NCic.term) ->
36 stack_term -> env_term
38 reduce: (config -> config) ->
39 unwind: (config -> NCic.term) ->
40 int -> env_term list ->
42 val compute_to_stack :
43 reduce: (config -> config) ->
44 unwind: (config -> NCic.term) ->
49 module CallByValueByNameForUnwind' =
51 type config = int * env_term list * NCic.term * stack_term list
52 and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
53 and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
54 let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
55 let from_stack (c,_) = Lazy.force c
56 let from_stack_list_for_unwind ~unwind:_ l =
57 List.map (function (_,c) -> Lazy.force c) l
58 let from_env (c,_) = Lazy.force c
59 let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c
60 let stack_to_env ~reduce:_ ~unwind:_ config = config
61 let compute_to_env ~reduce ~unwind k e t =
62 lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[]))
63 let compute_to_stack ~reduce ~unwind config =
64 lazy (reduce config), lazy (unwind config)
69 (* {{{ module CallByValueByNameForUnwind =
71 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
72 and stack_term = config
73 and env_term = config * config (* cbv, cbn *)
74 and ens_term = config * config (* cbv, cbn *)
78 let from_stack config = config
79 let from_stack_list_for_unwind ~unwind l = List.map unwind l
80 let from_env (c,_) = c
81 let from_ens (c,_) = c
82 let from_env_for_unwind ~unwind (_,c) = unwind c
83 let from_ens_for_unwind ~unwind (_,c) = unwind c
84 let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
85 let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
86 let compute_to_stack ~reduce ~unwind config = config
92 module CallByNameStrategy =
94 type stack_term = Cic.term
95 type env_term = Cic.term
96 type ens_term = Cic.term
97 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
100 let from_stack ~unwind v = v
101 let from_stack_list ~unwind l = l
104 let from_env_for_unwind ~unwind v = v
105 let from_ens_for_unwind ~unwind v = v
106 let stack_to_env ~reduce ~unwind v = v
107 let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
108 let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
112 module CallByNameStrategy =
114 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
115 and stack_term = config
116 and env_term = config
117 and ens_term = config
121 let from_stack config = config
122 let from_stack_list_for_unwind ~unwind l = List.map unwind l
125 let from_env_for_unwind ~unwind c = unwind c
126 let from_ens_for_unwind ~unwind c = unwind c
127 let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
128 let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
129 let compute_to_stack ~reduce ~unwind config = config
133 module CallByValueStrategy =
135 type stack_term = Cic.term
136 type env_term = Cic.term
137 type ens_term = Cic.term
138 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
141 let from_stack ~unwind v = v
142 let from_stack_list ~unwind l = l
145 let from_env_for_unwind ~unwind v = v
146 let from_ens_for_unwind ~unwind v = v
147 let stack_to_env ~reduce ~unwind v = v
148 let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
149 let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
153 module CallByValueStrategyByNameOnConstants =
155 type stack_term = Cic.term
156 type env_term = Cic.term
157 type ens_term = Cic.term
158 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
161 let from_stack ~unwind v = v
162 let from_stack_list ~unwind l = l
165 let from_env_for_unwind ~unwind v = v
166 let from_ens_for_unwind ~unwind v = v
167 let stack_to_env ~reduce ~unwind v = v
168 let compute_to_stack ~reduce ~unwind k e ens =
170 Cic.Const _ as t -> unwind k e ens t
171 | t -> reduce (k,e,ens,t,[])
172 let compute_to_env ~reduce ~unwind k e ens =
174 Cic.Const _ as t -> unwind k e ens t
175 | t -> reduce (k,e,ens,t,[])
179 module LazyCallByValueStrategy =
181 type stack_term = Cic.term lazy_t
182 type env_term = Cic.term lazy_t
183 type ens_term = Cic.term lazy_t
184 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
185 let to_env v = lazy v
186 let to_ens v = lazy v
187 let from_stack ~unwind v = Lazy.force v
188 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
189 let from_env v = Lazy.force v
190 let from_ens v = Lazy.force v
191 let from_env_for_unwind ~unwind v = Lazy.force v
192 let from_ens_for_unwind ~unwind v = Lazy.force v
193 let stack_to_env ~reduce ~unwind v = v
194 let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
195 let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
199 module LazyCallByValueStrategyByNameOnConstants =
201 type stack_term = Cic.term lazy_t
202 type env_term = Cic.term lazy_t
203 type ens_term = Cic.term lazy_t
204 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
205 let to_env v = lazy v
206 let to_ens v = lazy v
207 let from_stack ~unwind v = Lazy.force v
208 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
209 let from_env v = Lazy.force v
210 let from_ens v = Lazy.force v
211 let from_env_for_unwind ~unwind v = Lazy.force v
212 let from_ens_for_unwind ~unwind v = Lazy.force v
213 let stack_to_env ~reduce ~unwind v = v
214 let compute_to_stack ~reduce ~unwind k e ens t =
217 Cic.Const _ as t -> unwind k e ens t
218 | t -> reduce (k,e,ens,t,[]))
219 let compute_to_env ~reduce ~unwind k e ens t =
222 Cic.Const _ as t -> unwind k e ens t
223 | t -> reduce (k,e,ens,t,[]))
227 module LazyCallByNameStrategy =
229 type stack_term = Cic.term lazy_t
230 type env_term = Cic.term lazy_t
231 type ens_term = Cic.term lazy_t
232 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
233 let to_env v = lazy v
234 let to_ens v = lazy v
235 let from_stack ~unwind v = Lazy.force v
236 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
237 let from_env v = Lazy.force v
238 let from_ens v = Lazy.force v
239 let from_env_for_unwind ~unwind v = Lazy.force v
240 let from_ens_for_unwind ~unwind v = Lazy.force v
241 let stack_to_env ~reduce ~unwind v = v
242 let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
243 let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
248 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
251 type stack_term = reduce:bool -> Cic.term
252 type env_term = reduce:bool -> Cic.term
253 type ens_term = reduce:bool -> Cic.term
254 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
256 let value = lazy v in
257 fun ~reduce -> Lazy.force value
259 let value = lazy v in
260 fun ~reduce -> Lazy.force value
261 let from_stack ~unwind v = (v ~reduce:false)
262 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
263 let from_env v = (v ~reduce:true)
264 let from_ens v = (v ~reduce:true)
265 let from_env_for_unwind ~unwind v = (v ~reduce:true)
266 let from_ens_for_unwind ~unwind v = (v ~reduce:true)
267 let stack_to_env ~reduce ~unwind v = v
268 let compute_to_stack ~reduce ~unwind k e ens t =
272 Cic.Const _ as t -> unwind k e ens t
273 | t -> reduce (k,e,ens,t,[])
276 lazy (unwind k e ens t)
279 if reduce then Lazy.force svalue else Lazy.force lvalue
280 let compute_to_env ~reduce ~unwind k e ens t =
284 Cic.Const _ as t -> unwind k e ens t
285 | t -> reduce (k,e,ens,t,[])
288 lazy (unwind k e ens t)
291 if reduce then Lazy.force svalue else Lazy.force lvalue
295 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
297 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
298 and stack_term = config
299 and env_term = config
300 and ens_term = config
302 let to_env config = config
303 let to_ens config = config
304 let from_stack config = config
305 let from_stack_list_for_unwind ~unwind l = List.map unwind l
308 let from_env_for_unwind ~unwind config = unwind config
309 let from_ens_for_unwind ~unwind config = unwind config
310 let stack_to_env ~reduce ~unwind config = reduce config
311 let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
312 let compute_to_stack ~reduce ~unwind config = config
316 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
319 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
320 type env_term = Cic.term
321 type ens_term = Cic.term
322 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
325 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
326 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
329 let from_env_for_unwind ~unwind v = v
330 let from_ens_for_unwind ~unwind v = v
331 let stack_to_env ~reduce ~unwind (k,e,ens,t) =
333 Cic.Const _ as t -> unwind k e ens t
334 | t -> reduce (k,e,ens,t,[])
335 let compute_to_env ~reduce ~unwind k e ens t =
337 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
343 module Reduction(RS : Strategy) =
345 type env = RS.env_term list
346 type stack = RS.stack_term list
347 type config = int * env * NCic.term * stack
349 let rec unwind (k,e,t,s) =
353 NCicSubstitution.psubst ~avoid_beta_redexes:true
354 (RS.from_env_for_unwind ~unwind) e t
357 else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
360 let list_nth l n = try List.nth l n with Failure _ -> assert false;;
361 let rec replace i s t =
364 | n,he::tl -> he::(replace (n - 1) tl t)
365 | _,_ -> assert false
368 let rec reduce ~delta ?(subst = []) context : config -> config =
369 let rec aux = function
370 | k, e, NCic.Rel n, s when n <= k ->
371 let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
373 | k, _, NCic.Rel n, s as config (* when n > k *) ->
374 let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
376 | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
378 | (k, e, NCic.Meta (n,l), s) as config ->
380 let _,_, term,_ = NCicUtils.lookup_subst n subst in
381 aux (k, e, NCicSubstitution.subst_meta l term,s)
382 with NCicUtils.Subst_not_found _ -> config)
383 | (_, _, NCic.Sort _, _) as config -> config
384 | (_, _, NCic.Implicit _, _) -> assert false
385 | (_, _, NCic.Prod _, _) as config -> config
386 | (_, _, NCic.Lambda _, []) as config -> config
387 | (k, e, NCic.Lambda (_,_,t), p::s) ->
388 aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
389 | (k, e, NCic.LetIn (_,_,m,t), s) ->
390 let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
391 aux (k+1, m'::e, t, s)
392 | (_, _, NCic.Appl [], _) -> assert false
393 | (k, e, NCic.Appl (he::tl), s) ->
395 List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
397 aux (k, e, he, tl' @ s)
399 (NReference.Ref (_,NReference.Def height) as refer), s) as config ->
400 if delta >= height then config else
401 let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
403 | (_, _, NCic.Const (NReference.Ref (_,
404 (NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config
405 | (_, _, NCic.Const (NReference.Ref
406 (_,NReference.Fix (fixno,recindex,height)) as refer),s) as config ->
407 if delta >= height then config else
409 try Some (RS.from_stack (List.nth s recindex))
410 with Failure _ -> None
414 let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
415 match reduce ~delta:0 ~subst context recparam with
416 | (_,_,NCic.Const (NReference.Ref (_,NReference.Con _)), _) as c ->
418 replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
420 let _,_,_,_,body = List.nth fixes fixno in
421 aux (0, [], body, new_s)
423 | (k, e, NCic.Match (_,_,term,pl),s) as config ->
424 let decofix = function
425 | (_,_,NCic.Const(NReference.Ref(_,NReference.CoFix c)as refer),s)->
426 let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
427 let _,_,_,_,body = List.nth cofixes c in
428 reduce ~delta:0 ~subst context (0,[],body,s)
431 (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
432 | (_, _, NCic.Const (NReference.Ref (_,NReference.Con (_,j))),[]) ->
433 aux (k, e, List.nth pl (j-1), s)
435 (NReference.Ref (_,NReference.Con (_,j)) as refer), s') ->
436 let leftno = NCicEnvironment.get_indty_leftno refer in
437 let _,params = HExtlib.split_nth leftno s' in
438 aux (k, e, List.nth pl (j-1), params@s)
444 let whd ?(delta=0) ?(subst=[]) context t =
445 unwind (reduce ~delta ~subst context (0, [], t, []))
452 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
453 senza ridurre la testa
454 module R = Reduction CallByNameStrategy;; OK 56.368s
455 module R = Reduction CallByValueStrategy;; ROTTO
456 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
457 module R = Reduction LazyCallByValueStrategy;; ROTTO
458 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
459 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
461 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
463 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
465 ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
466 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
467 module R = Reduction(CallByValueByNameForUnwind);;
468 module R = Reduction(CallByNameStrategy);;
469 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
470 module RS = CallByValueByNameForUnwind';;
472 module R = Reduction(RS);;
473 module U = UriManager;;
479 let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
480 fun ?(delta=true) ?(subst=[]) context t ->
481 profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
484 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
485 * fallbacks to structural equality *)
486 let (===) x y = Pervasives.compare x y = 0 ;;
490 (* t1, t2 must be well-typed *)
491 let are_convertible whd ?(subst=[]) =
492 let rec aux test_eq_only context t1 t2 =
493 let rec alpha_eq test_eq_only t1 t2 =
498 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
499 NCicEnvironment.universe_leq a b
500 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
501 NCicEnvironment.universe_eq a b
502 | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only)
503 | (C.Sort s1, C.Sort s2) -> s1 = s2
505 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
506 aux true context s1 s2 &&
507 aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
508 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
509 aux true context s1 s2 &&
510 aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
511 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
512 aux test_eq_only context ty1 ty2 &&
513 aux test_eq_only context s1 s2 &&
514 aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2
516 | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2)))
517 when n1 = n2 && s1 = s2 -> true
518 | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 &&
519 let l1 = NCicUtils.expand_local_context l1 in
520 let l2 = NCicUtils.expand_local_context l2 in
522 (fun t1 t2 -> aux test_eq_only context
523 (NCicSubstitution.lift s1 t1)
524 (NCicSubstitution.lift s2 t2))
526 with Invalid_argument _ -> assert false) -> true
528 | C.Meta (n1,l1), _ ->
530 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
531 let term = NCicSubstitution.subst_meta l1 term in
532 aux test_eq_only context term t2
533 with NCicUtils.Subst_not_found _ -> false)
534 | _, C.Meta (n2,l2) ->
536 let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
537 let term = NCicSubstitution.subst_meta l2 term in
538 aux test_eq_only context t1 term
539 with NCicUtils.Subst_not_found _ -> false)
541 | (C.Appl (C.Const r1::tl1), C.Appl (C.Const r2::tl2)) ->
543 let relevance = NCicEnvironment.get_relevance r1 in
545 HExtlib.list_forall_default3
546 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
547 tl1 tl2 true relevance
548 with Invalid_argument _ -> false)
550 | (C.Appl l1, C.Appl l2) ->
551 (try List.for_all2 (aux test_eq_only context) l1 l2
552 with Invalid_argument _ -> false)
554 | (C.Match (ref1,outtype1,term1,pl1),
555 C.Match (ref2,outtype2,term2,pl2)) ->
556 NReference.eq ref1 ref2 &&
557 aux test_eq_only context outtype1 outtype2 &&
558 aux test_eq_only context term1 term2 &&
559 (try List.for_all2 (aux test_eq_only context) pl1 pl2
560 with Invalid_argument _ -> false)
562 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
565 if alpha_eq test_eq_only t1 t2 then
568 let height_of = function
569 | NCic.Const (NReference.Ref (_,NReference.Def h))
570 | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h)))
571 | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_)
572 | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
575 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
576 let h1 = height_of t1 in
577 let h2 = height_of t2 in
578 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
579 R.reduce ~delta ~subst context m1,
580 R.reduce ~delta ~subst context m2,
583 let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
584 (alpha_eq test_eq_only
585 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
588 C.Const r -> NCicEnvironment.get_relevance r
591 HExtlib.list_forall_default3
594 let t1 = RS.from_stack t1 in
595 let t2 = RS.from_stack t2 in
596 convert_machines (small_delta_step t1 t2)) s1 s2 true relevance
597 with Invalid_argument _ -> false) ||
599 let delta = delta - 1 in
600 let red = R.reduce ~delta ~subst context in
601 convert_machines (red m1,red m2,delta))
603 convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
608 let are_convertible = are_convertible whd
610 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
611 match upto, t, l with
612 | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
614 | 0, t, _ -> C.Appl (t::l)
615 | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
616 | _, C.Lambda(_,_,bo), arg::tl ->
617 let bo = NCicSubstitution.subst arg bo in
618 head_beta_reduce ~delta ~upto:(upto - 1) bo tl
619 | _, C.Const (NReference.Ref (_, NReference.Def height) as re), _
620 when delta <= height ->
621 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
622 head_beta_reduce ~upto ~delta bo l
624 | _, t, _ -> C.Appl (t::l)
627 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
629 (* vim:set foldmethod=marker: *)