]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/proofEngineReduction.ml
More warnings.
[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 module C = Cic
50 module S = CicSubstitution
51
52 let debug = false
53 let prerr_endline =
54   if debug then prerr_endline else (fun x -> ())
55 ;;
56
57 exception WhatAndWithWhatDoNotHaveTheSameLength;;
58
59 (* Replaces "textually" in "where" every term in "what" with the corresponding
60    term in "with_what". The terms in "what" ARE NOT lifted when binders are
61    crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
62    Every free variable in "where" IS NOT lifted by nnn.
63 *)
64 let replace ~equality ~what ~with_what ~where =
65   let find_image t =
66    let rec find_image_aux =
67     function
68        [],[] -> raise Not_found
69      | what::tl1,with_what::tl2 ->
70         if equality what t then with_what else find_image_aux (tl1,tl2)
71      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
72    in
73     find_image_aux (what,with_what)
74   in
75   let rec aux t =
76    try
77     find_image t
78    with Not_found ->
79     match t with
80        C.Rel _ -> t
81      | C.Var (uri,exp_named_subst) ->
82         C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
83      | C.Meta _ -> t
84      | C.Sort _ -> t
85      | C.Implicit _ as t -> t
86      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
87      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
88      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
89      | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
90      | C.Appl l ->
91         (* Invariant enforced: no application of an application *)
92         (match List.map aux l with
93             (C.Appl l')::tl -> C.Appl (l'@tl)
94           | l' -> C.Appl l')
95      | C.Const (uri,exp_named_subst) ->
96         C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
97      | C.MutInd (uri,i,exp_named_subst) ->
98         C.MutInd
99          (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
100      | C.MutConstruct (uri,i,j,exp_named_subst) ->
101         C.MutConstruct
102          (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
103      | C.MutCase (sp,i,outt,t,pl) ->
104         C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
105      | C.Fix (i,fl) ->
106         let substitutedfl =
107          List.map
108           (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
109            fl
110         in
111          C.Fix (i, substitutedfl)
112      | C.CoFix (i,fl) ->
113         let substitutedfl =
114          List.map
115           (fun (name,ty,bo) -> (name, aux ty, aux bo))
116            fl
117         in
118          C.CoFix (i, substitutedfl)
119    in
120     aux where
121 ;;
122
123 (* Replaces in "where" every term in "what" with the corresponding
124    term in "with_what". The terms in "what" ARE lifted when binders are
125    crossed. The terms in "with_what" ARE lifted when binders are crossed.
126    Every free variable in "where" IS NOT lifted by nnn.
127    Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
128    inverse of subst up to the fact that free variables in "where" are NOT
129    lifted.  *)
130 let replace_lifting ~equality ~context ~what ~with_what ~where =
131   let find_image ctx what t =
132    let rec find_image_aux =
133     function
134        [],[] -> raise Not_found
135      | what::tl1,with_what::tl2 ->
136         if equality ctx what t then with_what else find_image_aux (tl1,tl2)
137      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
138    in
139     find_image_aux (what,with_what)
140   in
141   let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
142   let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
143   let rec substaux k ctx what t =
144    try
145     S.lift (k-1) (find_image ctx what t)
146    with Not_found ->
147     match t with
148       C.Rel n as t -> t
149     | C.Var (uri,exp_named_subst) ->
150        let exp_named_subst' =
151         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
152        in
153         C.Var (uri,exp_named_subst')
154     | C.Meta (i, l) -> 
155        let l' =
156         List.map
157          (function
158              None -> None
159            | Some t -> Some (substaux k ctx what t)
160          ) l
161        in
162         C.Meta(i,l')
163     | C.Sort _ as t -> t
164     | C.Implicit _ as t -> t
165     | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty)
166     | C.Prod (n,s,t) ->
167        C.Prod
168         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
169     | C.Lambda (n,s,t) ->
170        C.Lambda
171         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
172     | C.LetIn (n,s,t) ->
173        C.LetIn
174         (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
175     | C.Appl (he::tl) ->
176        (* Invariant: no Appl applied to another Appl *)
177        let tl' = List.map (substaux k ctx what) tl in
178         begin
179          match substaux k ctx what he with
180             C.Appl l -> C.Appl (l@tl')
181           | _ as he' -> C.Appl (he'::tl')
182         end
183     | C.Appl _ -> assert false
184     | C.Const (uri,exp_named_subst) ->
185        let exp_named_subst' =
186         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
187        in
188        C.Const (uri,exp_named_subst')
189     | C.MutInd (uri,i,exp_named_subst) ->
190        let exp_named_subst' =
191         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
192        in
193         C.MutInd (uri,i,exp_named_subst')
194     | C.MutConstruct (uri,i,j,exp_named_subst) ->
195        let exp_named_subst' =
196         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
197        in
198         C.MutConstruct (uri,i,j,exp_named_subst')
199     | C.MutCase (sp,i,outt,t,pl) ->
200        C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t,
201         List.map (substaux k ctx what) pl)
202     | C.Fix (i,fl) ->
203        let len = List.length fl in
204        let substitutedfl =
205         List.map
206          (fun (name,i,ty,bo) -> (* WRONG CTX *)
207            (name, i, substaux k ctx what ty,
208              substaux (k+len) ctx (List.map (S.lift len) what) bo)
209          ) fl
210        in
211         C.Fix (i, substitutedfl)
212     | C.CoFix (i,fl) ->
213        let len = List.length fl in
214        let substitutedfl =
215         List.map
216          (fun (name,ty,bo) -> (* WRONG CTX *)
217            (name, substaux k ctx what ty,
218              substaux (k+len) ctx (List.map (S.lift len) what) bo)
219          ) fl
220        in
221         C.CoFix (i, substitutedfl)
222  in
223   substaux 1 context what where
224 ;;
225
226 (* Replaces in "where" every term in "what" with the corresponding
227    term in "with_what". The terms in "what" ARE NOT lifted when binders are
228    crossed. The terms in "with_what" ARE lifted when binders are crossed.
229    Every free variable in "where" IS lifted by nnn.
230    Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
231    inverse of subst up to the fact that "what" terms are NOT lifted. *)
232 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
233   let find_image t =
234    let rec find_image_aux =
235     function
236        [],[] -> raise Not_found
237      | what::tl1,with_what::tl2 ->
238          if equality what t then with_what else find_image_aux (tl1,tl2)
239      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
240    in
241     find_image_aux (what,with_what)
242   in
243   let rec substaux k t =
244    try
245     S.lift (k-1) (find_image t)
246    with Not_found ->
247     match t with
248        C.Rel n ->
249         if n < k then C.Rel n else C.Rel (n + nnn)
250      | C.Var (uri,exp_named_subst) ->
251         let exp_named_subst' =
252          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
253         in
254          C.Var (uri,exp_named_subst')
255      | C.Meta (i, l) -> 
256         let l' =
257          List.map
258           (function
259               None -> None
260             | Some t -> Some (substaux k t)
261           ) l
262         in
263          C.Meta(i,l')
264      | C.Sort _ as t -> t
265      | C.Implicit _ as t -> t
266      | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
267      | C.Prod (n,s,t) ->
268         C.Prod (n, substaux k s, substaux (k + 1) t)
269      | C.Lambda (n,s,t) ->
270         C.Lambda (n, substaux k s, substaux (k + 1) t)
271      | C.LetIn (n,s,t) ->
272         C.LetIn (n, substaux k s, substaux (k + 1) t)
273      | C.Appl (he::tl) ->
274         (* Invariant: no Appl applied to another Appl *)
275         let tl' = List.map (substaux k) tl in
276          begin
277           match substaux k he with
278              C.Appl l -> C.Appl (l@tl')
279            | _ as he' -> C.Appl (he'::tl')
280          end
281      | C.Appl _ -> assert false
282      | C.Const (uri,exp_named_subst) ->
283         let exp_named_subst' =
284          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
285         in
286         C.Const (uri,exp_named_subst')
287      | C.MutInd (uri,i,exp_named_subst) ->
288         let exp_named_subst' =
289          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
290         in
291          C.MutInd (uri,i,exp_named_subst')
292      | C.MutConstruct (uri,i,j,exp_named_subst) ->
293         let exp_named_subst' =
294          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
295         in
296          C.MutConstruct (uri,i,j,exp_named_subst')
297      | C.MutCase (sp,i,outt,t,pl) ->
298         C.MutCase (sp,i,substaux k outt, substaux k t,
299          List.map (substaux k) pl)
300      | C.Fix (i,fl) ->
301         let len = List.length fl in
302         let substitutedfl =
303          List.map
304           (fun (name,i,ty,bo) ->
305             (name, i, substaux k ty, substaux (k+len) bo))
306            fl
307         in
308          C.Fix (i, substitutedfl)
309      | C.CoFix (i,fl) ->
310         let len = List.length fl in
311         let substitutedfl =
312          List.map
313           (fun (name,ty,bo) ->
314             (name, substaux k ty, substaux (k+len) bo))
315            fl
316         in
317          C.CoFix (i, substitutedfl)
318  in
319   substaux 1 where
320 ;;
321
322 (* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
323    up to the fact that the index to start from can be specified *)
324 let replace_with_rel_1_from ~equality ~what =
325    let rec find_image t = function
326       | []       -> false
327       | hd :: tl -> equality t hd || find_image t tl 
328    in
329    let rec subst_term k t =
330       if find_image t what then C.Rel k else inspect_term k t
331    and inspect_term k = function
332       | C.Rel i -> if i < k then C.Rel i else C.Rel (succ i)
333       | C.Sort _ as t -> t
334       | C.Implicit _ as t -> t
335       | C.Var (uri, enss) ->
336          let enss = List.map (subst_ens k) enss in
337          C.Var (uri, enss)
338       | C.Const (uri ,enss) ->
339          let enss = List.map (subst_ens k) enss in
340          C.Const (uri, enss)
341      | C.MutInd (uri, tyno, enss) ->
342          let enss = List.map (subst_ens k) enss in
343          C.MutInd (uri, tyno, enss)
344      | C.MutConstruct (uri, tyno, consno, enss) ->
345          let enss = List.map (subst_ens k) enss in
346          C.MutConstruct (uri, tyno, consno, enss)
347      | C.Meta (i, mss) -> 
348          let mss = List.map (subst_ms k) mss in
349          C.Meta(i, mss)
350      | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
351      | C.Appl ts ->      
352          let ts = List.map (subst_term k) ts in
353          C.Appl ts
354      | C.MutCase (uri, tyno, outty, t, cases) ->
355          let cases = List.map (subst_term k) cases in
356          C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
357      | C.Prod (n, v, t) ->
358         C.Prod (n, subst_term k v, subst_term (succ k) t)
359      | C.Lambda (n, v, t) ->
360         C.Lambda (n, subst_term k v, subst_term (succ k) t)
361      | C.LetIn (n, v, t) ->
362         C.LetIn (n, subst_term k v, subst_term (succ k) t)
363      | C.Fix (i, fixes) ->
364         let fixesno = List.length fixes in
365         let fixes = List.map (subst_fix fixesno k) fixes in
366         C.Fix (i, fixes)
367      | C.CoFix (i, cofixes) ->
368         let cofixesno = List.length cofixes in
369         let cofixes = List.map (subst_cofix cofixesno k) cofixes in
370          C.CoFix (i, cofixes)
371    and subst_ens k (uri, t) = uri, subst_term k t   
372    and subst_ms k = function
373       | None   -> None
374       | Some t -> Some (subst_term k t)
375    and subst_fix fixesno k (n, ind, ty, bo) =
376       n, ind, subst_term k ty, subst_term (k + fixesno) bo
377    and subst_cofix cofixesno k (n, ty, bo) =
378       n, subst_term k ty, subst_term (k + cofixesno) bo
379 in
380 subst_term
381    
382
383
384
385 (* Takes a well-typed term and fully reduces it. *)
386 (*CSC: It does not perform reduction in a Case *)
387 let reduce context =
388  let rec reduceaux context l =
389    function
390       C.Rel n as t ->
391        (match List.nth context (n-1) with
392            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
393          | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
394          | None -> raise RelToHiddenHypothesis
395        )
396     | C.Var (uri,exp_named_subst) ->
397        let exp_named_subst' =
398         reduceaux_exp_named_subst context l exp_named_subst
399        in
400        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
401          match o with
402            C.Constant _ -> raise ReferenceToConstant
403          | C.CurrentProof _ -> raise ReferenceToCurrentProof
404          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
405          | C.Variable (_,None,_,_,_) ->
406             let t' = C.Var (uri,exp_named_subst') in
407              if l = [] then t' else C.Appl (t'::l)
408          | C.Variable (_,Some body,_,_,_) ->
409             (reduceaux context l
410               (CicSubstitution.subst_vars exp_named_subst' body))
411        )
412     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
413     | C.Sort _ as t -> t (* l should be empty *)
414     | C.Implicit _ as t -> t
415     | C.Cast (te,ty) ->
416        C.Cast (reduceaux context l te, reduceaux context l ty)
417     | C.Prod (name,s,t) ->
418        assert (l = []) ;
419        C.Prod (name,
420         reduceaux context [] s,
421         reduceaux ((Some (name,C.Decl s))::context) [] t)
422     | C.Lambda (name,s,t) ->
423        (match l with
424            [] ->
425             C.Lambda (name,
426              reduceaux context [] s,
427              reduceaux ((Some (name,C.Decl s))::context) [] t)
428          | he::tl -> reduceaux context tl (S.subst he t)
429            (* when name is Anonimous the substitution should be superfluous *)
430        )
431     | C.LetIn (n,s,t) ->
432        reduceaux context l (S.subst (reduceaux context [] s) t)
433     | C.Appl (he::tl) ->
434        let tl' = List.map (reduceaux context []) tl in
435         reduceaux context (tl'@l) he
436     | C.Appl [] -> raise (Impossible 1)
437     | C.Const (uri,exp_named_subst) ->
438        let exp_named_subst' =
439         reduceaux_exp_named_subst context l exp_named_subst
440        in
441         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
442           match o with
443             C.Constant (_,Some body,_,_,_) ->
444              (reduceaux context l
445                (CicSubstitution.subst_vars exp_named_subst' body))
446           | C.Constant (_,None,_,_,_) ->
447              let t' = C.Const (uri,exp_named_subst') in
448               if l = [] then t' else C.Appl (t'::l)
449           | C.Variable _ -> raise ReferenceToVariable
450           | C.CurrentProof (_,_,body,_,_,_) ->
451              (reduceaux context l
452                (CicSubstitution.subst_vars exp_named_subst' body))
453           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
454         )
455     | C.MutInd (uri,i,exp_named_subst) ->
456        let exp_named_subst' =
457         reduceaux_exp_named_subst context l exp_named_subst
458        in
459         let t' = C.MutInd (uri,i,exp_named_subst') in
460          if l = [] then t' else C.Appl (t'::l)
461     | C.MutConstruct (uri,i,j,exp_named_subst) ->
462        let exp_named_subst' =
463         reduceaux_exp_named_subst context l exp_named_subst
464        in
465         let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
466          if l = [] then t' else C.Appl (t'::l)
467     | C.MutCase (mutind,i,outtype,term,pl) ->
468        let decofix =
469         function
470            C.CoFix (i,fl) ->
471              let (_,_,body) = List.nth fl i in
472               let body' =
473                let counter = ref (List.length fl) in
474                 List.fold_right
475                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
476                  fl
477                  body
478               in
479                reduceaux context [] body'
480          | C.Appl (C.CoFix (i,fl) :: tl) ->
481              let (_,_,body) = List.nth fl i in
482               let body' =
483                let counter = ref (List.length fl) in
484                 List.fold_right
485                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
486                  fl
487                  body
488               in
489                let tl' = List.map (reduceaux context []) tl in
490                 reduceaux context tl' body'
491          | t -> t
492        in
493         (match decofix (reduceaux context [] term) with
494             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
495           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
496              let (arity, r) =
497                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
498                  match o with
499                      C.InductiveDefinition (tl,_,r,_) ->
500                        let (_,_,arity,_) = List.nth tl i in
501                          (arity,r)
502                    | _ -> raise WrongUriToInductiveDefinition
503              in
504               let ts =
505                let rec eat_first =
506                 function
507                    (0,l) -> l
508                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
509                  | _ -> raise (Impossible 5)
510                in
511                 eat_first (r,tl)
512               in
513                reduceaux context (ts@l) (List.nth pl (j-1))
514          | C.Cast _ | C.Implicit _ ->
515             raise (Impossible 2) (* we don't trust our whd ;-) *)
516          | _ ->
517            let outtype' = reduceaux context [] outtype in
518            let term' = reduceaux context [] term in
519            let pl' = List.map (reduceaux context []) pl in
520             let res =
521              C.MutCase (mutind,i,outtype',term',pl')
522             in
523              if l = [] then res else C.Appl (res::l)
524        )
525     | C.Fix (i,fl) ->
526        let tys,_ =
527         List.fold_left
528           (fun (types,len) (n,_,ty,_) ->
529              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
530               len+1)
531          ) ([],0) fl 
532        in
533         let t' () =
534          let fl' =
535           List.map
536            (function (n,recindex,ty,bo) ->
537              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
538            ) fl
539          in
540           C.Fix (i, fl')
541         in
542          let (_,recindex,_,body) = List.nth fl i in
543           let recparam =
544            try
545             Some (List.nth l recindex)
546            with
547             _ -> None
548           in
549            (match recparam with
550                Some recparam ->
551                 (match reduceaux context [] recparam with
552                     C.MutConstruct _
553                   | C.Appl ((C.MutConstruct _)::_) ->
554                      let body' =
555                       let counter = ref (List.length fl) in
556                        List.fold_right
557                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
558                         fl
559                         body
560                      in
561                       (* Possible optimization: substituting whd recparam in l*)
562                       reduceaux context l body'
563                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
564                 )
565              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
566            )
567     | C.CoFix (i,fl) ->
568        let tys,_ =
569         List.fold_left
570           (fun (types,len) (n,ty,_) ->
571              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
572               len+1)
573          ) ([],0) fl
574        in
575         let t' =
576          let fl' =
577           List.map
578            (function (n,ty,bo) ->
579              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
580            ) fl
581          in
582           C.CoFix (i, fl')
583         in
584          if l = [] then t' else C.Appl (t'::l)
585  and reduceaux_exp_named_subst context l =
586   List.map (function uri,t -> uri,reduceaux context [] t)
587  in
588   reduceaux context []
589 ;;
590
591
592 let unfold ?what context where =
593  let contextlen = List.length context in
594  let first_is_the_expandable_head_of_second context' t1 t2 =
595   match t1,t2 with
596      Cic.Const (uri,_), Cic.Const (uri',_)
597    | Cic.Var (uri,_), Cic.Var (uri',_)
598    | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
599    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
600    | Cic.Const _, _
601    | Cic.Var _, _ -> false
602    | Cic.Rel n, Cic.Rel m
603    | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
604       n + (List.length context' - contextlen) = m
605    | Cic.Rel _, _ -> false
606    | _,_ ->
607      raise
608       (ProofEngineTypes.Fail
609         (lazy "The term to unfold is not a constant, a variable or a bound variable "))
610  in
611  let appl he tl =
612   if tl = [] then he else Cic.Appl (he::tl) in
613  let cannot_delta_expand t =
614   raise
615    (ProofEngineTypes.Fail
616      (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
617  let rec hd_delta_beta context tl =
618   function
619     Cic.Rel n as t ->
620      (try
621        match List.nth context (n-1) with
622           Some (_,Cic.Decl _) -> cannot_delta_expand t
623         | Some (_,Cic.Def (bo,_)) ->
624            CicReduction.head_beta_reduce
625             (appl (CicSubstitution.lift n bo) tl)
626         | None -> raise RelToHiddenHypothesis
627       with
628          Failure _ -> assert false)
629   | Cic.Const (uri,exp_named_subst) as t ->
630      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
631       (match o with
632           Cic.Constant (_,Some body,_,_,_) ->
633            CicReduction.head_beta_reduce
634             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
635         | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
636         | Cic.Variable _ -> raise ReferenceToVariable
637         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
638         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
639       )
640   | Cic.Var (uri,exp_named_subst) as t ->
641      let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
642       (match o with
643           Cic.Constant _ -> raise ReferenceToConstant
644         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
645         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
646         | Cic.Variable (_,Some body,_,_,_) ->
647            CicReduction.head_beta_reduce
648             (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
649         | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
650       )
651    | Cic.Appl [] -> assert false
652    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
653    | t -> cannot_delta_expand t
654  in
655  let context_and_matched_term_list =
656   match what with
657      None -> [context, where]
658    | Some what ->
659       let res =
660        ProofEngineHelpers.locate_in_term
661         ~equality:first_is_the_expandable_head_of_second
662         what ~where context
663       in
664        if res = [] then
665         raise
666          (ProofEngineTypes.Fail
667            (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
668        else
669         res
670  in
671   let reduced_terms =
672    List.map
673     (function (context,where) -> hd_delta_beta context [] where)
674     context_and_matched_term_list in
675   let whats = List.map snd context_and_matched_term_list in
676    replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
677 ;;
678
679 exception WrongShape;;
680 exception AlreadySimplified;;
681
682 (* Takes a well-typed term and                                               *)
683 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
684 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
685 (*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
686 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
687 (*     is applied again to the new redex; Step 3.1) is applied to the result *)
688 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
689 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
690 (*     not reduced. Otherwise, if the delta-residual is not the              *)
691 (*     lambda-abstraction of a Fix, then it performs step 3.2).              *)
692 (* 3.1) Folds the application of the constant to the arguments that did not  *)
693 (*     change in every iteration, i.e. to the actual arguments for the       *)
694 (*     lambda-abstractions that precede the Fix.                             *)
695 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries   *)
696 (*     reductions. If the reduction cannot be performed, it returns the      *)
697 (*     original term (not the head beta-zeta normal form of the definiendum) *)
698 (*CSC: It does not perform simplification in a Case *)
699
700 let simpl context =
701  (* a simplified term is active if it can create a redex when used as an *)
702  (* actual parameter                                                     *)
703  let rec is_active =
704   function
705      C.Lambda _
706    | C.MutConstruct _
707    | C.Appl (C.MutConstruct _::_)
708    | C.CoFix _ -> true
709    | C.Cast (bo,_) -> is_active bo
710    | C.LetIn _ -> assert false
711    | _ -> false
712  in
713  (* reduceaux is equal to the reduceaux locally defined inside *)
714  (* reduce, but for the const case.                            *) 
715  (**** Step 1 ****)
716  let rec reduceaux context l =
717    function
718       C.Rel n as t ->
719        (* we never perform delta expansion automatically *)
720        if l = [] then t else C.Appl (t::l)
721     | C.Var (uri,exp_named_subst) ->
722        let exp_named_subst' =
723         reduceaux_exp_named_subst context l exp_named_subst
724        in
725         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
726           match o with
727             C.Constant _ -> raise ReferenceToConstant
728           | C.CurrentProof _ -> raise ReferenceToCurrentProof
729           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
730           | C.Variable (_,None,_,_,_) ->
731             let t' = C.Var (uri,exp_named_subst') in
732              if l = [] then t' else C.Appl (t'::l)
733           | C.Variable (_,Some body,_,_,_) ->
734              reduceaux context l
735               (CicSubstitution.subst_vars exp_named_subst' body)
736         )
737     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
738     | C.Sort _ as t -> t (* l should be empty *)
739     | C.Implicit _ as t -> t
740     | C.Cast (te,ty) ->
741        C.Cast (reduceaux context l te, reduceaux context [] ty)
742     | C.Prod (name,s,t) ->
743        assert (l = []) ;
744        C.Prod (name,
745         reduceaux context [] s,
746         reduceaux ((Some (name,C.Decl s))::context) [] t)
747     | C.Lambda (name,s,t) ->
748        (match l with
749            [] ->
750             C.Lambda (name,
751              reduceaux context [] s,
752              reduceaux ((Some (name,C.Decl s))::context) [] t)
753          | he::tl -> reduceaux context tl (S.subst he t)
754            (* when name is Anonimous the substitution should be superfluous *)
755        )
756     | C.LetIn (n,s,t) ->
757        reduceaux context l (S.subst (reduceaux context [] s) t)
758     | C.Appl (he::tl) ->
759        let tl' = List.map (reduceaux context []) tl in
760         reduceaux context (tl'@l) he
761     | C.Appl [] -> raise (Impossible 1)
762     | C.Const (uri,exp_named_subst) ->
763        let exp_named_subst' =
764         reduceaux_exp_named_subst context l exp_named_subst
765        in
766         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
767           match o with
768            C.Constant (_,Some body,_,_,_) ->
769             if List.exists is_active l then
770              try_delta_expansion context l
771               (C.Const (uri,exp_named_subst'))
772               (CicSubstitution.subst_vars exp_named_subst' body)
773             else
774              let t' = C.Const (uri,exp_named_subst') in
775               if l = [] then t' else C.Appl (t'::l)
776          | C.Constant (_,None,_,_,_) ->
777             let t' = C.Const (uri,exp_named_subst') in
778              if l = [] then t' else C.Appl (t'::l)
779          | C.Variable _ -> raise ReferenceToVariable
780          | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
781          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
782        )
783     | C.MutInd (uri,i,exp_named_subst) ->
784        let exp_named_subst' =
785         reduceaux_exp_named_subst context l exp_named_subst
786        in
787         let t' = C.MutInd (uri,i,exp_named_subst') in
788          if l = [] then t' else C.Appl (t'::l)
789     | C.MutConstruct (uri,i,j,exp_named_subst) ->
790        let exp_named_subst' =
791         reduceaux_exp_named_subst context l exp_named_subst
792        in
793         let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
794          if l = [] then t' else C.Appl (t'::l)
795     | C.MutCase (mutind,i,outtype,term,pl) ->
796        let decofix =
797         function
798            C.CoFix (i,fl) ->
799              let (_,_,body) = List.nth fl i in
800               let body' =
801                let counter = ref (List.length fl) in
802                 List.fold_right
803                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
804                  fl
805                  body
806               in
807                reduceaux context [] body'
808          | C.Appl (C.CoFix (i,fl) :: tl) ->
809              let (_,_,body) = List.nth fl i in
810              let body' =
811               let counter = ref (List.length fl) in
812                List.fold_right
813                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
814                 fl
815                 body
816              in
817               let tl' = List.map (reduceaux context []) tl in
818                reduceaux context tl' body'
819          | t -> t
820        in
821         (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
822             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
823           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
824              let (arity, r) =
825                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
826                  match o with
827                      C.InductiveDefinition (tl,ingredients,r,_) ->
828                        let (_,_,arity,_) = List.nth tl i in
829                          (arity,r)
830                    | _ -> raise WrongUriToInductiveDefinition
831              in
832               let ts =
833                let rec eat_first =
834                 function
835                    (0,l) -> l
836                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
837                  | _ -> raise (Impossible 5)
838                in
839                 eat_first (r,tl)
840               in
841                reduceaux context (ts@l) (List.nth pl (j-1))
842          | C.Cast _ | C.Implicit _ ->
843             raise (Impossible 2) (* we don't trust our whd ;-) *)
844          | _ ->
845            let outtype' = reduceaux context [] outtype in
846            let term' = reduceaux context [] term in
847            let pl' = List.map (reduceaux context []) pl in
848             let res =
849              C.MutCase (mutind,i,outtype',term',pl')
850             in
851              if l = [] then res else C.Appl (res::l)
852        )
853     | C.Fix (i,fl) ->
854        let tys,_ =
855          List.fold_left
856            (fun (types,len) (n,_,ty,_) ->
857               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
858                len+1)
859           ) ([],0) fl 
860        in
861         let t' () =
862          let fl' =
863           List.map
864            (function (n,recindex,ty,bo) ->
865              (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
866            ) fl
867          in
868           C.Fix (i, fl')
869         in
870          let (_,recindex,_,body) = List.nth fl i in
871           let recparam =
872            try
873             Some (List.nth l recindex)
874            with
875             _ -> None
876           in
877            (match recparam with
878                Some recparam ->
879                 (match reduceaux context [] recparam with
880                     C.MutConstruct _
881                   | C.Appl ((C.MutConstruct _)::_) ->
882                      let body' =
883                       let counter = ref (List.length fl) in
884                        List.fold_right
885                         (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
886                         fl
887                         body
888                      in
889                       (* Possible optimization: substituting whd recparam in l*)
890                       reduceaux context l body'
891                   | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
892                 )
893              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
894            )
895     | C.CoFix (i,fl) ->
896        let tys,_ =
897         List.fold_left
898           (fun (types,len) (n,ty,_) ->
899              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
900               len+1)
901          ) ([],0) fl
902        in
903         let t' =
904          let fl' =
905           List.map
906            (function (n,ty,bo) ->
907              (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
908            ) fl
909          in
910          C.CoFix (i, fl')
911        in
912          if l = [] then t' else C.Appl (t'::l)
913  and reduceaux_exp_named_subst context l =
914   List.map (function uri,t -> uri,reduceaux context [] t)
915  (**** Step 2 ****)
916  and reduce_with_no_hope_to_fold_back t l =
917     prerr_endline "reduce_with_no_hope_to_fold_back";
918     let simplified = reduceaux context l t in
919     let t' = if l = [] then t else C.Appl (t::l) in
920     if t' = simplified then
921       raise AlreadySimplified
922     else
923       simplified
924
925  and try_delta_expansion context l term body =
926    try
927     let res,constant_args =
928      let rec aux rev_constant_args l =
929       function
930          C.Lambda (name,s,t) ->
931           begin
932            match l with
933               [] -> raise WrongShape
934             | he::tl ->
935                (* when name is Anonimous the substitution should *)
936                (* be superfluous                                 *)
937                aux (he::rev_constant_args) tl (S.subst he t)
938           end
939        | C.LetIn (_,s,t) ->
940           aux rev_constant_args l (S.subst s t)
941        | C.Fix (i,fl) ->
942            let (_,recindex,_,body) = List.nth fl i in
943             let recparam =
944              try
945               List.nth l recindex
946              with
947               _ -> raise AlreadySimplified
948             in
949              (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
950                  C.MutConstruct _
951                | C.Appl ((C.MutConstruct _)::_) ->
952                   let body' =
953                    let counter = ref (List.length fl) in
954                     List.fold_right
955                      (function _ ->
956                        decr counter ; S.subst (C.Fix (!counter,fl))
957                      ) fl body
958                   in
959                    (* Possible optimization: substituting whd *)
960                    (* recparam in l                           *)
961                    reduceaux context l body',
962                     List.rev rev_constant_args
963                | _ -> raise AlreadySimplified
964              )
965        | _ -> raise WrongShape
966      in
967       aux [] l body
968     in
969      (**** Step 3.1 ****)
970      let term_to_fold, delta_expanded_term_to_fold =
971       match constant_args with
972          [] -> term,body
973        | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
974      in
975       let simplified_term_to_fold =
976        reduceaux context [] delta_expanded_term_to_fold
977       in
978        replace_lifting ~equality:(fun _ x y -> x = y) ~context
979          ~what:[simplified_term_to_fold] ~with_what:[term_to_fold] ~where:res
980    with
981       WrongShape ->
982        let rec skip_lambda n = function
983          | Cic.Lambda (_,_,t) -> skip_lambda (n+1) t | t -> t, n
984        in
985        let is_fix uri = 
986          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
987          | Cic.Constant (_,Some bo, _, _,_) ->
988              (let t, _ = skip_lambda 0 bo in
989              match t with | Cic.Fix _ -> true | _ -> false) 
990          | _ -> false
991        in
992        let guess_recno uri = 
993          prerr_endline ("GUESS: " ^ UriManager.string_of_uri uri);
994          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
995          | Cic.Constant (_,Some bo, _, _,_ ) -> 
996              let t, n = skip_lambda 0 bo in
997              (match t with
998              | Cic.Fix (i,fl) ->
999                  let _,recno,_,_ = List.nth fl i in
1000                  prerr_endline ("GUESSED: " ^ string_of_int recno ^ " after " ^
1001                  string_of_int n ^ " lambdas");
1002                  recno + n
1003              | _ -> assert false)    
1004          | _ -> assert false
1005        in
1006        let original_args = l in 
1007        (**** Step 3.2 ****)
1008        let rec aux l =
1009         function
1010          | C.Lambda (name,s,t) ->
1011              (match l with
1012               | [] -> raise AlreadySimplified
1013               | he::tl ->
1014                  (* when name is Anonimous the substitution should *)
1015                  (* be superfluous                                 *)
1016                  aux tl (S.subst he t))
1017          | C.LetIn (_,s,t) -> aux l (S.subst s t)
1018          | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
1019              let recno =
1020                prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
1021                  ^ " in: " ^ String.concat " " 
1022                  (List.map (fun x -> CicPp.ppterm x) args));
1023                prerr_endline ("e piglio il rispettivo in :"^String.concat " " 
1024                  (List.map (fun x -> CicPp.ppterm x) original_args));
1025                (* look for args[regno] in saved_args *)
1026                let wanted = List.nth (args@l) (guess_recno uri) in
1027                let rec aux n = function
1028                  | [] -> n (* DA CAPIRE *)
1029                  | t::_ when t = wanted -> n
1030                  | _::tl -> aux (n+1) tl
1031                in
1032                aux 0 original_args
1033              in
1034              if recno = List.length original_args then
1035                reduce_with_no_hope_to_fold_back t l
1036              else
1037                let simplified = reduceaux context l t in
1038                let rec mk_implicits = function
1039                  | n,_::tl when n = recno -> 
1040                      Cic.Implicit None :: (mk_implicits (n+1,tl))
1041                  | n,arg::tl -> arg :: (mk_implicits (n+1,tl))
1042                  | _,[] -> []
1043                in
1044                (* we try to fold back constant that do not expand to Fix *)
1045                let _ = prerr_endline 
1046                  ("INIZIO (" ^ string_of_int recno ^ ") : " ^ CicPp.ppterm
1047                  simplified) in
1048                let term_to_fold = 
1049                  Cic.Appl (term:: mk_implicits (0,original_args)) 
1050                in
1051                (try
1052                  let term_to_fold, _, metasenv, _ = 
1053                    CicRefine.type_of_aux' [] context term_to_fold
1054                      CicUniv.oblivion_ugraph
1055                  in
1056                  let _ = 
1057                    prerr_endline ("RAFFINA: "^CicPp.ppterm term_to_fold) in
1058                  let _ = 
1059                    prerr_endline 
1060                      ("RAFFINA: "^CicMetaSubst.ppmetasenv [] metasenv) in
1061                  let simplified_term_to_fold = unfold context term_to_fold in
1062                  let _ = 
1063                    prerr_endline ("SEMPLIFICA: " ^ 
1064                      CicPp.ppterm simplified_term_to_fold) 
1065                  in
1066                  let rec do_n f t = 
1067                    let t1 = f t in
1068                    if t1 = t then t else do_n f t1
1069                  in
1070                  do_n 
1071                  (fun simplified -> 
1072                    let subst = ref [] in
1073                    let myunif ctx t1 t2 =
1074                      if !subst <> [] then false 
1075                      else
1076                      try 
1077                        prerr_endline "MUNIF";
1078                        prerr_endline (CicPp.ppterm t1);
1079                        prerr_endline "VS";
1080                        prerr_endline (CicPp.ppterm t2 ^ "\n");
1081                        let subst1, _, _ = 
1082                          CicUnification.fo_unif metasenv ctx t1 t2
1083                            CicUniv.empty_ugraph
1084                        in
1085                        prerr_endline "UNIFICANO\n\n\n";
1086                        subst := subst1;
1087                        true
1088                      with 
1089                      | CicUnification.UnificationFailure s
1090                      | CicUnification.Uncertain s
1091                      | CicUnification.AssertFailure s ->
1092                          prerr_endline (Lazy.force s); false
1093                      | CicUtil.Meta_not_found _ -> false
1094                      (*
1095                      | _ as exn -> 
1096                          prerr_endline (Printexc.to_string exn);
1097                          false*)
1098                    in
1099                    let t = 
1100                      replace_lifting myunif context
1101                        [simplified_term_to_fold] [term_to_fold] simplified
1102                    in
1103                    let _ = prerr_endline "UNIFICA" in
1104                    if List.length metasenv <> List.length !subst then 
1105                      let _ = prerr_endline ("SUBST CORTA " ^
1106                        CicMetaSubst.ppsubst !subst ~metasenv) 
1107                      in
1108                        simplified 
1109                    else
1110                      if t = simplified then 
1111                        let _ = prerr_endline "NULLA DI FATTO" in
1112                        simplified 
1113                      else
1114                        let t = CicMetaSubst.apply_subst !subst t in
1115                        prerr_endline ("ECCO: " ^ CicPp.ppterm t); t)
1116                    simplified 
1117                with 
1118                | CicRefine.RefineFailure s 
1119                | CicRefine.Uncertain s
1120                | CicRefine.AssertFailure s ->
1121                    prerr_endline (Lazy.force s); simplified 
1122                (*| exn -> prerr_endline (Printexc.to_string exn); simplified*))
1123          | t -> reduce_with_no_hope_to_fold_back t l
1124       in
1125         (try aux l body
1126          with
1127           AlreadySimplified ->
1128            if l = [] then term else C.Appl (term::l))
1129     | AlreadySimplified ->
1130        (* If we performed delta-reduction, we would find a Fix   *)
1131        (* not applied to a constructor. So, we refuse to perform *)
1132        (* delta-reduction.                                       *)
1133        if l = [] then term else C.Appl (term::l)
1134  in
1135   reduceaux context []
1136 ;;