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;;
37 let debug_print s = if debug then prerr_endline (Lazy.force s)
41 let rec debug_aux t i =
43 let module U = UriManager in
44 CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
47 debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
50 module type Strategy =
55 val to_stack : Cic.term -> stack_term
56 val to_stack_list : Cic.term list -> stack_term list
57 val to_env : Cic.term -> env_term
58 val to_ens : Cic.term -> ens_term
61 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
62 Cic.term -> Cic.term) ->
63 stack_term -> Cic.term
66 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
67 Cic.term -> Cic.term) ->
68 stack_term list -> Cic.term list
69 val from_env : env_term -> Cic.term
70 val from_ens : ens_term -> Cic.term
73 (int * env_term list * ens_term Cic.explicit_named_substitution *
74 Cic.term * stack_term list -> Cic.term) ->
76 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
77 Cic.term -> Cic.term) ->
78 stack_term -> env_term
81 (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
82 stack_term list -> Cic.term) ->
84 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
85 Cic.term -> Cic.term) ->
86 int -> env_term list -> ens_term Cic.explicit_named_substitution ->
88 val compute_to_stack :
90 (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
91 stack_term list -> Cic.term) ->
93 (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
94 Cic.term -> Cic.term) ->
95 int -> env_term list -> ens_term Cic.explicit_named_substitution ->
96 Cic.term -> stack_term
100 module CallByNameStrategy =
102 type stack_term = Cic.term
103 type env_term = Cic.term
104 type ens_term = Cic.term
106 let to_stack_list l = l
109 let from_stack ~unwind v = v
110 let from_stack_list ~unwind l = l
113 let stack_to_env ~reduce ~unwind v = v
114 let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
115 let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
119 module CallByValueStrategy =
121 type stack_term = Cic.term
122 type env_term = Cic.term
123 type ens_term = Cic.term
125 let to_stack_list l = l
128 let from_stack ~unwind v = v
129 let from_stack_list ~unwind l = l
132 let stack_to_env ~reduce ~unwind v = v
133 let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
134 let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
138 module CallByValueStrategyByNameOnConstants =
140 type stack_term = Cic.term
141 type env_term = Cic.term
142 type ens_term = Cic.term
144 let to_stack_list l = l
147 let from_stack ~unwind v = v
148 let from_stack_list ~unwind l = l
151 let stack_to_env ~reduce ~unwind v = v
152 let compute_to_stack ~reduce ~unwind k e ens =
154 Cic.Const _ as t -> unwind k e ens t
155 | t -> reduce (k,e,ens,t,[])
156 let compute_to_env ~reduce ~unwind k e ens =
158 Cic.Const _ as t -> unwind k e ens t
159 | t -> reduce (k,e,ens,t,[])
163 module LazyCallByValueStrategy =
165 type stack_term = Cic.term lazy_t
166 type env_term = Cic.term lazy_t
167 type ens_term = Cic.term lazy_t
168 let to_stack v = lazy v
169 let to_stack_list l = List.map to_stack l
170 let to_env v = lazy v
171 let to_ens v = lazy v
172 let from_stack ~unwind v = Lazy.force v
173 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
174 let from_env v = Lazy.force v
175 let from_ens v = Lazy.force v
176 let stack_to_env ~reduce ~unwind v = v
177 let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
178 let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
182 module LazyCallByValueStrategyByNameOnConstants =
184 type stack_term = Cic.term lazy_t
185 type env_term = Cic.term lazy_t
186 type ens_term = Cic.term lazy_t
187 let to_stack v = lazy v
188 let to_stack_list l = List.map to_stack l
189 let to_env v = lazy v
190 let to_ens v = lazy v
191 let from_stack ~unwind v = Lazy.force v
192 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
193 let from_env v = Lazy.force v
194 let from_ens v = Lazy.force v
195 let stack_to_env ~reduce ~unwind v = v
196 let compute_to_stack ~reduce ~unwind k e ens t =
199 Cic.Const _ as t -> unwind k e ens t
200 | t -> reduce (k,e,ens,t,[]))
201 let compute_to_env ~reduce ~unwind k e ens t =
204 Cic.Const _ as t -> unwind k e ens t
205 | t -> reduce (k,e,ens,t,[]))
209 module LazyCallByNameStrategy =
211 type stack_term = Cic.term lazy_t
212 type env_term = Cic.term lazy_t
213 type ens_term = Cic.term lazy_t
214 let to_stack v = lazy v
215 let to_stack_list l = List.map to_stack l
216 let to_env v = lazy v
217 let to_ens v = lazy v
218 let from_stack ~unwind v = Lazy.force v
219 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
220 let from_env v = Lazy.force v
221 let from_ens v = Lazy.force v
222 let stack_to_env ~reduce ~unwind v = v
223 let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
224 let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
229 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
232 type stack_term = reduce:bool -> Cic.term
233 type env_term = reduce:bool -> Cic.term
234 type ens_term = reduce:bool -> Cic.term
236 let value = lazy v in
237 fun ~reduce -> Lazy.force value
238 let to_stack_list l = List.map to_stack l
240 let value = lazy v in
241 fun ~reduce -> Lazy.force value
243 let value = lazy v in
244 fun ~reduce -> Lazy.force value
245 let from_stack ~unwind v = (v ~reduce:false)
246 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
247 let from_env v = (v ~reduce:true)
248 let from_ens v = (v ~reduce:true)
249 let stack_to_env ~reduce ~unwind v = v
250 let compute_to_stack ~reduce ~unwind k e ens t =
254 Cic.Const _ as t -> unwind k e ens t
255 | t -> reduce (k,e,ens,t,[])
258 lazy (unwind k e ens t)
261 if reduce then Lazy.force svalue else Lazy.force lvalue
262 let compute_to_env ~reduce ~unwind k e ens t =
266 Cic.Const _ as t -> unwind k e ens t
267 | t -> reduce (k,e,ens,t,[])
270 lazy (unwind k e ens t)
273 if reduce then Lazy.force svalue else Lazy.force lvalue
277 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
280 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
281 type env_term = Cic.term
282 type ens_term = Cic.term
283 let to_stack v = (0,[],[],v)
284 let to_stack_list l = List.map to_stack l
287 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
288 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
291 let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
292 let compute_to_env ~reduce ~unwind k e ens t =
294 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
298 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
301 int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
302 type env_term = Cic.term
303 type ens_term = Cic.term
304 let to_stack v = (0,[],[],v)
305 let to_stack_list l = List.map to_stack l
308 let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
309 let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
312 let stack_to_env ~reduce ~unwind (k,e,ens,t) =
314 Cic.Const _ as t -> unwind k e ens t
315 | t -> reduce (k,e,ens,t,[])
316 let compute_to_env ~reduce ~unwind k e ens t =
318 let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
322 module Reduction(RS : Strategy) =
324 type env = RS.env_term list
325 type ens = RS.ens_term Cic.explicit_named_substitution
326 type stack = RS.stack_term list
327 type config = int * env * ens * Cic.term * stack
329 (* k is the length of the environment e *)
330 (* m is the current depth inside the term *)
331 let unwind' m k e ens t =
332 let module C = Cic in
333 let module S = CicSubstitution in
334 if k = 0 && ens = [] then
337 let rec unwind_aux m =
340 if n <= m then t else
343 Some (RS.from_env (List.nth e (n-m-1)))
348 if m = 0 then t' else S.lift m t'
349 | None -> C.Rel (n-k)
351 | C.Var (uri,exp_named_subst) ->
353 debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
355 if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
356 CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
360 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
363 C.Constant _ -> raise ReferenceToConstant
364 | C.Variable (_,_,_,params,_) -> params
365 | C.CurrentProof _ -> raise ReferenceToCurrentProof
366 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
369 let exp_named_subst' =
370 substaux_in_exp_named_subst params exp_named_subst m
372 C.Var (uri,exp_named_subst')
378 | Some t -> Some (unwind_aux m t)
383 | C.Implicit _ as t -> t
384 | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
385 | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
386 | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
387 | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
388 | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
389 | C.Const (uri,exp_named_subst) ->
392 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
395 C.Constant (_,_,_,params,_) -> params
396 | C.Variable _ -> raise ReferenceToVariable
397 | C.CurrentProof (_,_,_,_,params,_) -> params
398 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
401 let exp_named_subst' =
402 substaux_in_exp_named_subst params exp_named_subst m
404 C.Const (uri,exp_named_subst')
405 | C.MutInd (uri,i,exp_named_subst) ->
408 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
411 C.Constant _ -> raise ReferenceToConstant
412 | C.Variable _ -> raise ReferenceToVariable
413 | C.CurrentProof _ -> raise ReferenceToCurrentProof
414 | C.InductiveDefinition (_,params,_,_) -> params
417 let exp_named_subst' =
418 substaux_in_exp_named_subst params exp_named_subst m
420 C.MutInd (uri,i,exp_named_subst')
421 | C.MutConstruct (uri,i,j,exp_named_subst) ->
424 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
427 C.Constant _ -> raise ReferenceToConstant
428 | C.Variable _ -> raise ReferenceToVariable
429 | C.CurrentProof _ -> raise ReferenceToCurrentProof
430 | C.InductiveDefinition (_,params,_,_) -> params
433 let exp_named_subst' =
434 substaux_in_exp_named_subst params exp_named_subst m
436 C.MutConstruct (uri,i,j,exp_named_subst')
437 | C.MutCase (sp,i,outt,t,pl) ->
438 C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
439 List.map (unwind_aux m) pl)
441 let len = List.length fl in
444 (fun (name,i,ty,bo) ->
445 (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
448 C.Fix (i, substitutedfl)
450 let len = List.length fl in
453 (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
456 C.CoFix (i, substitutedfl)
457 and substaux_in_exp_named_subst params exp_named_subst' m =
458 (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
460 List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
461 (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
462 List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
464 let rec filter_and_lift =
468 let r = filter_and_lift tl in
470 (uri,(List.assq uri ens'))::r
475 filter_and_lift params
478 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
479 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
481 (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
482 (*CSC: codice altamente inefficiente *)
483 let rec filter_and_lift already_instantiated =
488 (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
490 not (List.mem uri already_instantiated)
494 (uri,CicSubstitution.lift m (RS.from_ens t)) ::
495 (filter_and_lift (uri::already_instantiated) tl)
496 | _::tl -> filter_and_lift already_instantiated tl
499 debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
500 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
501 exp_named_subst' then debug_print (lazy "---- OK1") ;
502 debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
503 if List.mem uri params then debug_print (lazy "---- OK2") ;
507 List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
508 (filter_and_lift [] (List.rev ens))
513 let profiler_unwind = HExtlib.profile "are_convertible.unwind"
514 let unwind k e ens t =
518 profiler_unwind.HExtlib.profile foo ()
521 let reduce ~delta ?(subst = []) context : config -> Cic.term =
522 let module C = Cic in
523 let module S = CicSubstitution in
526 (k, e, _, (C.Rel n as t), s) ->
529 Some (RS.from_env (List.nth e (n-1)))
534 match List.nth context (n - 1 - k) with
536 | Some (_,C.Decl _) -> None
537 | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
543 Some t' -> reduce (0,[],[],t',s)
547 else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
549 | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
550 if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
551 reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
554 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
557 C.Constant _ -> raise ReferenceToConstant
558 | C.CurrentProof _ -> raise ReferenceToCurrentProof
559 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
560 | C.Variable (_,None,_,_,_) ->
561 let t' = unwind k e ens t in
562 if s = [] then t' else
563 C.Appl (t'::(RS.from_stack_list ~unwind s))
564 | C.Variable (_,Some body,_,_,_) ->
565 let ens' = push_exp_named_subst k e ens exp_named_subst in
566 reduce (0, [], ens', body, s)
568 | (k, e, ens, (C.Meta (n,l) as t), s) ->
570 let (_, term,_) = CicUtil.lookup_subst n subst in
571 reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
572 with CicUtil.Subst_not_found _ ->
573 let t' = unwind k e ens t in
574 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
575 | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
576 | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
577 | (k, e, ens, (C.Cast (te,ty) as t), s) ->
578 reduce (k, e, ens, te, s) (* s should be empty *)
579 | (k, e, ens, (C.Prod _ as t), s) ->
580 unwind k e ens t (* s should be empty *)
581 | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
582 | (k, e, ens, C.Lambda (_,_,t), p::s) ->
583 reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
584 | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
585 let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
586 reduce (k+1, m'::e, ens, t, s)
587 | (_, _, _, C.Appl [], _) -> assert false
588 | (k, e, ens, C.Appl (he::tl), s) ->
591 (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
593 reduce (k, e, ens, he, (List.append tl') s)
594 (* CSC: Old Dead Code
595 | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
596 | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
597 | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
598 | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
599 (* strict evaluation, but constants are NOT unfolded *)
602 C.Const _ as t -> unwind k e ens t
603 | t -> reduce (k,e,ens,t,[])
605 let tl' = List.map red tl in
606 reduce (k, e, ens, he , List.append tl' s)
607 | (k, e, ens, C.Appl l, s) ->
608 C.Appl (List.append (List.map (unwind k e ens) l) s)
610 | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false->
611 let t' = unwind k e ens t in
612 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
613 | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
615 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
618 C.Constant (_,Some body,_,_,_) ->
619 let ens' = push_exp_named_subst k e ens exp_named_subst in
620 (* constants are closed *)
621 reduce (0, [], ens', body, s)
622 | C.Constant (_,None,_,_,_) ->
623 let t' = unwind k e ens t in
624 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
625 | C.Variable _ -> raise ReferenceToVariable
626 | C.CurrentProof (_,_,body,_,_,_) ->
627 let ens' = push_exp_named_subst k e ens exp_named_subst in
628 (* constants are closed *)
629 reduce (0, [], ens', body, s)
630 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
632 | (k, e, ens, (C.MutInd _ as t),s) ->
633 let t' = unwind k e ens t in
634 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
635 | (k, e, ens, (C.MutConstruct _ as t),s) ->
636 let t' = unwind k e ens t in
637 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
638 | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
641 C.CoFix (i,fl) as t ->
642 let (_,_,body) = List.nth fl i in
644 let counter = ref (List.length fl) in
646 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
650 (* the term is the result of a reduction; *)
651 (* so it is already unwinded. *)
652 reduce (0,[],[],body',[])
653 | C.Appl (C.CoFix (i,fl) :: tl) ->
654 let (_,_,body) = List.nth fl i in
656 let counter = ref (List.length fl) in
658 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
662 (* the term is the result of a reduction; *)
663 (* so it is already unwinded. *)
664 reduce (0,[],[],body',RS.to_stack_list tl)
667 (match decofix (reduce (k,e,ens,term,[])) with
668 C.MutConstruct (_,_,j,_) ->
669 reduce (k, e, ens, (List.nth pl (j-1)), s)
670 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
673 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
676 C.InductiveDefinition (tl,ingredients,r,_) ->
677 let (_,_,arity,_) = List.nth tl i in
679 | _ -> raise WrongUriToInductiveDefinition
682 let num_to_eat = r in
686 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
687 | _ -> raise (Impossible 5)
689 eat_first (num_to_eat,tl)
691 (* ts are already unwinded because they are a sublist of tl *)
692 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
693 | C.Cast _ | C.Implicit _ ->
694 raise (Impossible 2) (* we don't trust our whd ;-) *)
696 let t' = unwind k e ens t in
697 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
699 | (k, e, ens, (C.Fix (i,fl) as t), s) ->
700 let (_,recindex,_,body) = List.nth fl i in
703 Some (RS.from_stack ~unwind (List.nth s recindex))
709 (match reduce (0,[],[],recparam,[]) with
710 (* match recparam with *)
712 | C.Appl ((C.MutConstruct _)::_) ->
715 let counter = ref (List.length fl) in
717 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
721 reduce (k, e, ens, body', s) *)
723 let leng = List.length fl in
725 let unwind_fl (name,recindex,typ,body) =
726 (name,recindex,unwind k e ens typ,
727 unwind' leng k e ens body)
729 List.map unwind_fl fl
732 let counter = ref 0 in
733 let rec build_env e =
734 if !counter = leng then e
737 build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
741 reduce (k+leng, new_env, ens, body, s)
743 let t' = unwind k e ens t in
744 if s = [] then t' else
745 C.Appl (t'::(RS.from_stack_list ~unwind s))
748 let t' = unwind k e ens t in
749 if s = [] then t' else
750 C.Appl (t'::(RS.from_stack_list ~unwind s))
752 | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
753 let t' = unwind k e ens t in
754 if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
755 and push_exp_named_subst k e ens =
759 push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
764 let rec whd context t =
766 reduce context (0, [], [], t, [])
768 debug_print (lazy (CicPp.ppterm t)) ;
773 let rec whd ?(delta=true) ?(subst=[]) context t =
774 reduce ~delta ~subst context (0, [], [], t, [])
782 (* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
783 senza ridurre la testa
784 module R = Reduction CallByNameStrategy;; OK 56.368s
785 module R = Reduction CallByValueStrategy;; ROTTO
786 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
787 module R = Reduction LazyCallByValueStrategy;; ROTTO
788 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
789 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
791 LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
793 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
795 ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
796 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
798 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
799 module U = UriManager;;
801 let profiler_whd = HExtlib.profile "are_convertible.whd"
804 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
805 * fallbacks to structural equality *)
807 Pervasives.compare x y = 0
809 (* t1, t2 must be well-typed *)
810 let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
811 let rec aux test_equality_only context t1 t2 ugraph =
812 let aux2 test_equality_only t1 t2 ugraph =
814 (* this trivial euristic cuts down the total time of about five times ;-) *)
815 (* this because most of the time t1 and t2 are "sintactically" the same *)
820 let module C = Cic in
822 (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
823 | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
824 if U.eq uri1 uri2 then
827 (fun (uri1,x) (uri2,y) (b,ugraph) ->
828 let b',ugraph' = aux test_equality_only context x y ugraph in
829 (U.eq uri1 uri2 && b' && b),ugraph'
830 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
832 Invalid_argument _ -> false,ugraph
836 | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
839 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
840 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
842 (fun (b,ugraph) t1 t2 ->
846 | _,None -> true,ugraph
847 | Some t1',Some t2' ->
848 aux test_equality_only context t1' t2' ugraph
851 ) (true,ugraph) l1 l2
853 if b2 then true,ugraph1 else false,ugraph
856 (* TASSI: CONSTRAINTS *)
857 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
858 true,(CicUniv.add_eq t2 t1 ugraph)
859 (* TASSI: CONSTRAINTS *)
860 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
861 true,(CicUniv.add_ge t2 t1 ugraph)
862 (* TASSI: CONSTRAINTS *)
863 | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
864 (* TASSI: CONSTRAINTS *)
865 | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
866 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
867 let b',ugraph' = aux true context s1 s2 ugraph in
869 aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
873 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
874 let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
876 aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
880 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
881 let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
883 aux test_equality_only
884 ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
887 | (C.Appl l1, C.Appl l2) ->
890 (fun x y (b,ugraph) ->
892 aux test_equality_only context x y ugraph
894 false,ugraph) l1 l2 (true,ugraph)
896 Invalid_argument _ -> false,ugraph
898 | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
899 let b' = U.eq uri1 uri2 in
903 (fun (uri1,x) (uri2,y) (b,ugraph) ->
904 if b && U.eq uri1 uri2 then
905 aux test_equality_only context x y ugraph
908 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
910 Invalid_argument _ -> false,ugraph
914 | (C.MutInd (uri1,i1,exp_named_subst1),
915 C.MutInd (uri2,i2,exp_named_subst2)
917 let b' = U.eq uri1 uri2 && i1 = i2 in
921 (fun (uri1,x) (uri2,y) (b,ugraph) ->
922 if b && U.eq uri1 uri2 then
923 aux test_equality_only context x y ugraph
926 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
928 Invalid_argument _ -> false,ugraph
932 | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
933 C.MutConstruct (uri2,i2,j2,exp_named_subst2)
935 let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
939 (fun (uri1,x) (uri2,y) (b,ugraph) ->
940 if b && U.eq uri1 uri2 then
941 aux test_equality_only context x y ugraph
944 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
946 Invalid_argument _ -> false,ugraph
950 | (C.MutCase (uri1,i1,outtype1,term1,pl1),
951 C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
952 let b' = U.eq uri1 uri2 && i1 = i2 in
954 let b'',ugraph''=aux test_equality_only context
955 outtype1 outtype2 ugraph in
957 let b''',ugraph'''= aux test_equality_only context
958 term1 term2 ugraph'' in
960 (fun x y (b,ugraph) ->
962 aux test_equality_only context x y ugraph
965 pl1 pl2 (b''',ugraph''')
970 | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
972 List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
976 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
977 if b && recindex1 = recindex2 then
978 let b',ugraph' = aux test_equality_only context ty1 ty2
981 aux test_equality_only (tys@context) bo1 bo2 ugraph'
986 fl1 fl2 (true,ugraph)
989 | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
991 List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
995 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
997 let b',ugraph' = aux test_equality_only context ty1 ty2
1000 aux test_equality_only (tys@context) bo1 bo2 ugraph'
1005 fl1 fl2 (true,ugraph)
1008 | (C.Cast _, _) | (_, C.Cast _)
1009 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
1010 | (_,_) -> false,ugraph
1014 debug t1 [t2] "PREWHD";
1018 debug_print (lazy (CicPp.ppterm t1));
1019 debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
1020 debug_print (lazy (CicPp.ppterm t2));
1021 debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
1025 whd ?delta:(Some true) ?subst:(Some subst) context t1
1027 profiler_whd.HExtlib.profile foo ()
1031 whd ?delta:(Some true) ?subst:(Some subst) context t2
1033 profiler_whd.HExtlib.profile foo ()
1035 debug t1' [t2'] "POSTWHD";
1036 aux2 test_equality_only t1' t2' ugraph
1039 aux false (*c t1 t2 ugraph *)
1043 let whd ?(delta=true) ?(subst=[]) context t =
1044 let res = whd ~delta ~subst context t in
1045 let rescsc = CicReductionNaif.whd ~delta ~subst context t in
1046 if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
1048 debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
1050 debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
1052 debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
1055 let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
1063 let are_convertible = are_convertible whd
1065 let profiler_other_whd = HExtlib.profile "~are_convertible.whd"
1066 let whd ?(delta=true) ?(subst=[]) context t =
1068 whd ~delta ~subst context t
1070 profiler_other_whd.HExtlib.profile foo ()
1072 let rec normalize ?(delta=true) ?(subst=[]) ctx term =
1073 let module C = Cic in
1074 let t = whd ~delta ~subst ctx term in
1075 let aux = normalize ~delta ~subst in
1076 let decl name t = Some (name, C.Decl t) in
1077 let def name t = Some (name, C.Def (t,None)) in
1080 | C.Var (uri,exp_named_subst) ->
1081 C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1083 C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
1086 | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
1088 let s' = aux ctx s in
1089 C.Prod (n, s', aux ((decl n s')::ctx) t)
1090 | C.Lambda (n,s,t) ->
1091 let s' = aux ctx s in
1092 C.Lambda (n, s', aux ((decl n s')::ctx) t)
1093 | C.LetIn (n,s,t) ->
1094 (* the term is already in weak head normal form *)
1096 | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
1097 | C.Appl [] -> assert false
1098 | C.Const (uri,exp_named_subst) ->
1099 C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1100 | C.MutInd (uri,typeno,exp_named_subst) ->
1101 C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1102 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
1103 C.MutConstruct (uri, typeno, consno,
1104 List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1105 | C.MutCase (sp,i,outt,t,pl) ->
1106 C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
1107 (*CSC: to be completed, I suppose *)
1111 let normalize ?delta ?subst ctx term =
1112 (* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
1113 let t = normalize ?delta ?subst ctx term in
1114 (* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
1118 (* performs an head beta/cast reduction *)
1119 let rec head_beta_reduce =
1121 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
1122 let he'' = CicSubstitution.subst he' t in
1128 Cic.Appl l -> Cic.Appl (l@tl')
1129 | _ -> Cic.Appl (he''::tl')
1131 head_beta_reduce he'''
1132 | Cic.Cast (te,_) -> head_beta_reduce te