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 exception WrongUriToInductiveDefinition;;
17 exception Impossible of int;;
18 exception ReferenceToConstant;;
19 exception ReferenceToVariable;;
20 exception ReferenceToCurrentProof;;
21 exception ReferenceToInductiveDefinition;;
25 let debug_print s = if debug then prerr_endline (Lazy.force s)
29 let rec debug_aux t i =
31 let module U = UriManager in
32 CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
35 debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
38 module type Strategy =
42 type config = int * env_term list * NCic.term * stack_term list
44 reduce: (config -> config) ->
45 unwind: (config -> NCic.term) ->
47 val from_stack : stack_term -> config
48 val from_stack_list_for_unwind :
49 unwind: (config -> NCic.term) ->
50 stack_term list -> NCic.term list
51 val from_env : env_term -> config
52 val from_env_for_unwind :
53 unwind: (config -> NCic.term) ->
56 reduce: (config -> config) ->
57 unwind: (config -> NCic.term) ->
58 stack_term -> env_term
60 reduce: (config -> config) ->
61 unwind: (config -> NCic.term) ->
62 int -> env_term list ->
64 val compute_to_stack :
65 reduce: (config -> config) ->
66 unwind: (config -> NCic.term) ->
71 module CallByValueByNameForUnwind' =
73 type config = int * env_term list * NCic.term * stack_term list
74 and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
75 and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
76 let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
77 let from_stack (c,_) = Lazy.force c
78 let from_stack_list_for_unwind ~unwind:_ l =
79 List.map (function (_,c) -> Lazy.force c) l
80 let from_env (c,_) = Lazy.force c
81 let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c
82 let stack_to_env ~reduce:_ ~unwind:_ config = config
83 let compute_to_env ~reduce ~unwind k e t =
84 lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[]))
85 let compute_to_stack ~reduce ~unwind config =
86 lazy (reduce config), lazy (unwind config)
91 (* {{{ module CallByValueByNameForUnwind =
93 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
94 and stack_term = config
95 and env_term = config * config (* cbv, cbn *)
96 and ens_term = config * config (* cbv, cbn *)
100 let from_stack config = config
101 let from_stack_list_for_unwind ~unwind l = List.map unwind l
102 let from_env (c,_) = c
103 let from_ens (c,_) = c
104 let from_env_for_unwind ~unwind (_,c) = unwind c
105 let from_ens_for_unwind ~unwind (_,c) = unwind c
106 let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
107 let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
108 let compute_to_stack ~reduce ~unwind config = config
114 module CallByNameStrategy =
116 type stack_term = Cic.term
117 type env_term = Cic.term
118 type ens_term = Cic.term
119 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
122 let from_stack ~unwind v = v
123 let from_stack_list ~unwind l = l
126 let from_env_for_unwind ~unwind v = v
127 let from_ens_for_unwind ~unwind v = v
128 let stack_to_env ~reduce ~unwind v = v
129 let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
130 let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
134 module CallByNameStrategy =
136 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
137 and stack_term = config
138 and env_term = config
139 and ens_term = config
143 let from_stack config = config
144 let from_stack_list_for_unwind ~unwind l = List.map unwind l
147 let from_env_for_unwind ~unwind c = unwind c
148 let from_ens_for_unwind ~unwind c = unwind c
149 let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
150 let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
151 let compute_to_stack ~reduce ~unwind config = config
155 module CallByValueStrategy =
157 type stack_term = Cic.term
158 type env_term = Cic.term
159 type ens_term = Cic.term
160 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
163 let from_stack ~unwind v = v
164 let from_stack_list ~unwind l = l
167 let from_env_for_unwind ~unwind v = v
168 let from_ens_for_unwind ~unwind v = v
169 let stack_to_env ~reduce ~unwind v = v
170 let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
171 let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
175 module CallByValueStrategyByNameOnConstants =
177 type stack_term = Cic.term
178 type env_term = Cic.term
179 type ens_term = Cic.term
180 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
183 let from_stack ~unwind v = v
184 let from_stack_list ~unwind l = l
187 let from_env_for_unwind ~unwind v = v
188 let from_ens_for_unwind ~unwind v = v
189 let stack_to_env ~reduce ~unwind v = v
190 let compute_to_stack ~reduce ~unwind k e ens =
192 Cic.Const _ as t -> unwind k e ens t
193 | t -> reduce (k,e,ens,t,[])
194 let compute_to_env ~reduce ~unwind k e ens =
196 Cic.Const _ as t -> unwind k e ens t
197 | t -> reduce (k,e,ens,t,[])
201 module LazyCallByValueStrategy =
203 type stack_term = Cic.term lazy_t
204 type env_term = Cic.term lazy_t
205 type ens_term = Cic.term lazy_t
206 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
207 let to_env v = lazy v
208 let to_ens v = lazy v
209 let from_stack ~unwind v = Lazy.force v
210 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
211 let from_env v = Lazy.force v
212 let from_ens v = Lazy.force v
213 let from_env_for_unwind ~unwind v = Lazy.force v
214 let from_ens_for_unwind ~unwind v = Lazy.force v
215 let stack_to_env ~reduce ~unwind v = v
216 let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
217 let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
221 module LazyCallByValueStrategyByNameOnConstants =
223 type stack_term = Cic.term lazy_t
224 type env_term = Cic.term lazy_t
225 type ens_term = Cic.term lazy_t
226 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
227 let to_env v = lazy v
228 let to_ens v = lazy v
229 let from_stack ~unwind v = Lazy.force v
230 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
231 let from_env v = Lazy.force v
232 let from_ens v = Lazy.force v
233 let from_env_for_unwind ~unwind v = Lazy.force v
234 let from_ens_for_unwind ~unwind v = Lazy.force v
235 let stack_to_env ~reduce ~unwind v = v
236 let compute_to_stack ~reduce ~unwind k e ens t =
239 Cic.Const _ as t -> unwind k e ens t
240 | t -> reduce (k,e,ens,t,[]))
241 let compute_to_env ~reduce ~unwind k e ens t =
244 Cic.Const _ as t -> unwind k e ens t
245 | t -> reduce (k,e,ens,t,[]))
249 module LazyCallByNameStrategy =
251 type stack_term = Cic.term lazy_t
252 type env_term = Cic.term lazy_t
253 type ens_term = Cic.term lazy_t
254 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
255 let to_env v = lazy v
256 let to_ens v = lazy v
257 let from_stack ~unwind v = Lazy.force v
258 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
259 let from_env v = Lazy.force v
260 let from_ens v = Lazy.force v
261 let from_env_for_unwind ~unwind v = Lazy.force v
262 let from_ens_for_unwind ~unwind v = Lazy.force v
263 let stack_to_env ~reduce ~unwind v = v
264 let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
265 let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
270 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
273 type stack_term = reduce:bool -> Cic.term
274 type env_term = reduce:bool -> Cic.term
275 type ens_term = reduce:bool -> Cic.term
276 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
278 let value = lazy v in
279 fun ~reduce -> Lazy.force value
281 let value = lazy v in
282 fun ~reduce -> Lazy.force value
283 let from_stack ~unwind v = (v ~reduce:false)
284 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
285 let from_env v = (v ~reduce:true)
286 let from_ens v = (v ~reduce:true)
287 let from_env_for_unwind ~unwind v = (v ~reduce:true)
288 let from_ens_for_unwind ~unwind v = (v ~reduce:true)
289 let stack_to_env ~reduce ~unwind v = v
290 let compute_to_stack ~reduce ~unwind k e ens t =
294 Cic.Const _ as t -> unwind k e ens t
295 | t -> reduce (k,e,ens,t,[])
298 lazy (unwind k e ens t)
301 if reduce then Lazy.force svalue else Lazy.force lvalue
302 let compute_to_env ~reduce ~unwind k e ens t =
306 Cic.Const _ as t -> unwind k e ens t
307 | t -> reduce (k,e,ens,t,[])
310 lazy (unwind k e ens t)
313 if reduce then Lazy.force svalue else Lazy.force lvalue
317 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
319 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
320 and stack_term = config
321 and env_term = config
322 and ens_term = config
324 let to_env config = config
325 let to_ens config = config
326 let from_stack config = config
327 let from_stack_list_for_unwind ~unwind l = List.map unwind l
330 let from_env_for_unwind ~unwind config = unwind config
331 let from_ens_for_unwind ~unwind config = unwind config
332 let stack_to_env ~reduce ~unwind config = reduce config
333 let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
334 let compute_to_stack ~reduce ~unwind config = config
338 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
341 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
342 type env_term = Cic.term
343 type ens_term = Cic.term
344 type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
347 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
348 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
351 let from_env_for_unwind ~unwind v = v
352 let from_ens_for_unwind ~unwind v = v
353 let stack_to_env ~reduce ~unwind (k,e,ens,t) =
355 Cic.Const _ as t -> unwind k e ens t
356 | t -> reduce (k,e,ens,t,[])
357 let compute_to_env ~reduce ~unwind k e ens t =
359 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
365 module Reduction(RS : Strategy) =
367 type env = RS.env_term list
368 type stack = RS.stack_term list
369 type config = int * env * NCic.term * stack
371 let rec unwind (k,e,t,s) =
375 NCicSubstitution.psubst ~avoid_beta_redexes:true
376 true 0 (RS.from_env_for_unwind ~unwind) e t
379 else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
382 let list_nth l n = try List.nth l n with Failure _ -> assert false;;
383 let rec replace i s t =
386 | n,he::tl -> he::(replace (n - 1) tl t)
387 | _,_ -> assert false
390 let rec reduce ~delta ?(subst = []) context : config -> config =
391 let rec aux = function
392 | k, e, NCic.Rel n, s when n <= k ->
393 let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
395 | k, _, NCic.Rel n, s as config (* when n > k *) ->
396 let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
398 | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
400 | (k, e, NCic.Meta (n,l), s) as config ->
402 let _,_, term,_ = NCicUtils.lookup_subst n subst in
403 aux (k, e, NCicSubstitution.subst_meta l term,s)
404 with NCicUtils.Subst_not_found _ -> config)
405 | (_, _, NCic.Sort _, _) as config -> config
406 | (_, _, NCic.Implicit _, _) -> assert false
407 | (_, _, NCic.Prod _, _) as config -> config
408 | (_, _, NCic.Lambda _, []) as config -> config
409 | (k, e, NCic.Lambda (_,_,t), p::s) ->
410 aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
411 | (k, e, NCic.LetIn (_,_,m,t), s) ->
412 let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
413 aux (k+1, m'::e, t, s)
414 | (_, _, NCic.Appl [], _) -> assert false
415 | (k, e, NCic.Appl (he::tl), s) ->
417 List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
419 aux (k, e, he, tl' @ s)
421 (NReference.Ref (_,_,NReference.Def) as refer), s) as config ->
422 let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
423 if delta > height then config else aux (0, [], body, s)
424 | (_, _, NCic.Const (NReference.Ref
425 (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
426 let fixes,_, height = NCicEnvironment.get_checked_fixes refer in
427 if delta > height then config else
429 try Some (RS.from_stack (List.nth s recindex))
430 with Failure _ -> None
434 match reduce ~delta:0 ~subst context recparam with
435 | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
437 replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
439 let _,_,_,_,body = List.nth fixes fixno in
440 aux (0, [], body, new_s)
442 | (_, _, NCic.Const _, _) as config -> config
443 | (k, e, NCic.Match (_,_,term,pl),s) as config ->
444 let decofix = function
445 | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
446 let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in
447 let _,_,_,_,body = List.nth cofixes c in
448 reduce ~delta:0 ~subst context (0,[],body,s)
451 (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
452 | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) ->
453 aux (k, e, List.nth pl (j-1), s)
455 (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') ->
456 let leftno = NCicEnvironment.get_indty_leftno refer in
457 let _,params = HExtlib.split_nth leftno s' in
458 aux (k, e, List.nth pl (j-1), params@s)
464 let whd ?(delta=0) ?(subst=[]) context t =
465 unwind (reduce ~delta ~subst context (0, [], t, []))
472 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
473 senza ridurre la testa
474 module R = Reduction CallByNameStrategy;; OK 56.368s
475 module R = Reduction CallByValueStrategy;; ROTTO
476 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
477 module R = Reduction LazyCallByValueStrategy;; ROTTO
478 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
479 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
481 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
483 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
485 ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
486 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
487 module R = Reduction(CallByValueByNameForUnwind);;
488 module R = Reduction(CallByNameStrategy);;
489 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
490 module RS = CallByValueByNameForUnwind';;
492 module R = Reduction(RS);;
493 module U = UriManager;;
499 let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
500 fun ?(delta=true) ?(subst=[]) context t ->
501 profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
504 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
505 * fallbacks to structural equality *)
506 let (===) x y = Pervasives.compare x y = 0 ;;
510 (* t1, t2 must be well-typed *)
511 let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
512 let rec aux test_equality_only context t1 t2 =
513 let rec aux2 test_equality_only t1 t2 =
518 | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
519 | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
520 | (C.Sort s1, C.Sort s2) -> s1 = s2
522 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
523 aux true context s1 s2 &&
524 aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
525 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
526 aux true context s1 s2 &&
527 aux true ((name1, C.Decl s1)::context) t1 t2
528 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
529 aux test_equality_only context ty1 ty2 &&
530 aux test_equality_only context s1 s2 &&
531 aux test_equality_only ((name1, C.Def (s1,ty1))::context) t1 t2
533 | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2)))
534 when n1 = n2 && s1 = s2 -> true
535 | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 ->
536 let l1 = NCicUtils.expand_local_context l1 in
537 let l2 = NCicUtils.expand_local_context l2 in
539 (fun t1 t2 -> aux test_equality_only context
540 (NCicSubstitution.lift s1 t1)
541 (NCicSubstitution.lift s2 t2))
543 with Invalid_argument _ -> false)
545 | C.Meta (n1,l1), _ ->
547 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
548 let term = NCicSubstitution.subst_meta l1 term in
549 aux test_equality_only context term t2
550 with NCicUtils.Subst_not_found _ -> false)
551 | _, C.Meta (n2,l2) ->
553 let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
554 let term = NCicSubstitution.subst_meta l2 term in
555 aux test_equality_only context t1 term
556 with NCicUtils.Subst_not_found _ -> false)
558 | (C.Appl l1, C.Appl l2) ->
559 (try List.for_all2 (aux test_equality_only context) l1 l2
560 with Invalid_argument _ -> false)
562 | (C.Match (ref1,outtype1,term1,pl1),
563 C.Match (ref2,outtype2,term2,pl2)) ->
564 NReference.eq ref1 ref2 &&
565 aux test_equality_only context outtype1 outtype2 &&
566 aux test_equality_only context term1 term2 &&
567 (try List.for_all2 (aux test_equality_only context) pl1 pl2
568 with Invalid_argument _ -> false)
570 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
573 if aux2 test_equality_only t1 t2 then
576 let rec convert_machines = function
578 | ((k1,env1,h1,s1),(k2,env2,h2,s2))::tl ->
579 aux2 test_equality_only
580 (R.unwind (k1,env1,h1,[])) (R.unwind (k2,env2,h2,[])) &&
584 (fun si-> R.reduce ~delta:0 ~subst context(RS.from_stack si))
586 try Some (List.combine (red_stack s1) (red_stack s2) @ tl)
587 with Invalid_argument _ -> None
591 | Some problems -> convert_machines problems
594 [R.reduce ~delta:0 ~subst context (0,[],t1,[]),
595 R.reduce ~delta:0 ~subst context (0,[],t2,[])]
600 let are_convertible = are_convertible whd
602 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
603 match upto, t, l with
604 | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
606 | 0, t, _ -> C.Appl (t::l)
607 | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
608 | _, C.Lambda(_,_,bo), arg::tl ->
609 let bo = NCicSubstitution.subst arg bo in
610 head_beta_reduce ~delta ~upto:(upto - 1) bo tl
611 | _, C.Const (NReference.Ref (height, _, NReference.Def) as re), _
612 when delta <= height ->
613 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
614 head_beta_reduce ~upto ~delta bo l
616 | _, t, _ -> C.Appl (t::l)
619 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
621 (* vim:set foldmethod=marker: *)