]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/cicReductionMachine.ml
select and click signal added
[helm.git] / helm / ocaml / cic_proof_checking / cicReductionMachine.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 exception CicReductionInternalError;;
27 exception WrongUriToInductiveDefinition;;
28 exception Impossible of int;;
29 exception ReferenceToConstant;;
30 exception ReferenceToVariable;;
31 exception ReferenceToCurrentProof;;
32 exception ReferenceToInductiveDefinition;;
33
34 let fdebug = ref 1;;
35 let debug t env s =
36  let rec debug_aux t i =
37   let module C = Cic in
38   let module U = UriManager in
39    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
40  in
41   if !fdebug = 0 then
42    begin
43     print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
44     flush stdout
45    end
46 ;;
47
48 module type Strategy =
49  sig
50   type stack_term
51   type env_term
52   type ens_term
53   val to_stack : Cic.term -> stack_term
54   val to_stack_list : Cic.term list -> stack_term list
55   val to_env : Cic.term -> env_term
56   val to_ens : Cic.term -> ens_term
57   val from_stack :
58    unwind:
59     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
60       Cic.term -> Cic.term) ->
61    stack_term -> Cic.term
62   val from_stack_list :
63    unwind:
64     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
65       Cic.term -> Cic.term) ->
66    stack_term list -> Cic.term list
67   val from_env : env_term -> Cic.term
68   val from_ens : ens_term -> Cic.term
69   val stack_to_env :
70    reduce:
71     (int * env_term list * ens_term Cic.explicit_named_substitution *
72       Cic.term * stack_term list -> Cic.term) ->
73    unwind:
74     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
75       Cic.term -> Cic.term) ->
76    stack_term -> env_term
77   val compute_to_env :
78    reduce:
79     (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
80       stack_term list -> Cic.term) ->
81    unwind:
82     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
83       Cic.term -> Cic.term) ->
84    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
85     Cic.term -> env_term
86   val compute_to_stack :
87    reduce:
88     (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
89       stack_term list -> Cic.term) ->
90    unwind:
91     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
92       Cic.term -> Cic.term) ->
93    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
94     Cic.term -> stack_term
95  end
96 ;;
97
98 module CallByNameStrategy =
99  struct
100   type stack_term = Cic.term
101   type env_term = Cic.term
102   type ens_term = Cic.term
103   let to_stack v = v
104   let to_stack_list l = l
105   let to_env v = v
106   let to_ens v = v
107   let from_stack ~unwind v = v
108   let from_stack_list ~unwind l = l
109   let from_env v = v
110   let from_ens v = v
111   let stack_to_env ~reduce ~unwind v = v
112   let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
113   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
114  end
115 ;;
116
117 module CallByValueStrategy =
118  struct
119   type stack_term = Cic.term
120   type env_term = Cic.term
121   type ens_term = Cic.term
122   let to_stack v = v
123   let to_stack_list l = l
124   let to_env v = v
125   let to_ens v = v
126   let from_stack ~unwind v = v
127   let from_stack_list ~unwind l = l
128   let from_env v = v
129   let from_ens v = v
130   let stack_to_env ~reduce ~unwind v = v
131   let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
132   let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
133  end
134 ;;
135
136 module CallByValueStrategyByNameOnConstants =
137  struct
138   type stack_term = Cic.term
139   type env_term = Cic.term
140   type ens_term = Cic.term
141   let to_stack v = v
142   let to_stack_list l = l
143   let to_env v = v
144   let to_ens v = v
145   let from_stack ~unwind v = v
146   let from_stack_list ~unwind l = l
147   let from_env v = v
148   let from_ens v = v
149   let stack_to_env ~reduce ~unwind v = v
150   let compute_to_stack ~reduce ~unwind k e ens =
151    function
152       Cic.Const _ as t -> unwind k e ens t    
153     | t -> reduce (k,e,ens,t,[])
154   let compute_to_env ~reduce ~unwind k e ens =
155    function
156       Cic.Const _ as t -> unwind k e ens t    
157     | t -> reduce (k,e,ens,t,[])
158  end
159 ;;
160
161 module LazyCallByValueStrategy =
162  struct
163   type stack_term = Cic.term lazy_t
164   type env_term = Cic.term lazy_t
165   type ens_term = Cic.term lazy_t
166   let to_stack v = lazy v
167   let to_stack_list l = List.map to_stack l
168   let to_env v = lazy v
169   let to_ens v = lazy v
170   let from_stack ~unwind v = Lazy.force v
171   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
172   let from_env v = Lazy.force v
173   let from_ens v = Lazy.force v
174   let stack_to_env ~reduce ~unwind v = v
175   let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
176   let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
177  end
178 ;;
179
180 module LazyCallByValueStrategyByNameOnConstants =
181  struct
182   type stack_term = Cic.term lazy_t
183   type env_term = Cic.term lazy_t
184   type ens_term = Cic.term lazy_t
185   let to_stack v = lazy v
186   let to_stack_list l = List.map to_stack l
187   let to_env v = lazy v
188   let to_ens v = lazy v
189   let from_stack ~unwind v = Lazy.force v
190   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
191   let from_env v = Lazy.force v
192   let from_ens v = Lazy.force v
193   let stack_to_env ~reduce ~unwind v = v
194   let compute_to_stack ~reduce ~unwind k e ens t =
195    lazy (
196     match t with
197        Cic.Const _ as t -> unwind k e ens t    
198      | t -> reduce (k,e,ens,t,[]))
199   let compute_to_env ~reduce ~unwind k e ens t =
200    lazy (
201     match t with
202        Cic.Const _ as t -> unwind k e ens t    
203      | t -> reduce (k,e,ens,t,[]))
204  end
205 ;;
206
207 module LazyCallByNameStrategy =
208  struct
209   type stack_term = Cic.term lazy_t
210   type env_term = Cic.term lazy_t
211   type ens_term = Cic.term lazy_t
212   let to_stack v = lazy v
213   let to_stack_list l = List.map to_stack l
214   let to_env v = lazy v
215   let to_ens v = lazy v
216   let from_stack ~unwind v = Lazy.force v
217   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
218   let from_env v = Lazy.force v
219   let from_ens v = Lazy.force v
220   let stack_to_env ~reduce ~unwind v = v
221   let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
222   let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
223  end
224 ;;
225
226 module
227  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
228 =
229  struct
230   type stack_term = reduce:bool -> Cic.term
231   type env_term = reduce:bool -> Cic.term
232   type ens_term = reduce:bool -> Cic.term
233   let to_stack v =
234    let value = lazy v in
235     fun ~reduce -> Lazy.force value
236   let to_stack_list l = List.map to_stack l
237   let to_env v =
238    let value = lazy v in
239     fun ~reduce -> Lazy.force value
240   let to_ens v =
241    let value = lazy v in
242     fun ~reduce -> Lazy.force value
243   let from_stack ~unwind v = (v ~reduce:false)
244   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
245   let from_env v = (v ~reduce:true)
246   let from_ens v = (v ~reduce:true)
247   let stack_to_env ~reduce ~unwind v = v
248   let compute_to_stack ~reduce ~unwind k e ens t =
249    let svalue =
250      lazy (
251       match t with
252          Cic.Const _ as t -> unwind k e ens t    
253        | t -> reduce (k,e,ens,t,[])
254      ) in
255    let lvalue =
256     lazy (unwind k e ens t)
257    in
258     fun ~reduce ->
259      if reduce then Lazy.force svalue else Lazy.force lvalue
260   let compute_to_env ~reduce ~unwind k e ens t =
261    let svalue =
262      lazy (
263       match t with
264          Cic.Const _ as t -> unwind k e ens t    
265        | t -> reduce (k,e,ens,t,[])
266      ) in
267    let lvalue =
268     lazy (unwind k e ens t)
269    in
270     fun ~reduce ->
271      if reduce then Lazy.force svalue else Lazy.force lvalue
272  end
273 ;;
274
275 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
276  struct
277   type stack_term =
278    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
279   type env_term = Cic.term
280   type ens_term = Cic.term
281   let to_stack v = (0,[],[],v)
282   let to_stack_list l = List.map to_stack l
283   let to_env v = v
284   let to_ens v = v
285   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
286   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
287   let from_env v = v
288   let from_ens v = v
289   let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
290   let compute_to_env ~reduce ~unwind k e ens t =
291    unwind k e ens t
292   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
293  end
294 ;;
295
296 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
297  struct
298   type stack_term =
299    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
300   type env_term = Cic.term
301   type ens_term = Cic.term
302   let to_stack v = (0,[],[],v)
303   let to_stack_list l = List.map to_stack l
304   let to_env v = v
305   let to_ens v = v
306   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
307   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
308   let from_env v = v
309   let from_ens v = v
310   let stack_to_env ~reduce ~unwind (k,e,ens,t) =
311    match t with
312       Cic.Const _ as t -> unwind k e ens t    
313     | t -> reduce (k,e,ens,t,[])
314   let compute_to_env ~reduce ~unwind k e ens t =
315    unwind k e ens t
316   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
317  end
318 ;;
319
320 module Reduction(RS : Strategy) =
321  struct
322   type env = RS.env_term list
323   type ens = RS.ens_term Cic.explicit_named_substitution
324   type stack = RS.stack_term list
325   type config = int * env * ens * Cic.term * stack
326
327   (* k is the length of the environment e *)
328   (* m is the current depth inside the term *)
329   let unwind' m k e ens t = 
330    let module C = Cic in
331    let module S = CicSubstitution in
332     if k = 0 && ens = [] then
333      t
334     else 
335      let rec unwind_aux m =
336       function
337          C.Rel n as t ->
338           if n <= m then t else
339            let d =
340             try
341              Some (RS.from_env (List.nth e (n-m-1)))
342             with _ -> None
343            in
344             (match d with 
345                 Some t' ->
346                  if m = 0 then t' else S.lift m t'
347               | None -> C.Rel (n-k)
348             )
349        | C.Var (uri,exp_named_subst) ->
350 (*
351 prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
352 *)
353          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
354           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
355          else
356           let params =
357            (match CicEnvironment.get_obj uri with
358                C.Constant _ -> raise ReferenceToConstant
359              | C.Variable (_,_,_,params) -> params
360              | C.CurrentProof _ -> raise ReferenceToCurrentProof
361              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
362            )
363           in
364            let exp_named_subst' =
365             substaux_in_exp_named_subst params exp_named_subst m 
366            in
367             C.Var (uri,exp_named_subst')
368        | C.Meta (i,l) ->
369           let l' =
370            List.map
371             (function
372                 None -> None
373               | Some t -> Some (unwind_aux m t)
374             ) l
375           in
376            C.Meta (i, l')
377        | C.Sort _ as t -> t
378        | C.Implicit as t -> t
379        | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
380        | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
381        | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
382        | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
383        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
384        | C.Const (uri,exp_named_subst) ->
385           let params =
386            (match CicEnvironment.get_obj uri with
387                C.Constant (_,_,_,params) -> params
388              | C.Variable _ -> raise ReferenceToVariable
389              | C.CurrentProof (_,_,_,_,params) -> params
390              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
391            )
392           in
393            let exp_named_subst' =
394             substaux_in_exp_named_subst params exp_named_subst m 
395            in
396             C.Const (uri,exp_named_subst')
397        | C.MutInd (uri,i,exp_named_subst) ->
398           let params =
399            (match CicEnvironment.get_obj uri with
400                C.Constant _ -> raise ReferenceToConstant
401              | C.Variable _ -> raise ReferenceToVariable
402              | C.CurrentProof _ -> raise ReferenceToCurrentProof
403              | C.InductiveDefinition (_,params,_) -> params
404            )
405           in
406            let exp_named_subst' =
407             substaux_in_exp_named_subst params exp_named_subst m 
408            in
409             C.MutInd (uri,i,exp_named_subst')
410        | C.MutConstruct (uri,i,j,exp_named_subst) ->
411           let params =
412            (match CicEnvironment.get_obj uri with
413                C.Constant _ -> raise ReferenceToConstant
414              | C.Variable _ -> raise ReferenceToVariable
415              | C.CurrentProof _ -> raise ReferenceToCurrentProof
416              | C.InductiveDefinition (_,params,_) -> params
417            )
418           in
419            let exp_named_subst' =
420             substaux_in_exp_named_subst params exp_named_subst m 
421            in
422             C.MutConstruct (uri,i,j,exp_named_subst')
423        | C.MutCase (sp,i,outt,t,pl) ->
424           C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
425            List.map (unwind_aux m) pl)
426        | C.Fix (i,fl) ->
427           let len = List.length fl in
428           let substitutedfl =
429            List.map
430             (fun (name,i,ty,bo) ->
431               (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
432              fl
433           in
434            C.Fix (i, substitutedfl)
435        | C.CoFix (i,fl) ->
436           let len = List.length fl in
437           let substitutedfl =
438            List.map
439             (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
440              fl
441           in
442            C.CoFix (i, substitutedfl)
443      and substaux_in_exp_named_subst params exp_named_subst' m  =
444   (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
445       let ens' =
446        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
447   (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
448         List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
449       in
450       let rec filter_and_lift =
451        function
452           [] -> []
453         | uri::tl ->
454            let r = filter_and_lift tl in
455             (try
456               (uri,(List.assq uri ens'))::r
457              with
458               Not_found -> r
459             )
460       in
461        filter_and_lift params
462   *)
463   
464   (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
465   (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
466   
467   (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
468   (*CSC: codice altamente inefficiente *)
469       let rec filter_and_lift already_instantiated =
470        function
471           [] -> []
472         | (uri,t)::tl when
473             List.for_all
474              (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
475             &&
476              not (List.mem uri already_instantiated)
477             &&
478              List.mem uri params
479            ->
480             (uri,CicSubstitution.lift m (RS.from_ens t)) ::
481              (filter_and_lift (uri::already_instantiated) tl)
482         | _::tl -> filter_and_lift already_instantiated tl
483 (*
484         | (uri,_)::tl ->
485 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
486 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
487 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
488 if List.mem uri params then prerr_endline "---- OK2" ;
489         filter_and_lift tl
490 *)
491       in
492        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
493         (filter_and_lift [] (List.rev ens))
494      in
495       unwind_aux m t          
496   ;;
497   
498   let unwind =
499    unwind' 0 
500   ;;
501   
502   let reduce context : config -> Cic.term = 
503    let module C = Cic in
504    let module S = CicSubstitution in 
505    let rec reduce =
506     function
507        (k, e, _, (C.Rel n as t), s) ->
508         let d =
509          try
510           Some (RS.from_env (List.nth e (n-1)))
511          with
512           _ ->
513            try
514             begin
515              match List.nth context (n - 1 - k) with
516                 None -> assert false
517               | Some (_,C.Decl _) -> None
518               | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
519             end
520            with
521             _ -> None
522         in
523          (match d with 
524              Some t' -> reduce (0,[],[],t',s)
525            | None ->
526               if s = [] then
527                C.Rel (n-k)
528               else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
529          )
530      | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) -> 
531          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
532           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
533          else
534           (match CicEnvironment.get_obj uri with
535               C.Constant _ -> raise ReferenceToConstant
536             | C.CurrentProof _ -> raise ReferenceToCurrentProof
537             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
538             | C.Variable (_,None,_,_) ->
539                let t' = unwind k e ens t in
540                 if s = [] then t' else
541                  C.Appl (t'::(RS.from_stack_list ~unwind s))
542             | C.Variable (_,Some body,_,_) ->
543                let ens' = push_exp_named_subst k e ens exp_named_subst in
544                 reduce (0, [], ens', body, s)
545           )
546      | (k, e, ens, (C.Meta _ as t), s) ->
547         let t' = unwind k e ens t in
548          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
549      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
550      | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *)
551      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
552         reduce (k, e, ens, te, s) (* s should be empty *)
553      | (k, e, ens, (C.Prod _ as t), s) ->
554          unwind k e ens t (* s should be empty *)
555      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' 
556      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
557          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
558      | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
559         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
560          reduce (k+1, m'::e, ens, t, s)
561      | (_, _, _, C.Appl [], _) -> raise (Impossible 1)
562      | (k, e, ens, C.Appl (he::tl), s) ->
563         let tl' =
564          List.map
565           (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
566         in
567          reduce (k, e, ens, he, (List.append tl') s)
568   (* CSC: Old Dead Code 
569      | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) 
570      | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)  
571      | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) 
572      | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
573   (* strict evaluation, but constants are NOT unfolded *)
574         let red =
575          function
576             C.Const _ as t -> unwind k e ens t
577           | t -> reduce (k,e,ens,t,[])
578         in
579          let tl' = List.map red tl in
580           reduce (k, e, ens, he , List.append tl' s)
581      | (k, e, ens, C.Appl l, s) ->
582          C.Appl (List.append (List.map (unwind k e ens) l) s)
583   *)
584      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
585         (match CicEnvironment.get_obj uri with
586             C.Constant (_,Some body,_,_) ->
587              let ens' = push_exp_named_subst k e ens exp_named_subst in
588               (* constants are closed *)
589               reduce (0, [], ens', body, s) 
590           | C.Constant (_,None,_,_) ->
591              let t' = unwind k e ens t in
592               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
593           | C.Variable _ -> raise ReferenceToVariable
594           | C.CurrentProof (_,_,body,_,_) ->
595              let ens' = push_exp_named_subst k e ens exp_named_subst in
596               (* constants are closed *)
597               reduce (0, [], ens', body, s)
598           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
599         )
600      | (k, e, ens, (C.MutInd _ as t),s) ->
601         let t' = unwind k e ens t in 
602          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
603      | (k, e, ens, (C.MutConstruct _ 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.MutCase (mutind,i,_,term,pl) as t),s) ->
607         let decofix =
608          function
609             C.CoFix (i,fl) as t ->
610              let (_,_,body) = List.nth fl i in
611               let body' =
612                let counter = ref (List.length fl) in
613                 List.fold_right
614                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
615                  fl
616                  body
617               in
618                (* the term is the result of a reduction; *)
619                (* so it is already unwinded.             *)
620                reduce (0,[],[],body',[])
621           | C.Appl (C.CoFix (i,fl) :: tl) ->
622              let (_,_,body) = List.nth fl i in
623               let body' =
624                let counter = ref (List.length fl) in
625                 List.fold_right
626                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
627                  fl
628                  body
629               in
630                (* the term is the result of a reduction; *)
631                (* so it is already unwinded.             *)
632                reduce (0,[],[],body',RS.to_stack_list tl)
633           | t -> t
634         in
635          (match decofix (reduce (k,e,ens,term,[])) with
636              C.MutConstruct (_,_,j,_) ->
637               reduce (k, e, ens, (List.nth pl (j-1)), s)
638            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
639               let (arity, r) =
640                match CicEnvironment.get_obj mutind with
641                   C.InductiveDefinition (tl,ingredients,r) ->
642                     let (_,_,arity,_) = List.nth tl i in
643                      (arity,r)
644                 | _ -> raise WrongUriToInductiveDefinition
645               in
646                let ts =
647                 let num_to_eat = r in
648                  let rec eat_first =
649                   function
650                      (0,l) -> l
651                    | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
652                    | _ -> raise (Impossible 5)
653                  in
654                   eat_first (num_to_eat,tl)
655                in
656                 (* ts are already unwinded because they are a sublist of tl *)
657                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
658            | C.Cast _ | C.Implicit ->
659               raise (Impossible 2) (* we don't trust our whd ;-) *)
660            | _ ->
661              let t' = unwind k e ens t in
662               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
663          )
664      | (k, e, ens, (C.Fix (i,fl) as t), s) ->
665         let (_,recindex,_,body) = List.nth fl i in
666          let recparam =
667           try
668            Some (RS.from_stack ~unwind (List.nth s recindex))
669           with
670            _ -> None
671          in
672           (match recparam with
673               Some recparam ->
674                (match reduce (0,[],[],recparam,[]) with
675                    (* match recparam with *) 
676                    C.MutConstruct _
677                  | C.Appl ((C.MutConstruct _)::_) ->
678                     (* OLD 
679                     let body' =
680                      let counter = ref (List.length fl) in
681                       List.fold_right
682                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
683                        fl
684                        body
685                     in 
686                      reduce (k, e, ens, body', s) *)
687                     (* NEW *)
688                     let leng = List.length fl in
689                     let fl' = 
690                      let unwind_fl (name,recindex,typ,body) = 
691                       (name,recindex,unwind k e ens typ,
692                         unwind' leng k e ens body)
693                      in
694                       List.map unwind_fl fl
695                     in
696                      let new_env =
697                       let counter = ref 0 in
698                       let rec build_env e =
699                        if !counter = leng then e
700                        else
701                         (incr counter ;
702                          build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
703                       in
704                        build_env e
705                      in
706                       reduce (k+leng, new_env, ens, body, s)  
707                  | _ ->
708                    let t' = unwind k e ens t in 
709                     if s = [] then t' else
710                      C.Appl (t'::(RS.from_stack_list ~unwind s))
711                )
712             | None ->
713                let t' = unwind k e ens t in 
714                 if s = [] then t' else
715                  C.Appl (t'::(RS.from_stack_list ~unwind s))
716           )
717      | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
718         let t' = unwind k e ens t in 
719          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
720    and push_exp_named_subst k e ens =
721     function
722        [] -> ens
723      | (uri,t)::tl ->
724          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
725    in
726     reduce
727   ;;
728   
729   let rec whd context t = reduce context (0, [], [], t, []);;
730   
731 (* DEBUGGING ONLY
732 let whd context t =
733  let res = whd context t in
734  let rescsc = CicReductionNaif.whd context t in
735   if not (CicReductionNaif.are_convertible context res rescsc) then
736    begin
737     prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
738     flush stderr ;
739     prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
740     flush stderr ;
741     prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
742     flush stderr ;
743 CicReductionNaif.fdebug := 0 ;
744 let _ =  CicReductionNaif.are_convertible context res rescsc in
745     assert false ;
746    end
747   else 
748    res
749 ;;
750 *)
751  end
752 ;;
753
754
755 (*
756 module R = Reduction CallByNameStrategy;;
757 module R = Reduction CallByValueStrategy;;
758 module R = Reduction CallByValueStrategyByNameOnConstants;;
759 module R = Reduction LazyCallByValueStrategy;;
760 module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
761 module R = Reduction LazyCallByNameStrategy;;
762 module R = Reduction
763  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
764 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
765 module R = Reduction
766  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
767 *)
768 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
769
770 let whd = R.whd;;
771
772 (* t1, t2 must be well-typed *)
773 let are_convertible =
774  let module U = UriManager in
775  let rec aux context t1 t2 =
776   let aux2 t1 t2 =
777    (* this trivial euristic cuts down the total time of about five times ;-) *)
778    (* this because most of the time t1 and t2 are "sintactically" the same   *)
779    if t1 = t2 then
780     true
781    else
782     begin
783      let module C = Cic in
784        match (t1,t2) with
785           (C.Rel n1, C.Rel n2) -> n1 = n2
786         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
787             U.eq uri1 uri2 &&
788              (try
789                List.fold_right2
790                 (fun (uri1,x) (uri2,y) b ->
791                   U.eq uri1 uri2 && aux context x y && b
792                 ) exp_named_subst1 exp_named_subst2 true 
793               with
794                Invalid_argument _ -> false
795              )
796         | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
797             n1 = n2 &&
798              List.fold_left2
799               (fun b t1 t2 ->
800                 b &&
801                  match t1,t2 with
802                     None,_
803                   | _,None  -> true
804                   | Some t1',Some t2' -> aux context t1' t2'
805               ) true l1 l2
806         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
807         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
808            aux context s1 s2 &&
809             aux ((Some (name1, (C.Decl s1)))::context) t1 t2
810         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
811            aux context s1 s2 &&
812             aux ((Some (name1, (C.Decl s1)))::context) t1 t2
813         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
814            aux context s1 s2 &&
815             aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2
816         | (C.Appl l1, C.Appl l2) ->
817            (try
818              List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
819             with
820              Invalid_argument _ -> false
821            )
822         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
823             U.eq uri1 uri2 &&
824              (try
825                List.fold_right2
826                 (fun (uri1,x) (uri2,y) b ->
827                   U.eq uri1 uri2 && aux context x y && b
828                 ) exp_named_subst1 exp_named_subst2 true 
829               with
830                Invalid_argument _ -> false
831              )
832         | (C.MutInd (uri1,i1,exp_named_subst1),
833            C.MutInd (uri2,i2,exp_named_subst2)
834           ) ->
835             U.eq uri1 uri2 && i1 = i2 &&
836              (try
837                List.fold_right2
838                 (fun (uri1,x) (uri2,y) b ->
839                   U.eq uri1 uri2 && aux context x y && b
840                 ) exp_named_subst1 exp_named_subst2 true 
841               with
842                Invalid_argument _ -> false
843              )
844         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
845            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
846           ) ->
847             U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
848              (try
849                List.fold_right2
850                 (fun (uri1,x) (uri2,y) b ->
851                   U.eq uri1 uri2 && aux context x y && b
852                 ) exp_named_subst1 exp_named_subst2 true 
853               with
854                Invalid_argument _ -> false
855              )
856         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
857            C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
858             U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 &&
859              aux context term1 term2 &&
860              List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true
861         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
862            let tys =
863             List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
864            in
865             i1 = i2 &&
866              List.fold_right2
867               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
868                 b && recindex1 = recindex2 && aux context ty1 ty2 &&
869                  aux (tys@context) bo1 bo2)
870               fl1 fl2 true
871         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
872            let tys =
873             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
874            in
875             i1 = i2 &&
876              List.fold_right2
877               (fun (_,ty1,bo1) (_,ty2,bo2) b ->
878                 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
879               fl1 fl2 true
880         | (C.Cast _, _) | (_, C.Cast _)
881         | (C.Implicit, _) | (_, C.Implicit) ->
882            raise (Impossible 3) (* we don't trust our whd ;-) *)
883         | (_,_) -> false
884     end
885   in
886    if aux2 t1 t2 then true
887    else
888     begin
889      debug t1 [t2] "PREWHD";
890      let t1' = whd context t1 in
891      let t2' = whd context t2 in
892       debug t1' [t2'] "POSTWHD";
893       aux2 t1' t2'
894     end
895  in
896   aux
897 ;;