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 term with another one. *)
265 (* Lifting are performed as usual. *)
266 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
268 let module C = Cic in
269 let module S = CicSubstitution in
271 t when (equality t what) -> S.lift (k-1) with_what
273 if n < k then C.Rel n else C.Rel (n + nnn)
274 | C.Var (uri,exp_named_subst) ->
275 let exp_named_subst' =
276 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
278 C.Var (uri,exp_named_subst')
279 | C.Meta (i, l) as t ->
284 | Some t -> Some (substaux k t)
289 | C.Implicit as t -> t
290 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
292 C.Prod (n, substaux k s, substaux (k + 1) t)
293 | C.Lambda (n,s,t) ->
294 C.Lambda (n, substaux k s, substaux (k + 1) t)
296 C.LetIn (n, substaux k s, substaux (k + 1) t)
298 (* Invariant: no Appl applied to another Appl *)
299 let tl' = List.map (substaux k) tl in
301 match substaux k he with
302 C.Appl l -> C.Appl (l@tl')
303 | _ as he' -> C.Appl (he'::tl')
305 | C.Appl _ -> assert false
306 | C.Const (uri,exp_named_subst) ->
307 let exp_named_subst' =
308 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
310 C.Const (uri,exp_named_subst')
311 | C.MutInd (uri,i,exp_named_subst) ->
312 let exp_named_subst' =
313 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
315 C.MutInd (uri,i,exp_named_subst')
316 | C.MutConstruct (uri,i,j,exp_named_subst) ->
317 let exp_named_subst' =
318 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
320 C.MutConstruct (uri,i,j,exp_named_subst')
321 | C.MutCase (sp,i,outt,t,pl) ->
322 C.MutCase (sp,i,substaux k outt, substaux k t,
323 List.map (substaux k) pl)
325 let len = List.length fl in
328 (fun (name,i,ty,bo) ->
329 (name, i, substaux k ty, substaux (k+len) bo))
332 C.Fix (i, substitutedfl)
334 let len = List.length fl in
338 (name, substaux k ty, substaux (k+len) bo))
341 C.CoFix (i, substitutedfl)
345 in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
348 (* Takes a well-typed term and fully reduces it. *)
349 (*CSC: It does not perform reduction in a Case *)
351 let rec reduceaux context l =
352 let module C = Cic in
353 let module S = CicSubstitution in
356 (match List.nth context (n-1) with
357 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
358 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
359 | None -> raise RelToHiddenHypothesis
361 | C.Var (uri,exp_named_subst) ->
362 let exp_named_subst' =
363 reduceaux_exp_named_subst context l exp_named_subst
365 (match CicEnvironment.get_obj uri with
366 C.Constant _ -> raise ReferenceToConstant
367 | C.CurrentProof _ -> raise ReferenceToCurrentProof
368 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
369 | C.Variable (_,None,_,_) ->
370 let t' = C.Var (uri,exp_named_subst') in
371 if l = [] then t' else C.Appl (t'::l)
372 | C.Variable (_,Some body,_,_) ->
374 (CicSubstitution.subst_vars exp_named_subst' body))
376 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
377 | C.Sort _ as t -> t (* l should be empty *)
378 | C.Implicit as t -> t
380 C.Cast (reduceaux context l te, reduceaux context l ty)
381 | C.Prod (name,s,t) ->
384 reduceaux context [] s,
385 reduceaux ((Some (name,C.Decl s))::context) [] t)
386 | C.Lambda (name,s,t) ->
390 reduceaux context [] s,
391 reduceaux ((Some (name,C.Decl s))::context) [] t)
392 | he::tl -> reduceaux context tl (S.subst he t)
393 (* when name is Anonimous the substitution should be superfluous *)
396 reduceaux context l (S.subst (reduceaux context [] s) t)
398 let tl' = List.map (reduceaux context []) tl in
399 reduceaux context (tl'@l) he
400 | C.Appl [] -> raise (Impossible 1)
401 | C.Const (uri,exp_named_subst) ->
402 let exp_named_subst' =
403 reduceaux_exp_named_subst context l exp_named_subst
405 (match CicEnvironment.get_obj uri with
406 C.Constant (_,Some body,_,_) ->
408 (CicSubstitution.subst_vars exp_named_subst' body))
409 | C.Constant (_,None,_,_) ->
410 let t' = C.Const (uri,exp_named_subst') in
411 if l = [] then t' else C.Appl (t'::l)
412 | C.Variable _ -> raise ReferenceToVariable
413 | C.CurrentProof (_,_,body,_,_) ->
415 (CicSubstitution.subst_vars exp_named_subst' body))
416 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
418 | C.MutInd (uri,i,exp_named_subst) ->
419 let exp_named_subst' =
420 reduceaux_exp_named_subst context l exp_named_subst
422 let t' = C.MutInd (uri,i,exp_named_subst') in
423 if l = [] then t' else C.Appl (t'::l)
424 | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
425 let exp_named_subst' =
426 reduceaux_exp_named_subst context l exp_named_subst
428 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
429 if l = [] then t' else C.Appl (t'::l)
430 | C.MutCase (mutind,i,outtype,term,pl) ->
433 C.CoFix (i,fl) as t ->
435 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
437 let (_,_,body) = List.nth fl i in
439 let counter = ref (List.length fl) in
441 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
445 reduceaux context [] body'
446 | C.Appl (C.CoFix (i,fl) :: tl) ->
448 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
450 let (_,_,body) = List.nth fl i in
452 let counter = ref (List.length fl) in
454 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
458 let tl' = List.map (reduceaux context []) tl in
459 reduceaux context tl' body'
462 (match decofix (reduceaux context [] term) with
463 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
464 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
466 match CicEnvironment.get_obj mutind with
467 C.InductiveDefinition (tl,_,r) ->
468 let (_,_,arity,_) = List.nth tl i in
470 | _ -> raise WrongUriToInductiveDefinition
476 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
477 | _ -> raise (Impossible 5)
481 reduceaux context (ts@l) (List.nth pl (j-1))
482 | C.Cast _ | C.Implicit ->
483 raise (Impossible 2) (* we don't trust our whd ;-) *)
485 let outtype' = reduceaux context [] outtype in
486 let term' = reduceaux context [] term in
487 let pl' = List.map (reduceaux context []) pl in
489 C.MutCase (mutind,i,outtype',term',pl')
491 if l = [] then res else C.Appl (res::l)
495 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
500 (function (n,recindex,ty,bo) ->
501 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
506 let (_,recindex,_,body) = List.nth fl i in
509 Some (List.nth l recindex)
515 (match reduceaux context [] recparam with
517 | C.Appl ((C.MutConstruct _)::_) ->
519 let counter = ref (List.length fl) in
521 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
525 (* Possible optimization: substituting whd recparam in l*)
526 reduceaux context l body'
527 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
529 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
533 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
538 (function (n,ty,bo) ->
539 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
544 if l = [] then t' else C.Appl (t'::l)
545 and reduceaux_exp_named_subst context l =
546 List.map (function uri,t -> uri,reduceaux context [] t)
551 exception WrongShape;;
552 exception AlreadySimplified;;
554 (* Takes a well-typed term and *)
555 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
556 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
557 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
558 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
559 (* is applied again to the new redex; Step 3) is applied to the result *)
560 (* of the recursive simplification. Otherwise, if the Fix can not be *)
561 (* reduced, than the delta-reductions fails and the delta-redex is *)
562 (* not reduced. Otherwise, if the delta-residual is not the *)
563 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
564 (* directly returned, without performing step 3). *)
565 (* 3) Folds the application of the constant to the arguments that did not *)
566 (* change in every iteration, i.e. to the actual arguments for the *)
567 (* lambda-abstractions that precede the Fix. *)
568 (*CSC: It does not perform simplification in a Case *)
570 (* reduceaux is equal to the reduceaux locally defined inside *)
571 (* reduce, but for the const case. *)
573 let rec reduceaux context l =
574 let module C = Cic in
575 let module S = CicSubstitution in
578 (match List.nth context (n-1) with
579 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
580 | Some (_,C.Def bo) ->
581 try_delta_expansion l t (S.lift n bo)
582 | None -> raise RelToHiddenHypothesis
584 | C.Var (uri,exp_named_subst) ->
585 let exp_named_subst' =
586 reduceaux_exp_named_subst context l exp_named_subst
588 (match CicEnvironment.get_obj uri with
589 C.Constant _ -> raise ReferenceToConstant
590 | C.CurrentProof _ -> raise ReferenceToCurrentProof
591 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
592 | C.Variable (_,None,_,_) ->
593 let t' = C.Var (uri,exp_named_subst') in
594 if l = [] then t' else C.Appl (t'::l)
595 | C.Variable (_,Some body,_,_) ->
597 (CicSubstitution.subst_vars exp_named_subst' body)
599 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
600 | C.Sort _ as t -> t (* l should be empty *)
601 | C.Implicit as t -> t
603 C.Cast (reduceaux context l te, reduceaux context l ty)
604 | C.Prod (name,s,t) ->
607 reduceaux context [] s,
608 reduceaux ((Some (name,C.Decl s))::context) [] t)
609 | C.Lambda (name,s,t) ->
613 reduceaux context [] s,
614 reduceaux ((Some (name,C.Decl s))::context) [] t)
615 | he::tl -> reduceaux context tl (S.subst he t)
616 (* when name is Anonimous the substitution should be superfluous *)
619 reduceaux context l (S.subst (reduceaux context [] s) t)
621 let tl' = List.map (reduceaux context []) tl in
622 reduceaux context (tl'@l) he
623 | C.Appl [] -> raise (Impossible 1)
624 | C.Const (uri,exp_named_subst) ->
625 let exp_named_subst' =
626 reduceaux_exp_named_subst context l exp_named_subst
628 (match CicEnvironment.get_obj uri with
629 C.Constant (_,Some body,_,_) ->
630 try_delta_expansion l
631 (C.Const (uri,exp_named_subst'))
632 (CicSubstitution.subst_vars exp_named_subst' body)
633 | C.Constant (_,None,_,_) ->
634 let t' = C.Const (uri,exp_named_subst') in
635 if l = [] then t' else C.Appl (t'::l)
636 | C.Variable _ -> raise ReferenceToVariable
637 | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
638 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
640 | C.MutInd (uri,i,exp_named_subst) ->
641 let exp_named_subst' =
642 reduceaux_exp_named_subst context l exp_named_subst
644 let t' = C.MutInd (uri,i,exp_named_subst') in
645 if l = [] then t' else C.Appl (t'::l)
646 | C.MutConstruct (uri,i,j,exp_named_subst) ->
647 let exp_named_subst' =
648 reduceaux_exp_named_subst context l exp_named_subst
650 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
651 if l = [] then t' else C.Appl (t'::l)
652 | C.MutCase (mutind,i,outtype,term,pl) ->
655 C.CoFix (i,fl) as t ->
657 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
658 let (_,_,body) = List.nth fl i in
660 let counter = ref (List.length fl) in
662 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
666 reduceaux context [] body'
667 | C.Appl (C.CoFix (i,fl) :: tl) ->
669 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
670 let (_,_,body) = List.nth fl i in
672 let counter = ref (List.length fl) in
674 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
678 let tl' = List.map (reduceaux context []) tl in
679 reduceaux context tl body'
682 (match decofix (reduceaux context [] term) with
683 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
684 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
686 match CicEnvironment.get_obj mutind with
687 C.InductiveDefinition (tl,ingredients,r) ->
688 let (_,_,arity,_) = List.nth tl i in
690 | _ -> raise WrongUriToInductiveDefinition
696 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
697 | _ -> raise (Impossible 5)
701 reduceaux context (ts@l) (List.nth pl (j-1))
702 | C.Cast _ | C.Implicit ->
703 raise (Impossible 2) (* we don't trust our whd ;-) *)
705 let outtype' = reduceaux context [] outtype in
706 let term' = reduceaux context [] term in
707 let pl' = List.map (reduceaux context []) pl in
709 C.MutCase (mutind,i,outtype',term',pl')
711 if l = [] then res else C.Appl (res::l)
715 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
720 (function (n,recindex,ty,bo) ->
721 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
726 let (_,recindex,_,body) = List.nth fl i in
729 Some (List.nth l recindex)
735 (match reduceaux context [] recparam with
737 | C.Appl ((C.MutConstruct _)::_) ->
739 let counter = ref (List.length fl) in
741 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
745 (* Possible optimization: substituting whd recparam in l*)
746 reduceaux context l body'
747 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
749 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
753 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
758 (function (n,ty,bo) ->
759 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
764 if l = [] then t' else C.Appl (t'::l)
765 and reduceaux_exp_named_subst context l =
766 List.map (function uri,t -> uri,reduceaux context [] t)
768 and try_delta_expansion l term body =
769 let module C = Cic in
770 let module S = CicSubstitution in
772 let res,constant_args =
773 let rec aux rev_constant_args l =
775 C.Lambda (name,s,t) as t' ->
778 [] -> raise WrongShape
780 (* when name is Anonimous the substitution should *)
782 aux (he::rev_constant_args) tl (S.subst he t)
785 aux rev_constant_args l (S.subst s t)
786 | C.Fix (i,fl) as t ->
788 List.map (function (name,_,ty,_) ->
789 Some (C.Name name, C.Decl ty)) fl
791 let (_,recindex,_,body) = List.nth fl i in
796 _ -> raise AlreadySimplified
798 (match CicReduction.whd context recparam with
800 | C.Appl ((C.MutConstruct _)::_) ->
802 let counter = ref (List.length fl) in
805 decr counter ; S.subst (C.Fix (!counter,fl))
808 (* Possible optimization: substituting whd *)
810 reduceaux context l body',
811 List.rev rev_constant_args
812 | _ -> raise AlreadySimplified
814 | _ -> raise WrongShape
819 let term_to_fold, delta_expanded_term_to_fold =
820 match constant_args with
822 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
824 let simplified_term_to_fold =
825 reduceaux context [] delta_expanded_term_to_fold
827 replace (=) [simplified_term_to_fold] [term_to_fold] res
830 (* The constant does not unfold to a Fix lambda-abstracted *)
831 (* w.r.t. zero or more variables. We just perform reduction.*)
832 reduceaux context l body
833 | AlreadySimplified ->
834 (* If we performed delta-reduction, we would find a Fix *)
835 (* not applied to a constructor. So, we refuse to perform *)
836 (* delta-reduction. *)
837 if l = [] then term else C.Appl (term::l)