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 (******************************************************************************)
38 (* The code of this module is derived from the code of CicReduction *)
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;;
50 module S = CicSubstitution
52 exception WhatAndWithWhatDoNotHaveTheSameLength;;
54 (* Replaces "textually" in "where" every term in "what" with the corresponding
55 term in "with_what". The terms in "what" ARE NOT lifted when binders are
56 crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
57 Every free variable in "where" IS NOT lifted by nnn.
59 let replace ~equality ~what ~with_what ~where =
61 let rec find_image_aux =
63 [],[] -> raise Not_found
64 | what::tl1,with_what::tl2 ->
65 if equality what t then with_what else find_image_aux (tl1,tl2)
66 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
68 find_image_aux (what,with_what)
76 | C.Var (uri,exp_named_subst) ->
77 C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
80 | C.Implicit _ as t -> t
81 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
82 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
83 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
84 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
86 (* Invariant enforced: no application of an application *)
87 (match List.map aux l with
88 (C.Appl l')::tl -> C.Appl (l'@tl)
90 | C.Const (uri,exp_named_subst) ->
91 C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
92 | C.MutInd (uri,i,exp_named_subst) ->
94 (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
95 | C.MutConstruct (uri,i,j,exp_named_subst) ->
97 (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
98 | C.MutCase (sp,i,outt,t,pl) ->
99 C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
103 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
106 C.Fix (i, substitutedfl)
110 (fun (name,ty,bo) -> (name, aux ty, aux bo))
113 C.CoFix (i, substitutedfl)
118 (* Replaces in "where" every term in "what" with the corresponding
119 term in "with_what". The terms in "what" ARE lifted when binders are
120 crossed. The terms in "with_what" ARE lifted when binders are crossed.
121 Every free variable in "where" IS NOT lifted by nnn.
122 Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
123 inverse of subst up to the fact that free variables in "where" are NOT
125 let replace_lifting ~equality ~what ~with_what ~where =
126 let find_image what t =
127 let rec find_image_aux =
129 [],[] -> raise Not_found
130 | what::tl1,with_what::tl2 ->
131 if equality what t then with_what else find_image_aux (tl1,tl2)
132 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
134 find_image_aux (what,with_what)
136 let rec substaux k what t =
138 S.lift (k-1) (find_image what t)
142 | C.Var (uri,exp_named_subst) ->
143 let exp_named_subst' =
144 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
146 C.Var (uri,exp_named_subst')
152 | Some t -> Some (substaux k what t)
157 | C.Implicit _ as t -> t
158 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
161 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
162 | C.Lambda (n,s,t) ->
164 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
167 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
169 (* Invariant: no Appl applied to another Appl *)
170 let tl' = List.map (substaux k what) tl in
172 match substaux k what he with
173 C.Appl l -> C.Appl (l@tl')
174 | _ as he' -> C.Appl (he'::tl')
176 | C.Appl _ -> assert false
177 | C.Const (uri,exp_named_subst) ->
178 let exp_named_subst' =
179 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
181 C.Const (uri,exp_named_subst')
182 | C.MutInd (uri,i,exp_named_subst) ->
183 let exp_named_subst' =
184 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
186 C.MutInd (uri,i,exp_named_subst')
187 | C.MutConstruct (uri,i,j,exp_named_subst) ->
188 let exp_named_subst' =
189 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
191 C.MutConstruct (uri,i,j,exp_named_subst')
192 | C.MutCase (sp,i,outt,t,pl) ->
193 C.MutCase (sp,i,substaux k what outt, substaux k what t,
194 List.map (substaux k what) pl)
196 let len = List.length fl in
199 (fun (name,i,ty,bo) ->
200 (name, i, substaux k what ty,
201 substaux (k+len) (List.map (S.lift len) what) bo)
204 C.Fix (i, substitutedfl)
206 let len = List.length fl in
210 (name, substaux k what ty,
211 substaux (k+len) (List.map (S.lift len) what) bo)
214 C.CoFix (i, substitutedfl)
216 substaux 1 what where
219 (* Replaces in "where" every term in "what" with the corresponding
220 term in "with_what". The terms in "what" ARE NOT lifted when binders are
221 crossed. The terms in "with_what" ARE lifted when binders are crossed.
222 Every free variable in "where" IS lifted by nnn.
223 Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
224 inverse of subst up to the fact that "what" terms are NOT lifted. *)
225 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
227 let rec find_image_aux =
229 [],[] -> raise Not_found
230 | what::tl1,with_what::tl2 ->
231 if equality what t then with_what else find_image_aux (tl1,tl2)
232 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
234 find_image_aux (what,with_what)
236 let rec substaux k t =
238 S.lift (k-1) (find_image t)
242 if n < k then C.Rel n else C.Rel (n + nnn)
243 | C.Var (uri,exp_named_subst) ->
244 let exp_named_subst' =
245 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
247 C.Var (uri,exp_named_subst')
253 | Some t -> Some (substaux k t)
258 | C.Implicit _ as t -> t
259 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
261 C.Prod (n, substaux k s, substaux (k + 1) t)
262 | C.Lambda (n,s,t) ->
263 C.Lambda (n, substaux k s, substaux (k + 1) t)
265 C.LetIn (n, substaux k s, substaux (k + 1) t)
267 (* Invariant: no Appl applied to another Appl *)
268 let tl' = List.map (substaux k) tl in
270 match substaux k he with
271 C.Appl l -> C.Appl (l@tl')
272 | _ as he' -> C.Appl (he'::tl')
274 | C.Appl _ -> assert false
275 | C.Const (uri,exp_named_subst) ->
276 let exp_named_subst' =
277 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
279 C.Const (uri,exp_named_subst')
280 | C.MutInd (uri,i,exp_named_subst) ->
281 let exp_named_subst' =
282 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
284 C.MutInd (uri,i,exp_named_subst')
285 | C.MutConstruct (uri,i,j,exp_named_subst) ->
286 let exp_named_subst' =
287 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
289 C.MutConstruct (uri,i,j,exp_named_subst')
290 | C.MutCase (sp,i,outt,t,pl) ->
291 C.MutCase (sp,i,substaux k outt, substaux k t,
292 List.map (substaux k) pl)
294 let len = List.length fl in
297 (fun (name,i,ty,bo) ->
298 (name, i, substaux k ty, substaux (k+len) bo))
301 C.Fix (i, substitutedfl)
303 let len = List.length fl in
307 (name, substaux k ty, substaux (k+len) bo))
310 C.CoFix (i, substitutedfl)
315 (* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
316 up to the fact that the index to start from can be specified *)
317 let replace_with_rel_1_from ~equality ~what =
318 let rec find_image t = function
320 | hd :: tl -> equality t hd || find_image t tl
322 let rec subst_term k t =
323 if find_image t what then C.Rel k else inspect_term k t
324 and inspect_term k = function
325 | C.Rel i -> if i < k then C.Rel i else C.Rel (succ i)
327 | C.Implicit _ as t -> t
328 | C.Var (uri, enss) ->
329 let enss = List.map (subst_ens k) enss in
331 | C.Const (uri ,enss) ->
332 let enss = List.map (subst_ens k) enss in
334 | C.MutInd (uri, tyno, enss) ->
335 let enss = List.map (subst_ens k) enss in
336 C.MutInd (uri, tyno, enss)
337 | C.MutConstruct (uri, tyno, consno, enss) ->
338 let enss = List.map (subst_ens k) enss in
339 C.MutConstruct (uri, tyno, consno, enss)
341 let mss = List.map (subst_ms k) mss in
343 | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
345 let ts = List.map (subst_term k) ts in
347 | C.MutCase (uri, tyno, outty, t, cases) ->
348 let cases = List.map (subst_term k) cases in
349 C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
350 | C.Prod (n, v, t) ->
351 C.Prod (n, subst_term k v, subst_term (succ k) t)
352 | C.Lambda (n, v, t) ->
353 C.Lambda (n, subst_term k v, subst_term (succ k) t)
354 | C.LetIn (n, v, t) ->
355 C.LetIn (n, subst_term k v, subst_term (succ k) t)
356 | C.Fix (i, fixes) ->
357 let fixesno = List.length fixes in
358 let fixes = List.map (subst_fix fixesno k) fixes in
360 | C.CoFix (i, cofixes) ->
361 let cofixesno = List.length cofixes in
362 let cofixes = List.map (subst_cofix cofixesno k) cofixes in
364 and subst_ens k (uri, t) = uri, subst_term k t
365 and subst_ms k = function
367 | Some t -> Some (subst_term k t)
368 and subst_fix fixesno k (n, ind, ty, bo) =
369 n, ind, subst_term k ty, subst_term (k + fixesno) bo
370 and subst_cofix cofixesno k (n, ty, bo) =
371 n, subst_term k ty, subst_term (k + cofixesno) bo
378 (* Takes a well-typed term and fully reduces it. *)
379 (*CSC: It does not perform reduction in a Case *)
381 let rec reduceaux context l =
384 (match List.nth context (n-1) with
385 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
386 | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
387 | None -> raise RelToHiddenHypothesis
389 | C.Var (uri,exp_named_subst) ->
390 let exp_named_subst' =
391 reduceaux_exp_named_subst context l exp_named_subst
393 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
395 C.Constant _ -> raise ReferenceToConstant
396 | C.CurrentProof _ -> raise ReferenceToCurrentProof
397 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
398 | C.Variable (_,None,_,_,_) ->
399 let t' = C.Var (uri,exp_named_subst') in
400 if l = [] then t' else C.Appl (t'::l)
401 | C.Variable (_,Some body,_,_,_) ->
403 (CicSubstitution.subst_vars exp_named_subst' body))
405 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
406 | C.Sort _ as t -> t (* l should be empty *)
407 | C.Implicit _ as t -> t
409 C.Cast (reduceaux context l te, reduceaux context l ty)
410 | C.Prod (name,s,t) ->
413 reduceaux context [] s,
414 reduceaux ((Some (name,C.Decl s))::context) [] t)
415 | C.Lambda (name,s,t) ->
419 reduceaux context [] s,
420 reduceaux ((Some (name,C.Decl s))::context) [] t)
421 | he::tl -> reduceaux context tl (S.subst he t)
422 (* when name is Anonimous the substitution should be superfluous *)
425 reduceaux context l (S.subst (reduceaux context [] s) t)
427 let tl' = List.map (reduceaux context []) tl in
428 reduceaux context (tl'@l) he
429 | C.Appl [] -> raise (Impossible 1)
430 | C.Const (uri,exp_named_subst) ->
431 let exp_named_subst' =
432 reduceaux_exp_named_subst context l exp_named_subst
434 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
436 C.Constant (_,Some body,_,_,_) ->
438 (CicSubstitution.subst_vars exp_named_subst' body))
439 | C.Constant (_,None,_,_,_) ->
440 let t' = C.Const (uri,exp_named_subst') in
441 if l = [] then t' else C.Appl (t'::l)
442 | C.Variable _ -> raise ReferenceToVariable
443 | C.CurrentProof (_,_,body,_,_,_) ->
445 (CicSubstitution.subst_vars exp_named_subst' body))
446 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
448 | C.MutInd (uri,i,exp_named_subst) ->
449 let exp_named_subst' =
450 reduceaux_exp_named_subst context l exp_named_subst
452 let t' = C.MutInd (uri,i,exp_named_subst') in
453 if l = [] then t' else C.Appl (t'::l)
454 | C.MutConstruct (uri,i,j,exp_named_subst) ->
455 let exp_named_subst' =
456 reduceaux_exp_named_subst context l exp_named_subst
458 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
459 if l = [] then t' else C.Appl (t'::l)
460 | C.MutCase (mutind,i,outtype,term,pl) ->
464 let (_,_,body) = List.nth fl i in
466 let counter = ref (List.length fl) in
468 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
472 reduceaux context [] body'
473 | C.Appl (C.CoFix (i,fl) :: tl) ->
474 let (_,_,body) = List.nth fl i in
476 let counter = ref (List.length fl) in
478 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
482 let tl' = List.map (reduceaux context []) tl in
483 reduceaux context tl' body'
486 (match decofix (reduceaux context [] term) with
487 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
488 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
490 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
492 C.InductiveDefinition (tl,_,r,_) ->
493 let (_,_,arity,_) = List.nth tl i in
495 | _ -> raise WrongUriToInductiveDefinition
501 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
502 | _ -> raise (Impossible 5)
506 reduceaux context (ts@l) (List.nth pl (j-1))
507 | C.Cast _ | C.Implicit _ ->
508 raise (Impossible 2) (* we don't trust our whd ;-) *)
510 let outtype' = reduceaux context [] outtype in
511 let term' = reduceaux context [] term in
512 let pl' = List.map (reduceaux context []) pl in
514 C.MutCase (mutind,i,outtype',term',pl')
516 if l = [] then res else C.Appl (res::l)
521 (fun (types,len) (n,_,ty,_) ->
522 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
529 (function (n,recindex,ty,bo) ->
530 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
535 let (_,recindex,_,body) = List.nth fl i in
538 Some (List.nth l recindex)
544 (match reduceaux context [] recparam with
546 | C.Appl ((C.MutConstruct _)::_) ->
548 let counter = ref (List.length fl) in
550 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
554 (* Possible optimization: substituting whd recparam in l*)
555 reduceaux context l body'
556 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
558 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
563 (fun (types,len) (n,ty,_) ->
564 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
571 (function (n,ty,bo) ->
572 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
577 if l = [] then t' else C.Appl (t'::l)
578 and reduceaux_exp_named_subst context l =
579 List.map (function uri,t -> uri,reduceaux context [] t)
584 exception WrongShape;;
585 exception AlreadySimplified;;
587 (* Takes a well-typed term and *)
588 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
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.1) 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 performs step 3.2). *)
597 (* 3.1) Folds the application of the constant to the arguments that did not *)
598 (* change in every iteration, i.e. to the actual arguments for the *)
599 (* lambda-abstractions that precede the Fix. *)
600 (* 3.2) Computes the head beta-zeta normal form of the term. Then it tries *)
601 (* reductions. If the reduction cannot be performed, it returns the *)
602 (* original term (not the head beta-zeta normal form of the definiendum) *)
603 (*CSC: It does not perform simplification in a Case *)
606 (* a simplified term is active if it can create a redex when used as an *)
607 (* actual parameter *)
612 | C.Appl (C.MutConstruct _::_)
614 | C.Cast (bo,_) -> is_active bo
615 | C.LetIn _ -> assert false
618 (* reduceaux is equal to the reduceaux locally defined inside *)
619 (* reduce, but for the const case. *)
621 let rec reduceaux context l =
624 (* we never perform delta expansion automatically *)
625 if l = [] then t else C.Appl (t::l)
626 | C.Var (uri,exp_named_subst) ->
627 let exp_named_subst' =
628 reduceaux_exp_named_subst context l exp_named_subst
630 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
632 C.Constant _ -> raise ReferenceToConstant
633 | C.CurrentProof _ -> raise ReferenceToCurrentProof
634 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
635 | C.Variable (_,None,_,_,_) ->
636 let t' = C.Var (uri,exp_named_subst') in
637 if l = [] then t' else C.Appl (t'::l)
638 | C.Variable (_,Some body,_,_,_) ->
640 (CicSubstitution.subst_vars exp_named_subst' body)
642 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
643 | C.Sort _ as t -> t (* l should be empty *)
644 | C.Implicit _ as t -> t
646 C.Cast (reduceaux context l te, reduceaux context [] ty)
647 | C.Prod (name,s,t) ->
650 reduceaux context [] s,
651 reduceaux ((Some (name,C.Decl s))::context) [] t)
652 | C.Lambda (name,s,t) ->
656 reduceaux context [] s,
657 reduceaux ((Some (name,C.Decl s))::context) [] t)
658 | he::tl -> reduceaux context tl (S.subst he t)
659 (* when name is Anonimous the substitution should be superfluous *)
662 reduceaux context l (S.subst (reduceaux context [] s) t)
664 let tl' = List.map (reduceaux context []) tl in
665 reduceaux context (tl'@l) he
666 | C.Appl [] -> raise (Impossible 1)
667 | C.Const (uri,exp_named_subst) ->
668 let exp_named_subst' =
669 reduceaux_exp_named_subst context l exp_named_subst
671 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
673 C.Constant (_,Some body,_,_,_) ->
674 if List.exists is_active l then
675 try_delta_expansion context l
676 (C.Const (uri,exp_named_subst'))
677 (CicSubstitution.subst_vars exp_named_subst' body)
679 let t' = C.Const (uri,exp_named_subst') in
680 if l = [] then t' else C.Appl (t'::l)
681 | C.Constant (_,None,_,_,_) ->
682 let t' = C.Const (uri,exp_named_subst') in
683 if l = [] then t' else C.Appl (t'::l)
684 | C.Variable _ -> raise ReferenceToVariable
685 | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
686 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
688 | C.MutInd (uri,i,exp_named_subst) ->
689 let exp_named_subst' =
690 reduceaux_exp_named_subst context l exp_named_subst
692 let t' = C.MutInd (uri,i,exp_named_subst') in
693 if l = [] then t' else C.Appl (t'::l)
694 | C.MutConstruct (uri,i,j,exp_named_subst) ->
695 let exp_named_subst' =
696 reduceaux_exp_named_subst context l exp_named_subst
698 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
699 if l = [] then t' else C.Appl (t'::l)
700 | C.MutCase (mutind,i,outtype,term,pl) ->
704 let (_,_,body) = List.nth fl i in
706 let counter = ref (List.length fl) in
708 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
712 reduceaux context [] body'
713 | C.Appl (C.CoFix (i,fl) :: tl) ->
714 let (_,_,body) = List.nth fl i in
716 let counter = ref (List.length fl) in
718 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
722 let tl' = List.map (reduceaux context []) tl in
723 reduceaux context tl' body'
726 (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
727 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
728 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
730 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
732 C.InductiveDefinition (tl,ingredients,r,_) ->
733 let (_,_,arity,_) = List.nth tl i in
735 | _ -> raise WrongUriToInductiveDefinition
741 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
742 | _ -> raise (Impossible 5)
746 reduceaux context (ts@l) (List.nth pl (j-1))
747 | C.Cast _ | C.Implicit _ ->
748 raise (Impossible 2) (* we don't trust our whd ;-) *)
750 let outtype' = reduceaux context [] outtype in
751 let term' = reduceaux context [] term in
752 let pl' = List.map (reduceaux context []) pl in
754 C.MutCase (mutind,i,outtype',term',pl')
756 if l = [] then res else C.Appl (res::l)
761 (fun (types,len) (n,_,ty,_) ->
762 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
769 (function (n,recindex,ty,bo) ->
770 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
775 let (_,recindex,_,body) = List.nth fl i in
778 Some (List.nth l recindex)
784 (match reduceaux context [] recparam with
786 | C.Appl ((C.MutConstruct _)::_) ->
788 let counter = ref (List.length fl) in
790 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
794 (* Possible optimization: substituting whd recparam in l*)
795 reduceaux context l body'
796 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
798 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
803 (fun (types,len) (n,ty,_) ->
804 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
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 =
823 let res,constant_args =
824 let rec aux rev_constant_args l =
826 C.Lambda (name,s,t) ->
829 [] -> raise WrongShape
831 (* when name is Anonimous the substitution should *)
833 aux (he::rev_constant_args) tl (S.subst he t)
836 aux rev_constant_args l (S.subst s t)
838 let (_,recindex,_,body) = List.nth fl i in
843 _ -> raise AlreadySimplified
845 (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
847 | C.Appl ((C.MutConstruct _)::_) ->
849 let counter = ref (List.length fl) in
852 decr counter ; S.subst (C.Fix (!counter,fl))
855 (* Possible optimization: substituting whd *)
857 reduceaux context l body',
858 List.rev rev_constant_args
859 | _ -> raise AlreadySimplified
861 | _ -> raise WrongShape
866 let term_to_fold, delta_expanded_term_to_fold =
867 match constant_args with
869 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
871 let simplified_term_to_fold =
872 reduceaux context [] delta_expanded_term_to_fold
874 replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res
880 C.Lambda (name,s,t) ->
882 [] -> raise AlreadySimplified
884 (* when name is Anonimous the substitution should *)
886 aux tl (S.subst he t))
887 | C.LetIn (_,s,t) -> aux l (S.subst s t)
889 let simplified = reduceaux context l t in
890 let t' = if l = [] then t else C.Appl (t::l) in
891 if t' = simplified then
892 raise AlreadySimplified
899 if l = [] then term else C.Appl (term::l))
900 | AlreadySimplified ->
901 (* If we performed delta-reduction, we would find a Fix *)
902 (* not applied to a constructor. So, we refuse to perform *)
903 (* delta-reduction. *)
904 if l = [] then term else C.Appl (term::l)
909 let unfold ?what context where =
910 let contextlen = List.length context in
911 let first_is_the_expandable_head_of_second context' t1 t2 =
913 Cic.Const (uri,_), Cic.Const (uri',_)
914 | Cic.Var (uri,_), Cic.Var (uri',_)
915 | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
916 | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
918 | Cic.Var _, _ -> false
919 | Cic.Rel n, Cic.Rel m
920 | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
921 n + (List.length context' - contextlen) = m
922 | Cic.Rel _, _ -> false
925 (ProofEngineTypes.Fail
926 (lazy "The term to unfold is not a constant, a variable or a bound variable "))
929 if tl = [] then he else Cic.Appl (he::tl) in
930 let cannot_delta_expand t =
932 (ProofEngineTypes.Fail
933 (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
934 let rec hd_delta_beta context tl =
938 match List.nth context (n-1) with
939 Some (_,Cic.Decl _) -> cannot_delta_expand t
940 | Some (_,Cic.Def (bo,_)) ->
941 CicReduction.head_beta_reduce
942 (appl (CicSubstitution.lift n bo) tl)
943 | None -> raise RelToHiddenHypothesis
945 Failure _ -> assert false)
946 | Cic.Const (uri,exp_named_subst) as t ->
947 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
949 Cic.Constant (_,Some body,_,_,_) ->
950 CicReduction.head_beta_reduce
951 (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
952 | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
953 | Cic.Variable _ -> raise ReferenceToVariable
954 | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
955 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
957 | Cic.Var (uri,exp_named_subst) as t ->
958 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
960 Cic.Constant _ -> raise ReferenceToConstant
961 | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
962 | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
963 | Cic.Variable (_,Some body,_,_,_) ->
964 CicReduction.head_beta_reduce
965 (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
966 | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
968 | Cic.Appl [] -> assert false
969 | Cic.Appl (he::tl) -> hd_delta_beta context tl he
970 | t -> cannot_delta_expand t
972 let context_and_matched_term_list =
974 None -> [context, where]
977 ProofEngineHelpers.locate_in_term
978 ~equality:first_is_the_expandable_head_of_second
983 (ProofEngineTypes.Fail
984 (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
990 (function (context,where) -> hd_delta_beta context [] where)
991 context_and_matched_term_list in
992 let whats = List.map snd context_and_matched_term_list in
993 replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where