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) as refer), s) as config ->
400 let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
401 if delta > height then config else aux (0, [], body, s)
402 | (_, _, NCic.Const (NReference.Ref
403 (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
404 let fixes,_, height = NCicEnvironment.get_checked_fixes_or_cofixes refer in
405 if delta > height then config else
407 try Some (RS.from_stack (List.nth s recindex))
408 with Failure _ -> None
412 match reduce ~delta:0 ~subst context recparam with
413 | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
415 replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
417 let _,_,_,_,body = List.nth fixes fixno in
418 aux (0, [], body, new_s)
420 | (_, _, NCic.Const _, _) as config -> config
421 | (k, e, NCic.Match (_,_,term,pl),s) as config ->
422 let decofix = function
423 | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
424 let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
425 let _,_,_,_,body = List.nth cofixes c in
426 reduce ~delta:0 ~subst context (0,[],body,s)
429 (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
430 | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) ->
431 aux (k, e, List.nth pl (j-1), s)
433 (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') ->
434 let leftno = NCicEnvironment.get_indty_leftno refer in
435 let _,params = HExtlib.split_nth leftno s' in
436 aux (k, e, List.nth pl (j-1), params@s)
442 let whd ?(delta=0) ?(subst=[]) context t =
443 unwind (reduce ~delta ~subst context (0, [], t, []))
450 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
451 senza ridurre la testa
452 module R = Reduction CallByNameStrategy;; OK 56.368s
453 module R = Reduction CallByValueStrategy;; ROTTO
454 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
455 module R = Reduction LazyCallByValueStrategy;; ROTTO
456 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
457 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
459 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
461 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
463 ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
464 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
465 module R = Reduction(CallByValueByNameForUnwind);;
466 module R = Reduction(CallByNameStrategy);;
467 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
468 module RS = CallByValueByNameForUnwind';;
470 module R = Reduction(RS);;
471 module U = UriManager;;
477 let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
478 fun ?(delta=true) ?(subst=[]) context t ->
479 profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
482 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
483 * fallbacks to structural equality *)
484 let (===) x y = Pervasives.compare x y = 0 ;;
488 (* t1, t2 must be well-typed *)
489 let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
490 let rec aux test_equality_only context t1 t2 =
491 let rec aux2 test_equality_only t1 t2 =
496 | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
497 | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
498 | (C.Sort s1, C.Sort s2) -> s1 = s2
500 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
501 aux true context s1 s2 &&
502 aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
503 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
504 aux true context s1 s2 &&
505 aux true ((name1, C.Decl s1)::context) t1 t2
506 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
507 aux test_equality_only context ty1 ty2 &&
508 aux test_equality_only context s1 s2 &&
509 aux test_equality_only ((name1, C.Def (s1,ty1))::context) t1 t2
511 | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2)))
512 when n1 = n2 && s1 = s2 -> true
513 | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 ->
514 let l1 = NCicUtils.expand_local_context l1 in
515 let l2 = NCicUtils.expand_local_context l2 in
517 (fun t1 t2 -> aux test_equality_only context
518 (NCicSubstitution.lift s1 t1)
519 (NCicSubstitution.lift s2 t2))
521 with Invalid_argument _ -> false)
523 | C.Meta (n1,l1), _ ->
525 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
526 let term = NCicSubstitution.subst_meta l1 term in
527 aux test_equality_only context term t2
528 with NCicUtils.Subst_not_found _ -> false)
529 | _, C.Meta (n2,l2) ->
531 let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
532 let term = NCicSubstitution.subst_meta l2 term in
533 aux test_equality_only context t1 term
534 with NCicUtils.Subst_not_found _ -> false)
536 | (C.Appl l1, C.Appl l2) ->
537 (try List.for_all2 (aux test_equality_only context) l1 l2
538 with Invalid_argument _ -> false)
540 | (C.Match (ref1,outtype1,term1,pl1),
541 C.Match (ref2,outtype2,term2,pl2)) ->
542 NReference.eq ref1 ref2 &&
543 aux test_equality_only context outtype1 outtype2 &&
544 aux test_equality_only context term1 term2 &&
545 (try List.for_all2 (aux test_equality_only context) pl1 pl2
546 with Invalid_argument _ -> false)
548 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
551 if aux2 test_equality_only t1 t2 then
554 let rec convert_machines = function
556 | ((k1,env1,h1,s1),(k2,env2,h2,s2))::tl ->
557 aux2 test_equality_only
558 (R.unwind (k1,env1,h1,[])) (R.unwind (k2,env2,h2,[])) &&
562 (fun si-> R.reduce ~delta:0 ~subst context(RS.from_stack si))
564 try Some (List.combine (red_stack s1) (red_stack s2) @ tl)
565 with Invalid_argument _ -> None
569 | Some problems -> convert_machines problems
572 [R.reduce ~delta:0 ~subst context (0,[],t1,[]),
573 R.reduce ~delta:0 ~subst context (0,[],t2,[])]
578 let are_convertible = are_convertible whd
580 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
581 match upto, t, l with
582 | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
584 | 0, t, _ -> C.Appl (t::l)
585 | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
586 | _, C.Lambda(_,_,bo), arg::tl ->
587 let bo = NCicSubstitution.subst arg bo in
588 head_beta_reduce ~delta ~upto:(upto - 1) bo tl
589 | _, C.Const (NReference.Ref (height, _, NReference.Def) as re), _
590 when delta <= height ->
591 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
592 head_beta_reduce ~upto ~delta bo l
594 | _, t, _ -> C.Appl (t::l)
597 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
599 (* vim:set foldmethod=marker: *)