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 (* Takes a well-typed term and fully reduces it. *)
251 (*CSC: It does not perform reduction in a Case *)
253 let rec reduceaux context l =
254 let module C = Cic in
255 let module S = CicSubstitution in
258 (match List.nth context (n-1) with
259 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
260 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
261 | None -> raise RelToHiddenHypothesis
263 | C.Var (uri,exp_named_subst) ->
264 let exp_named_subst' =
265 reduceaux_exp_named_subst context l exp_named_subst
267 (match CicEnvironment.get_obj uri with
268 C.Constant _ -> raise ReferenceToConstant
269 | C.CurrentProof _ -> raise ReferenceToCurrentProof
270 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
271 | C.Variable (_,None,_,_) ->
272 let t' = C.Var (uri,exp_named_subst') in
273 if l = [] then t' else C.Appl (t'::l)
274 | C.Variable (_,Some body,_,_) ->
276 (CicSubstitution.subst_vars exp_named_subst' body))
278 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
279 | C.Sort _ as t -> t (* l should be empty *)
280 | C.Implicit as t -> t
282 C.Cast (reduceaux context l te, reduceaux context l ty)
283 | C.Prod (name,s,t) ->
286 reduceaux context [] s,
287 reduceaux ((Some (name,C.Decl s))::context) [] t)
288 | C.Lambda (name,s,t) ->
292 reduceaux context [] s,
293 reduceaux ((Some (name,C.Decl s))::context) [] t)
294 | he::tl -> reduceaux context tl (S.subst he t)
295 (* when name is Anonimous the substitution should be superfluous *)
298 reduceaux context l (S.subst (reduceaux context [] s) t)
300 let tl' = List.map (reduceaux context []) tl in
301 reduceaux context (tl'@l) he
302 | C.Appl [] -> raise (Impossible 1)
303 | C.Const (uri,exp_named_subst) ->
304 let exp_named_subst' =
305 reduceaux_exp_named_subst context l exp_named_subst
307 (match CicEnvironment.get_obj uri with
308 C.Constant (_,Some body,_,_) ->
310 (CicSubstitution.subst_vars exp_named_subst' body))
311 | C.Constant (_,None,_,_) ->
312 let t' = C.Const (uri,exp_named_subst') in
313 if l = [] then t' else C.Appl (t'::l)
314 | C.Variable _ -> raise ReferenceToVariable
315 | C.CurrentProof (_,_,body,_,_) ->
317 (CicSubstitution.subst_vars exp_named_subst' body))
318 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
320 | C.MutInd (uri,i,exp_named_subst) ->
321 let exp_named_subst' =
322 reduceaux_exp_named_subst context l exp_named_subst
324 let t' = C.MutInd (uri,i,exp_named_subst') in
325 if l = [] then t' else C.Appl (t'::l)
326 | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
327 let exp_named_subst' =
328 reduceaux_exp_named_subst context l exp_named_subst
330 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
331 if l = [] then t' else C.Appl (t'::l)
332 | C.MutCase (mutind,i,outtype,term,pl) ->
335 C.CoFix (i,fl) as t ->
337 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
339 let (_,_,body) = List.nth fl i in
341 let counter = ref (List.length fl) in
343 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
347 reduceaux context [] body'
348 | C.Appl (C.CoFix (i,fl) :: tl) ->
350 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
352 let (_,_,body) = List.nth fl i in
354 let counter = ref (List.length fl) in
356 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
360 let tl' = List.map (reduceaux context []) tl in
361 reduceaux context tl' body'
364 (match decofix (reduceaux context [] term) with
365 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
366 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
368 match CicEnvironment.get_obj mutind with
369 C.InductiveDefinition (tl,_,r) ->
370 let (_,_,arity,_) = List.nth tl i in
372 | _ -> raise WrongUriToInductiveDefinition
378 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
379 | _ -> raise (Impossible 5)
383 reduceaux context (ts@l) (List.nth pl (j-1))
384 | C.Cast _ | C.Implicit ->
385 raise (Impossible 2) (* we don't trust our whd ;-) *)
387 let outtype' = reduceaux context [] outtype in
388 let term' = reduceaux context [] term in
389 let pl' = List.map (reduceaux context []) pl in
391 C.MutCase (mutind,i,outtype',term',pl')
393 if l = [] then res else C.Appl (res::l)
397 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
402 (function (n,recindex,ty,bo) ->
403 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
408 let (_,recindex,_,body) = List.nth fl i in
411 Some (List.nth l recindex)
417 (match reduceaux context [] recparam with
419 | C.Appl ((C.MutConstruct _)::_) ->
421 let counter = ref (List.length fl) in
423 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
427 (* Possible optimization: substituting whd recparam in l*)
428 reduceaux context l body'
429 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
431 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
435 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
440 (function (n,ty,bo) ->
441 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
446 if l = [] then t' else C.Appl (t'::l)
447 and reduceaux_exp_named_subst context l =
448 List.map (function uri,t -> uri,reduceaux context [] t)
453 exception WrongShape;;
454 exception AlreadySimplified;;
456 (* Takes a well-typed term and *)
457 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
458 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
459 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
460 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
461 (* is applied again to the new redex; Step 3) is applied to the result *)
462 (* of the recursive simplification. Otherwise, if the Fix can not be *)
463 (* reduced, than the delta-reductions fails and the delta-redex is *)
464 (* not reduced. Otherwise, if the delta-residual is not the *)
465 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
466 (* directly returned, without performing step 3). *)
467 (* 3) Folds the application of the constant to the arguments that did not *)
468 (* change in every iteration, i.e. to the actual arguments for the *)
469 (* lambda-abstractions that precede the Fix. *)
470 (*CSC: It does not perform simplification in a Case *)
472 (* reduceaux is equal to the reduceaux locally defined inside *)
473 (* reduce, but for the const case. *)
475 let rec reduceaux context l =
476 let module C = Cic in
477 let module S = CicSubstitution in
480 (match List.nth context (n-1) with
481 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
482 | Some (_,C.Def bo) ->
483 try_delta_expansion l t (S.lift n bo)
484 | None -> raise RelToHiddenHypothesis
486 | C.Var (uri,exp_named_subst) ->
487 let exp_named_subst' =
488 reduceaux_exp_named_subst context l exp_named_subst
490 (match CicEnvironment.get_obj uri with
491 C.Constant _ -> raise ReferenceToConstant
492 | C.CurrentProof _ -> raise ReferenceToCurrentProof
493 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
494 | C.Variable (_,None,_,_) ->
495 let t' = C.Var (uri,exp_named_subst') in
496 if l = [] then t' else C.Appl (t'::l)
497 | C.Variable (_,Some body,_,_) ->
499 (CicSubstitution.subst_vars exp_named_subst' body)
501 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
502 | C.Sort _ as t -> t (* l should be empty *)
503 | C.Implicit as t -> t
505 C.Cast (reduceaux context l te, reduceaux context l ty)
506 | C.Prod (name,s,t) ->
509 reduceaux context [] s,
510 reduceaux ((Some (name,C.Decl s))::context) [] t)
511 | C.Lambda (name,s,t) ->
515 reduceaux context [] s,
516 reduceaux ((Some (name,C.Decl s))::context) [] t)
517 | he::tl -> reduceaux context tl (S.subst he t)
518 (* when name is Anonimous the substitution should be superfluous *)
521 reduceaux context l (S.subst (reduceaux context [] s) t)
523 let tl' = List.map (reduceaux context []) tl in
524 reduceaux context (tl'@l) he
525 | C.Appl [] -> raise (Impossible 1)
526 | C.Const (uri,exp_named_subst) ->
527 let exp_named_subst' =
528 reduceaux_exp_named_subst context l exp_named_subst
530 (match CicEnvironment.get_obj uri with
531 C.Constant (_,Some body,_,_) ->
532 try_delta_expansion l
533 (C.Const (uri,exp_named_subst'))
534 (CicSubstitution.subst_vars exp_named_subst' body)
535 | C.Constant (_,None,_,_) ->
536 let t' = C.Const (uri,exp_named_subst') in
537 if l = [] then t' else C.Appl (t'::l)
538 | C.Variable _ -> raise ReferenceToVariable
539 | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
540 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
542 | C.MutInd (uri,i,exp_named_subst) ->
543 let exp_named_subst' =
544 reduceaux_exp_named_subst context l exp_named_subst
546 let t' = C.MutInd (uri,i,exp_named_subst') in
547 if l = [] then t' else C.Appl (t'::l)
548 | C.MutConstruct (uri,i,j,exp_named_subst) ->
549 let exp_named_subst' =
550 reduceaux_exp_named_subst context l exp_named_subst
552 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
553 if l = [] then t' else C.Appl (t'::l)
554 | C.MutCase (mutind,i,outtype,term,pl) ->
557 C.CoFix (i,fl) as t ->
559 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
560 let (_,_,body) = List.nth fl i in
562 let counter = ref (List.length fl) in
564 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
568 reduceaux context [] body'
569 | C.Appl (C.CoFix (i,fl) :: tl) ->
571 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
572 let (_,_,body) = List.nth fl i in
574 let counter = ref (List.length fl) in
576 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
580 let tl' = List.map (reduceaux context []) tl in
581 reduceaux context tl body'
584 (match decofix (reduceaux context [] term) with
585 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
586 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
588 match CicEnvironment.get_obj mutind with
589 C.InductiveDefinition (tl,ingredients,r) ->
590 let (_,_,arity,_) = List.nth tl i in
592 | _ -> raise WrongUriToInductiveDefinition
598 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
599 | _ -> raise (Impossible 5)
603 reduceaux context (ts@l) (List.nth pl (j-1))
604 | C.Cast _ | C.Implicit ->
605 raise (Impossible 2) (* we don't trust our whd ;-) *)
607 let outtype' = reduceaux context [] outtype in
608 let term' = reduceaux context [] term in
609 let pl' = List.map (reduceaux context []) pl in
611 C.MutCase (mutind,i,outtype',term',pl')
613 if l = [] then res else C.Appl (res::l)
617 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
622 (function (n,recindex,ty,bo) ->
623 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
628 let (_,recindex,_,body) = List.nth fl i in
631 Some (List.nth l recindex)
637 (match reduceaux context [] recparam with
639 | C.Appl ((C.MutConstruct _)::_) ->
641 let counter = ref (List.length fl) in
643 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
647 (* Possible optimization: substituting whd recparam in l*)
648 reduceaux context l body'
649 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
651 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
655 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
660 (function (n,ty,bo) ->
661 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
666 if l = [] then t' else C.Appl (t'::l)
667 and reduceaux_exp_named_subst context l =
668 List.map (function uri,t -> uri,reduceaux context [] t)
670 and try_delta_expansion l term body =
671 let module C = Cic in
672 let module S = CicSubstitution in
674 let res,constant_args =
675 let rec aux rev_constant_args l =
677 C.Lambda (name,s,t) as t' ->
680 [] -> raise WrongShape
682 (* when name is Anonimous the substitution should *)
684 aux (he::rev_constant_args) tl (S.subst he t)
687 aux rev_constant_args l (S.subst s t)
688 | C.Fix (i,fl) as t ->
690 List.map (function (name,_,ty,_) ->
691 Some (C.Name name, C.Decl ty)) fl
693 let (_,recindex,_,body) = List.nth fl i in
698 _ -> raise AlreadySimplified
700 (match CicReduction.whd context recparam with
702 | C.Appl ((C.MutConstruct _)::_) ->
704 let counter = ref (List.length fl) in
707 decr counter ; S.subst (C.Fix (!counter,fl))
710 (* Possible optimization: substituting whd *)
712 reduceaux context l body',
713 List.rev rev_constant_args
714 | _ -> raise AlreadySimplified
716 | _ -> raise WrongShape
721 let term_to_fold, delta_expanded_term_to_fold =
722 match constant_args with
724 | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
726 let simplified_term_to_fold =
727 reduceaux context [] delta_expanded_term_to_fold
729 replace (=) simplified_term_to_fold term_to_fold res
732 (* The constant does not unfold to a Fix lambda-abstracted *)
733 (* w.r.t. zero or more variables. We just perform reduction.*)
734 reduceaux context l body
735 | AlreadySimplified ->
736 (* If we performed delta-reduction, we would find a Fix *)
737 (* not applied to a constructor. So, we refuse to perform *)
738 (* delta-reduction. *)
739 if l = [] then term else C.Appl (term::l)