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 t what 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 rec substaux k what =
187 let module C = Cic in
188 let module S = CicSubstitution in
190 t when (equality t what) -> S.lift (k-1) with_what
192 | C.Var (uri,exp_named_subst) ->
193 let exp_named_subst' =
194 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
196 C.Var (uri,exp_named_subst')
197 | C.Meta (i, l) as t ->
202 | Some t -> Some (substaux k what t)
207 | C.Implicit as t -> t
208 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
210 C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
211 | C.Lambda (n,s,t) ->
212 C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
214 C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
216 (* Invariant: no Appl applied to another Appl *)
217 let tl' = List.map (substaux k what) tl in
219 match substaux k what he with
220 C.Appl l -> C.Appl (l@tl')
221 | _ as he' -> C.Appl (he'::tl')
223 | C.Appl _ -> assert false
224 | C.Const (uri,exp_named_subst) ->
225 let exp_named_subst' =
226 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
228 C.Const (uri,exp_named_subst')
229 | C.MutInd (uri,i,exp_named_subst) ->
230 let exp_named_subst' =
231 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
233 C.MutInd (uri,i,exp_named_subst')
234 | C.MutConstruct (uri,i,j,exp_named_subst) ->
235 let exp_named_subst' =
236 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
238 C.MutConstruct (uri,i,j,exp_named_subst')
239 | C.MutCase (sp,i,outt,t,pl) ->
240 C.MutCase (sp,i,substaux k what outt, substaux k what t,
241 List.map (substaux k what) pl)
243 let len = List.length fl in
246 (fun (name,i,ty,bo) ->
247 (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
250 C.Fix (i, substitutedfl)
252 let len = List.length fl in
256 (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
259 C.CoFix (i, substitutedfl)
261 substaux 1 what where
264 (* replaces in a term a list of terms with other ones. *)
265 (* Lifting are performed as usual. *)
266 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
267 let module C = Cic in
268 let module S = CicSubstitution in
270 let rec find_image_aux =
272 [],[] -> raise Not_found
273 | what::tl1,with_what::tl2 ->
274 if equality t what then with_what else find_image_aux (tl1,tl2)
275 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
277 find_image_aux (what,with_what)
279 let rec substaux k t =
281 S.lift (k-1) (find_image t)
285 if n < k then C.Rel n else C.Rel (n + nnn)
286 | C.Var (uri,exp_named_subst) ->
287 let exp_named_subst' =
288 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
290 C.Var (uri,exp_named_subst')
291 | C.Meta (i, l) as t ->
296 | Some t -> Some (substaux k t)
301 | C.Implicit as t -> t
302 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
304 C.Prod (n, substaux k s, substaux (k + 1) t)
305 | C.Lambda (n,s,t) ->
306 C.Lambda (n, substaux k s, substaux (k + 1) t)
308 C.LetIn (n, substaux k s, substaux (k + 1) t)
310 (* Invariant: no Appl applied to another Appl *)
311 let tl' = List.map (substaux k) tl in
313 match substaux k he with
314 C.Appl l -> C.Appl (l@tl')
315 | _ as he' -> C.Appl (he'::tl')
317 | C.Appl _ -> assert false
318 | C.Const (uri,exp_named_subst) ->
319 let exp_named_subst' =
320 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
322 C.Const (uri,exp_named_subst')
323 | C.MutInd (uri,i,exp_named_subst) ->
324 let exp_named_subst' =
325 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
327 C.MutInd (uri,i,exp_named_subst')
328 | C.MutConstruct (uri,i,j,exp_named_subst) ->
329 let exp_named_subst' =
330 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
332 C.MutConstruct (uri,i,j,exp_named_subst')
333 | C.MutCase (sp,i,outt,t,pl) ->
334 C.MutCase (sp,i,substaux k outt, substaux k t,
335 List.map (substaux k) pl)
337 let len = List.length fl in
340 (fun (name,i,ty,bo) ->
341 (name, i, substaux k ty, substaux (k+len) bo))
344 C.Fix (i, substitutedfl)
346 let len = List.length fl in
350 (name, substaux k ty, substaux (k+len) bo))
353 C.CoFix (i, substitutedfl)
358 (* Takes a well-typed term and fully reduces it. *)
359 (*CSC: It does not perform reduction in a Case *)
361 let rec reduceaux context l =
362 let module C = Cic in
363 let module S = CicSubstitution in
366 (match List.nth context (n-1) with
367 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
368 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
369 | None -> raise RelToHiddenHypothesis
371 | C.Var (uri,exp_named_subst) ->
372 let exp_named_subst' =
373 reduceaux_exp_named_subst context l exp_named_subst
375 (match CicEnvironment.get_obj uri with
376 C.Constant _ -> raise ReferenceToConstant
377 | C.CurrentProof _ -> raise ReferenceToCurrentProof
378 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
379 | C.Variable (_,None,_,_) ->
380 let t' = C.Var (uri,exp_named_subst') in
381 if l = [] then t' else C.Appl (t'::l)
382 | C.Variable (_,Some body,_,_) ->
384 (CicSubstitution.subst_vars exp_named_subst' body))
386 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
387 | C.Sort _ as t -> t (* l should be empty *)
388 | C.Implicit as t -> t
390 C.Cast (reduceaux context l te, reduceaux context l ty)
391 | C.Prod (name,s,t) ->
394 reduceaux context [] s,
395 reduceaux ((Some (name,C.Decl s))::context) [] t)
396 | C.Lambda (name,s,t) ->
400 reduceaux context [] s,
401 reduceaux ((Some (name,C.Decl s))::context) [] t)
402 | he::tl -> reduceaux context tl (S.subst he t)
403 (* when name is Anonimous the substitution should be superfluous *)
406 reduceaux context l (S.subst (reduceaux context [] s) t)
408 let tl' = List.map (reduceaux context []) tl in
409 reduceaux context (tl'@l) he
410 | C.Appl [] -> raise (Impossible 1)
411 | C.Const (uri,exp_named_subst) ->
412 let exp_named_subst' =
413 reduceaux_exp_named_subst context l exp_named_subst
415 (match CicEnvironment.get_obj uri with
416 C.Constant (_,Some body,_,_) ->
418 (CicSubstitution.subst_vars exp_named_subst' body))
419 | C.Constant (_,None,_,_) ->
420 let t' = C.Const (uri,exp_named_subst') in
421 if l = [] then t' else C.Appl (t'::l)
422 | C.Variable _ -> raise ReferenceToVariable
423 | C.CurrentProof (_,_,body,_,_) ->
425 (CicSubstitution.subst_vars exp_named_subst' body))
426 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
428 | C.MutInd (uri,i,exp_named_subst) ->
429 let exp_named_subst' =
430 reduceaux_exp_named_subst context l exp_named_subst
432 let t' = C.MutInd (uri,i,exp_named_subst') in
433 if l = [] then t' else C.Appl (t'::l)
434 | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
435 let exp_named_subst' =
436 reduceaux_exp_named_subst context l exp_named_subst
438 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
439 if l = [] then t' else C.Appl (t'::l)
440 | C.MutCase (mutind,i,outtype,term,pl) ->
443 C.CoFix (i,fl) as t ->
445 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
447 let (_,_,body) = List.nth fl i in
449 let counter = ref (List.length fl) in
451 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
455 reduceaux context [] body'
456 | C.Appl (C.CoFix (i,fl) :: tl) ->
458 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
460 let (_,_,body) = List.nth fl i in
462 let counter = ref (List.length fl) in
464 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
468 let tl' = List.map (reduceaux context []) tl in
469 reduceaux context tl' body'
472 (match decofix (reduceaux context [] term) with
473 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
474 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
476 match CicEnvironment.get_obj mutind with
477 C.InductiveDefinition (tl,_,r) ->
478 let (_,_,arity,_) = List.nth tl i in
480 | _ -> raise WrongUriToInductiveDefinition
486 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
487 | _ -> raise (Impossible 5)
491 reduceaux context (ts@l) (List.nth pl (j-1))
492 | C.Cast _ | C.Implicit ->
493 raise (Impossible 2) (* we don't trust our whd ;-) *)
495 let outtype' = reduceaux context [] outtype in
496 let term' = reduceaux context [] term in
497 let pl' = List.map (reduceaux context []) pl in
499 C.MutCase (mutind,i,outtype',term',pl')
501 if l = [] then res else C.Appl (res::l)
505 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
510 (function (n,recindex,ty,bo) ->
511 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
516 let (_,recindex,_,body) = List.nth fl i in
519 Some (List.nth l recindex)
525 (match reduceaux context [] recparam with
527 | C.Appl ((C.MutConstruct _)::_) ->
529 let counter = ref (List.length fl) in
531 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
535 (* Possible optimization: substituting whd recparam in l*)
536 reduceaux context l body'
537 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
539 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
543 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
548 (function (n,ty,bo) ->
549 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
554 if l = [] then t' else C.Appl (t'::l)
555 and reduceaux_exp_named_subst context l =
556 List.map (function uri,t -> uri,reduceaux context [] t)
561 exception WrongShape;;
562 exception AlreadySimplified;;
564 (* Takes a well-typed term and *)
565 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
566 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
567 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
568 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
569 (* is applied again to the new redex; Step 3) is applied to the result *)
570 (* of the recursive simplification. Otherwise, if the Fix can not be *)
571 (* reduced, than the delta-reductions fails and the delta-redex is *)
572 (* not reduced. Otherwise, if the delta-residual is not the *)
573 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
574 (* directly returned, without performing step 3). *)
575 (* 3) Folds the application of the constant to the arguments that did not *)
576 (* change in every iteration, i.e. to the actual arguments for the *)
577 (* lambda-abstractions that precede the Fix. *)
578 (*CSC: It does not perform simplification in a Case *)
580 (* reduceaux is equal to the reduceaux locally defined inside *)
581 (* reduce, but for the const case. *)
583 let rec reduceaux context l =
584 let module C = Cic in
585 let module S = CicSubstitution in
588 (match List.nth context (n-1) with
589 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
590 | Some (_,C.Def bo) ->
591 try_delta_expansion l t (S.lift n bo)
592 | None -> raise RelToHiddenHypothesis
594 | C.Var (uri,exp_named_subst) ->
595 let exp_named_subst' =
596 reduceaux_exp_named_subst context l exp_named_subst
598 (match CicEnvironment.get_obj uri with
599 C.Constant _ -> raise ReferenceToConstant
600 | C.CurrentProof _ -> raise ReferenceToCurrentProof
601 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
602 | C.Variable (_,None,_,_) ->
603 let t' = C.Var (uri,exp_named_subst') in
604 if l = [] then t' else C.Appl (t'::l)
605 | C.Variable (_,Some body,_,_) ->
607 (CicSubstitution.subst_vars exp_named_subst' body)
609 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
610 | C.Sort _ as t -> t (* l should be empty *)
611 | C.Implicit as t -> t
613 C.Cast (reduceaux context l te, reduceaux context l ty)
614 | C.Prod (name,s,t) ->
617 reduceaux context [] s,
618 reduceaux ((Some (name,C.Decl s))::context) [] t)
619 | C.Lambda (name,s,t) ->
623 reduceaux context [] s,
624 reduceaux ((Some (name,C.Decl s))::context) [] t)
625 | he::tl -> reduceaux context tl (S.subst he t)
626 (* when name is Anonimous the substitution should be superfluous *)
629 reduceaux context l (S.subst (reduceaux context [] s) t)
631 let tl' = List.map (reduceaux context []) tl in
632 reduceaux context (tl'@l) he
633 | C.Appl [] -> raise (Impossible 1)
634 | C.Const (uri,exp_named_subst) ->
635 let exp_named_subst' =
636 reduceaux_exp_named_subst context l exp_named_subst
638 (match CicEnvironment.get_obj uri with
639 C.Constant (_,Some body,_,_) ->
640 try_delta_expansion l
641 (C.Const (uri,exp_named_subst'))
642 (CicSubstitution.subst_vars exp_named_subst' body)
643 | C.Constant (_,None,_,_) ->
644 let t' = C.Const (uri,exp_named_subst') in
645 if l = [] then t' else C.Appl (t'::l)
646 | C.Variable _ -> raise ReferenceToVariable
647 | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
648 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
650 | C.MutInd (uri,i,exp_named_subst) ->
651 let exp_named_subst' =
652 reduceaux_exp_named_subst context l exp_named_subst
654 let t' = C.MutInd (uri,i,exp_named_subst') in
655 if l = [] then t' else C.Appl (t'::l)
656 | C.MutConstruct (uri,i,j,exp_named_subst) ->
657 let exp_named_subst' =
658 reduceaux_exp_named_subst context l exp_named_subst
660 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
661 if l = [] then t' else C.Appl (t'::l)
662 | C.MutCase (mutind,i,outtype,term,pl) ->
665 C.CoFix (i,fl) as t ->
667 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
668 let (_,_,body) = List.nth fl i in
670 let counter = ref (List.length fl) in
672 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
676 reduceaux context [] body'
677 | C.Appl (C.CoFix (i,fl) :: tl) ->
679 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
680 let (_,_,body) = List.nth fl i in
682 let counter = ref (List.length fl) in
684 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
688 let tl' = List.map (reduceaux context []) tl in
689 reduceaux context tl body'
692 (match decofix (reduceaux context [] term) with
693 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
694 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
696 match CicEnvironment.get_obj mutind with
697 C.InductiveDefinition (tl,ingredients,r) ->
698 let (_,_,arity,_) = List.nth tl i in
700 | _ -> raise WrongUriToInductiveDefinition
706 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
707 | _ -> raise (Impossible 5)
711 reduceaux context (ts@l) (List.nth pl (j-1))
712 | C.Cast _ | C.Implicit ->
713 raise (Impossible 2) (* we don't trust our whd ;-) *)
715 let outtype' = reduceaux context [] outtype in
716 let term' = reduceaux context [] term in
717 let pl' = List.map (reduceaux context []) pl in
719 C.MutCase (mutind,i,outtype',term',pl')
721 if l = [] then res else C.Appl (res::l)
725 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
730 (function (n,recindex,ty,bo) ->
731 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
736 let (_,recindex,_,body) = List.nth fl i in
739 Some (List.nth l recindex)
745 (match reduceaux context [] recparam with
747 | C.Appl ((C.MutConstruct _)::_) ->
749 let counter = ref (List.length fl) in
751 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
755 (* Possible optimization: substituting whd recparam in l*)
756 reduceaux context l body'
757 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
759 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
763 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
768 (function (n,ty,bo) ->
769 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
774 if l = [] then t' else C.Appl (t'::l)
775 and reduceaux_exp_named_subst context l =
776 List.map (function uri,t -> uri,reduceaux context [] t)
778 and try_delta_expansion l term body =
779 let module C = Cic in
780 let module S = CicSubstitution in
782 let res,constant_args =
783 let rec aux rev_constant_args l =
785 C.Lambda (name,s,t) as t' ->
788 [] -> raise WrongShape
790 (* when name is Anonimous the substitution should *)
792 aux (he::rev_constant_args) tl (S.subst he t)
795 aux rev_constant_args l (S.subst s t)
796 | C.Fix (i,fl) as t ->
798 List.map (function (name,_,ty,_) ->
799 Some (C.Name name, C.Decl ty)) fl
801 let (_,recindex,_,body) = List.nth fl i in
806 _ -> raise AlreadySimplified
808 (match CicReduction.whd context recparam with
810 | C.Appl ((C.MutConstruct _)::_) ->
812 let counter = ref (List.length fl) in
815 decr counter ; S.subst (C.Fix (!counter,fl))
818 (* Possible optimization: substituting whd *)
820 reduceaux context l body',
821 List.rev rev_constant_args
822 | _ -> raise AlreadySimplified
824 | _ -> raise WrongShape
829 let term_to_fold, delta_expanded_term_to_fold =
830 match constant_args with
832 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
834 let simplified_term_to_fold =
835 reduceaux context [] delta_expanded_term_to_fold
837 replace (=) [simplified_term_to_fold] [term_to_fold] res
840 (* The constant does not unfold to a Fix lambda-abstracted *)
841 (* w.r.t. zero or more variables. We just perform reduction.*)
842 reduceaux context l body
843 | AlreadySimplified ->
844 (* If we performed delta-reduction, we would find a Fix *)
845 (* not applied to a constructor. So, we refuse to perform *)
846 (* delta-reduction. *)
847 if l = [] then term else C.Appl (term::l)