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')
209 | C.Meta (i, l) as t ->
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')
308 | C.Meta (i, l) as t ->
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) as t ->
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) ->
462 C.CoFix (i,fl) as t ->
464 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
466 let (_,_,body) = List.nth fl i in
468 let counter = ref (List.length fl) in
470 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
474 reduceaux context [] body'
475 | C.Appl (C.CoFix (i,fl) :: tl) ->
477 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
479 let (_,_,body) = List.nth fl i in
481 let counter = ref (List.length fl) in
483 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
487 let tl' = List.map (reduceaux context []) tl in
488 reduceaux context tl' body'
491 (match decofix (reduceaux context [] term) with
492 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
493 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
495 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
497 C.InductiveDefinition (tl,_,r,_) ->
498 let (_,_,arity,_) = List.nth tl i in
500 | _ -> raise WrongUriToInductiveDefinition
506 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
507 | _ -> raise (Impossible 5)
511 reduceaux context (ts@l) (List.nth pl (j-1))
512 | C.Cast _ | C.Implicit _ ->
513 raise (Impossible 2) (* we don't trust our whd ;-) *)
515 let outtype' = reduceaux context [] outtype in
516 let term' = reduceaux context [] term in
517 let pl' = List.map (reduceaux context []) pl in
519 C.MutCase (mutind,i,outtype',term',pl')
521 if l = [] then res else C.Appl (res::l)
525 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
530 (function (n,recindex,ty,bo) ->
531 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
536 let (_,recindex,_,body) = List.nth fl i in
539 Some (List.nth l recindex)
545 (match reduceaux context [] recparam with
547 | C.Appl ((C.MutConstruct _)::_) ->
549 let counter = ref (List.length fl) in
551 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
555 (* Possible optimization: substituting whd recparam in l*)
556 reduceaux context l body'
557 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
559 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
563 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
568 (function (n,ty,bo) ->
569 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
574 if l = [] then t' else C.Appl (t'::l)
575 and reduceaux_exp_named_subst context l =
576 List.map (function uri,t -> uri,reduceaux context [] t)
581 exception WrongShape;;
582 exception AlreadySimplified;;
584 (* Takes a well-typed term and *)
585 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
586 (* Zeta-reduction is performed if and only if the simplified form of its *)
587 (* definiendum (applied to the actual arguments) is different from the *)
588 (* non-simplified form. *)
589 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
590 (* w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
591 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
592 (* is applied again to the new redex; Step 3) is applied to the result *)
593 (* of the recursive simplification. Otherwise, if the Fix can not be *)
594 (* reduced, than the delta-reductions fails and the delta-redex is *)
595 (* not reduced. Otherwise, if the delta-residual is not the *)
596 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
597 (* directly returned, without performing step 3). *)
598 (* 3) Folds the application of the constant to the arguments that did not *)
599 (* change in every iteration, i.e. to the actual arguments for the *)
600 (* lambda-abstractions that precede the Fix. *)
601 (*CSC: It does not perform simplification in a Case *)
609 | Cic.Appl l' -> Cic.Appl (l'@l)
610 | _ -> Cic.Appl (t::l)
612 (* reduceaux is equal to the reduceaux locally defined inside *)
613 (* reduce, but for the const case. *)
615 let rec reduceaux context l =
616 let module C = Cic in
617 let module S = CicSubstitution in
621 match List.nth context (n-1) with
622 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
623 | Some (_,C.Def (bo,_)) ->
624 let lifted_bo = S.lift n bo in
625 let applied_lifted_bo = mk_appl lifted_bo l in
626 let simplified = try_delta_expansion context l t lifted_bo in
627 if simplified = applied_lifted_bo then
628 if l = [] then t else C.Appl (t::l)
631 | None -> raise RelToHiddenHypothesis
633 Failure _ -> assert false)
634 | C.Var (uri,exp_named_subst) ->
635 let exp_named_subst' =
636 reduceaux_exp_named_subst context l exp_named_subst
638 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
640 C.Constant _ -> raise ReferenceToConstant
641 | C.CurrentProof _ -> raise ReferenceToCurrentProof
642 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
643 | C.Variable (_,None,_,_,_) ->
644 let t' = C.Var (uri,exp_named_subst') in
645 if l = [] then t' else C.Appl (t'::l)
646 | C.Variable (_,Some body,_,_,_) ->
648 (CicSubstitution.subst_vars exp_named_subst' body)
650 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
651 | C.Sort _ as t -> t (* l should be empty *)
652 | C.Implicit _ as t -> t
654 C.Cast (reduceaux context l te, reduceaux context l ty)
655 | C.Prod (name,s,t) ->
658 reduceaux context [] s,
659 reduceaux ((Some (name,C.Decl s))::context) [] t)
660 | C.Lambda (name,s,t) ->
664 reduceaux context [] s,
665 reduceaux ((Some (name,C.Decl s))::context) [] t)
666 | he::tl -> reduceaux context tl (S.subst he t)
667 (* when name is Anonimous the substitution should be superfluous *)
670 reduceaux context l (S.subst (reduceaux context [] s) t)
672 let tl' = List.map (reduceaux context []) tl in
673 reduceaux context (tl'@l) he
674 | C.Appl [] -> raise (Impossible 1)
675 | C.Const (uri,exp_named_subst) ->
676 let exp_named_subst' =
677 reduceaux_exp_named_subst context l exp_named_subst
679 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
681 C.Constant (_,Some body,_,_,_) ->
682 try_delta_expansion context l
683 (C.Const (uri,exp_named_subst'))
684 (CicSubstitution.subst_vars exp_named_subst' body)
685 | C.Constant (_,None,_,_,_) ->
686 let t' = C.Const (uri,exp_named_subst') in
687 if l = [] then t' else C.Appl (t'::l)
688 | C.Variable _ -> raise ReferenceToVariable
689 | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
690 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
692 | C.MutInd (uri,i,exp_named_subst) ->
693 let exp_named_subst' =
694 reduceaux_exp_named_subst context l exp_named_subst
696 let t' = C.MutInd (uri,i,exp_named_subst') in
697 if l = [] then t' else C.Appl (t'::l)
698 | C.MutConstruct (uri,i,j,exp_named_subst) ->
699 let exp_named_subst' =
700 reduceaux_exp_named_subst context l exp_named_subst
702 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
703 if l = [] then t' else C.Appl (t'::l)
704 | C.MutCase (mutind,i,outtype,term,pl) ->
707 C.CoFix (i,fl) as t ->
709 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
710 let (_,_,body) = List.nth fl i in
712 let counter = ref (List.length fl) in
714 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
718 reduceaux context [] body'
719 | C.Appl (C.CoFix (i,fl) :: tl) ->
721 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
722 let (_,_,body) = List.nth fl i in
724 let counter = ref (List.length fl) in
726 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
730 let tl' = List.map (reduceaux context []) tl in
731 reduceaux context tl body'
734 (match decofix (CicReduction.whd context term) with
735 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
736 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
738 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
740 C.InductiveDefinition (tl,ingredients,r,_) ->
741 let (_,_,arity,_) = List.nth tl i in
743 | _ -> raise WrongUriToInductiveDefinition
749 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
750 | _ -> raise (Impossible 5)
754 reduceaux context (ts@l) (List.nth pl (j-1))
755 | C.Cast _ | C.Implicit _ ->
756 raise (Impossible 2) (* we don't trust our whd ;-) *)
758 let outtype' = reduceaux context [] outtype in
759 let term' = reduceaux context [] term in
760 let pl' = List.map (reduceaux context []) pl in
762 C.MutCase (mutind,i,outtype',term',pl')
764 if l = [] then res else C.Appl (res::l)
768 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
773 (function (n,recindex,ty,bo) ->
774 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
779 let (_,recindex,_,body) = List.nth fl i in
782 Some (List.nth l recindex)
788 (match reduceaux context [] recparam with
790 | C.Appl ((C.MutConstruct _)::_) ->
792 let counter = ref (List.length fl) in
794 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
798 (* Possible optimization: substituting whd recparam in l*)
799 reduceaux context l body'
800 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
802 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
806 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
811 (function (n,ty,bo) ->
812 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
817 if l = [] then t' else C.Appl (t'::l)
818 and reduceaux_exp_named_subst context l =
819 List.map (function uri,t -> uri,reduceaux context [] t)
821 and try_delta_expansion context l term body =
822 let module C = Cic in
823 let module S = CicSubstitution in
825 let res,constant_args =
826 let rec aux rev_constant_args l =
828 C.Lambda (name,s,t) as t' ->
831 [] -> raise WrongShape
833 (* when name is Anonimous the substitution should *)
835 aux (he::rev_constant_args) tl (S.subst he t)
838 aux rev_constant_args l (S.subst s t)
839 | C.Fix (i,fl) as t ->
841 List.map (function (name,_,ty,_) ->
842 Some (C.Name name, C.Decl ty)) fl
844 let (_,recindex,_,body) = List.nth fl i in
849 _ -> raise AlreadySimplified
851 (match CicReduction.whd context recparam with
853 | C.Appl ((C.MutConstruct _)::_) ->
855 let counter = ref (List.length fl) in
858 decr counter ; S.subst (C.Fix (!counter,fl))
861 (* Possible optimization: substituting whd *)
863 reduceaux context l body',
864 List.rev rev_constant_args
865 | _ -> raise AlreadySimplified
867 | _ -> raise WrongShape
872 let term_to_fold, delta_expanded_term_to_fold =
873 match constant_args with
875 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
877 let simplified_term_to_fold =
878 reduceaux context [] delta_expanded_term_to_fold
880 replace (=) [simplified_term_to_fold] [term_to_fold] res
883 (* The constant does not unfold to a Fix lambda-abstracted *)
884 (* w.r.t. zero or more variables. We just perform reduction.*)
885 reduceaux context l body
886 | AlreadySimplified ->
887 (* If we performed delta-reduction, we would find a Fix *)
888 (* not applied to a constructor. So, we refuse to perform *)
889 (* delta-reduction. *)
890 if l = [] then term else C.Appl (term::l)
895 let unfold ?what context where =
896 let contextlen = List.length context in
897 let first_is_the_expandable_head_of_second context' t1 t2 =
899 Cic.Const (uri,_), Cic.Const (uri',_)
900 | Cic.Var (uri,_), Cic.Var (uri',_)
901 | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
902 | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
904 | Cic.Var _, _ -> false
905 | Cic.Rel n, Cic.Rel m
906 | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
907 n + (List.length context' - contextlen) = m
908 | Cic.Rel _, _ -> false
911 (ProofEngineTypes.Fail
912 "The term to unfold is not a constant, a variable or a bound variable ")
915 if tl = [] then he else Cic.Appl (he::tl) in
916 let cannot_delta_expand t =
918 (ProofEngineTypes.Fail
919 ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in
920 let rec hd_delta_beta context tl =
924 match List.nth context (n-1) with
925 Some (_,Cic.Decl _) -> cannot_delta_expand t
926 | Some (_,Cic.Def (bo,_)) ->
927 CicReduction.head_beta_reduce
928 (appl (CicSubstitution.lift n bo) tl)
929 | None -> raise RelToHiddenHypothesis
931 Failure _ -> assert false)
932 | Cic.Const (uri,exp_named_subst) as t ->
933 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
935 Cic.Constant (_,Some body,_,_,_) ->
936 CicReduction.head_beta_reduce
937 (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
938 | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
939 | Cic.Variable _ -> raise ReferenceToVariable
940 | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
941 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
943 | Cic.Var (uri,exp_named_subst) as t ->
944 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
946 Cic.Constant _ -> raise ReferenceToConstant
947 | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
948 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
949 | Cic.Variable (_,Some body,_,_,_) ->
950 CicReduction.head_beta_reduce
951 (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
952 | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
954 | Cic.Appl [] -> assert false
955 | Cic.Appl (he::tl) -> hd_delta_beta context tl he
956 | t -> cannot_delta_expand t
958 let context_and_matched_term_list =
960 None -> [context, where]
963 ProofEngineHelpers.locate_in_term
964 ~equality:first_is_the_expandable_head_of_second
969 (ProofEngineTypes.Fail
970 ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
976 (function (context,where) -> hd_delta_beta context [] where)
977 context_and_matched_term_list in
978 let whats = List.map snd context_and_matched_term_list in
979 replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where