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 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
457 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
459 (*CSC: {foo [n,m:nat]:nat := *)
460 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
462 (* Takes a well-typed term and *)
463 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
464 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
465 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
466 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
467 (* is applied again to the new redex; Step 3) is applied to the result *)
468 (* of the recursive simplification. Otherwise, if the Fix can not be *)
469 (* reduced, than the delta-reductions fails and the delta-redex is *)
470 (* not reduced. Otherwise, if the delta-residual is not the *)
471 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
472 (* directly returned, without performing step 3). *)
473 (* 3) Folds the application of the constant to the arguments that did not *)
474 (* change in every iteration, i.e. to the actual arguments for the *)
475 (* lambda-abstractions that precede the Fix. *)
476 (*CSC: It does not perform simplification in a Case *)
478 (* reduceaux is equal to the reduceaux locally defined inside *)
479 (* reduce, but for the const case. *)
481 let rec reduceaux context l =
482 let module C = Cic in
483 let module S = CicSubstitution in
486 (match List.nth context (n-1) with
487 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
488 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
489 | None -> raise RelToHiddenHypothesis
491 | C.Var (uri,exp_named_subst) ->
492 let exp_named_subst' =
493 reduceaux_exp_named_subst context l exp_named_subst
495 (match CicEnvironment.get_obj uri with
496 C.Constant _ -> raise ReferenceToConstant
497 | C.CurrentProof _ -> raise ReferenceToCurrentProof
498 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
499 | C.Variable (_,None,_,_) ->
500 let t' = C.Var (uri,exp_named_subst') in
501 if l = [] then t' else C.Appl (t'::l)
502 | C.Variable (_,Some body,_,_) ->
504 (CicSubstitution.subst_vars exp_named_subst' body)
506 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
507 | C.Sort _ as t -> t (* l should be empty *)
508 | C.Implicit as t -> t
510 C.Cast (reduceaux context l te, reduceaux context l ty)
511 | C.Prod (name,s,t) ->
514 reduceaux context [] s,
515 reduceaux ((Some (name,C.Decl s))::context) [] t)
516 | C.Lambda (name,s,t) ->
520 reduceaux context [] s,
521 reduceaux ((Some (name,C.Decl s))::context) [] t)
522 | he::tl -> reduceaux context tl (S.subst he t)
523 (* when name is Anonimous the substitution should be superfluous *)
526 reduceaux context l (S.subst (reduceaux context [] s) t)
528 let tl' = List.map (reduceaux context []) tl in
529 reduceaux context (tl'@l) he
530 | C.Appl [] -> raise (Impossible 1)
531 | C.Const (uri,exp_named_subst) ->
532 let exp_named_subst' =
533 reduceaux_exp_named_subst context l exp_named_subst
535 (match CicEnvironment.get_obj uri with
536 C.Constant (_,Some body,_,_) ->
540 let res,constant_args =
541 let rec aux rev_constant_args l =
543 C.Lambda (name,s,t) as t' ->
546 [] -> raise WrongShape
548 (* when name is Anonimous the substitution should *)
550 aux (he::rev_constant_args) tl (S.subst he t)
553 aux rev_constant_args l (S.subst s t)
554 | C.Fix (i,fl) as t ->
556 List.map (function (name,_,ty,_) ->
557 Some (C.Name name, C.Decl ty)) fl
559 let (_,recindex,_,body) = List.nth fl i in
564 _ -> raise AlreadySimplified
566 (match CicReduction.whd context recparam with
568 | C.Appl ((C.MutConstruct _)::_) ->
570 let counter = ref (List.length fl) in
573 decr counter ; S.subst (C.Fix (!counter,fl))
576 (* Possible optimization: substituting whd *)
578 reduceaux context l body',
579 List.rev rev_constant_args
580 | _ -> raise AlreadySimplified
582 | _ -> raise WrongShape
584 aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
587 let term_to_fold, delta_expanded_term_to_fold =
588 let body' = CicSubstitution.subst_vars exp_named_subst' body in
589 match constant_args with
590 [] -> C.Const (uri,exp_named_subst'), body'
592 C.Appl ((C.Const (uri,exp_named_subst'))::constant_args),
593 C.Appl (body'::constant_args)
595 let simplified_term_to_fold =
596 reduceaux context [] delta_expanded_term_to_fold
598 replace (=) simplified_term_to_fold term_to_fold res
601 (* The constant does not unfold to a Fix lambda-abstracted *)
602 (* w.r.t. zero or more variables. We just perform reduction.*)
604 (CicSubstitution.subst_vars exp_named_subst' body)
605 | AlreadySimplified ->
606 (* If we performed delta-reduction, we would find a Fix *)
607 (* not applied to a constructor. So, we refuse to perform *)
608 (* delta-reduction. *)
609 let t' = C.Const (uri,exp_named_subst') in
610 if l = [] then t' else C.Appl (t'::l)
612 | C.Constant (_,None,_,_) ->
613 let t' = C.Const (uri,exp_named_subst') in
614 if l = [] then t' else C.Appl (t'::l)
615 | C.Variable _ -> raise ReferenceToVariable
616 | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
617 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
619 | C.MutInd (uri,i,exp_named_subst) ->
620 let exp_named_subst' =
621 reduceaux_exp_named_subst context l exp_named_subst
623 let t' = C.MutInd (uri,i,exp_named_subst') in
624 if l = [] then t' else C.Appl (t'::l)
625 | C.MutConstruct (uri,i,j,exp_named_subst) ->
626 let exp_named_subst' =
627 reduceaux_exp_named_subst context l exp_named_subst
629 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
630 if l = [] then t' else C.Appl (t'::l)
631 | C.MutCase (mutind,i,outtype,term,pl) ->
634 C.CoFix (i,fl) as t ->
636 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
637 let (_,_,body) = List.nth fl i in
639 let counter = ref (List.length fl) in
641 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
645 reduceaux context [] body'
646 | C.Appl (C.CoFix (i,fl) :: tl) ->
648 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
649 let (_,_,body) = List.nth fl i in
651 let counter = ref (List.length fl) in
653 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
657 let tl' = List.map (reduceaux context []) tl in
658 reduceaux context tl body'
661 (match decofix (reduceaux context [] term) with
662 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
663 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
665 match CicEnvironment.get_obj mutind with
666 C.InductiveDefinition (tl,ingredients,r) ->
667 let (_,_,arity,_) = List.nth tl i in
669 | _ -> raise WrongUriToInductiveDefinition
675 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
676 | _ -> raise (Impossible 5)
680 reduceaux context (ts@l) (List.nth pl (j-1))
681 | C.Cast _ | C.Implicit ->
682 raise (Impossible 2) (* we don't trust our whd ;-) *)
684 let outtype' = reduceaux context [] outtype in
685 let term' = reduceaux context [] term in
686 let pl' = List.map (reduceaux context []) pl in
688 C.MutCase (mutind,i,outtype',term',pl')
690 if l = [] then res else C.Appl (res::l)
694 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
699 (function (n,recindex,ty,bo) ->
700 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
705 let (_,recindex,_,body) = List.nth fl i in
708 Some (List.nth l recindex)
714 (match reduceaux context [] recparam with
716 | C.Appl ((C.MutConstruct _)::_) ->
718 let counter = ref (List.length fl) in
720 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
724 (* Possible optimization: substituting whd recparam in l*)
725 reduceaux context l body'
726 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
728 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
732 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
737 (function (n,ty,bo) ->
738 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
743 if l = [] then t' else C.Appl (t'::l)
744 and reduceaux_exp_named_subst context l =
745 List.map (function uri,t -> uri,reduceaux context [] t)