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 ReferenceToDefinition;;
41 exception ReferenceToAxiom;;
42 exception ReferenceToVariable;;
43 exception ReferenceToCurrentProof;;
44 exception ReferenceToInductiveDefinition;;
45 exception WrongUriToInductiveDefinition;;
46 exception RelToHiddenHypothesis;;
48 (* syntactic_equality up to cookingsno for uris *)
49 (* (which is often syntactically irrilevant) *)
50 let syntactic_equality ~alpha_equivalence =
60 | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
61 | C.Cast (te,ty), C.Cast (te',ty') ->
62 aux te te' && aux ty ty'
63 | C.Prod (n,s,t), C.Prod (n',s',t') ->
64 (alpha_equivalence || n = n') && aux s s' && aux t t'
65 | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
66 (alpha_equivalence || n = n') && aux s s' && aux t t'
67 | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
68 (alpha_equivalence || n = n') && aux s s' && aux t t'
69 | C.Appl l, C.Appl l' ->
72 (fun b t1 t2 -> b && aux t1 t2) true l l'
74 Invalid_argument _ -> false)
75 | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
76 | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
77 UriManager.eq uri uri' && i = i'
78 | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
79 UriManager.eq uri uri' && i = i' && j = j'
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 (name,i,ty,bo) (name',i',ty',bo') ->
93 b && (alpha_equivalence || name = name') && i = i' &&
94 aux ty ty' && aux bo bo') true fl fl'
96 Invalid_argument _ -> false)
97 | C.CoFix (i,fl), C.CoFix (i',fl') ->
101 (fun b (name,ty,bo) (name',ty',bo') ->
102 b && (alpha_equivalence || name = name') &&
103 aux ty ty' && aux bo bo') true fl fl'
105 Invalid_argument _ -> false)
111 (* "textual" replacement of a subterm with another one *)
112 let replace ~equality ~what ~with_what ~where =
113 let module C = Cic in
116 t when (equality t what) -> with_what
121 | C.Implicit as t -> t
122 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
123 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
124 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
125 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
127 (* Invariant enforced: no application of an application *)
128 (match List.map aux l with
129 (C.Appl l')::tl -> C.Appl (l'@tl)
131 | C.Const _ as t -> t
132 | C.MutInd _ as t -> t
133 | C.MutConstruct _ as t -> t
134 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
135 C.MutCase (sp,cookingsno,i,aux outt, aux t,
140 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
143 C.Fix (i, substitutedfl)
147 (fun (name,ty,bo) -> (name, aux ty, aux bo))
150 C.CoFix (i, substitutedfl)
155 (* replaces in a term a term with another one. *)
156 (* Lifting are performed as usual. *)
157 let replace_lifting ~equality ~what ~with_what ~where =
158 let rec substaux k what =
159 let module C = Cic in
160 let module S = CicSubstitution in
162 t when (equality t what) -> S.lift (k-1) with_what
165 | C.Meta (i, l) as t ->
170 | Some t -> Some (substaux k what t)
175 | C.Implicit as t -> t
176 | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
178 C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
179 | C.Lambda (n,s,t) ->
180 C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
182 C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
184 (* Invariant: no Appl applied to another Appl *)
185 let tl' = List.map (substaux k what) tl in
187 match substaux k what he with
188 C.Appl l -> C.Appl (l@tl')
189 | _ as he' -> C.Appl (he'::tl')
191 | C.Appl _ -> assert false
192 | C.Const _ as t -> t
193 | C.MutInd _ as t -> t
194 | C.MutConstruct _ as t -> t
195 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
196 C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t,
197 List.map (substaux k what) pl)
199 let len = List.length fl in
202 (fun (name,i,ty,bo) ->
203 (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
206 C.Fix (i, substitutedfl)
208 let len = List.length fl in
212 (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
215 C.CoFix (i, substitutedfl)
217 substaux 1 what where
220 (* Takes a well-typed term and fully reduces it. *)
221 (*CSC: It does not perform reduction in a Case *)
223 let rec reduceaux context l =
224 let module C = Cic in
225 let module S = CicSubstitution in
228 (match List.nth context (n-1) with
229 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
230 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
231 | None -> raise RelToHiddenHypothesis
234 (match CicEnvironment.get_cooked_obj uri 0 with
235 C.Definition _ -> raise ReferenceToDefinition
236 | C.Axiom _ -> raise ReferenceToAxiom
237 | C.CurrentProof _ -> raise ReferenceToCurrentProof
238 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
239 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
240 | C.Variable (_,Some body,_) -> reduceaux context l body
242 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
243 | C.Sort _ as t -> t (* l should be empty *)
244 | C.Implicit as t -> t
246 C.Cast (reduceaux context l te, reduceaux context l ty)
247 | C.Prod (name,s,t) ->
250 reduceaux context [] s,
251 reduceaux ((Some (name,C.Decl s))::context) [] t)
252 | C.Lambda (name,s,t) ->
256 reduceaux context [] s,
257 reduceaux ((Some (name,C.Decl s))::context) [] t)
258 | he::tl -> reduceaux context tl (S.subst he t)
259 (* when name is Anonimous the substitution should be superfluous *)
262 reduceaux context l (S.subst (reduceaux context [] s) t)
264 let tl' = List.map (reduceaux context []) tl in
265 reduceaux context (tl'@l) he
266 | C.Appl [] -> raise (Impossible 1)
267 | C.Const (uri,cookingsno) as t ->
268 (match CicEnvironment.get_cooked_obj uri cookingsno with
269 C.Definition (_,body,_,_) -> reduceaux context l body
270 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
271 | C.Variable _ -> raise ReferenceToVariable
272 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
273 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
275 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
276 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
277 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
280 C.CoFix (i,fl) as t ->
282 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
284 let (_,_,body) = List.nth fl i in
286 let counter = ref (List.length fl) in
288 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
292 reduceaux (tys@context) [] body'
293 | C.Appl (C.CoFix (i,fl) :: tl) ->
295 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
297 let (_,_,body) = List.nth fl i in
299 let counter = ref (List.length fl) in
301 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
305 let tl' = List.map (reduceaux context []) tl in
306 reduceaux (tys@context) tl' body'
309 (match decofix (reduceaux context [] term) with
310 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
311 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
312 let (arity, r, num_ingredients) =
313 match CicEnvironment.get_obj mutind with
314 C.InductiveDefinition (tl,ingredients,r) ->
315 let (_,_,arity,_) = List.nth tl i
316 and num_ingredients =
319 if k < cookingsno then i + List.length l else i
322 (arity,r,num_ingredients)
323 | _ -> raise WrongUriToInductiveDefinition
326 let num_to_eat = r + num_ingredients in
330 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
331 | _ -> raise (Impossible 5)
333 eat_first (num_to_eat,tl)
335 reduceaux context (ts@l) (List.nth pl (j-1))
336 | C.Cast _ | C.Implicit ->
337 raise (Impossible 2) (* we don't trust our whd ;-) *)
339 let outtype' = reduceaux context [] outtype in
340 let term' = reduceaux context [] term in
341 let pl' = List.map (reduceaux context []) pl in
343 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
345 if l = [] then res else C.Appl (res::l)
349 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
354 (function (n,recindex,ty,bo) ->
355 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
360 let (_,recindex,_,body) = List.nth fl i in
363 Some (List.nth l recindex)
369 (match reduceaux context [] recparam with
371 | C.Appl ((C.MutConstruct _)::_) ->
373 let counter = ref (List.length fl) in
375 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
379 (* Possible optimization: substituting whd recparam in l*)
380 reduceaux context l body'
381 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
383 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
387 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
392 (function (n,ty,bo) ->
393 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
398 if l = [] then t' else C.Appl (t'::l)
403 exception WrongShape;;
404 exception AlreadySimplified;;
406 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
407 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
409 (*CSC: {foo [n,m:nat]:nat := *)
410 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
412 (* Takes a well-typed term and *)
413 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
414 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
415 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
416 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
417 (* is applied again to the new redex; Step 3) is applied to the result *)
418 (* of the recursive simplification. Otherwise, if the Fix can not be *)
419 (* reduced, than the delta-reductions fails and the delta-redex is *)
420 (* not reduced. Otherwise, if the delta-residual is not the *)
421 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
422 (* directly returned, without performing step 3). *)
423 (* 3) Folds the application of the constant to the arguments that did not *)
424 (* change in every iteration, i.e. to the actual arguments for the *)
425 (* lambda-abstractions that precede the Fix. *)
426 (*CSC: It does not perform simplification in a Case *)
428 (* reduceaux is equal to the reduceaux locally defined inside *)
429 (*reduce, but for the const case. *)
431 let rec reduceaux context l =
432 let module C = Cic in
433 let module S = CicSubstitution in
436 (match List.nth context (n-1) with
437 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
438 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
439 | None -> raise RelToHiddenHypothesis
442 (match CicEnvironment.get_cooked_obj uri 0 with
443 C.Definition _ -> raise ReferenceToDefinition
444 | C.Axiom _ -> raise ReferenceToAxiom
445 | C.CurrentProof _ -> raise ReferenceToCurrentProof
446 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
447 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
448 | C.Variable (_,Some body,_) -> reduceaux context l body
450 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
451 | C.Sort _ as t -> t (* l should be empty *)
452 | C.Implicit as t -> t
454 C.Cast (reduceaux context l te, reduceaux context l ty)
455 | C.Prod (name,s,t) ->
458 reduceaux context [] s,
459 reduceaux ((Some (name,C.Decl s))::context) [] t)
460 | C.Lambda (name,s,t) ->
464 reduceaux context [] s,
465 reduceaux ((Some (name,C.Decl s))::context) [] t)
466 | he::tl -> reduceaux context tl (S.subst he t)
467 (* when name is Anonimous the substitution should be superfluous *)
470 reduceaux context l (S.subst (reduceaux context [] s) t)
472 let tl' = List.map (reduceaux context []) tl in
473 reduceaux context (tl'@l) he
474 | C.Appl [] -> raise (Impossible 1)
475 | C.Const (uri,cookingsno) as t ->
476 (match CicEnvironment.get_cooked_obj uri cookingsno with
477 C.Definition (_,body,_,_) ->
481 let res,constant_args =
482 let rec aux rev_constant_args l =
484 C.Lambda (name,s,t) as t' ->
487 [] -> raise WrongShape
489 (* when name is Anonimous the substitution should be *)
491 aux (he::rev_constant_args) tl (S.subst he t)
494 aux rev_constant_args l (S.subst s t)
495 | C.Fix (i,fl) as t ->
497 List.map (function (name,_,ty,_) ->
498 Some (C.Name name, C.Decl ty)) fl
500 let (_,recindex,_,body) = List.nth fl i in
505 _ -> raise AlreadySimplified
507 (match CicReduction.whd context recparam with
509 | C.Appl ((C.MutConstruct _)::_) ->
511 let counter = ref (List.length fl) in
514 decr counter ; S.subst (C.Fix (!counter,fl))
517 (* Possible optimization: substituting whd *)
519 reduceaux (tys@context) l body',
520 List.rev rev_constant_args
521 | _ -> raise AlreadySimplified
523 | _ -> raise WrongShape
529 match constant_args with
530 [] -> C.Const (uri,cookingsno)
531 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
533 let reduced_term_to_fold = reduce context term_to_fold in
534 replace (=) reduced_term_to_fold term_to_fold res
537 (* The constant does not unfold to a Fix lambda-abstracted *)
538 (* w.r.t. zero or more variables. We just perform reduction. *)
539 reduceaux context l body
540 | AlreadySimplified ->
541 (* If we performed delta-reduction, we would find a Fix *)
542 (* not applied to a constructor. So, we refuse to perform *)
543 (* delta-reduction. *)
549 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
550 | C.Variable _ -> raise ReferenceToVariable
551 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
552 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
554 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
555 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
556 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
559 C.CoFix (i,fl) as t ->
561 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
562 let (_,_,body) = List.nth fl i in
564 let counter = ref (List.length fl) in
566 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
570 reduceaux (tys@context) [] body'
571 | C.Appl (C.CoFix (i,fl) :: tl) ->
573 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
574 let (_,_,body) = List.nth fl i in
576 let counter = ref (List.length fl) in
578 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
582 let tl' = List.map (reduceaux context []) tl in
583 reduceaux (tys@context) tl body'
586 (match decofix (reduceaux context [] term) with
587 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
588 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
589 let (arity, r, num_ingredients) =
590 match CicEnvironment.get_obj mutind with
591 C.InductiveDefinition (tl,ingredients,r) ->
592 let (_,_,arity,_) = List.nth tl i
593 and num_ingredients =
596 if k < cookingsno then i + List.length l else i
599 (arity,r,num_ingredients)
600 | _ -> raise WrongUriToInductiveDefinition
603 let num_to_eat = r + num_ingredients in
607 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
608 | _ -> raise (Impossible 5)
610 eat_first (num_to_eat,tl)
612 reduceaux context (ts@l) (List.nth pl (j-1))
613 | C.Cast _ | C.Implicit ->
614 raise (Impossible 2) (* we don't trust our whd ;-) *)
616 let outtype' = reduceaux context [] outtype in
617 let term' = reduceaux context [] term in
618 let pl' = List.map (reduceaux context []) pl in
620 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
622 if l = [] then res else C.Appl (res::l)
626 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
631 (function (n,recindex,ty,bo) ->
632 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
637 let (_,recindex,_,body) = List.nth fl i in
640 Some (List.nth l recindex)
646 (match reduceaux context [] recparam with
648 | C.Appl ((C.MutConstruct _)::_) ->
650 let counter = ref (List.length fl) in
652 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
656 (* Possible optimization: substituting whd recparam in l*)
657 reduceaux context l body'
658 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
660 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
664 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
669 (function (n,ty,bo) ->
670 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
675 if l = [] then t' else C.Appl (t'::l)