1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* TODO unify exceptions *)
28 exception CicReductionInternalError;;
29 exception WrongUriToInductiveDefinition;;
30 exception Impossible of int;;
31 exception ReferenceToConstant;;
32 exception ReferenceToVariable;;
33 exception ReferenceToCurrentProof;;
34 exception ReferenceToInductiveDefinition;;
38 let rec debug_aux t i =
40 let module U = UriManager in
41 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
44 prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
47 module type Strategy =
52 val to_stack : Cic.term -> stack_term
53 val to_stack_list : Cic.term list -> stack_term list
54 val to_env : Cic.term -> env_term
55 val to_ens : Cic.term -> ens_term
58 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
59 Cic.term -> Cic.term) ->
60 stack_term -> Cic.term
63 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
64 Cic.term -> Cic.term) ->
65 stack_term list -> Cic.term list
66 val from_env : env_term -> Cic.term
67 val from_ens : ens_term -> Cic.term
70 (int * env_term list * ens_term Cic.explicit_named_substitution *
71 Cic.term * stack_term list -> Cic.term) ->
73 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
74 Cic.term -> Cic.term) ->
75 stack_term -> env_term
78 (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
79 stack_term list -> Cic.term) ->
81 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
82 Cic.term -> Cic.term) ->
83 int -> env_term list -> ens_term Cic.explicit_named_substitution ->
85 val compute_to_stack :
87 (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
88 stack_term list -> Cic.term) ->
90 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
91 Cic.term -> Cic.term) ->
92 int -> env_term list -> ens_term Cic.explicit_named_substitution ->
93 Cic.term -> stack_term
97 module CallByNameStrategy =
99 type stack_term = Cic.term
100 type env_term = Cic.term
101 type ens_term = Cic.term
103 let to_stack_list l = l
106 let from_stack ~unwind v = v
107 let from_stack_list ~unwind l = l
110 let stack_to_env ~reduce ~unwind v = v
111 let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
112 let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
116 module CallByValueStrategy =
118 type stack_term = Cic.term
119 type env_term = Cic.term
120 type ens_term = Cic.term
122 let to_stack_list l = l
125 let from_stack ~unwind v = v
126 let from_stack_list ~unwind l = l
129 let stack_to_env ~reduce ~unwind v = v
130 let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
131 let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
135 module CallByValueStrategyByNameOnConstants =
137 type stack_term = Cic.term
138 type env_term = Cic.term
139 type ens_term = Cic.term
141 let to_stack_list l = l
144 let from_stack ~unwind v = v
145 let from_stack_list ~unwind l = l
148 let stack_to_env ~reduce ~unwind v = v
149 let compute_to_stack ~reduce ~unwind k e ens =
151 Cic.Const _ as t -> unwind k e ens t
152 | t -> reduce (k,e,ens,t,[])
153 let compute_to_env ~reduce ~unwind k e ens =
155 Cic.Const _ as t -> unwind k e ens t
156 | t -> reduce (k,e,ens,t,[])
160 module LazyCallByValueStrategy =
162 type stack_term = Cic.term lazy_t
163 type env_term = Cic.term lazy_t
164 type ens_term = Cic.term lazy_t
165 let to_stack v = lazy v
166 let to_stack_list l = List.map to_stack l
167 let to_env v = lazy v
168 let to_ens v = lazy v
169 let from_stack ~unwind v = Lazy.force v
170 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
171 let from_env v = Lazy.force v
172 let from_ens v = Lazy.force v
173 let stack_to_env ~reduce ~unwind v = v
174 let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
175 let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
179 module LazyCallByValueStrategyByNameOnConstants =
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 let to_stack v = lazy v
185 let to_stack_list l = List.map to_stack l
186 let to_env v = lazy v
187 let to_ens v = lazy v
188 let from_stack ~unwind v = Lazy.force v
189 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
190 let from_env v = Lazy.force v
191 let from_ens v = Lazy.force v
192 let stack_to_env ~reduce ~unwind v = v
193 let compute_to_stack ~reduce ~unwind k e ens t =
196 Cic.Const _ as t -> unwind k e ens t
197 | t -> reduce (k,e,ens,t,[]))
198 let compute_to_env ~reduce ~unwind k e ens t =
201 Cic.Const _ as t -> unwind k e ens t
202 | t -> reduce (k,e,ens,t,[]))
206 module LazyCallByNameStrategy =
208 type stack_term = Cic.term lazy_t
209 type env_term = Cic.term lazy_t
210 type ens_term = Cic.term lazy_t
211 let to_stack v = lazy v
212 let to_stack_list l = List.map to_stack l
213 let to_env v = lazy v
214 let to_ens v = lazy v
215 let from_stack ~unwind v = Lazy.force v
216 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
217 let from_env v = Lazy.force v
218 let from_ens v = Lazy.force v
219 let stack_to_env ~reduce ~unwind v = v
220 let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
221 let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
226 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
229 type stack_term = reduce:bool -> Cic.term
230 type env_term = reduce:bool -> Cic.term
231 type ens_term = reduce:bool -> Cic.term
233 let value = lazy v in
234 fun ~reduce -> Lazy.force value
235 let to_stack_list l = List.map to_stack l
237 let value = lazy v in
238 fun ~reduce -> Lazy.force value
240 let value = lazy v in
241 fun ~reduce -> Lazy.force value
242 let from_stack ~unwind v = (v ~reduce:false)
243 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
244 let from_env v = (v ~reduce:true)
245 let from_ens v = (v ~reduce:true)
246 let stack_to_env ~reduce ~unwind v = v
247 let compute_to_stack ~reduce ~unwind k e ens t =
251 Cic.Const _ as t -> unwind k e ens t
252 | t -> reduce (k,e,ens,t,[])
255 lazy (unwind k e ens t)
258 if reduce then Lazy.force svalue else Lazy.force lvalue
259 let compute_to_env ~reduce ~unwind k e ens t =
263 Cic.Const _ as t -> unwind k e ens t
264 | t -> reduce (k,e,ens,t,[])
267 lazy (unwind k e ens t)
270 if reduce then Lazy.force svalue else Lazy.force lvalue
274 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
277 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
278 type env_term = Cic.term
279 type ens_term = Cic.term
280 let to_stack v = (0,[],[],v)
281 let to_stack_list l = List.map to_stack l
284 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
285 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
288 let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
289 let compute_to_env ~reduce ~unwind k e ens t =
291 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
295 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
298 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
299 type env_term = Cic.term
300 type ens_term = Cic.term
301 let to_stack v = (0,[],[],v)
302 let to_stack_list l = List.map to_stack l
305 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
306 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
309 let stack_to_env ~reduce ~unwind (k,e,ens,t) =
311 Cic.Const _ as t -> unwind k e ens t
312 | t -> reduce (k,e,ens,t,[])
313 let compute_to_env ~reduce ~unwind k e ens t =
315 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
319 module Reduction(RS : Strategy) =
321 type env = RS.env_term list
322 type ens = RS.ens_term Cic.explicit_named_substitution
323 type stack = RS.stack_term list
324 type config = int * env * ens * Cic.term * stack
326 (* k is the length of the environment e *)
327 (* m is the current depth inside the term *)
328 let unwind' m k e ens t =
329 let module C = Cic in
330 let module S = CicSubstitution in
331 if k = 0 && ens = [] then
334 let rec unwind_aux m =
337 if n <= m then t else
340 Some (RS.from_env (List.nth e (n-m-1)))
345 if m = 0 then t' else S.lift m t'
346 | None -> C.Rel (n-k)
348 | C.Var (uri,exp_named_subst) ->
350 prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
352 if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
353 CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
356 (match CicEnvironment.get_obj uri with
357 C.Constant _ -> raise ReferenceToConstant
358 | C.Variable (_,_,_,params) -> params
359 | C.CurrentProof _ -> raise ReferenceToCurrentProof
360 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
363 let exp_named_subst' =
364 substaux_in_exp_named_subst params exp_named_subst m
366 C.Var (uri,exp_named_subst')
372 | Some t -> Some (unwind_aux m t)
377 | C.Implicit _ as t -> t
378 | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
379 | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
380 | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
381 | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
382 | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
383 | C.Const (uri,exp_named_subst) ->
385 (match CicEnvironment.get_obj uri with
386 C.Constant (_,_,_,params) -> params
387 | C.Variable _ -> raise ReferenceToVariable
388 | C.CurrentProof (_,_,_,_,params) -> params
389 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
392 let exp_named_subst' =
393 substaux_in_exp_named_subst params exp_named_subst m
395 C.Const (uri,exp_named_subst')
396 | C.MutInd (uri,i,exp_named_subst) ->
398 (match CicEnvironment.get_obj uri with
399 C.Constant _ -> raise ReferenceToConstant
400 | C.Variable _ -> raise ReferenceToVariable
401 | C.CurrentProof _ -> raise ReferenceToCurrentProof
402 | C.InductiveDefinition (_,params,_) -> params
405 let exp_named_subst' =
406 substaux_in_exp_named_subst params exp_named_subst m
408 C.MutInd (uri,i,exp_named_subst')
409 | C.MutConstruct (uri,i,j,exp_named_subst) ->
411 (match CicEnvironment.get_obj uri with
412 C.Constant _ -> raise ReferenceToConstant
413 | C.Variable _ -> raise ReferenceToVariable
414 | C.CurrentProof _ -> raise ReferenceToCurrentProof
415 | C.InductiveDefinition (_,params,_) -> params
418 let exp_named_subst' =
419 substaux_in_exp_named_subst params exp_named_subst m
421 C.MutConstruct (uri,i,j,exp_named_subst')
422 | C.MutCase (sp,i,outt,t,pl) ->
423 C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
424 List.map (unwind_aux m) pl)
426 let len = List.length fl in
429 (fun (name,i,ty,bo) ->
430 (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
433 C.Fix (i, substitutedfl)
435 let len = List.length fl in
438 (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
441 C.CoFix (i, substitutedfl)
442 and substaux_in_exp_named_subst params exp_named_subst' m =
443 (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
445 List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
446 (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
447 List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
449 let rec filter_and_lift =
453 let r = filter_and_lift tl in
455 (uri,(List.assq uri ens'))::r
460 filter_and_lift params
463 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
464 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
466 (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
467 (*CSC: codice altamente inefficiente *)
468 let rec filter_and_lift already_instantiated =
473 (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
475 not (List.mem uri already_instantiated)
479 (uri,CicSubstitution.lift m (RS.from_ens t)) ::
480 (filter_and_lift (uri::already_instantiated) tl)
481 | _::tl -> filter_and_lift already_instantiated tl
484 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
485 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
486 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
487 if List.mem uri params then prerr_endline "---- OK2" ;
491 List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
492 (filter_and_lift [] (List.rev ens))
501 let reduce ?(subst = []) context : config -> Cic.term =
502 let module C = Cic in
503 let module S = CicSubstitution in
506 (k, e, _, (C.Rel n as t), s) ->
509 Some (RS.from_env (List.nth e (n-1)))
514 match List.nth context (n - 1 - k) with
516 | Some (_,C.Decl _) -> None
517 | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
523 Some t' -> reduce (0,[],[],t',s)
527 else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
529 | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
530 if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
531 reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
533 (match CicEnvironment.get_obj uri with
534 C.Constant _ -> raise ReferenceToConstant
535 | C.CurrentProof _ -> raise ReferenceToCurrentProof
536 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
537 | C.Variable (_,None,_,_) ->
538 let t' = unwind k e ens t in
539 if s = [] then t' else
540 C.Appl (t'::(RS.from_stack_list ~unwind s))
541 | C.Variable (_,Some body,_,_) ->
542 let ens' = push_exp_named_subst k e ens exp_named_subst in
543 reduce (0, [], ens', body, s)
545 | (k, e, ens, (C.Meta (n,l) as t), s) ->
547 let (_, term,_) = CicUtil.lookup_subst n subst in
548 reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
549 with CicUtil.Subst_not_found _ ->
550 let t' = unwind k e ens t in
551 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
552 | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
553 | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
554 | (k, e, ens, (C.Cast (te,ty) as t), s) ->
555 reduce (k, e, ens, te, s) (* s should be empty *)
556 | (k, e, ens, (C.Prod _ as t), s) ->
557 unwind k e ens t (* s should be empty *)
558 | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
559 | (k, e, ens, C.Lambda (_,_,t), p::s) ->
560 reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
561 | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
562 let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
563 reduce (k+1, m'::e, ens, t, s)
564 | (_, _, _, C.Appl [], _) -> assert false
565 | (k, e, ens, C.Appl (he::tl), s) ->
568 (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
570 reduce (k, e, ens, he, (List.append tl') s)
571 (* CSC: Old Dead Code
572 | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
573 | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
574 | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
575 | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
576 (* strict evaluation, but constants are NOT unfolded *)
579 C.Const _ as t -> unwind k e ens t
580 | t -> reduce (k,e,ens,t,[])
582 let tl' = List.map red tl in
583 reduce (k, e, ens, he , List.append tl' s)
584 | (k, e, ens, C.Appl l, s) ->
585 C.Appl (List.append (List.map (unwind k e ens) l) s)
587 | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
588 (match CicEnvironment.get_obj uri with
589 C.Constant (_,Some body,_,_) ->
590 let ens' = push_exp_named_subst k e ens exp_named_subst in
591 (* constants are closed *)
592 reduce (0, [], ens', body, s)
593 | C.Constant (_,None,_,_) ->
594 let t' = unwind k e ens t in
595 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
596 | C.Variable _ -> raise ReferenceToVariable
597 | C.CurrentProof (_,_,body,_,_) ->
598 let ens' = push_exp_named_subst k e ens exp_named_subst in
599 (* constants are closed *)
600 reduce (0, [], ens', body, s)
601 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
603 | (k, e, ens, (C.MutInd _ as t),s) ->
604 let t' = unwind k e ens t in
605 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
606 | (k, e, ens, (C.MutConstruct _ as t),s) ->
607 let t' = unwind k e ens t in
608 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
609 | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
612 C.CoFix (i,fl) as t ->
613 let (_,_,body) = List.nth fl i in
615 let counter = ref (List.length fl) in
617 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
621 (* the term is the result of a reduction; *)
622 (* so it is already unwinded. *)
623 reduce (0,[],[],body',[])
624 | C.Appl (C.CoFix (i,fl) :: tl) ->
625 let (_,_,body) = List.nth fl i in
627 let counter = ref (List.length fl) in
629 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
633 (* the term is the result of a reduction; *)
634 (* so it is already unwinded. *)
635 reduce (0,[],[],body',RS.to_stack_list tl)
638 (match decofix (reduce (k,e,ens,term,[])) with
639 C.MutConstruct (_,_,j,_) ->
640 reduce (k, e, ens, (List.nth pl (j-1)), s)
641 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
643 match CicEnvironment.get_obj mutind with
644 C.InductiveDefinition (tl,ingredients,r) ->
645 let (_,_,arity,_) = List.nth tl i in
647 | _ -> raise WrongUriToInductiveDefinition
650 let num_to_eat = r in
654 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
655 | _ -> raise (Impossible 5)
657 eat_first (num_to_eat,tl)
659 (* ts are already unwinded because they are a sublist of tl *)
660 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
661 | C.Cast _ | C.Implicit _ ->
662 raise (Impossible 2) (* we don't trust our whd ;-) *)
664 let t' = unwind k e ens t in
665 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
667 | (k, e, ens, (C.Fix (i,fl) as t), s) ->
668 let (_,recindex,_,body) = List.nth fl i in
671 Some (RS.from_stack ~unwind (List.nth s recindex))
677 (match reduce (0,[],[],recparam,[]) with
678 (* match recparam with *)
680 | C.Appl ((C.MutConstruct _)::_) ->
683 let counter = ref (List.length fl) in
685 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
689 reduce (k, e, ens, body', s) *)
691 let leng = List.length fl in
693 let unwind_fl (name,recindex,typ,body) =
694 (name,recindex,unwind k e ens typ,
695 unwind' leng k e ens body)
697 List.map unwind_fl fl
700 let counter = ref 0 in
701 let rec build_env e =
702 if !counter = leng then e
705 build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
709 reduce (k+leng, new_env, ens, body, s)
711 let t' = unwind k e ens t in
712 if s = [] then t' else
713 C.Appl (t'::(RS.from_stack_list ~unwind s))
716 let t' = unwind k e ens t in
717 if s = [] then t' else
718 C.Appl (t'::(RS.from_stack_list ~unwind s))
720 | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
721 let t' = unwind k e ens t in
722 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
723 and push_exp_named_subst k e ens =
727 push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
732 let rec whd ?(subst=[]) context t = reduce ~subst context (0, [], [], t, []);;
736 let res = whd context t in
737 let rescsc = CicReductionNaif.whd context t in
738 if not (CicReductionNaif.are_convertible context res rescsc) then
740 prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
742 prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
744 prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
746 CicReductionNaif.fdebug := 0 ;
747 let _ = CicReductionNaif.are_convertible context res rescsc in
759 module R = Reduction CallByNameStrategy;;
760 module R = Reduction CallByValueStrategy;;
761 module R = Reduction CallByValueStrategyByNameOnConstants;;
762 module R = Reduction LazyCallByValueStrategy;;
763 module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
764 module R = Reduction LazyCallByNameStrategy;;
766 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
767 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
769 ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
771 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
772 module U = UriManager;;
776 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
777 * fallbacks to structural equality *)
778 let (===) x y = (Pervasives.compare x y = 0)
780 (* t1, t2 must be well-typed *)
781 let are_convertible ?(subst=[]) ?(metasenv=[]) =
782 let rec aux test_equality_only context t1 t2 =
783 let aux2 test_equality_only t1 t2 =
784 (* this trivial euristic cuts down the total time of about five times ;-) *)
785 (* this because most of the time t1 and t2 are "sintactically" the same *)
790 let module C = Cic in
792 (C.Rel n1, C.Rel n2) -> n1 = n2
793 | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
797 (fun (uri1,x) (uri2,y) b ->
798 U.eq uri1 uri2 && aux test_equality_only context x y && b
799 ) exp_named_subst1 exp_named_subst2 true
801 Invalid_argument _ -> false
803 | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
805 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
806 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
813 | Some t1',Some t2' -> aux test_equality_only context t1' t2'
815 (* TASSI: CONSTRAINTS *)
816 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
818 (* TASSI: CONSTRAINTS *)
819 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
821 (* TASSI: CONSTRAINTS *)
822 | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
823 (* TASSI: CONSTRAINTS *)
824 | (C.Sort s1, C.Sort s2) -> s1 = s2
825 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
826 aux true context s1 s2 &&
827 aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
828 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
829 aux test_equality_only context s1 s2 &&
830 aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
831 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
832 aux test_equality_only context s1 s2 &&
833 aux test_equality_only
834 ((Some (name1, (C.Def (s1,None))))::context) t1 t2
835 | (C.Appl l1, C.Appl l2) ->
838 (fun x y b -> aux test_equality_only context x y && b) l1 l2 true
840 Invalid_argument _ -> false
842 | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
846 (fun (uri1,x) (uri2,y) b ->
847 U.eq uri1 uri2 && aux test_equality_only context x y && b
848 ) exp_named_subst1 exp_named_subst2 true
850 Invalid_argument _ -> false
852 | (C.MutInd (uri1,i1,exp_named_subst1),
853 C.MutInd (uri2,i2,exp_named_subst2)
855 U.eq uri1 uri2 && i1 = i2 &&
858 (fun (uri1,x) (uri2,y) b ->
859 U.eq uri1 uri2 && aux test_equality_only context x y && b
860 ) exp_named_subst1 exp_named_subst2 true
862 Invalid_argument _ -> false
864 | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
865 C.MutConstruct (uri2,i2,j2,exp_named_subst2)
867 U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
870 (fun (uri1,x) (uri2,y) b ->
871 U.eq uri1 uri2 && aux test_equality_only context x y && b
872 ) exp_named_subst1 exp_named_subst2 true
874 Invalid_argument _ -> false
876 | (C.MutCase (uri1,i1,outtype1,term1,pl1),
877 C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
878 U.eq uri1 uri2 && i1 = i2 &&
879 aux test_equality_only context outtype1 outtype2 &&
880 aux test_equality_only context term1 term2 &&
882 (fun x y b -> b && aux test_equality_only context x y)
884 | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
886 List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
890 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
891 b && recindex1 = recindex2 &&
892 aux test_equality_only context ty1 ty2 &&
893 aux test_equality_only (tys@context) bo1 bo2)
895 | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
897 List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
901 (fun (_,ty1,bo1) (_,ty2,bo2) b ->
902 b && aux test_equality_only context ty1 ty2 &&
903 aux test_equality_only (tys@context) bo1 bo2)
905 | (C.Cast _, _) | (_, C.Cast _)
906 | (C.Implicit _, _) | (_, C.Implicit _) ->
912 if aux2 test_equality_only t1 t2 then true
916 debug t1 [t2] "PREWHD";
920 prerr_endline (CicPp.ppterm t1);
921 prerr_endline (CicPp.ppterm (whd ~subst context t1));
922 prerr_endline (CicPp.ppterm t2);
923 prerr_endline (CicPp.ppterm (whd ~subst context t2))
925 let t1' = whd ~subst context t1 in
926 let t2' = whd ~subst context t2 in
927 debug t1' [t2'] "POSTWHD";
928 aux2 test_equality_only t1' t2'