]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/nCicReduction.ml
added mk_fix i j r that given an r of a fix generated another fix on i and j
[helm.git] / helm / software / components / ng_kernel / nCicReduction.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 (* TODO unify exceptions *)
15
16 exception WrongUriToInductiveDefinition;;
17 exception Impossible of int;;
18 exception ReferenceToConstant;;
19 exception ReferenceToVariable;;
20 exception ReferenceToCurrentProof;;
21 exception ReferenceToInductiveDefinition;;
22
23 let debug = false
24 let profile = false
25 let debug_print s = if debug then prerr_endline (Lazy.force s)
26
27 let fdebug = ref 1;;
28 let debug t env s =
29  let rec debug_aux t i =
30   let module C = Cic in
31   let module U = UriManager in
32    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
33  in
34   if !fdebug = 0 then
35    debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
36 ;;
37
38 module type Strategy =
39  sig
40   type stack_term
41   type env_term
42   type config = int * env_term list * NCic.term * stack_term list
43   val to_env :
44    reduce: (config -> config) ->
45    unwind: (config -> NCic.term) ->
46    config -> env_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) ->
54    env_term -> NCic.term
55   val stack_to_env :
56    reduce: (config -> config) ->
57    unwind: (config -> NCic.term) ->
58    stack_term -> env_term
59   val compute_to_env :
60    reduce: (config -> config) ->
61    unwind: (config -> NCic.term) ->
62    int -> env_term list -> 
63     NCic.term -> env_term
64   val compute_to_stack :
65    reduce: (config -> config) ->
66    unwind: (config -> NCic.term) ->
67    config -> stack_term
68  end
69 ;;
70
71 module CallByValueByNameForUnwind' =
72  struct
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)
87  end
88 ;;
89
90
91 (* {{{ module CallByValueByNameForUnwind =
92  struct
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 *)
97
98   let to_env c = c,c
99   let to_ens c = c,c
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
109  end
110 ;;
111
112
113 (* Old Machine *)
114 module CallByNameStrategy =
115  struct
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
120   let to_env v = v
121   let to_ens v = v
122   let from_stack ~unwind v = v
123   let from_stack_list ~unwind l = l
124   let from_env v = v
125   let from_ens v = v
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
131  end
132 ;;
133
134 module CallByNameStrategy =
135  struct
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
140
141   let to_env c = c
142   let to_ens c = c
143   let from_stack config = config
144   let from_stack_list_for_unwind ~unwind l = List.map unwind l
145   let from_env c = c
146   let from_ens c = c
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
152  end
153 ;;
154
155 module CallByValueStrategy =
156  struct
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
161   let to_env v = v
162   let to_ens v = v
163   let from_stack ~unwind v = v
164   let from_stack_list ~unwind l = l
165   let from_env v = v
166   let from_ens v = v
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,[])
172  end
173 ;;
174
175 module CallByValueStrategyByNameOnConstants =
176  struct
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
181   let to_env v = v
182   let to_ens v = v
183   let from_stack ~unwind v = v
184   let from_stack_list ~unwind l = l
185   let from_env v = v
186   let from_ens v = v
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 =
191    function
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 =
195    function
196       Cic.Const _ as t -> unwind k e ens t    
197     | t -> reduce (k,e,ens,t,[])
198  end
199 ;;
200
201 module LazyCallByValueStrategy =
202  struct
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,[]))
218  end
219 ;;
220
221 module LazyCallByValueStrategyByNameOnConstants =
222  struct
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 =
237    lazy (
238     match t with
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 =
242    lazy (
243     match t with
244        Cic.Const _ as t -> unwind k e ens t    
245      | t -> reduce (k,e,ens,t,[]))
246  end
247 ;;
248
249 module LazyCallByNameStrategy =
250  struct
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)
266  end
267 ;;
268
269 module
270  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
271 =
272  struct
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
277   let to_env v =
278    let value = lazy v in
279     fun ~reduce -> Lazy.force value
280   let to_ens v =
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 =
291    let svalue =
292      lazy (
293       match t with
294          Cic.Const _ as t -> unwind k e ens t    
295        | t -> reduce (k,e,ens,t,[])
296      ) in
297    let lvalue =
298     lazy (unwind k e ens t)
299    in
300     fun ~reduce ->
301      if reduce then Lazy.force svalue else Lazy.force lvalue
302   let compute_to_env ~reduce ~unwind k e ens t =
303    let svalue =
304      lazy (
305       match t with
306          Cic.Const _ as t -> unwind k e ens t    
307        | t -> reduce (k,e,ens,t,[])
308      ) in
309    let lvalue =
310     lazy (unwind k e ens t)
311    in
312     fun ~reduce ->
313      if reduce then Lazy.force svalue else Lazy.force lvalue
314  end
315 ;;
316
317 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
318  struct
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
323
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
328   let from_env v = v
329   let from_ens v = v
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
335  end
336 ;;
337
338 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
339  struct
340   type stack_term =
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
345   let to_env v = v
346   let to_ens v = v
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
349   let from_env v = v
350   let from_ens v = v
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) =
354    match t with
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 =
358    unwind k e ens t
359   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
360  end
361 ;;
362
363 }}} *)
364
365 module Reduction(RS : Strategy) =
366  struct
367   type env = RS.env_term list
368   type stack = RS.stack_term list
369   type config = int * env * NCic.term * stack
370
371   let rec unwind (k,e,t,s) =
372     let t = 
373       if k = 0 then t 
374       else 
375         NCicSubstitution.psubst ~avoid_beta_redexes:true  
376           true 0 (RS.from_env_for_unwind ~unwind) e t
377     in
378     if s = [] then t 
379     else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
380   ;;
381
382   let list_nth l n = try List.nth l n with Failure _ -> assert false;;
383   let rec replace i s t =
384     match i,s with
385     |  0,_::tl -> t::tl
386     | n,he::tl -> he::(replace (n - 1) tl t)
387     | _,_ -> assert false
388   ;;
389
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
394         aux (k',e',t',s'@s)
395      | k, _, NCic.Rel n, s as config (* when n > k *) ->
396         (match List.nth context (n - 1 - k) with
397         | (_,NCic.Decl _) -> config
398         | (_,NCic.Def (x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s))
399      | (k, e, NCic.Meta (n,l), s) as config ->
400         (try 
401            let _,_, term,_ = NCicUtils.lookup_subst n subst in
402            aux (k, e, NCicSubstitution.subst_meta l term,s)
403          with  NCicUtils.Subst_not_found _ -> config)
404      | (_, _, NCic.Sort _, _) as config -> config
405      | (_, _, NCic.Implicit _, _) -> assert false
406      | (_, _, NCic.Prod _, _) as config -> config
407      | (_, _, NCic.Lambda _, []) as config -> config
408      | (k, e, NCic.Lambda (_,_,t), p::s) ->
409          aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
410      | (k, e, NCic.LetIn (_,_,m,t), s) ->
411         let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
412          aux (k+1, m'::e, t, s)
413      | (_, _, NCic.Appl [], _) -> assert false
414      | (k, e, NCic.Appl (he::tl), s) ->
415         let tl' =
416          List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
417         in
418          aux (k, e, he, tl' @ s)
419      | (_, _, NCic.Const
420             (NReference.Ref (_,_,NReference.Def) as refer), s) as config ->
421          let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
422          if delta > height then config else aux (0, [], body, s) 
423      | (_, _, NCic.Const (NReference.Ref 
424                (_,_,NReference.Fix (_,recindex)) as refer),s) as config ->
425         let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in
426         if delta > height then config else
427         (match
428           try Some (RS.from_stack (List.nth s recindex))
429           with Failure _ -> None
430         with 
431         | None -> config
432         | Some recparam ->
433            match reduce ~delta:0 ~subst context recparam with
434            | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
435                let new_s =
436                  replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
437                in
438                aux (0, [], body, new_s)
439            | _ -> config)
440      | (_, _, NCic.Const _, _) as config -> config
441      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
442         let decofix = function
443           | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix _)as refer),s)->
444              let _,_,body,_,_,_ = NCicEnvironment.get_checked_cofix refer in
445              reduce ~delta:0 ~subst context (0,[],body,s)
446           | config -> config
447         in
448         (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
449         | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) ->
450             aux (k, e, List.nth pl (j-1), s)
451         | (_, _, NCic.Const 
452              (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') ->
453           let leftno = NCicEnvironment.get_indty_leftno refer in
454           let _,params = HExtlib.split_nth leftno s' in
455           aux (k, e, List.nth pl (j-1), params@s)
456         | _ -> config)
457    in
458     aux
459   ;;
460
461   let whd ?(delta=0) ?(subst=[]) context t = 
462    unwind (reduce ~delta ~subst context (0, [], t, []))
463   ;;
464
465  end
466 ;;
467
468
469 (* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
470            senza ridurre la testa
471 module R = Reduction CallByNameStrategy;; OK 56.368s
472 module R = Reduction CallByValueStrategy;; ROTTO
473 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
474 module R = Reduction LazyCallByValueStrategy;; ROTTO
475 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
476 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
477 module R = Reduction
478  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
479  OK 59.058s
480 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
481 module R = Reduction
482  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
483 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
484 module R = Reduction(CallByValueByNameForUnwind);; 
485 module R = Reduction(CallByNameStrategy);;
486 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
487 module RS = CallByValueByNameForUnwind';;
488
489 module R = Reduction(RS);;
490 module U = UriManager;;
491
492 let whd = R.whd
493
494 (*
495 let whd =
496  let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
497   fun ?(delta=true) ?(subst=[]) context t ->
498    profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
499 *)
500
501 (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
502  * fallbacks to structural equality *)
503 let (===) x y = Pervasives.compare x y = 0 ;;
504
505 module C = NCic
506
507 (* t1, t2 must be well-typed *)
508 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
509  let rec aux test_equality_only context t1 t2 =
510    let rec aux2 test_equality_only t1 t2 =
511      if t1 === t2 then
512        true
513      else
514        match (t1,t2) with
515        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
516        | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
517        | (C.Sort s1, C.Sort s2) -> s1 = s2
518
519        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
520            aux true context s1 s2 &&
521            aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
522        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
523           aux true context s1 s2 && 
524           aux true ((name1, C.Decl s1)::context) t1 t2
525        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
526           aux test_equality_only context ty1 ty2 &&
527           aux test_equality_only context s1 s2 &&
528           aux test_equality_only ((name1, C.Def (s1,ty1))::context) t1 t2
529
530        | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2))) 
531           when n1 = n2 && s1 = s2 -> true
532        | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 -> 
533           let l1 = NCicUtils.expand_local_context l1 in
534           let l2 = NCicUtils.expand_local_context l2 in
535           (try List.for_all2 
536             (fun t1 t2 -> aux test_equality_only context 
537               (NCicSubstitution.lift s1 t1) 
538               (NCicSubstitution.lift s2 t2))  
539             l1 l2
540           with Invalid_argument _ -> false)
541
542        | C.Meta (n1,l1), _ ->
543           (try 
544              let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
545              let term = NCicSubstitution.subst_meta l1 term in
546               aux test_equality_only context term t2
547            with NCicUtils.Subst_not_found _ -> false)
548        | _, C.Meta (n2,l2) ->
549           (try 
550              let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
551              let term = NCicSubstitution.subst_meta l2 term in
552               aux test_equality_only context t1 term
553            with NCicUtils.Subst_not_found _ -> false)
554
555        | (C.Appl l1, C.Appl l2) ->
556           (try List.for_all2 (aux test_equality_only context) l1 l2
557            with Invalid_argument _ -> false)
558
559        | (C.Match (ref1,outtype1,term1,pl1),
560           C.Match (ref2,outtype2,term2,pl2)) -> 
561            NReference.eq ref1 ref2 &&
562            aux test_equality_only context outtype1 outtype2 &&
563            aux test_equality_only context term1 term2 &&
564            (try List.for_all2 (aux test_equality_only context) pl1 pl2
565             with Invalid_argument _ -> false)
566
567        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
568        | (_,_) -> false
569   in
570    if aux2 test_equality_only t1 t2 then 
571      true
572    else
573      let rec convert_machines = function
574       | [] -> true
575       | ((k1,env1,h1,s1),(k2,env2,h2,s2))::tl ->
576           aux2 test_equality_only
577            (R.unwind (k1,env1,h1,[])) (R.unwind (k2,env2,h2,[])) &&
578           let problems =
579            let red_stack =
580              List.map
581                (fun si-> R.reduce ~delta:0 ~subst context(RS.from_stack si))
582            in
583            try Some (List.combine (red_stack s1) (red_stack s2) @ tl)
584            with Invalid_argument _ -> None
585           in
586           match problems with
587            | None -> false
588            | Some problems -> convert_machines problems
589      in
590       convert_machines 
591        [R.reduce ~delta:0 ~subst context (0,[],t1,[]),
592         R.reduce ~delta:0 ~subst context (0,[],t2,[])]
593  in
594   aux false 
595 ;;
596
597 let are_convertible = are_convertible whd
598
599 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
600  match upto, t, l with
601   | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
602   | 0, t, [] -> t
603   | 0, t, _ -> C.Appl (t::l)
604   | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
605   | _, C.Lambda(_,_,bo), arg::tl ->
606      let bo = NCicSubstitution.subst arg bo in
607      head_beta_reduce ~delta ~upto:(upto - 1) bo tl
608   | _, C.Const (NReference.Ref (height, _, NReference.Def) as re), _ 
609     when delta <= height ->
610       let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
611       head_beta_reduce ~upto ~delta bo l
612   | _, t, [] -> t
613   | _, t, _ -> C.Appl (t::l)
614 ;;
615
616 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
617
618 (* vim:set foldmethod=marker: *)