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 true 0 (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)) -> a <= b
499 | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only)
500 | (C.Sort s1, C.Sort s2) -> s1 = s2
502 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
503 aux true context s1 s2 &&
504 aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
505 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
506 aux true context s1 s2 &&
507 aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
508 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
509 aux test_eq_only context ty1 ty2 &&
510 aux test_eq_only context s1 s2 &&
511 aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2
513 | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2)))
514 when n1 = n2 && s1 = s2 -> true
515 | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 ->
516 let l1 = NCicUtils.expand_local_context l1 in
517 let l2 = NCicUtils.expand_local_context l2 in
519 (fun t1 t2 -> aux test_eq_only context
520 (NCicSubstitution.lift s1 t1)
521 (NCicSubstitution.lift s2 t2))
523 with Invalid_argument _ -> assert false)
525 | C.Meta (n1,l1), _ ->
527 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
528 let term = NCicSubstitution.subst_meta l1 term in
529 aux test_eq_only context term t2
530 with NCicUtils.Subst_not_found _ -> false)
531 | _, C.Meta (n2,l2) ->
533 let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
534 let term = NCicSubstitution.subst_meta l2 term in
535 aux test_eq_only context t1 term
536 with NCicUtils.Subst_not_found _ -> false)
538 | (C.Appl l1, C.Appl l2) ->
539 (try List.for_all2 (aux test_eq_only context) l1 l2
540 with Invalid_argument _ -> false)
542 | (C.Match (ref1,outtype1,term1,pl1),
543 C.Match (ref2,outtype2,term2,pl2)) ->
544 NReference.eq ref1 ref2 &&
545 aux test_eq_only context outtype1 outtype2 &&
546 aux test_eq_only context term1 term2 &&
547 (try List.for_all2 (aux test_eq_only context) pl1 pl2
548 with Invalid_argument _ -> false)
550 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
553 if alpha_eq test_eq_only t1 t2 then
556 let height_of = function
557 | NCic.Const (NReference.Ref (_,NReference.Def h)) -> h
558 | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h))) -> h
559 | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_) -> h
560 | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
563 let small_delta_step (k1,env1,t1,s1 as m1) (k2,env2,t2,s2 as m2) =
564 let h1 = height_of t1 and h2 = height_of t2 in
566 R.reduce ~delta:h2 ~subst context (k1,env1,t1,s1), m2, h2
568 m1, R.reduce ~delta:h1 ~subst context (k2,env2,t2,s2), h1
570 let delta = max 0 (h1-1) in
571 R.reduce ~delta ~subst context (k1,env1,t1,s1),
572 R.reduce ~delta ~subst context (k2,env2,t2,s2),
575 let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
576 (alpha_eq test_eq_only
577 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
581 let t1 = RS.from_stack t1 and t2 = RS.from_stack t2 in
582 convert_machines (small_delta_step t1 t2))
584 with Invalid_argument _ -> false) ||
585 (let red delta = R.reduce ~delta ~subst context in
587 alpha_eq test_eq_only (R.unwind (red 0 m1)) (R.unwind (red 0 m2))
589 let delta = delta - 1 in
590 convert_machines (red delta m1,red delta m2,delta))
592 convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
597 let are_convertible = are_convertible whd
599 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
600 match upto, t, l with
601 | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
603 | 0, t, _ -> C.Appl (t::l)
604 | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
605 | _, C.Lambda(_,_,bo), arg::tl ->
606 let bo = NCicSubstitution.subst arg bo in
607 head_beta_reduce ~delta ~upto:(upto - 1) bo tl
608 | _, C.Const (NReference.Ref (_, NReference.Def height) as re), _
609 when delta <= height ->
610 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
611 head_beta_reduce ~upto ~delta bo l
613 | _, t, _ -> C.Appl (t::l)
616 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
618 (* vim:set foldmethod=marker: *)