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 module C = Cic in
187 let module S = CicSubstitution in
188 let find_image what t =
189 let rec find_image_aux =
191 [],[] -> raise Not_found
192 | what::tl1,with_what::tl2 ->
193 if equality t what then with_what else find_image_aux (tl1,tl2)
194 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
196 find_image_aux (what,with_what)
198 let rec substaux k what t =
200 S.lift (k-1) (find_image what t)
204 | C.Var (uri,exp_named_subst) ->
205 let exp_named_subst' =
206 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
208 C.Var (uri,exp_named_subst')
209 | C.Meta (i, l) as t ->
214 | Some t -> Some (substaux k what t)
219 | C.Implicit _ as t -> t
220 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
223 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
224 | C.Lambda (n,s,t) ->
226 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
229 (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
231 (* Invariant: no Appl applied to another Appl *)
232 let tl' = List.map (substaux k what) tl in
234 match substaux k what he with
235 C.Appl l -> C.Appl (l@tl')
236 | _ as he' -> C.Appl (he'::tl')
238 | C.Appl _ -> assert false
239 | C.Const (uri,exp_named_subst) ->
240 let exp_named_subst' =
241 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
243 C.Const (uri,exp_named_subst')
244 | C.MutInd (uri,i,exp_named_subst) ->
245 let exp_named_subst' =
246 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
248 C.MutInd (uri,i,exp_named_subst')
249 | C.MutConstruct (uri,i,j,exp_named_subst) ->
250 let exp_named_subst' =
251 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
253 C.MutConstruct (uri,i,j,exp_named_subst')
254 | C.MutCase (sp,i,outt,t,pl) ->
255 C.MutCase (sp,i,substaux k what outt, substaux k what t,
256 List.map (substaux k what) pl)
258 let len = List.length fl in
261 (fun (name,i,ty,bo) ->
262 (name, i, substaux k what ty,
263 substaux (k+len) (List.map (S.lift len) what) bo)
266 C.Fix (i, substitutedfl)
268 let len = List.length fl in
272 (name, substaux k what ty,
273 substaux (k+len) (List.map (S.lift len) what) bo)
276 C.CoFix (i, substitutedfl)
278 substaux 1 what where
281 (* replaces in a term a list of terms with other ones. *)
282 (* Lifting are performed as usual. *)
283 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
284 let module C = Cic in
285 let module S = CicSubstitution in
287 let rec find_image_aux =
289 [],[] -> raise Not_found
290 | what::tl1,with_what::tl2 ->
291 if equality t what then with_what else find_image_aux (tl1,tl2)
292 | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
294 find_image_aux (what,with_what)
296 let rec substaux k t =
298 S.lift (k-1) (find_image t)
302 if n < k then C.Rel n else C.Rel (n + nnn)
303 | C.Var (uri,exp_named_subst) ->
304 let exp_named_subst' =
305 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
307 C.Var (uri,exp_named_subst')
308 | C.Meta (i, l) as t ->
313 | Some t -> Some (substaux k t)
318 | C.Implicit _ as t -> t
319 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
321 C.Prod (n, substaux k s, substaux (k + 1) t)
322 | C.Lambda (n,s,t) ->
323 C.Lambda (n, substaux k s, substaux (k + 1) t)
325 C.LetIn (n, substaux k s, substaux (k + 1) t)
327 (* Invariant: no Appl applied to another Appl *)
328 let tl' = List.map (substaux k) tl in
330 match substaux k he with
331 C.Appl l -> C.Appl (l@tl')
332 | _ as he' -> C.Appl (he'::tl')
334 | C.Appl _ -> assert false
335 | C.Const (uri,exp_named_subst) ->
336 let exp_named_subst' =
337 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
339 C.Const (uri,exp_named_subst')
340 | C.MutInd (uri,i,exp_named_subst) ->
341 let exp_named_subst' =
342 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
344 C.MutInd (uri,i,exp_named_subst')
345 | C.MutConstruct (uri,i,j,exp_named_subst) ->
346 let exp_named_subst' =
347 List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
349 C.MutConstruct (uri,i,j,exp_named_subst')
350 | C.MutCase (sp,i,outt,t,pl) ->
351 C.MutCase (sp,i,substaux k outt, substaux k t,
352 List.map (substaux k) pl)
354 let len = List.length fl in
357 (fun (name,i,ty,bo) ->
358 (name, i, substaux k ty, substaux (k+len) bo))
361 C.Fix (i, substitutedfl)
363 let len = List.length fl in
367 (name, substaux k ty, substaux (k+len) bo))
370 C.CoFix (i, substitutedfl)
375 (* Takes a well-typed term and fully reduces it. *)
376 (*CSC: It does not perform reduction in a Case *)
378 let rec reduceaux context l =
379 let module C = Cic in
380 let module S = CicSubstitution in
383 (match List.nth context (n-1) with
384 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
385 | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
386 | None -> raise RelToHiddenHypothesis
388 | C.Var (uri,exp_named_subst) ->
389 let exp_named_subst' =
390 reduceaux_exp_named_subst context l exp_named_subst
392 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
394 C.Constant _ -> raise ReferenceToConstant
395 | C.CurrentProof _ -> raise ReferenceToCurrentProof
396 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
397 | C.Variable (_,None,_,_,_) ->
398 let t' = C.Var (uri,exp_named_subst') in
399 if l = [] then t' else C.Appl (t'::l)
400 | C.Variable (_,Some body,_,_,_) ->
402 (CicSubstitution.subst_vars exp_named_subst' body))
404 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
405 | C.Sort _ as t -> t (* l should be empty *)
406 | C.Implicit _ as t -> t
408 C.Cast (reduceaux context l te, reduceaux context l ty)
409 | C.Prod (name,s,t) ->
412 reduceaux context [] s,
413 reduceaux ((Some (name,C.Decl s))::context) [] t)
414 | C.Lambda (name,s,t) ->
418 reduceaux context [] s,
419 reduceaux ((Some (name,C.Decl s))::context) [] t)
420 | he::tl -> reduceaux context tl (S.subst he t)
421 (* when name is Anonimous the substitution should be superfluous *)
424 reduceaux context l (S.subst (reduceaux context [] s) t)
426 let tl' = List.map (reduceaux context []) tl in
427 reduceaux context (tl'@l) he
428 | C.Appl [] -> raise (Impossible 1)
429 | C.Const (uri,exp_named_subst) ->
430 let exp_named_subst' =
431 reduceaux_exp_named_subst context l exp_named_subst
433 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
435 C.Constant (_,Some body,_,_,_) ->
437 (CicSubstitution.subst_vars exp_named_subst' body))
438 | C.Constant (_,None,_,_,_) ->
439 let t' = C.Const (uri,exp_named_subst') in
440 if l = [] then t' else C.Appl (t'::l)
441 | C.Variable _ -> raise ReferenceToVariable
442 | C.CurrentProof (_,_,body,_,_,_) ->
444 (CicSubstitution.subst_vars exp_named_subst' body))
445 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
447 | C.MutInd (uri,i,exp_named_subst) ->
448 let exp_named_subst' =
449 reduceaux_exp_named_subst context l exp_named_subst
451 let t' = C.MutInd (uri,i,exp_named_subst') in
452 if l = [] then t' else C.Appl (t'::l)
453 | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
454 let exp_named_subst' =
455 reduceaux_exp_named_subst context l exp_named_subst
457 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
458 if l = [] then t' else C.Appl (t'::l)
459 | C.MutCase (mutind,i,outtype,term,pl) ->
462 C.CoFix (i,fl) as t ->
464 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
466 let (_,_,body) = List.nth fl i in
468 let counter = ref (List.length fl) in
470 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
474 reduceaux context [] body'
475 | C.Appl (C.CoFix (i,fl) :: tl) ->
477 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
479 let (_,_,body) = List.nth fl i in
481 let counter = ref (List.length fl) in
483 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
487 let tl' = List.map (reduceaux context []) tl in
488 reduceaux context tl' body'
491 (match decofix (reduceaux context [] term) with
492 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
493 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
495 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
497 C.InductiveDefinition (tl,_,r,_) ->
498 let (_,_,arity,_) = List.nth tl i in
500 | _ -> raise WrongUriToInductiveDefinition
506 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
507 | _ -> raise (Impossible 5)
511 reduceaux context (ts@l) (List.nth pl (j-1))
512 | C.Cast _ | C.Implicit _ ->
513 raise (Impossible 2) (* we don't trust our whd ;-) *)
515 let outtype' = reduceaux context [] outtype in
516 let term' = reduceaux context [] term in
517 let pl' = List.map (reduceaux context []) pl in
519 C.MutCase (mutind,i,outtype',term',pl')
521 if l = [] then res else C.Appl (res::l)
525 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
530 (function (n,recindex,ty,bo) ->
531 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
536 let (_,recindex,_,body) = List.nth fl i in
539 Some (List.nth l recindex)
545 (match reduceaux context [] recparam with
547 | C.Appl ((C.MutConstruct _)::_) ->
549 let counter = ref (List.length fl) in
551 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
555 (* Possible optimization: substituting whd recparam in l*)
556 reduceaux context l body'
557 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
559 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
563 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
568 (function (n,ty,bo) ->
569 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
574 if l = [] then t' else C.Appl (t'::l)
575 and reduceaux_exp_named_subst context l =
576 List.map (function uri,t -> uri,reduceaux context [] t)
581 exception WrongShape;;
582 exception AlreadySimplified;;
584 (* Takes a well-typed term and *)
585 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
586 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
587 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
588 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
589 (* is applied again to the new redex; Step 3) is applied to the result *)
590 (* of the recursive simplification. Otherwise, if the Fix can not be *)
591 (* reduced, than the delta-reductions fails and the delta-redex is *)
592 (* not reduced. Otherwise, if the delta-residual is not the *)
593 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
594 (* directly returned, without performing step 3). *)
595 (* 3) Folds the application of the constant to the arguments that did not *)
596 (* change in every iteration, i.e. to the actual arguments for the *)
597 (* lambda-abstractions that precede the Fix. *)
598 (*CSC: It does not perform simplification in a Case *)
600 (* reduceaux is equal to the reduceaux locally defined inside *)
601 (* reduce, but for the const case. *)
603 let rec reduceaux context l =
604 let module C = Cic in
605 let module S = CicSubstitution in
608 (match List.nth context (n-1) with
609 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
610 | Some (_,C.Def (bo,_)) ->
611 try_delta_expansion l t (S.lift n bo)
612 | None -> raise RelToHiddenHypothesis
614 | C.Var (uri,exp_named_subst) ->
615 let exp_named_subst' =
616 reduceaux_exp_named_subst context l exp_named_subst
618 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
620 C.Constant _ -> raise ReferenceToConstant
621 | C.CurrentProof _ -> raise ReferenceToCurrentProof
622 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
623 | C.Variable (_,None,_,_,_) ->
624 let t' = C.Var (uri,exp_named_subst') in
625 if l = [] then t' else C.Appl (t'::l)
626 | C.Variable (_,Some body,_,_,_) ->
628 (CicSubstitution.subst_vars exp_named_subst' body)
630 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
631 | C.Sort _ as t -> t (* l should be empty *)
632 | C.Implicit _ as t -> t
634 C.Cast (reduceaux context l te, reduceaux context l ty)
635 | C.Prod (name,s,t) ->
638 reduceaux context [] s,
639 reduceaux ((Some (name,C.Decl s))::context) [] t)
640 | C.Lambda (name,s,t) ->
644 reduceaux context [] s,
645 reduceaux ((Some (name,C.Decl s))::context) [] t)
646 | he::tl -> reduceaux context tl (S.subst he t)
647 (* when name is Anonimous the substitution should be superfluous *)
650 reduceaux context l (S.subst (reduceaux context [] s) t)
652 let tl' = List.map (reduceaux context []) tl in
653 reduceaux context (tl'@l) he
654 | C.Appl [] -> raise (Impossible 1)
655 | C.Const (uri,exp_named_subst) ->
656 let exp_named_subst' =
657 reduceaux_exp_named_subst context l exp_named_subst
659 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
661 C.Constant (_,Some body,_,_,_) ->
662 try_delta_expansion l
663 (C.Const (uri,exp_named_subst'))
664 (CicSubstitution.subst_vars exp_named_subst' body)
665 | C.Constant (_,None,_,_,_) ->
666 let t' = C.Const (uri,exp_named_subst') in
667 if l = [] then t' else C.Appl (t'::l)
668 | C.Variable _ -> raise ReferenceToVariable
669 | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
670 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
672 | C.MutInd (uri,i,exp_named_subst) ->
673 let exp_named_subst' =
674 reduceaux_exp_named_subst context l exp_named_subst
676 let t' = C.MutInd (uri,i,exp_named_subst') in
677 if l = [] then t' else C.Appl (t'::l)
678 | C.MutConstruct (uri,i,j,exp_named_subst) ->
679 let exp_named_subst' =
680 reduceaux_exp_named_subst context l exp_named_subst
682 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
683 if l = [] then t' else C.Appl (t'::l)
684 | C.MutCase (mutind,i,outtype,term,pl) ->
687 C.CoFix (i,fl) as t ->
689 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
690 let (_,_,body) = List.nth fl i in
692 let counter = ref (List.length fl) in
694 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
698 reduceaux context [] body'
699 | C.Appl (C.CoFix (i,fl) :: tl) ->
701 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
702 let (_,_,body) = List.nth fl i in
704 let counter = ref (List.length fl) in
706 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
710 let tl' = List.map (reduceaux context []) tl in
711 reduceaux context tl body'
714 (match decofix (reduceaux context [] term) with
715 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
716 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
718 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
720 C.InductiveDefinition (tl,ingredients,r,_) ->
721 let (_,_,arity,_) = List.nth tl i in
723 | _ -> raise WrongUriToInductiveDefinition
729 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
730 | _ -> raise (Impossible 5)
734 reduceaux context (ts@l) (List.nth pl (j-1))
735 | C.Cast _ | C.Implicit _ ->
736 raise (Impossible 2) (* we don't trust our whd ;-) *)
738 let outtype' = reduceaux context [] outtype in
739 let term' = reduceaux context [] term in
740 let pl' = List.map (reduceaux context []) pl in
742 C.MutCase (mutind,i,outtype',term',pl')
744 if l = [] then res else C.Appl (res::l)
748 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
753 (function (n,recindex,ty,bo) ->
754 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
759 let (_,recindex,_,body) = List.nth fl i in
762 Some (List.nth l recindex)
768 (match reduceaux context [] recparam with
770 | C.Appl ((C.MutConstruct _)::_) ->
772 let counter = ref (List.length fl) in
774 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
778 (* Possible optimization: substituting whd recparam in l*)
779 reduceaux context l body'
780 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
782 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
786 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
791 (function (n,ty,bo) ->
792 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
797 if l = [] then t' else C.Appl (t'::l)
798 and reduceaux_exp_named_subst context l =
799 List.map (function uri,t -> uri,reduceaux context [] t)
801 and try_delta_expansion l term body =
802 let module C = Cic in
803 let module S = CicSubstitution in
805 let res,constant_args =
806 let rec aux rev_constant_args l =
808 C.Lambda (name,s,t) as t' ->
811 [] -> raise WrongShape
813 (* when name is Anonimous the substitution should *)
815 aux (he::rev_constant_args) tl (S.subst he t)
818 aux rev_constant_args l (S.subst s t)
819 | C.Fix (i,fl) as t ->
821 List.map (function (name,_,ty,_) ->
822 Some (C.Name name, C.Decl ty)) fl
824 let (_,recindex,_,body) = List.nth fl i in
829 _ -> raise AlreadySimplified
831 (match CicReduction.whd context recparam with
833 | C.Appl ((C.MutConstruct _)::_) ->
835 let counter = ref (List.length fl) in
838 decr counter ; S.subst (C.Fix (!counter,fl))
841 (* Possible optimization: substituting whd *)
843 reduceaux context l body',
844 List.rev rev_constant_args
845 | _ -> raise AlreadySimplified
847 | _ -> raise WrongShape
852 let term_to_fold, delta_expanded_term_to_fold =
853 match constant_args with
855 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
857 let simplified_term_to_fold =
858 reduceaux context [] delta_expanded_term_to_fold
860 replace (=) [simplified_term_to_fold] [term_to_fold] res
863 (* The constant does not unfold to a Fix lambda-abstracted *)
864 (* w.r.t. zero or more variables. We just perform reduction.*)
865 reduceaux context l body
866 | AlreadySimplified ->
867 (* If we performed delta-reduction, we would find a Fix *)
868 (* not applied to a constructor. So, we refuse to perform *)
869 (* delta-reduction. *)
870 if l = [] then term else C.Appl (term::l)