]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/proofEngineReduction.ml
Huge commit for the release. Includes:
[helm.git] / helm / software / components / tactics / proofEngineReduction.ml
1 (* Copyright (C) 2002, 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 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 12/04/2002                                 *)
32 (*                                                                            *)
33 (*                                                                            *)
34 (******************************************************************************)
35
36 (* $Id$ *)
37
38 (* The code of this module is derived from the code of CicReduction *)
39
40 exception Impossible of int;;
41 exception ReferenceToConstant;;
42 exception ReferenceToVariable;;
43 exception ReferenceToCurrentProof;;
44 exception ReferenceToInductiveDefinition;;
45 exception WrongUriToInductiveDefinition;;
46 exception WrongUriToConstant;;
47 exception RelToHiddenHypothesis;;
48
49 let alpha_equivalence =
50  let module C = Cic in
51   let rec aux t t' =
52    if t = t' then true
53    else
54     match t,t' with
55        C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
56         UriManager.eq uri1 uri2 &&
57          aux_exp_named_subst exp_named_subst1 exp_named_subst2
58      | C.Cast (te,ty), C.Cast (te',ty') ->
59         aux te te' && aux ty ty'
60      | C.Prod (_,s,t), C.Prod (_,s',t') ->
61         aux s s' && aux t t'
62      | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
63         aux s s' && aux t t'
64      | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
65         aux s s' && aux t t'
66      | C.Appl l, C.Appl l' ->
67         (try
68           List.fold_left2
69            (fun b t1 t2 -> b && aux t1 t2) true l l'
70          with
71           Invalid_argument _ -> false)
72      | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
73         UriManager.eq uri uri' &&
74          aux_exp_named_subst exp_named_subst1 exp_named_subst2
75      | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
76         UriManager.eq uri uri' && i = i' &&
77          aux_exp_named_subst exp_named_subst1 exp_named_subst2
78      | C.MutConstruct (uri,i,j,exp_named_subst1),
79        C.MutConstruct (uri',i',j',exp_named_subst2) ->
80         UriManager.eq uri uri' && i = i' && j = j' &&
81          aux_exp_named_subst exp_named_subst1 exp_named_subst2
82      | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
83         UriManager.eq sp sp' && i = i' &&
84          aux outt outt' && aux t t' &&
85           (try
86             List.fold_left2
87              (fun b t1 t2 -> b && aux t1 t2) true pl pl'
88            with
89             Invalid_argument _ -> false)
90      | C.Fix (i,fl), C.Fix (i',fl') ->
91         i = i' &&
92         (try
93           List.fold_left2
94            (fun b (_,i,ty,bo) (_,i',ty',bo') ->
95              b && i = i' && aux ty ty' && aux bo bo'
96            ) true fl fl'
97          with
98           Invalid_argument _ -> false)
99      | C.CoFix (i,fl), C.CoFix (i',fl') ->
100         i = i' &&
101         (try
102           List.fold_left2
103            (fun b (_,ty,bo) (_,ty',bo') ->
104              b && aux ty ty' && aux bo bo'
105            ) true fl fl'
106          with
107           Invalid_argument _ -> false)
108      | _,_ -> false (* we already know that t != t' *)
109   and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
110    try
111      List.fold_left2
112       (fun b (uri1,t1) (uri2,t2) ->
113         b && UriManager.eq uri1 uri2 && aux t1 t2
114       ) true exp_named_subst1 exp_named_subst2
115     with
116      Invalid_argument _ -> false
117   in
118    aux
119 ;;
120
121 exception WhatAndWithWhatDoNotHaveTheSameLength;;
122
123 (* "textual" replacement of several subterms with other ones *)
124 let replace ~equality ~what ~with_what ~where =
125  let module C = Cic in
126   let find_image t =
127    let rec find_image_aux =
128     function
129        [],[] -> raise Not_found
130      | what::tl1,with_what::tl2 ->
131         if equality what t then with_what else find_image_aux (tl1,tl2)
132      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
133    in
134     find_image_aux (what,with_what)
135   in
136   let rec aux t =
137    try
138     find_image t
139    with Not_found ->
140     match t with
141        C.Rel _ -> t
142      | C.Var (uri,exp_named_subst) ->
143         C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
144      | C.Meta _ -> t
145      | C.Sort _ -> t
146      | C.Implicit _ as t -> t
147      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
148      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
149      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
150      | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
151      | C.Appl l ->
152         (* Invariant enforced: no application of an application *)
153         (match List.map aux l with
154             (C.Appl l')::tl -> C.Appl (l'@tl)
155           | l' -> C.Appl l')
156      | C.Const (uri,exp_named_subst) ->
157         C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
158      | C.MutInd (uri,i,exp_named_subst) ->
159         C.MutInd
160          (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
161      | C.MutConstruct (uri,i,j,exp_named_subst) ->
162         C.MutConstruct
163          (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
164      | C.MutCase (sp,i,outt,t,pl) ->
165         C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
166      | C.Fix (i,fl) ->
167         let substitutedfl =
168          List.map
169           (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
170            fl
171         in
172          C.Fix (i, substitutedfl)
173      | C.CoFix (i,fl) ->
174         let substitutedfl =
175          List.map
176           (fun (name,ty,bo) -> (name, aux ty, aux bo))
177            fl
178         in
179          C.CoFix (i, substitutedfl)
180    in
181     aux where
182 ;;
183
184 (* replaces in a term a term with another one. *)
185 (* Lifting are performed as usual.             *)
186 let replace_lifting ~equality ~what ~with_what ~where =
187  let module C = Cic in
188  let module S = CicSubstitution in
189   let find_image what t =
190    let rec find_image_aux =
191     function
192        [],[] -> raise Not_found
193      | what::tl1,with_what::tl2 ->
194         if equality what t then with_what else find_image_aux (tl1,tl2)
195      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
196    in
197     find_image_aux (what,with_what)
198   in
199   let rec substaux k what t =
200    try
201     S.lift (k-1) (find_image what t)
202    with Not_found ->
203     match t with
204       C.Rel n as t -> t
205     | C.Var (uri,exp_named_subst) ->
206        let exp_named_subst' =
207         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
208        in
209         C.Var (uri,exp_named_subst')
210     | C.Meta (i, l) -> 
211        let l' =
212         List.map
213          (function
214              None -> None
215            | Some t -> Some (substaux k what t)
216          ) l
217        in
218         C.Meta(i,l')
219     | C.Sort _ as t -> t
220     | C.Implicit _ as t -> t
221     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
222     | C.Prod (n,s,t) ->
223        C.Prod
224         (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
225     | C.Lambda (n,s,t) ->
226        C.Lambda
227         (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
228     | C.LetIn (n,s,t) ->
229        C.LetIn
230         (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
231     | C.Appl (he::tl) ->
232        (* Invariant: no Appl applied to another Appl *)
233        let tl' = List.map (substaux k what) tl in
234         begin
235          match substaux k what he with
236             C.Appl l -> C.Appl (l@tl')
237           | _ as he' -> C.Appl (he'::tl')
238         end
239     | C.Appl _ -> assert false
240     | C.Const (uri,exp_named_subst) ->
241        let exp_named_subst' =
242         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
243        in
244        C.Const (uri,exp_named_subst')
245     | C.MutInd (uri,i,exp_named_subst) ->
246        let exp_named_subst' =
247         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
248        in
249         C.MutInd (uri,i,exp_named_subst')
250     | C.MutConstruct (uri,i,j,exp_named_subst) ->
251        let exp_named_subst' =
252         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
253        in
254         C.MutConstruct (uri,i,j,exp_named_subst')
255     | C.MutCase (sp,i,outt,t,pl) ->
256        C.MutCase (sp,i,substaux k what outt, substaux k what t,
257         List.map (substaux k what) pl)
258     | C.Fix (i,fl) ->
259        let len = List.length fl in
260        let substitutedfl =
261         List.map
262          (fun (name,i,ty,bo) ->
263            (name, i, substaux k what ty,
264              substaux (k+len) (List.map (S.lift len) what) bo)
265          ) fl
266        in
267         C.Fix (i, substitutedfl)
268     | C.CoFix (i,fl) ->
269        let len = List.length fl in
270        let substitutedfl =
271         List.map
272          (fun (name,ty,bo) ->
273            (name, substaux k what ty,
274              substaux (k+len) (List.map (S.lift len) what) bo)
275          ) fl
276        in
277         C.CoFix (i, substitutedfl)
278  in
279   substaux 1 what where
280 ;;
281
282 (* replaces in a term a list of terms with other ones. *)
283 (* Lifting are performed as usual.                     *)
284 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
285  let module C = Cic in
286  let module S = CicSubstitution in
287   let find_image t =
288    let rec find_image_aux =
289     function
290        [],[] -> raise Not_found
291      | what::tl1,with_what::tl2 ->
292         if equality what t then with_what else find_image_aux (tl1,tl2)
293      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
294    in
295     find_image_aux (what,with_what)
296   in
297   let rec substaux k t =
298    try
299     S.lift (k-1) (find_image t)
300    with Not_found ->
301     match t with
302        C.Rel n ->
303         if n < k then C.Rel n else C.Rel (n + nnn)
304      | C.Var (uri,exp_named_subst) ->
305         let exp_named_subst' =
306          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
307         in
308          C.Var (uri,exp_named_subst')
309      | C.Meta (i, l) -> 
310         let l' =
311          List.map
312           (function
313               None -> None
314             | Some t -> Some (substaux k t)
315           ) l
316         in
317          C.Meta(i,l')
318      | C.Sort _ as t -> t
319      | C.Implicit _ as t -> t
320      | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
321      | C.Prod (n,s,t) ->
322         C.Prod (n, substaux k s, substaux (k + 1) t)
323      | C.Lambda (n,s,t) ->
324         C.Lambda (n, substaux k s, substaux (k + 1) t)
325      | C.LetIn (n,s,t) ->
326         C.LetIn (n, substaux k s, substaux (k + 1) t)
327      | C.Appl (he::tl) ->
328         (* Invariant: no Appl applied to another Appl *)
329         let tl' = List.map (substaux k) tl in
330          begin
331           match substaux k he with
332              C.Appl l -> C.Appl (l@tl')
333            | _ as he' -> C.Appl (he'::tl')
334          end
335      | C.Appl _ -> assert false
336      | C.Const (uri,exp_named_subst) ->
337         let exp_named_subst' =
338          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
339         in
340         C.Const (uri,exp_named_subst')
341      | C.MutInd (uri,i,exp_named_subst) ->
342         let exp_named_subst' =
343          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
344         in
345          C.MutInd (uri,i,exp_named_subst')
346      | C.MutConstruct (uri,i,j,exp_named_subst) ->
347         let exp_named_subst' =
348          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
349         in
350          C.MutConstruct (uri,i,j,exp_named_subst')
351      | C.MutCase (sp,i,outt,t,pl) ->
352         C.MutCase (sp,i,substaux k outt, substaux k t,
353          List.map (substaux k) pl)
354      | C.Fix (i,fl) ->
355         let len = List.length fl in
356         let substitutedfl =
357          List.map
358           (fun (name,i,ty,bo) ->
359             (name, i, substaux k ty, substaux (k+len) bo))
360            fl
361         in
362          C.Fix (i, substitutedfl)
363      | C.CoFix (i,fl) ->
364         let len = List.length fl in
365         let substitutedfl =
366          List.map
367           (fun (name,ty,bo) ->
368             (name, substaux k ty, substaux (k+len) bo))
369            fl
370         in
371          C.CoFix (i, substitutedfl)
372  in
373   substaux 1 where
374 ;;
375
376 (* Takes a well-typed term and fully reduces it. *)
377 (*CSC: It does not perform reduction in a Case *)
378 let reduce context =
379  let rec reduceaux context l =
380   let module C = Cic in
381   let module S = CicSubstitution in
382    function
383       C.Rel n as t ->
384        (match List.nth context (n-1) with
385            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
386          | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
387          | None -> raise RelToHiddenHypothesis
388        )
389     | C.Var (uri,exp_named_subst) ->
390        let exp_named_subst' =
391         reduceaux_exp_named_subst context l exp_named_subst
392        in
393        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
394          match o with
395            C.Constant _ -> raise ReferenceToConstant
396          | C.CurrentProof _ -> raise ReferenceToCurrentProof
397          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
398          | C.Variable (_,None,_,_,_) ->
399             let t' = C.Var (uri,exp_named_subst') in
400              if l = [] then t' else C.Appl (t'::l)
401          | C.Variable (_,Some body,_,_,_) ->
402             (reduceaux context l
403               (CicSubstitution.subst_vars exp_named_subst' body))
404        )
405     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
406     | C.Sort _ as t -> t (* l should be empty *)
407     | C.Implicit _ as t -> t
408     | C.Cast (te,ty) ->
409        C.Cast (reduceaux context l te, reduceaux context l ty)
410     | C.Prod (name,s,t) ->
411        assert (l = []) ;
412        C.Prod (name,
413         reduceaux context [] s,
414         reduceaux ((Some (name,C.Decl s))::context) [] t)
415     | C.Lambda (name,s,t) ->
416        (match l with
417            [] ->
418             C.Lambda (name,
419              reduceaux context [] s,
420              reduceaux ((Some (name,C.Decl s))::context) [] t)
421          | he::tl -> reduceaux context tl (S.subst he t)
422            (* when name is Anonimous the substitution should be superfluous *)
423        )
424     | C.LetIn (n,s,t) ->
425        reduceaux context l (S.subst (reduceaux context [] s) t)
426     | C.Appl (he::tl) ->
427        let tl' = List.map (reduceaux context []) tl in
428         reduceaux context (tl'@l) he
429     | C.Appl [] -> raise (Impossible 1)
430     | C.Const (uri,exp_named_subst) ->
431        let exp_named_subst' =
432         reduceaux_exp_named_subst context l exp_named_subst
433        in
434         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
435           match o with
436             C.Constant (_,Some body,_,_,_) ->
437              (reduceaux context l
438                (CicSubstitution.subst_vars exp_named_subst' body))
439           | C.Constant (_,None,_,_,_) ->
440              let t' = C.Const (uri,exp_named_subst') in
441               if l = [] then t' else C.Appl (t'::l)
442           | C.Variable _ -> raise ReferenceToVariable
443           | C.CurrentProof (_,_,body,_,_,_) ->
444              (reduceaux context l
445                (CicSubstitution.subst_vars exp_named_subst' body))
446           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
447         )
448     | C.MutInd (uri,i,exp_named_subst) ->
449        let exp_named_subst' =
450         reduceaux_exp_named_subst context l exp_named_subst
451        in
452         let t' = C.MutInd (uri,i,exp_named_subst') in
453          if l = [] then t' else C.Appl (t'::l)
454     | C.MutConstruct (uri,i,j,exp_named_subst) ->
455        let exp_named_subst' =
456         reduceaux_exp_named_subst context l exp_named_subst
457        in
458         let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
459          if l = [] then t' else C.Appl (t'::l)
460     | C.MutCase (mutind,i,outtype,term,pl) ->
461        let decofix =
462         function
463            C.CoFix (i,fl) ->
464              let (_,_,body) = List.nth fl i in
465               let body' =
466                let counter = ref (List.length fl) in
467                 List.fold_right
468                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
469                  fl
470                  body
471               in
472                reduceaux context [] body'
473          | C.Appl (C.CoFix (i,fl) :: tl) ->
474              let (_,_,body) = List.nth fl i in
475               let body' =
476                let counter = ref (List.length fl) in
477                 List.fold_right
478                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
479                  fl
480                  body
481               in
482                let tl' = List.map (reduceaux context []) tl in
483                 reduceaux context tl' body'
484          | t -> t
485        in
486         (match decofix (reduceaux context [] term) with
487             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
488           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
489              let (arity, r) =
490                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
491                  match o with
492                      C.InductiveDefinition (tl,_,r,_) ->
493                        let (_,_,arity,_) = List.nth tl i in
494                          (arity,r)
495                    | _ -> raise WrongUriToInductiveDefinition
496              in
497               let ts =
498                let rec eat_first =
499                 function
500                    (0,l) -> l
501                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
502                  | _ -> raise (Impossible 5)
503                in
504                 eat_first (r,tl)
505               in
506                reduceaux context (ts@l) (List.nth pl (j-1))
507          | C.Cast _ | C.Implicit _ ->
508             raise (Impossible 2) (* we don't trust our whd ;-) *)
509          | _ ->
510            let outtype' = reduceaux context [] outtype in
511            let term' = reduceaux context [] term in
512            let pl' = List.map (reduceaux context []) pl in
513             let res =
514              C.MutCase (mutind,i,outtype',term',pl')
515             in
516              if l = [] then res else C.Appl (res::l)
517        )
518     | C.Fix (i,fl) ->
519        let tys =
520         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
521        in
522         let t' () =
523          let fl' =
524           List.map
525            (function (n,recindex,ty,bo) ->
526              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
527            ) fl
528          in
529           C.Fix (i, fl')
530         in
531          let (_,recindex,_,body) = List.nth fl i in
532           let recparam =
533            try
534             Some (List.nth l recindex)
535            with
536             _ -> None
537           in
538            (match recparam with
539                Some recparam ->
540                 (match reduceaux context [] recparam with
541                     C.MutConstruct _
542                   | C.Appl ((C.MutConstruct _)::_) ->
543                      let body' =
544                       let counter = ref (List.length fl) in
545                        List.fold_right
546                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
547                         fl
548                         body
549                      in
550                       (* Possible optimization: substituting whd recparam in l*)
551                       reduceaux context l body'
552                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
553                 )
554              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
555            )
556     | C.CoFix (i,fl) ->
557        let tys =
558         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
559        in
560         let t' =
561          let fl' =
562           List.map
563            (function (n,ty,bo) ->
564              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
565            ) fl
566          in
567           C.CoFix (i, fl')
568         in
569          if l = [] then t' else C.Appl (t'::l)
570  and reduceaux_exp_named_subst context l =
571   List.map (function uri,t -> uri,reduceaux context [] t)
572  in
573   reduceaux context []
574 ;;
575
576 exception WrongShape;;
577 exception AlreadySimplified;;
578
579 (* Takes a well-typed term and                                               *)
580 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
581 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
582 (*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
583 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
584 (*     is applied again to the new redex; Step 3.1) is applied to the result *)
585 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
586 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
587 (*     not reduced. Otherwise, if the delta-residual is not the              *)
588 (*     lambda-abstraction of a Fix, then it performs step 3.2).              *)
589 (* 3.1) Folds the application of the constant to the arguments that did not  *)
590 (*     change in every iteration, i.e. to the actual arguments for the       *)
591 (*     lambda-abstractions that precede the Fix.                             *)
592 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries   *)
593 (*     reductions. If the reduction cannot be performed, it returns the      *)
594 (*     original term (not the head beta-zeta normal form of the definiendum) *)
595 (*CSC: It does not perform simplification in a Case *)
596
597 let simpl context =
598  let module C = Cic in
599  let module S = CicSubstitution in
600  (* a simplified term is active if it can create a redex when used as an *)
601  (* actual parameter                                                     *)
602  let rec is_active =
603   function
604      C.Lambda _
605    | C.MutConstruct _
606    | C.Appl (C.MutConstruct _::_)
607    | C.CoFix _ -> true
608    | C.Cast (bo,_) -> is_active bo
609    | C.LetIn _ -> assert false
610    | _ -> false
611  in
612  (* reduceaux is equal to the reduceaux locally defined inside *)
613  (* reduce, but for the const case.                            *) 
614  (**** Step 1 ****)
615  let rec reduceaux context l =
616    function
617       C.Rel n as t ->
618        (* we never perform delta expansion automatically *)
619        if l = [] then t else C.Appl (t::l)
620     | C.Var (uri,exp_named_subst) ->
621        let exp_named_subst' =
622         reduceaux_exp_named_subst context l exp_named_subst
623        in
624         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
625           match o with
626             C.Constant _ -> raise ReferenceToConstant
627           | C.CurrentProof _ -> raise ReferenceToCurrentProof
628           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
629           | C.Variable (_,None,_,_,_) ->
630             let t' = C.Var (uri,exp_named_subst') in
631              if l = [] then t' else C.Appl (t'::l)
632           | C.Variable (_,Some body,_,_,_) ->
633              reduceaux context l
634               (CicSubstitution.subst_vars exp_named_subst' body)
635         )
636     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
637     | C.Sort _ as t -> t (* l should be empty *)
638     | C.Implicit _ as t -> t
639     | C.Cast (te,ty) ->
640        C.Cast (reduceaux context l te, reduceaux context [] ty)
641     | C.Prod (name,s,t) ->
642        assert (l = []) ;
643        C.Prod (name,
644         reduceaux context [] s,
645         reduceaux ((Some (name,C.Decl s))::context) [] t)
646     | C.Lambda (name,s,t) ->
647        (match l with
648            [] ->
649             C.Lambda (name,
650              reduceaux context [] s,
651              reduceaux ((Some (name,C.Decl s))::context) [] t)
652          | he::tl -> reduceaux context tl (S.subst he t)
653            (* when name is Anonimous the substitution should be superfluous *)
654        )
655     | C.LetIn (n,s,t) ->
656        reduceaux context l (S.subst (reduceaux context [] s) t)
657     | C.Appl (he::tl) ->
658        let tl' = List.map (reduceaux context []) tl in
659         reduceaux context (tl'@l) he
660     | C.Appl [] -> raise (Impossible 1)
661     | C.Const (uri,exp_named_subst) ->
662        let exp_named_subst' =
663         reduceaux_exp_named_subst context l exp_named_subst
664        in
665         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
666           match o with
667            C.Constant (_,Some body,_,_,_) ->
668             if List.exists is_active l then
669              try_delta_expansion context l
670               (C.Const (uri,exp_named_subst'))
671               (CicSubstitution.subst_vars exp_named_subst' body)
672             else
673              let t' = C.Const (uri,exp_named_subst') in
674               if l = [] then t' else C.Appl (t'::l)
675          | C.Constant (_,None,_,_,_) ->
676             let t' = C.Const (uri,exp_named_subst') in
677              if l = [] then t' else C.Appl (t'::l)
678          | C.Variable _ -> raise ReferenceToVariable
679          | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
680          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
681        )
682     | C.MutInd (uri,i,exp_named_subst) ->
683        let exp_named_subst' =
684         reduceaux_exp_named_subst context l exp_named_subst
685        in
686         let t' = C.MutInd (uri,i,exp_named_subst') in
687          if l = [] then t' else C.Appl (t'::l)
688     | C.MutConstruct (uri,i,j,exp_named_subst) ->
689        let exp_named_subst' =
690         reduceaux_exp_named_subst context l exp_named_subst
691        in
692         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
693          if l = [] then t' else C.Appl (t'::l)
694     | C.MutCase (mutind,i,outtype,term,pl) ->
695        let decofix =
696         function
697            C.CoFix (i,fl) ->
698              let (_,_,body) = List.nth fl i in
699               let body' =
700                let counter = ref (List.length fl) in
701                 List.fold_right
702                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
703                  fl
704                  body
705               in
706                reduceaux context [] body'
707          | C.Appl (C.CoFix (i,fl) :: tl) ->
708              let (_,_,body) = List.nth fl i in
709              let body' =
710               let counter = ref (List.length fl) in
711                List.fold_right
712                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
713                 fl
714                 body
715              in
716               let tl' = List.map (reduceaux context []) tl in
717                reduceaux context tl' body'
718          | t -> t
719        in
720         (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
721             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
722           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
723              let (arity, r) =
724                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
725                  match o with
726                      C.InductiveDefinition (tl,ingredients,r,_) ->
727                        let (_,_,arity,_) = List.nth tl i in
728                          (arity,r)
729                    | _ -> raise WrongUriToInductiveDefinition
730              in
731               let ts =
732                let rec eat_first =
733                 function
734                    (0,l) -> l
735                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
736                  | _ -> raise (Impossible 5)
737                in
738                 eat_first (r,tl)
739               in
740                reduceaux context (ts@l) (List.nth pl (j-1))
741          | C.Cast _ | C.Implicit _ ->
742             raise (Impossible 2) (* we don't trust our whd ;-) *)
743          | _ ->
744            let outtype' = reduceaux context [] outtype in
745            let term' = reduceaux context [] term in
746            let pl' = List.map (reduceaux context []) pl in
747             let res =
748              C.MutCase (mutind,i,outtype',term',pl')
749             in
750              if l = [] then res else C.Appl (res::l)
751        )
752     | C.Fix (i,fl) ->
753        let tys =
754         List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
755        in
756         let t' () =
757          let fl' =
758           List.map
759            (function (n,recindex,ty,bo) ->
760              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
761            ) fl
762          in
763           C.Fix (i, fl')
764         in
765          let (_,recindex,_,body) = List.nth fl i in
766           let recparam =
767            try
768             Some (List.nth l recindex)
769            with
770             _ -> None
771           in
772            (match recparam with
773                Some recparam ->
774                 (match reduceaux context [] recparam with
775                     C.MutConstruct _
776                   | C.Appl ((C.MutConstruct _)::_) ->
777                      let body' =
778                       let counter = ref (List.length fl) in
779                        List.fold_right
780                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
781                         fl
782                         body
783                      in
784                       (* Possible optimization: substituting whd recparam in l*)
785                       reduceaux context l body'
786                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
787                 )
788              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
789            )
790     | C.CoFix (i,fl) ->
791        let tys =
792         List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
793        in
794         let t' =
795          let fl' =
796           List.map
797            (function (n,ty,bo) ->
798              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
799            ) fl
800          in
801          C.CoFix (i, fl')
802        in
803          if l = [] then t' else C.Appl (t'::l)
804  and reduceaux_exp_named_subst context l =
805   List.map (function uri,t -> uri,reduceaux context [] t)
806  (**** Step 2 ****)
807  and try_delta_expansion context l term body =
808   let module C = Cic in
809   let module S = CicSubstitution in
810    try
811     let res,constant_args =
812      let rec aux rev_constant_args l =
813       function
814          C.Lambda (name,s,t) ->
815           begin
816            match l with
817               [] -> raise WrongShape
818             | he::tl ->
819                (* when name is Anonimous the substitution should *)
820                (* be superfluous                                 *)
821                aux (he::rev_constant_args) tl (S.subst he t)
822           end
823        | C.LetIn (_,s,t) ->
824           aux rev_constant_args l (S.subst s t)
825        | C.Fix (i,fl) ->
826            let (_,recindex,_,body) = List.nth fl i in
827             let recparam =
828              try
829               List.nth l recindex
830              with
831               _ -> raise AlreadySimplified
832             in
833              (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
834                  C.MutConstruct _
835                | C.Appl ((C.MutConstruct _)::_) ->
836                   let body' =
837                    let counter = ref (List.length fl) in
838                     List.fold_right
839                      (function _ ->
840                        decr counter ; S.subst (C.Fix (!counter,fl))
841                      ) fl body
842                   in
843                    (* Possible optimization: substituting whd *)
844                    (* recparam in l                           *)
845                    reduceaux context l body',
846                     List.rev rev_constant_args
847                | _ -> raise AlreadySimplified
848              )
849        | _ -> raise WrongShape
850      in
851       aux [] l body
852     in
853      (**** Step 3.1 ****)
854      let term_to_fold, delta_expanded_term_to_fold =
855       match constant_args with
856          [] -> term,body
857        | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
858      in
859       let simplified_term_to_fold =
860        reduceaux context [] delta_expanded_term_to_fold
861       in
862        replace (=) [simplified_term_to_fold] [term_to_fold] res
863    with
864       WrongShape ->
865        (**** Step 3.2 ****)
866        let rec aux l =
867         function
868            C.Lambda (name,s,t) ->
869              (match l with
870                 [] -> raise AlreadySimplified
871               | he::tl ->
872                  (* when name is Anonimous the substitution should *)
873                  (* be superfluous                                 *)
874                  aux tl (S.subst he t))
875          | C.LetIn (_,s,t) -> aux l (S.subst s t)
876          | t ->
877             let simplified = reduceaux context l t in
878             let t' = if l = [] then t else C.Appl (t::l) in
879              if t' = simplified then
880               raise AlreadySimplified
881              else
882               simplified
883        in
884         (try aux l body
885          with
886           AlreadySimplified ->
887            if l = [] then term else C.Appl (term::l))
888     | AlreadySimplified ->
889        (* If we performed delta-reduction, we would find a Fix   *)
890        (* not applied to a constructor. So, we refuse to perform *)
891        (* delta-reduction.                                       *)
892        if l = [] then term else C.Appl (term::l)
893  in
894   reduceaux context []
895 ;;
896
897 let unfold ?what context where =
898  let contextlen = List.length context in
899  let first_is_the_expandable_head_of_second context' t1 t2 =
900   match t1,t2 with
901      Cic.Const (uri,_), Cic.Const (uri',_)
902    | Cic.Var (uri,_), Cic.Var (uri',_)
903    | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
904    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
905    | Cic.Const _, _
906    | Cic.Var _, _ -> false
907    | Cic.Rel n, Cic.Rel m
908    | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
909       n + (List.length context' - contextlen) = m
910    | Cic.Rel _, _ -> false
911    | _,_ ->
912      raise
913       (ProofEngineTypes.Fail
914         (lazy "The term to unfold is not a constant, a variable or a bound variable "))
915  in
916  let appl he tl =
917   if tl = [] then he else Cic.Appl (he::tl) in
918  let cannot_delta_expand t =
919   raise
920    (ProofEngineTypes.Fail
921      (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
922  let rec hd_delta_beta context tl =
923   function
924     Cic.Rel n as t ->
925      (try
926        match List.nth context (n-1) with
927           Some (_,Cic.Decl _) -> cannot_delta_expand t
928         | Some (_,Cic.Def (bo,_)) ->
929            CicReduction.head_beta_reduce
930             (appl (CicSubstitution.lift n bo) tl)
931         | None -> raise RelToHiddenHypothesis
932       with
933          Failure _ -> assert false)
934   | Cic.Const (uri,exp_named_subst) as t ->
935      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
936       (match o with
937           Cic.Constant (_,Some body,_,_,_) ->
938            CicReduction.head_beta_reduce
939             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
940         | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
941         | Cic.Variable _ -> raise ReferenceToVariable
942         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
943         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
944       )
945   | Cic.Var (uri,exp_named_subst) as t ->
946      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
947       (match o with
948           Cic.Constant _ -> raise ReferenceToConstant
949         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
950         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
951         | Cic.Variable (_,Some body,_,_,_) ->
952            CicReduction.head_beta_reduce
953             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
954         | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
955       )
956    | Cic.Appl [] -> assert false
957    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
958    | t -> cannot_delta_expand t
959  in
960  let context_and_matched_term_list =
961   match what with
962      None -> [context, where]
963    | Some what ->
964       let res =
965        ProofEngineHelpers.locate_in_term
966         ~equality:first_is_the_expandable_head_of_second
967         what ~where context
968       in
969        if res = [] then
970         raise
971          (ProofEngineTypes.Fail
972            (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
973        else
974         res
975  in
976   let reduced_terms =
977    List.map
978     (function (context,where) -> hd_delta_beta context [] where)
979     context_and_matched_term_list in
980   let whats = List.map snd context_and_matched_term_list in
981    replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
982 ;;