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 RelToHiddenHypothesis;;
47 let alpha_equivalence =
53 C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
54 UriManager.eq uri1 uri2 &&
55 aux_exp_named_subst exp_named_subst1 exp_named_subst2
56 | C.Cast (te,ty), C.Cast (te',ty') ->
57 aux te te' && aux ty ty'
58 | C.Prod (_,s,t), C.Prod (_,s',t') ->
60 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
62 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
64 | C.Appl l, C.Appl l' ->
67 (fun b t1 t2 -> b && aux t1 t2) true l l'
69 Invalid_argument _ -> false)
70 | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
71 UriManager.eq uri uri' &&
72 aux_exp_named_subst exp_named_subst1 exp_named_subst2
73 | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
74 UriManager.eq uri uri' && i = i' &&
75 aux_exp_named_subst exp_named_subst1 exp_named_subst2
76 | C.MutConstruct (uri,i,j,exp_named_subst1),
77 C.MutConstruct (uri',i',j',exp_named_subst2) ->
78 UriManager.eq uri uri' && i = i' && j = j' &&
79 aux_exp_named_subst exp_named_subst1 exp_named_subst2
80 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
81 UriManager.eq sp sp' && i = i' &&
82 aux outt outt' && aux t t' &&
85 (fun b t1 t2 -> b && aux t1 t2) true pl pl'
87 Invalid_argument _ -> false)
88 | C.Fix (i,fl), C.Fix (i',fl') ->
92 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
93 b && i = i' && aux ty ty' && aux bo bo'
96 Invalid_argument _ -> false)
97 | C.CoFix (i,fl), C.CoFix (i',fl') ->
101 (fun b (_,ty,bo) (_,ty',bo') ->
102 b && aux ty ty' && aux bo bo'
105 Invalid_argument _ -> false)
106 | _,_ -> false (* we already know that t != t' *)
107 and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
110 (fun b (uri1,t1) (uri2,t2) ->
111 b && UriManager.eq uri1 uri2 && aux t1 t2
112 ) true exp_named_subst1 exp_named_subst2
114 Invalid_argument _ -> false
119 (* "textual" replacement of a subterm with another one *)
120 let replace ~equality ~what ~with_what ~where =
121 let module C = Cic in
124 t when (equality t what) -> with_what
126 | C.Var (uri,exp_named_subst) ->
127 C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
130 | C.Implicit as t -> t
131 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
132 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
133 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
134 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
136 (* Invariant enforced: no application of an application *)
137 (match List.map aux l with
138 (C.Appl l')::tl -> C.Appl (l'@tl)
140 | C.Const (uri,exp_named_subst) ->
141 C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
142 | C.MutInd (uri,i,exp_named_subst) ->
144 (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
145 | C.MutConstruct (uri,i,j,exp_named_subst) ->
147 (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
148 | C.MutCase (sp,i,outt,t,pl) ->
149 C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
153 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
156 C.Fix (i, substitutedfl)
160 (fun (name,ty,bo) -> (name, aux ty, aux bo))
163 C.CoFix (i, substitutedfl)
168 (* replaces in a term a term with another one. *)
169 (* Lifting are performed as usual. *)
170 let replace_lifting ~equality ~what ~with_what ~where =
171 let rec substaux k what =
172 let module C = Cic in
173 let module S = CicSubstitution in
175 t when (equality t what) -> S.lift (k-1) with_what
177 | C.Var (uri,exp_named_subst) ->
178 let exp_named_subst' =
179 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
181 C.Var (uri,exp_named_subst')
182 | C.Meta (i, l) as t ->
187 | Some t -> Some (substaux k what t)
192 | C.Implicit as t -> t
193 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
195 C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
196 | C.Lambda (n,s,t) ->
197 C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
199 C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
201 (* Invariant: no Appl applied to another Appl *)
202 let tl' = List.map (substaux k what) tl in
204 match substaux k what he with
205 C.Appl l -> C.Appl (l@tl')
206 | _ as he' -> C.Appl (he'::tl')
208 | C.Appl _ -> assert false
209 | C.Const (uri,exp_named_subst) ->
210 let exp_named_subst' =
211 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
213 C.Const (uri,exp_named_subst')
214 | C.MutInd (uri,i,exp_named_subst) ->
215 let exp_named_subst' =
216 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
218 C.MutInd (uri,i,exp_named_subst')
219 | C.MutConstruct (uri,i,j,exp_named_subst) ->
220 let exp_named_subst' =
221 List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
223 C.MutConstruct (uri,i,j,exp_named_subst')
224 | C.MutCase (sp,i,outt,t,pl) ->
225 C.MutCase (sp,i,substaux k what outt, substaux k what t,
226 List.map (substaux k what) pl)
228 let len = List.length fl in
231 (fun (name,i,ty,bo) ->
232 (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
235 C.Fix (i, substitutedfl)
237 let len = List.length fl in
241 (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
244 C.CoFix (i, substitutedfl)
246 substaux 1 what where
249 (* Takes a well-typed term and fully reduces it. *)
250 (*CSC: It does not perform reduction in a Case *)
252 let rec reduceaux context l =
253 let module C = Cic in
254 let module S = CicSubstitution in
257 (match List.nth context (n-1) with
258 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
259 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
260 | None -> raise RelToHiddenHypothesis
262 | C.Var (uri,exp_named_subst) ->
263 let exp_named_subst' =
264 reduceaux_exp_named_subst context l exp_named_subst
266 (match CicEnvironment.get_obj uri with
267 C.Constant _ -> raise ReferenceToConstant
268 | C.CurrentProof _ -> raise ReferenceToCurrentProof
269 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
270 | C.Variable (_,None,_,_) ->
271 let t' = C.Var (uri,exp_named_subst') in
272 if l = [] then t' else C.Appl (t'::l)
273 | C.Variable (_,Some body,_,_) ->
275 (CicSubstitution.subst_vars exp_named_subst' body))
277 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
278 | C.Sort _ as t -> t (* l should be empty *)
279 | C.Implicit as t -> t
281 C.Cast (reduceaux context l te, reduceaux context l ty)
282 | C.Prod (name,s,t) ->
285 reduceaux context [] s,
286 reduceaux ((Some (name,C.Decl s))::context) [] t)
287 | C.Lambda (name,s,t) ->
291 reduceaux context [] s,
292 reduceaux ((Some (name,C.Decl s))::context) [] t)
293 | he::tl -> reduceaux context tl (S.subst he t)
294 (* when name is Anonimous the substitution should be superfluous *)
297 reduceaux context l (S.subst (reduceaux context [] s) t)
299 let tl' = List.map (reduceaux context []) tl in
300 reduceaux context (tl'@l) he
301 | C.Appl [] -> raise (Impossible 1)
302 | C.Const (uri,exp_named_subst) ->
303 let exp_named_subst' =
304 reduceaux_exp_named_subst context l exp_named_subst
306 (match CicEnvironment.get_obj uri with
307 C.Constant (_,Some body,_,_) ->
309 (CicSubstitution.subst_vars exp_named_subst' body))
310 | C.Constant (_,None,_,_) ->
311 let t' = C.Const (uri,exp_named_subst') in
312 if l = [] then t' else C.Appl (t'::l)
313 | C.Variable _ -> raise ReferenceToVariable
314 | C.CurrentProof (_,_,body,_,_) ->
316 (CicSubstitution.subst_vars exp_named_subst' body))
317 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
319 | C.MutInd (uri,i,exp_named_subst) ->
320 let exp_named_subst' =
321 reduceaux_exp_named_subst context l exp_named_subst
323 let t' = C.MutInd (uri,i,exp_named_subst') in
324 if l = [] then t' else C.Appl (t'::l)
325 | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
326 let exp_named_subst' =
327 reduceaux_exp_named_subst context l exp_named_subst
329 let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
330 if l = [] then t' else C.Appl (t'::l)
331 | C.MutCase (mutind,i,outtype,term,pl) ->
334 C.CoFix (i,fl) as t ->
336 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
338 let (_,_,body) = List.nth fl i in
340 let counter = ref (List.length fl) in
342 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
346 reduceaux (tys@context) [] body'
347 | C.Appl (C.CoFix (i,fl) :: tl) ->
349 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
351 let (_,_,body) = List.nth fl i in
353 let counter = ref (List.length fl) in
355 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
359 let tl' = List.map (reduceaux context []) tl in
360 reduceaux (tys@context) tl' body'
363 (match decofix (reduceaux context [] term) with
364 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
365 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
367 match CicEnvironment.get_obj mutind with
368 C.InductiveDefinition (tl,_,r) ->
369 let (_,_,arity,_) = List.nth tl i in
371 | _ -> raise WrongUriToInductiveDefinition
377 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
378 | _ -> raise (Impossible 5)
382 reduceaux context (ts@l) (List.nth pl (j-1))
383 | C.Cast _ | C.Implicit ->
384 raise (Impossible 2) (* we don't trust our whd ;-) *)
386 let outtype' = reduceaux context [] outtype in
387 let term' = reduceaux context [] term in
388 let pl' = List.map (reduceaux context []) pl in
390 C.MutCase (mutind,i,outtype',term',pl')
392 if l = [] then res else C.Appl (res::l)
396 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
401 (function (n,recindex,ty,bo) ->
402 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
407 let (_,recindex,_,body) = List.nth fl i in
410 Some (List.nth l recindex)
416 (match reduceaux context [] recparam with
418 | C.Appl ((C.MutConstruct _)::_) ->
420 let counter = ref (List.length fl) in
422 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
426 (* Possible optimization: substituting whd recparam in l*)
427 reduceaux context l body'
428 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
430 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
434 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
439 (function (n,ty,bo) ->
440 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
445 if l = [] then t' else C.Appl (t'::l)
446 and reduceaux_exp_named_subst context l =
447 List.map (function uri,t -> uri,reduceaux context [] t)
452 exception WrongShape;;
453 exception AlreadySimplified;;
455 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
456 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
458 (*CSC: {foo [n,m:nat]:nat := *)
459 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
461 (* Takes a well-typed term and *)
462 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
463 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
464 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
465 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
466 (* is applied again to the new redex; Step 3) is applied to the result *)
467 (* of the recursive simplification. Otherwise, if the Fix can not be *)
468 (* reduced, than the delta-reductions fails and the delta-redex is *)
469 (* not reduced. Otherwise, if the delta-residual is not the *)
470 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
471 (* directly returned, without performing step 3). *)
472 (* 3) Folds the application of the constant to the arguments that did not *)
473 (* change in every iteration, i.e. to the actual arguments for the *)
474 (* lambda-abstractions that precede the Fix. *)
475 (*CSC: It does not perform simplification in a Case *)
477 (* reduceaux is equal to the reduceaux locally defined inside *)
478 (*reduce, but for the const case. *)
480 let rec reduceaux context l =
481 let module C = Cic in
482 let module S = CicSubstitution in
485 (match List.nth context (n-1) with
486 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
487 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
488 | None -> raise RelToHiddenHypothesis
490 | C.Var (uri,exp_named_subst) ->
491 let exp_named_subst' =
492 reduceaux_exp_named_subst context l exp_named_subst
494 (match CicEnvironment.get_obj uri with
495 C.Constant _ -> raise ReferenceToConstant
496 | C.CurrentProof _ -> raise ReferenceToCurrentProof
497 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
498 | C.Variable (_,None,_,_) ->
499 let t' = C.Var (uri,exp_named_subst') in
500 if l = [] then t' else C.Appl (t'::l)
501 | C.Variable (_,Some body,_,_) ->
503 (CicSubstitution.subst_vars exp_named_subst' body)
505 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
506 | C.Sort _ as t -> t (* l should be empty *)
507 | C.Implicit as t -> t
509 C.Cast (reduceaux context l te, reduceaux context l ty)
510 | C.Prod (name,s,t) ->
513 reduceaux context [] s,
514 reduceaux ((Some (name,C.Decl s))::context) [] t)
515 | C.Lambda (name,s,t) ->
519 reduceaux context [] s,
520 reduceaux ((Some (name,C.Decl s))::context) [] t)
521 | he::tl -> reduceaux context tl (S.subst he t)
522 (* when name is Anonimous the substitution should be superfluous *)
525 reduceaux context l (S.subst (reduceaux context [] s) t)
527 let tl' = List.map (reduceaux context []) tl in
528 reduceaux context (tl'@l) he
529 | C.Appl [] -> raise (Impossible 1)
530 | C.Const (uri,exp_named_subst) ->
531 let exp_named_subst' =
532 reduceaux_exp_named_subst context l exp_named_subst
534 (match CicEnvironment.get_obj uri with
535 C.Constant (_,Some body,_,_) ->
539 let res,constant_args =
540 let rec aux rev_constant_args l =
542 C.Lambda (name,s,t) as t' ->
545 [] -> raise WrongShape
547 (* when name is Anonimous the substitution should *)
549 aux (he::rev_constant_args) tl (S.subst he t)
552 aux rev_constant_args l (S.subst s t)
553 | C.Fix (i,fl) as t ->
555 List.map (function (name,_,ty,_) ->
556 Some (C.Name name, C.Decl ty)) fl
558 let (_,recindex,_,body) = List.nth fl i in
563 _ -> raise AlreadySimplified
565 (match CicReduction.whd context recparam with
567 | C.Appl ((C.MutConstruct _)::_) ->
569 let counter = ref (List.length fl) in
572 decr counter ; S.subst (C.Fix (!counter,fl))
575 (* Possible optimization: substituting whd *)
577 reduceaux (tys@context) l body',
578 List.rev rev_constant_args
579 | _ -> raise AlreadySimplified
581 | _ -> raise WrongShape
583 aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
587 match constant_args with
588 [] -> C.Const (uri,exp_named_subst')
589 | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
591 let reduced_term_to_fold = reduce context term_to_fold in
592 replace (=) reduced_term_to_fold term_to_fold res
595 (* The constant does not unfold to a Fix lambda-abstracted *)
596 (* w.r.t. zero or more variables. We just perform reduction.*)
598 (CicSubstitution.subst_vars exp_named_subst' body)
599 | AlreadySimplified ->
600 (* If we performed delta-reduction, we would find a Fix *)
601 (* not applied to a constructor. So, we refuse to perform *)
602 (* delta-reduction. *)
603 let t' = C.Const (uri,exp_named_subst') in
604 if l = [] then t' else C.Appl (t'::l)
606 | C.Constant (_,None,_,_) ->
607 let t' = C.Const (uri,exp_named_subst') in
608 if l = [] then t' else C.Appl (t'::l)
609 | C.Variable _ -> raise ReferenceToVariable
610 | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
611 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
613 | C.MutInd (uri,i,exp_named_subst) ->
614 let exp_named_subst' =
615 reduceaux_exp_named_subst context l exp_named_subst
617 let t' = C.MutInd (uri,i,exp_named_subst') in
618 if l = [] then t' else C.Appl (t'::l)
619 | C.MutConstruct (uri,i,j,exp_named_subst) ->
620 let exp_named_subst' =
621 reduceaux_exp_named_subst context l exp_named_subst
623 let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
624 if l = [] then t' else C.Appl (t'::l)
625 | C.MutCase (mutind,i,outtype,term,pl) ->
628 C.CoFix (i,fl) as t ->
630 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
631 let (_,_,body) = List.nth fl i in
633 let counter = ref (List.length fl) in
635 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
639 reduceaux (tys@context) [] body'
640 | C.Appl (C.CoFix (i,fl) :: tl) ->
642 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
643 let (_,_,body) = List.nth fl i in
645 let counter = ref (List.length fl) in
647 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
651 let tl' = List.map (reduceaux context []) tl in
652 reduceaux (tys@context) tl body'
655 (match decofix (reduceaux context [] term) with
656 C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
657 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
659 match CicEnvironment.get_obj mutind with
660 C.InductiveDefinition (tl,ingredients,r) ->
661 let (_,_,arity,_) = List.nth tl i in
663 | _ -> raise WrongUriToInductiveDefinition
669 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
670 | _ -> raise (Impossible 5)
674 reduceaux context (ts@l) (List.nth pl (j-1))
675 | C.Cast _ | C.Implicit ->
676 raise (Impossible 2) (* we don't trust our whd ;-) *)
678 let outtype' = reduceaux context [] outtype in
679 let term' = reduceaux context [] term in
680 let pl' = List.map (reduceaux context []) pl in
682 C.MutCase (mutind,i,outtype',term',pl')
684 if l = [] then res else C.Appl (res::l)
688 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
693 (function (n,recindex,ty,bo) ->
694 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
699 let (_,recindex,_,body) = List.nth fl i in
702 Some (List.nth l recindex)
708 (match reduceaux context [] recparam with
710 | C.Appl ((C.MutConstruct _)::_) ->
712 let counter = ref (List.length fl) in
714 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
718 (* Possible optimization: substituting whd recparam in l*)
719 reduceaux context l body'
720 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
722 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
726 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
731 (function (n,ty,bo) ->
732 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
737 if l = [] then t' else C.Appl (t'::l)
738 and reduceaux_exp_named_subst context l =
739 List.map (function uri,t -> uri,reduceaux context [] t)