1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
37 (* The code of this module is derived from the code of CicReduction *)
39 exception Impossible of int;;
40 exception ReferenceToConstant;;
41 exception ReferenceToVariable;;
42 exception ReferenceToCurrentProof;;
43 exception ReferenceToInductiveDefinition;;
44 exception WrongUriToInductiveDefinition;;
45 exception WrongUriToConstant;;
46 exception RelToHiddenHypothesis;;
48 let alpha_equivalence =
54 C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
55 UriManager.eq uri1 uri2 &&
56 aux_exp_named_subst exp_named_subst1 exp_named_subst2
57 | C.Cast (te,ty), C.Cast (te',ty') ->
58 aux te te' && aux ty ty'
59 | C.Prod (_,s,t), C.Prod (_,s',t') ->
61 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
63 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
65 | C.Appl l, C.Appl l' ->
68 (fun b t1 t2 -> b && aux t1 t2) true l l'
70 Invalid_argument _ -> false)
71 | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
72 UriManager.eq uri uri' &&
73 aux_exp_named_subst exp_named_subst1 exp_named_subst2
74 | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
75 UriManager.eq uri uri' && i = i' &&
76 aux_exp_named_subst exp_named_subst1 exp_named_subst2
77 | C.MutConstruct (uri,i,j,exp_named_subst1),
78 C.MutConstruct (uri',i',j',exp_named_subst2) ->
79 UriManager.eq uri uri' && i = i' && j = j' &&
80 aux_exp_named_subst exp_named_subst1 exp_named_subst2
81 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
82 UriManager.eq sp sp' && i = i' &&
83 aux outt outt' && aux t t' &&
86 (fun b t1 t2 -> b && aux t1 t2) true pl pl'
88 Invalid_argument _ -> false)
89 | C.Fix (i,fl), C.Fix (i',fl') ->
93 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
94 b && i = i' && aux ty ty' && aux bo bo'
97 Invalid_argument _ -> false)
98 | C.CoFix (i,fl), C.CoFix (i',fl') ->
102 (fun b (_,ty,bo) (_,ty',bo') ->
103 b && aux ty ty' && aux bo bo'
106 Invalid_argument _ -> false)
107 | _,_ -> false (* we already know that t != t' *)
108 and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
111 (fun b (uri1,t1) (uri2,t2) ->
112 b && UriManager.eq uri1 uri2 && aux t1 t2
113 ) true exp_named_subst1 exp_named_subst2
115 Invalid_argument _ -> false
120 exception WhatAndWithWhatDoNotHaveTheSameLength;;
122 (* "textual" replacement of several subterms with other ones *)
123 let replace ~equality ~what ~with_what ~where =
124 let module C = Cic in
126 let rec find_image_aux =
128 [],[] -> raise Not_found
129 | what::tl1,with_what::tl2 ->
130 if equality what t then with_what else find_image_aux (tl1,tl2)
131 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
133 find_image_aux (what,with_what)
141 | C.Var (uri,exp_named_subst) ->
142 C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
145 | C.Implicit _ as t -> t
146 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
147 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
148 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
149 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
151 (* Invariant enforced: no application of an application *)
152 (match List.map aux l with
153 (C.Appl l')::tl -> C.Appl (l'@tl)
155 | C.Const (uri,exp_named_subst) ->
156 C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
157 | C.MutInd (uri,i,exp_named_subst) ->
159 (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
160 | C.MutConstruct (uri,i,j,exp_named_subst) ->
162 (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
163 | C.MutCase (sp,i,outt,t,pl) ->
164 C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
168 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
171 C.Fix (i, substitutedfl)
175 (fun (name,ty,bo) -> (name, aux ty, aux bo))
178 C.CoFix (i, substitutedfl)
183 (* replaces in a term a term with another one. *)
184 (* Lifting are performed as usual. *)
185 let replace_lifting ~equality ~what ~with_what ~where =
186 let module C = Cic in
187 let module S = CicSubstitution in
188 let find_image what t =
189 let rec find_image_aux =
191 [],[] -> raise Not_found
192 | what::tl1,with_what::tl2 ->
193 if equality what t then with_what else find_image_aux (tl1,tl2)
194 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
196 find_image_aux (what,with_what)
198 let rec substaux k what t =
200 S.lift (k-1) (find_image what t)
204 | C.Var (uri,exp_named_subst) ->
205 let exp_named_subst' =
206 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
208 C.Var (uri,exp_named_subst')
214 | Some t -> Some (substaux k what t)
219 | C.Implicit _ as t -> t
220 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
223 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
224 | C.Lambda (n,s,t) ->
226 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
229 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
231 (* Invariant: no Appl applied to another Appl *)
232 let tl' = List.map (substaux k what) tl in
234 match substaux k what he with
235 C.Appl l -> C.Appl (l@tl')
236 | _ as he' -> C.Appl (he'::tl')
238 | C.Appl _ -> assert false
239 | C.Const (uri,exp_named_subst) ->
240 let exp_named_subst' =
241 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
243 C.Const (uri,exp_named_subst')
244 | C.MutInd (uri,i,exp_named_subst) ->
245 let exp_named_subst' =
246 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
248 C.MutInd (uri,i,exp_named_subst')
249 | C.MutConstruct (uri,i,j,exp_named_subst) ->
250 let exp_named_subst' =
251 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
253 C.MutConstruct (uri,i,j,exp_named_subst')
254 | C.MutCase (sp,i,outt,t,pl) ->
255 C.MutCase (sp,i,substaux k what outt, substaux k what t,
256 List.map (substaux k what) pl)
258 let len = List.length fl in
261 (fun (name,i,ty,bo) ->
262 (name, i, substaux k what ty,
263 substaux (k+len) (List.map (S.lift len) what) bo)
266 C.Fix (i, substitutedfl)
268 let len = List.length fl in
272 (name, substaux k what ty,
273 substaux (k+len) (List.map (S.lift len) what) bo)
276 C.CoFix (i, substitutedfl)
278 substaux 1 what where
281 (* replaces in a term a list of terms with other ones. *)
282 (* Lifting are performed as usual. *)
283 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
284 let module C = Cic in
285 let module S = CicSubstitution in
287 let rec find_image_aux =
289 [],[] -> raise Not_found
290 | what::tl1,with_what::tl2 ->
291 if equality what t then with_what else find_image_aux (tl1,tl2)
292 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
294 find_image_aux (what,with_what)
296 let rec substaux k t =
298 S.lift (k-1) (find_image t)
302 if n < k then C.Rel n else C.Rel (n + nnn)
303 | C.Var (uri,exp_named_subst) ->
304 let exp_named_subst' =
305 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
307 C.Var (uri,exp_named_subst')
313 | Some t -> Some (substaux k t)
318 | C.Implicit _ as t -> t
319 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
321 C.Prod (n, substaux k s, substaux (k + 1) t)
322 | C.Lambda (n,s,t) ->
323 C.Lambda (n, substaux k s, substaux (k + 1) t)
325 C.LetIn (n, substaux k s, substaux (k + 1) t)
327 (* Invariant: no Appl applied to another Appl *)
328 let tl' = List.map (substaux k) tl in
330 match substaux k he with
331 C.Appl l -> C.Appl (l@tl')
332 | _ as he' -> C.Appl (he'::tl')
334 | C.Appl _ -> assert false
335 | C.Const (uri,exp_named_subst) ->
336 let exp_named_subst' =
337 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
339 C.Const (uri,exp_named_subst')
340 | C.MutInd (uri,i,exp_named_subst) ->
341 let exp_named_subst' =
342 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
344 C.MutInd (uri,i,exp_named_subst')
345 | C.MutConstruct (uri,i,j,exp_named_subst) ->
346 let exp_named_subst' =
347 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
349 C.MutConstruct (uri,i,j,exp_named_subst')
350 | C.MutCase (sp,i,outt,t,pl) ->
351 C.MutCase (sp,i,substaux k outt, substaux k t,
352 List.map (substaux k) pl)
354 let len = List.length fl in
357 (fun (name,i,ty,bo) ->
358 (name, i, substaux k ty, substaux (k+len) bo))
361 C.Fix (i, substitutedfl)
363 let len = List.length fl in
367 (name, substaux k ty, substaux (k+len) bo))
370 C.CoFix (i, substitutedfl)
375 (* Takes a well-typed term and fully reduces it. *)
376 (*CSC: It does not perform reduction in a Case *)
378 let rec reduceaux context l =
379 let module C = Cic in
380 let module S = CicSubstitution in
383 (match List.nth context (n-1) with
384 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
385 | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
386 | None -> raise RelToHiddenHypothesis
388 | C.Var (uri,exp_named_subst) ->
389 let exp_named_subst' =
390 reduceaux_exp_named_subst context l exp_named_subst
392 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
394 C.Constant _ -> raise ReferenceToConstant
395 | C.CurrentProof _ -> raise ReferenceToCurrentProof
396 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
397 | C.Variable (_,None,_,_,_) ->
398 let t' = C.Var (uri,exp_named_subst') in
399 if l = [] then t' else C.Appl (t'::l)
400 | C.Variable (_,Some body,_,_,_) ->
402 (CicSubstitution.subst_vars exp_named_subst' body))
404 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
405 | C.Sort _ as t -> t (* l should be empty *)
406 | C.Implicit _ as t -> t
408 C.Cast (reduceaux context l te, reduceaux context l ty)
409 | C.Prod (name,s,t) ->
412 reduceaux context [] s,
413 reduceaux ((Some (name,C.Decl s))::context) [] t)
414 | C.Lambda (name,s,t) ->
418 reduceaux context [] s,
419 reduceaux ((Some (name,C.Decl s))::context) [] t)
420 | he::tl -> reduceaux context tl (S.subst he t)
421 (* when name is Anonimous the substitution should be superfluous *)
424 reduceaux context l (S.subst (reduceaux context [] s) t)
426 let tl' = List.map (reduceaux context []) tl in
427 reduceaux context (tl'@l) he
428 | C.Appl [] -> raise (Impossible 1)
429 | C.Const (uri,exp_named_subst) ->
430 let exp_named_subst' =
431 reduceaux_exp_named_subst context l exp_named_subst
433 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
435 C.Constant (_,Some body,_,_,_) ->
437 (CicSubstitution.subst_vars exp_named_subst' body))
438 | C.Constant (_,None,_,_,_) ->
439 let t' = C.Const (uri,exp_named_subst') in
440 if l = [] then t' else C.Appl (t'::l)
441 | C.Variable _ -> raise ReferenceToVariable
442 | C.CurrentProof (_,_,body,_,_,_) ->
444 (CicSubstitution.subst_vars exp_named_subst' body))
445 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
447 | C.MutInd (uri,i,exp_named_subst) ->
448 let exp_named_subst' =
449 reduceaux_exp_named_subst context l exp_named_subst
451 let t' = C.MutInd (uri,i,exp_named_subst') in
452 if l = [] then t' else C.Appl (t'::l)
453 | C.MutConstruct (uri,i,j,exp_named_subst) ->
454 let exp_named_subst' =
455 reduceaux_exp_named_subst context l exp_named_subst
457 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
458 if l = [] then t' else C.Appl (t'::l)
459 | C.MutCase (mutind,i,outtype,term,pl) ->
463 let (_,_,body) = List.nth fl i in
465 let counter = ref (List.length fl) in
467 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
471 reduceaux context [] body'
472 | C.Appl (C.CoFix (i,fl) :: tl) ->
473 let (_,_,body) = List.nth fl i in
475 let counter = ref (List.length fl) in
477 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
481 let tl' = List.map (reduceaux context []) tl in
482 reduceaux context tl' body'
485 (match decofix (reduceaux context [] term) with
486 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
487 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
489 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
491 C.InductiveDefinition (tl,_,r,_) ->
492 let (_,_,arity,_) = List.nth tl i in
494 | _ -> raise WrongUriToInductiveDefinition
500 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
501 | _ -> raise (Impossible 5)
505 reduceaux context (ts@l) (List.nth pl (j-1))
506 | C.Cast _ | C.Implicit _ ->
507 raise (Impossible 2) (* we don't trust our whd ;-) *)
509 let outtype' = reduceaux context [] outtype in
510 let term' = reduceaux context [] term in
511 let pl' = List.map (reduceaux context []) pl in
513 C.MutCase (mutind,i,outtype',term',pl')
515 if l = [] then res else C.Appl (res::l)
519 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
524 (function (n,recindex,ty,bo) ->
525 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
530 let (_,recindex,_,body) = List.nth fl i in
533 Some (List.nth l recindex)
539 (match reduceaux context [] recparam with
541 | C.Appl ((C.MutConstruct _)::_) ->
543 let counter = ref (List.length fl) in
545 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
549 (* Possible optimization: substituting whd recparam in l*)
550 reduceaux context l body'
551 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
553 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
557 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
562 (function (n,ty,bo) ->
563 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
568 if l = [] then t' else C.Appl (t'::l)
569 and reduceaux_exp_named_subst context l =
570 List.map (function uri,t -> uri,reduceaux context [] t)
575 exception WrongShape;;
576 exception AlreadySimplified;;
578 (* Takes a well-typed term and *)
579 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
580 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
581 (* w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
582 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
583 (* is applied again to the new redex; Step 3.1) is applied to the result *)
584 (* of the recursive simplification. Otherwise, if the Fix can not be *)
585 (* reduced, than the delta-reductions fails and the delta-redex is *)
586 (* not reduced. Otherwise, if the delta-residual is not the *)
587 (* lambda-abstraction of a Fix, then it performs step 3.2). *)
588 (* 3.1) Folds the application of the constant to the arguments that did not *)
589 (* change in every iteration, i.e. to the actual arguments for the *)
590 (* lambda-abstractions that precede the Fix. *)
591 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries *)
592 (* reductions. If the reduction cannot be performed, it returns the *)
593 (* original term (not the head beta-zeta normal form of the definiendum) *)
594 (*CSC: It does not perform simplification in a Case *)
597 (* reduceaux is equal to the reduceaux locally defined inside *)
598 (* reduce, but for the const case. *)
600 let rec reduceaux context l =
601 let module C = Cic in
602 let module S = CicSubstitution in
606 match List.nth context (n-1) with
607 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
608 | Some (_,C.Def (bo,_)) ->
609 try_delta_expansion context l t (S.lift n bo)
610 | None -> raise RelToHiddenHypothesis
612 Failure _ -> assert false)
613 | C.Var (uri,exp_named_subst) ->
614 let exp_named_subst' =
615 reduceaux_exp_named_subst context l exp_named_subst
617 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
619 C.Constant _ -> raise ReferenceToConstant
620 | C.CurrentProof _ -> raise ReferenceToCurrentProof
621 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
622 | C.Variable (_,None,_,_,_) ->
623 let t' = C.Var (uri,exp_named_subst') in
624 if l = [] then t' else C.Appl (t'::l)
625 | C.Variable (_,Some body,_,_,_) ->
627 (CicSubstitution.subst_vars exp_named_subst' body)
629 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
630 | C.Sort _ as t -> t (* l should be empty *)
631 | C.Implicit _ as t -> t
633 C.Cast (reduceaux context l te, reduceaux context l ty)
634 | C.Prod (name,s,t) ->
637 reduceaux context [] s,
638 reduceaux ((Some (name,C.Decl s))::context) [] t)
639 | C.Lambda (name,s,t) ->
643 reduceaux context [] s,
644 reduceaux ((Some (name,C.Decl s))::context) [] t)
645 | he::tl -> reduceaux context tl (S.subst he t)
646 (* when name is Anonimous the substitution should be superfluous *)
649 reduceaux context l (S.subst (reduceaux context [] s) t)
651 let tl' = List.map (reduceaux context []) tl in
652 reduceaux context (tl'@l) he
653 | C.Appl [] -> raise (Impossible 1)
654 | C.Const (uri,exp_named_subst) ->
655 let exp_named_subst' =
656 reduceaux_exp_named_subst context l exp_named_subst
658 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
660 C.Constant (_,Some body,_,_,_) ->
661 try_delta_expansion context l
662 (C.Const (uri,exp_named_subst'))
663 (CicSubstitution.subst_vars exp_named_subst' body)
664 | C.Constant (_,None,_,_,_) ->
665 let t' = C.Const (uri,exp_named_subst') in
666 if l = [] then t' else C.Appl (t'::l)
667 | C.Variable _ -> raise ReferenceToVariable
668 | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
669 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
671 | C.MutInd (uri,i,exp_named_subst) ->
672 let exp_named_subst' =
673 reduceaux_exp_named_subst context l exp_named_subst
675 let t' = C.MutInd (uri,i,exp_named_subst') in
676 if l = [] then t' else C.Appl (t'::l)
677 | C.MutConstruct (uri,i,j,exp_named_subst) ->
678 let exp_named_subst' =
679 reduceaux_exp_named_subst context l exp_named_subst
681 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
682 if l = [] then t' else C.Appl (t'::l)
683 | C.MutCase (mutind,i,outtype,term,pl) ->
687 let (_,_,body) = List.nth fl i in
689 let counter = ref (List.length fl) in
691 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
695 reduceaux context [] body'
696 | C.Appl (C.CoFix (i,fl) :: tl) ->
698 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
699 let (_,_,body) = List.nth fl i in
701 let counter = ref (List.length fl) in
703 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
707 let tl' = List.map (reduceaux context []) tl in
708 reduceaux context tl' body'
711 (match decofix (CicReduction.whd context term) with
712 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
713 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
715 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
717 C.InductiveDefinition (tl,ingredients,r,_) ->
718 let (_,_,arity,_) = List.nth tl i in
720 | _ -> raise WrongUriToInductiveDefinition
726 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
727 | _ -> raise (Impossible 5)
731 reduceaux context (ts@l) (List.nth pl (j-1))
732 | C.Cast _ | C.Implicit _ ->
733 raise (Impossible 2) (* we don't trust our whd ;-) *)
735 let outtype' = reduceaux context [] outtype in
736 let term' = reduceaux context [] term in
737 let pl' = List.map (reduceaux context []) pl in
739 C.MutCase (mutind,i,outtype',term',pl')
741 if l = [] then res else C.Appl (res::l)
745 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
750 (function (n,recindex,ty,bo) ->
751 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
756 let (_,recindex,_,body) = List.nth fl i in
759 Some (List.nth l recindex)
765 (match reduceaux context [] recparam with
767 | C.Appl ((C.MutConstruct _)::_) ->
769 let counter = ref (List.length fl) in
771 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
775 (* Possible optimization: substituting whd recparam in l*)
776 reduceaux context l body'
777 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
779 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
783 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
788 (function (n,ty,bo) ->
789 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
794 if l = [] then t' else C.Appl (t'::l)
795 and reduceaux_exp_named_subst context l =
796 List.map (function uri,t -> uri,reduceaux context [] t)
798 and try_delta_expansion context l term body =
799 let module C = Cic in
800 let module S = CicSubstitution in
802 let res,constant_args =
803 let rec aux rev_constant_args l =
805 C.Lambda (name,s,t) ->
808 [] -> raise WrongShape
810 (* when name is Anonimous the substitution should *)
812 aux (he::rev_constant_args) tl (S.subst he t)
815 aux rev_constant_args l (S.subst s t)
817 let (_,recindex,_,body) = List.nth fl i in
822 _ -> raise AlreadySimplified
824 (match CicReduction.whd context recparam with
826 | C.Appl ((C.MutConstruct _)::_) ->
828 let counter = ref (List.length fl) in
831 decr counter ; S.subst (C.Fix (!counter,fl))
834 (* Possible optimization: substituting whd *)
836 reduceaux context l body',
837 List.rev rev_constant_args
838 | _ -> raise AlreadySimplified
840 | _ -> raise WrongShape
845 let term_to_fold, delta_expanded_term_to_fold =
846 match constant_args with
848 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
850 let simplified_term_to_fold =
851 reduceaux context [] delta_expanded_term_to_fold
853 replace (=) [simplified_term_to_fold] [term_to_fold] res
859 C.Lambda (name,s,t) ->
861 [] -> raise AlreadySimplified
863 (* when name is Anonimous the substitution should *)
865 aux tl (S.subst he t))
866 | C.LetIn (_,s,t) -> aux l (S.subst s t)
868 let simplified = reduceaux context l t in
869 if t = simplified then
870 raise AlreadySimplified
877 if l = [] then term else C.Appl (term::l))
878 | AlreadySimplified ->
879 (* If we performed delta-reduction, we would find a Fix *)
880 (* not applied to a constructor. So, we refuse to perform *)
881 (* delta-reduction. *)
882 if l = [] then term else C.Appl (term::l)
887 let unfold ?what context where =
888 let contextlen = List.length context in
889 let first_is_the_expandable_head_of_second context' t1 t2 =
891 Cic.Const (uri,_), Cic.Const (uri',_)
892 | Cic.Var (uri,_), Cic.Var (uri',_)
893 | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
894 | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
896 | Cic.Var _, _ -> false
897 | Cic.Rel n, Cic.Rel m
898 | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
899 n + (List.length context' - contextlen) = m
900 | Cic.Rel _, _ -> false
903 (ProofEngineTypes.Fail
904 (lazy "The term to unfold is not a constant, a variable or a bound variable "))
907 if tl = [] then he else Cic.Appl (he::tl) in
908 let cannot_delta_expand t =
910 (ProofEngineTypes.Fail
911 (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
912 let rec hd_delta_beta context tl =
916 match List.nth context (n-1) with
917 Some (_,Cic.Decl _) -> cannot_delta_expand t
918 | Some (_,Cic.Def (bo,_)) ->
919 CicReduction.head_beta_reduce
920 (appl (CicSubstitution.lift n bo) tl)
921 | None -> raise RelToHiddenHypothesis
923 Failure _ -> assert false)
924 | Cic.Const (uri,exp_named_subst) as t ->
925 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
927 Cic.Constant (_,Some body,_,_,_) ->
928 CicReduction.head_beta_reduce
929 (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
930 | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
931 | Cic.Variable _ -> raise ReferenceToVariable
932 | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
933 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
935 | Cic.Var (uri,exp_named_subst) as t ->
936 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
938 Cic.Constant _ -> raise ReferenceToConstant
939 | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
940 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
941 | Cic.Variable (_,Some body,_,_,_) ->
942 CicReduction.head_beta_reduce
943 (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
944 | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
946 | Cic.Appl [] -> assert false
947 | Cic.Appl (he::tl) -> hd_delta_beta context tl he
948 | t -> cannot_delta_expand t
950 let context_and_matched_term_list =
952 None -> [context, where]
955 ProofEngineHelpers.locate_in_term
956 ~equality:first_is_the_expandable_head_of_second
961 (ProofEngineTypes.Fail
962 (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
968 (function (context,where) -> hd_delta_beta context [] where)
969 context_and_matched_term_list in
970 let whats = List.map snd context_and_matched_term_list in
971 replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where