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 (* "textual" replacement of a subterm with another one *)
121 let replace ~equality ~what ~with_what ~where =
122 let module C = Cic in
125 t when (equality t what) -> with_what
127 | C.Var (uri,exp_named_subst) ->
128 C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
131 | C.Implicit as t -> t
132 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
133 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
134 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
135 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
137 (* Invariant enforced: no application of an application *)
138 (match List.map aux l with
139 (C.Appl l')::tl -> C.Appl (l'@tl)
141 | C.Const (uri,exp_named_subst) ->
142 C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
143 | C.MutInd (uri,i,exp_named_subst) ->
145 (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
146 | C.MutConstruct (uri,i,j,exp_named_subst) ->
148 (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
149 | C.MutCase (sp,i,outt,t,pl) ->
150 C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
154 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
157 C.Fix (i, substitutedfl)
161 (fun (name,ty,bo) -> (name, aux ty, aux bo))
164 C.CoFix (i, substitutedfl)
169 (* replaces in a term a term with another one. *)
170 (* Lifting are performed as usual. *)
171 let replace_lifting ~equality ~what ~with_what ~where =
172 let rec substaux k what =
173 let module C = Cic in
174 let module S = CicSubstitution in
176 t when (equality t what) -> S.lift (k-1) with_what
178 | C.Var (uri,exp_named_subst) ->
179 let exp_named_subst' =
180 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
182 C.Var (uri,exp_named_subst')
183 | C.Meta (i, l) as t ->
188 | Some t -> Some (substaux k what t)
193 | C.Implicit as t -> t
194 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
196 C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
197 | C.Lambda (n,s,t) ->
198 C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
200 C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
202 (* Invariant: no Appl applied to another Appl *)
203 let tl' = List.map (substaux k what) tl in
205 match substaux k what he with
206 C.Appl l -> C.Appl (l@tl')
207 | _ as he' -> C.Appl (he'::tl')
209 | C.Appl _ -> assert false
210 | C.Const (uri,exp_named_subst) ->
211 let exp_named_subst' =
212 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
214 C.Const (uri,exp_named_subst')
215 | C.MutInd (uri,i,exp_named_subst) ->
216 let exp_named_subst' =
217 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
219 C.MutInd (uri,i,exp_named_subst')
220 | C.MutConstruct (uri,i,j,exp_named_subst) ->
221 let exp_named_subst' =
222 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
224 C.MutConstruct (uri,i,j,exp_named_subst')
225 | C.MutCase (sp,i,outt,t,pl) ->
226 C.MutCase (sp,i,substaux k what outt, substaux k what t,
227 List.map (substaux k what) pl)
229 let len = List.length fl in
232 (fun (name,i,ty,bo) ->
233 (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
236 C.Fix (i, substitutedfl)
238 let len = List.length fl in
242 (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
245 C.CoFix (i, substitutedfl)
247 substaux 1 what where
250 (* replaces in a term a term with another one. *)
251 (* Lifting are performed as usual. *)
252 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
254 let module C = Cic in
255 let module S = CicSubstitution in
257 t when (equality t what) -> S.lift (k-1) with_what
259 if n < k then C.Rel n else C.Rel (n + nnn)
260 | C.Var (uri,exp_named_subst) ->
261 let exp_named_subst' =
262 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
264 C.Var (uri,exp_named_subst')
265 | C.Meta (i, l) as t ->
270 | Some t -> Some (substaux k t)
275 | C.Implicit as t -> t
276 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
278 C.Prod (n, substaux k s, substaux (k + 1) t)
279 | C.Lambda (n,s,t) ->
280 C.Lambda (n, substaux k s, substaux (k + 1) t)
282 C.LetIn (n, substaux k s, substaux (k + 1) t)
284 (* Invariant: no Appl applied to another Appl *)
285 let tl' = List.map (substaux k) tl in
287 match substaux k he with
288 C.Appl l -> C.Appl (l@tl')
289 | _ as he' -> C.Appl (he'::tl')
291 | C.Appl _ -> assert false
292 | C.Const (uri,exp_named_subst) ->
293 let exp_named_subst' =
294 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
296 C.Const (uri,exp_named_subst')
297 | C.MutInd (uri,i,exp_named_subst) ->
298 let exp_named_subst' =
299 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
301 C.MutInd (uri,i,exp_named_subst')
302 | C.MutConstruct (uri,i,j,exp_named_subst) ->
303 let exp_named_subst' =
304 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
306 C.MutConstruct (uri,i,j,exp_named_subst')
307 | C.MutCase (sp,i,outt,t,pl) ->
308 C.MutCase (sp,i,substaux k outt, substaux k t,
309 List.map (substaux k) pl)
311 let len = List.length fl in
314 (fun (name,i,ty,bo) ->
315 (name, i, substaux k ty, substaux (k+len) bo))
318 C.Fix (i, substitutedfl)
320 let len = List.length fl in
324 (name, substaux k ty, substaux (k+len) bo))
327 C.CoFix (i, substitutedfl)
331 in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
334 (* Takes a well-typed term and fully reduces it. *)
335 (*CSC: It does not perform reduction in a Case *)
337 let rec reduceaux context l =
338 let module C = Cic in
339 let module S = CicSubstitution in
342 (match List.nth context (n-1) with
343 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
344 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
345 | None -> raise RelToHiddenHypothesis
347 | C.Var (uri,exp_named_subst) ->
348 let exp_named_subst' =
349 reduceaux_exp_named_subst context l exp_named_subst
351 (match CicEnvironment.get_obj uri with
352 C.Constant _ -> raise ReferenceToConstant
353 | C.CurrentProof _ -> raise ReferenceToCurrentProof
354 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
355 | C.Variable (_,None,_,_) ->
356 let t' = C.Var (uri,exp_named_subst') in
357 if l = [] then t' else C.Appl (t'::l)
358 | C.Variable (_,Some body,_,_) ->
360 (CicSubstitution.subst_vars exp_named_subst' body))
362 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
363 | C.Sort _ as t -> t (* l should be empty *)
364 | C.Implicit as t -> t
366 C.Cast (reduceaux context l te, reduceaux context l ty)
367 | C.Prod (name,s,t) ->
370 reduceaux context [] s,
371 reduceaux ((Some (name,C.Decl s))::context) [] t)
372 | C.Lambda (name,s,t) ->
376 reduceaux context [] s,
377 reduceaux ((Some (name,C.Decl s))::context) [] t)
378 | he::tl -> reduceaux context tl (S.subst he t)
379 (* when name is Anonimous the substitution should be superfluous *)
382 reduceaux context l (S.subst (reduceaux context [] s) t)
384 let tl' = List.map (reduceaux context []) tl in
385 reduceaux context (tl'@l) he
386 | C.Appl [] -> raise (Impossible 1)
387 | C.Const (uri,exp_named_subst) ->
388 let exp_named_subst' =
389 reduceaux_exp_named_subst context l exp_named_subst
391 (match CicEnvironment.get_obj uri with
392 C.Constant (_,Some body,_,_) ->
394 (CicSubstitution.subst_vars exp_named_subst' body))
395 | C.Constant (_,None,_,_) ->
396 let t' = C.Const (uri,exp_named_subst') in
397 if l = [] then t' else C.Appl (t'::l)
398 | C.Variable _ -> raise ReferenceToVariable
399 | C.CurrentProof (_,_,body,_,_) ->
401 (CicSubstitution.subst_vars exp_named_subst' body))
402 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
404 | C.MutInd (uri,i,exp_named_subst) ->
405 let exp_named_subst' =
406 reduceaux_exp_named_subst context l exp_named_subst
408 let t' = C.MutInd (uri,i,exp_named_subst') in
409 if l = [] then t' else C.Appl (t'::l)
410 | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
411 let exp_named_subst' =
412 reduceaux_exp_named_subst context l exp_named_subst
414 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
415 if l = [] then t' else C.Appl (t'::l)
416 | C.MutCase (mutind,i,outtype,term,pl) ->
419 C.CoFix (i,fl) as t ->
421 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
423 let (_,_,body) = List.nth fl i in
425 let counter = ref (List.length fl) in
427 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
431 reduceaux context [] body'
432 | C.Appl (C.CoFix (i,fl) :: tl) ->
434 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
436 let (_,_,body) = List.nth fl i in
438 let counter = ref (List.length fl) in
440 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
444 let tl' = List.map (reduceaux context []) tl in
445 reduceaux context tl' body'
448 (match decofix (reduceaux context [] term) with
449 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
450 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
452 match CicEnvironment.get_obj mutind with
453 C.InductiveDefinition (tl,_,r) ->
454 let (_,_,arity,_) = List.nth tl i in
456 | _ -> raise WrongUriToInductiveDefinition
462 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
463 | _ -> raise (Impossible 5)
467 reduceaux context (ts@l) (List.nth pl (j-1))
468 | C.Cast _ | C.Implicit ->
469 raise (Impossible 2) (* we don't trust our whd ;-) *)
471 let outtype' = reduceaux context [] outtype in
472 let term' = reduceaux context [] term in
473 let pl' = List.map (reduceaux context []) pl in
475 C.MutCase (mutind,i,outtype',term',pl')
477 if l = [] then res else C.Appl (res::l)
481 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
486 (function (n,recindex,ty,bo) ->
487 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
492 let (_,recindex,_,body) = List.nth fl i in
495 Some (List.nth l recindex)
501 (match reduceaux context [] recparam with
503 | C.Appl ((C.MutConstruct _)::_) ->
505 let counter = ref (List.length fl) in
507 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
511 (* Possible optimization: substituting whd recparam in l*)
512 reduceaux context l body'
513 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
515 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
519 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
524 (function (n,ty,bo) ->
525 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
530 if l = [] then t' else C.Appl (t'::l)
531 and reduceaux_exp_named_subst context l =
532 List.map (function uri,t -> uri,reduceaux context [] t)
537 exception WrongShape;;
538 exception AlreadySimplified;;
540 (* Takes a well-typed term and *)
541 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
542 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
543 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
544 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
545 (* is applied again to the new redex; Step 3) is applied to the result *)
546 (* of the recursive simplification. Otherwise, if the Fix can not be *)
547 (* reduced, than the delta-reductions fails and the delta-redex is *)
548 (* not reduced. Otherwise, if the delta-residual is not the *)
549 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
550 (* directly returned, without performing step 3). *)
551 (* 3) Folds the application of the constant to the arguments that did not *)
552 (* change in every iteration, i.e. to the actual arguments for the *)
553 (* lambda-abstractions that precede the Fix. *)
554 (*CSC: It does not perform simplification in a Case *)
556 (* reduceaux is equal to the reduceaux locally defined inside *)
557 (* reduce, but for the const case. *)
559 let rec reduceaux context l =
560 let module C = Cic in
561 let module S = CicSubstitution in
564 (match List.nth context (n-1) with
565 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
566 | Some (_,C.Def bo) ->
567 try_delta_expansion l t (S.lift n bo)
568 | None -> raise RelToHiddenHypothesis
570 | C.Var (uri,exp_named_subst) ->
571 let exp_named_subst' =
572 reduceaux_exp_named_subst context l exp_named_subst
574 (match CicEnvironment.get_obj uri with
575 C.Constant _ -> raise ReferenceToConstant
576 | C.CurrentProof _ -> raise ReferenceToCurrentProof
577 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
578 | C.Variable (_,None,_,_) ->
579 let t' = C.Var (uri,exp_named_subst') in
580 if l = [] then t' else C.Appl (t'::l)
581 | C.Variable (_,Some body,_,_) ->
583 (CicSubstitution.subst_vars exp_named_subst' body)
585 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
586 | C.Sort _ as t -> t (* l should be empty *)
587 | C.Implicit as t -> t
589 C.Cast (reduceaux context l te, reduceaux context l ty)
590 | C.Prod (name,s,t) ->
593 reduceaux context [] s,
594 reduceaux ((Some (name,C.Decl s))::context) [] t)
595 | C.Lambda (name,s,t) ->
599 reduceaux context [] s,
600 reduceaux ((Some (name,C.Decl s))::context) [] t)
601 | he::tl -> reduceaux context tl (S.subst he t)
602 (* when name is Anonimous the substitution should be superfluous *)
605 reduceaux context l (S.subst (reduceaux context [] s) t)
607 let tl' = List.map (reduceaux context []) tl in
608 reduceaux context (tl'@l) he
609 | C.Appl [] -> raise (Impossible 1)
610 | C.Const (uri,exp_named_subst) ->
611 let exp_named_subst' =
612 reduceaux_exp_named_subst context l exp_named_subst
614 (match CicEnvironment.get_obj uri with
615 C.Constant (_,Some body,_,_) ->
616 try_delta_expansion l
617 (C.Const (uri,exp_named_subst'))
618 (CicSubstitution.subst_vars exp_named_subst' body)
619 | C.Constant (_,None,_,_) ->
620 let t' = C.Const (uri,exp_named_subst') in
621 if l = [] then t' else C.Appl (t'::l)
622 | C.Variable _ -> raise ReferenceToVariable
623 | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
624 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
626 | C.MutInd (uri,i,exp_named_subst) ->
627 let exp_named_subst' =
628 reduceaux_exp_named_subst context l exp_named_subst
630 let t' = C.MutInd (uri,i,exp_named_subst') in
631 if l = [] then t' else C.Appl (t'::l)
632 | C.MutConstruct (uri,i,j,exp_named_subst) ->
633 let exp_named_subst' =
634 reduceaux_exp_named_subst context l exp_named_subst
636 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
637 if l = [] then t' else C.Appl (t'::l)
638 | C.MutCase (mutind,i,outtype,term,pl) ->
641 C.CoFix (i,fl) as t ->
643 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
644 let (_,_,body) = List.nth fl i in
646 let counter = ref (List.length fl) in
648 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
652 reduceaux context [] body'
653 | C.Appl (C.CoFix (i,fl) :: tl) ->
655 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
656 let (_,_,body) = List.nth fl i in
658 let counter = ref (List.length fl) in
660 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
664 let tl' = List.map (reduceaux context []) tl in
665 reduceaux context tl body'
668 (match decofix (reduceaux context [] term) with
669 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
670 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
672 match CicEnvironment.get_obj mutind with
673 C.InductiveDefinition (tl,ingredients,r) ->
674 let (_,_,arity,_) = List.nth tl i in
676 | _ -> raise WrongUriToInductiveDefinition
682 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
683 | _ -> raise (Impossible 5)
687 reduceaux context (ts@l) (List.nth pl (j-1))
688 | C.Cast _ | C.Implicit ->
689 raise (Impossible 2) (* we don't trust our whd ;-) *)
691 let outtype' = reduceaux context [] outtype in
692 let term' = reduceaux context [] term in
693 let pl' = List.map (reduceaux context []) pl in
695 C.MutCase (mutind,i,outtype',term',pl')
697 if l = [] then res else C.Appl (res::l)
701 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
706 (function (n,recindex,ty,bo) ->
707 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
712 let (_,recindex,_,body) = List.nth fl i in
715 Some (List.nth l recindex)
721 (match reduceaux context [] recparam with
723 | C.Appl ((C.MutConstruct _)::_) ->
725 let counter = ref (List.length fl) in
727 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
731 (* Possible optimization: substituting whd recparam in l*)
732 reduceaux context l body'
733 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
735 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
739 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
744 (function (n,ty,bo) ->
745 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
750 if l = [] then t' else C.Appl (t'::l)
751 and reduceaux_exp_named_subst context l =
752 List.map (function uri,t -> uri,reduceaux context [] t)
754 and try_delta_expansion l term body =
755 let module C = Cic in
756 let module S = CicSubstitution in
758 let res,constant_args =
759 let rec aux rev_constant_args l =
761 C.Lambda (name,s,t) as t' ->
764 [] -> raise WrongShape
766 (* when name is Anonimous the substitution should *)
768 aux (he::rev_constant_args) tl (S.subst he t)
771 aux rev_constant_args l (S.subst s t)
772 | C.Fix (i,fl) as t ->
774 List.map (function (name,_,ty,_) ->
775 Some (C.Name name, C.Decl ty)) fl
777 let (_,recindex,_,body) = List.nth fl i in
782 _ -> raise AlreadySimplified
784 (match CicReduction.whd context recparam with
786 | C.Appl ((C.MutConstruct _)::_) ->
788 let counter = ref (List.length fl) in
791 decr counter ; S.subst (C.Fix (!counter,fl))
794 (* Possible optimization: substituting whd *)
796 reduceaux context l body',
797 List.rev rev_constant_args
798 | _ -> raise AlreadySimplified
800 | _ -> raise WrongShape
805 let term_to_fold, delta_expanded_term_to_fold =
806 match constant_args with
808 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
810 let simplified_term_to_fold =
811 reduceaux context [] delta_expanded_term_to_fold
813 replace (=) simplified_term_to_fold term_to_fold res
816 (* The constant does not unfold to a Fix lambda-abstracted *)
817 (* w.r.t. zero or more variables. We just perform reduction.*)
818 reduceaux context l body
819 | AlreadySimplified ->
820 (* If we performed delta-reduction, we would find a Fix *)
821 (* not applied to a constructor. So, we refuse to perform *)
822 (* delta-reduction. *)
823 if l = [] then term else C.Appl (term::l)