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 rec syntactic_equality t t' =
59 | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
60 | C.Cast (te,ty), C.Cast (te',ty') ->
61 syntactic_equality te te' &&
62 syntactic_equality ty ty'
63 | C.Prod (n,s,t), C.Prod (n',s',t') ->
65 syntactic_equality s s' &&
66 syntactic_equality t t'
67 | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
69 syntactic_equality s s' &&
70 syntactic_equality t t'
71 | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
73 syntactic_equality s s' &&
74 syntactic_equality t t'
75 | C.Appl l, C.Appl l' ->
78 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
80 Invalid_argument _ -> false)
81 | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
82 | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
83 UriManager.eq uri uri' && i = i'
84 | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
85 UriManager.eq uri uri' && i = i' && j = j'
86 | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
87 UriManager.eq sp sp' && i = i' &&
88 syntactic_equality outt outt' &&
89 syntactic_equality t t' &&
92 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
94 Invalid_argument _ -> false)
95 | C.Fix (i,fl), C.Fix (i',fl') ->
99 (fun b (name,i,ty,bo) (name',i',ty',bo') ->
100 b && name = name' && i = i' &&
101 syntactic_equality ty ty' &&
102 syntactic_equality bo bo') true fl fl'
104 Invalid_argument _ -> false)
105 | C.CoFix (i,fl), C.CoFix (i',fl') ->
109 (fun b (name,ty,bo) (name',ty',bo') ->
111 syntactic_equality ty ty' &&
112 syntactic_equality bo bo') true fl fl'
114 Invalid_argument _ -> false)
118 (* "textual" replacement of a subterm with another one *)
119 let replace ~equality ~what ~with_what ~where =
120 let module C = Cic in
123 t when (equality t what) -> with_what
128 | C.Implicit as t -> t
129 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
130 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
131 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
132 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
134 (* Invariant enforced: no application of an application *)
135 (match List.map aux l with
136 (C.Appl l')::tl -> C.Appl (l'@tl)
138 | C.Const _ as t -> t
139 | C.MutInd _ as t -> t
140 | C.MutConstruct _ as t -> t
141 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
142 C.MutCase (sp,cookingsno,i,aux outt, aux t,
147 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
150 C.Fix (i, substitutedfl)
154 (fun (name,ty,bo) -> (name, aux ty, aux bo))
157 C.CoFix (i, substitutedfl)
162 (* replaces in a term a term with another one. *)
163 (* Lifting are performed as usual. *)
164 let replace_lifting ~equality ~what ~with_what ~where =
166 let module C = Cic in
168 (*CSC: Possibile bug: debbo liftare di k what? *)
169 t when (equality t what) -> CicSubstitution.lift (k-1) with_what
170 | C.Rel n as t -> t (*CSC: ??? BUG ? *)
172 | C.Meta (i, l) as t ->
177 | Some t -> Some (substaux k t)
182 | C.Implicit as t -> t
183 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
184 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
185 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
186 | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
188 (* Invariant: no Appl applied to another Appl *)
189 let tl' = List.map (substaux k) tl in
191 match substaux k he with
192 C.Appl l -> C.Appl (l@tl')
193 | _ as he' -> C.Appl (he'::tl')
195 | C.Appl _ -> assert false
196 | C.Const _ as t -> t
197 | C.MutInd _ as t -> t
198 | C.MutConstruct _ as t -> t
199 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
200 C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
201 List.map (substaux k) pl)
203 let len = List.length fl in
206 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
209 C.Fix (i, substitutedfl)
211 let len = List.length fl in
214 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
217 C.CoFix (i, substitutedfl)
222 (* Takes a well-typed term and fully reduces it. *)
223 (*CSC: It does not perform reduction in a Case *)
225 let rec reduceaux context l =
226 let module C = Cic in
227 let module S = CicSubstitution in
230 (match List.nth context (n-1) with
231 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
232 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
233 | None -> raise RelToHiddenHypothesis
236 (match CicEnvironment.get_cooked_obj uri 0 with
237 C.Definition _ -> raise ReferenceToDefinition
238 | C.Axiom _ -> raise ReferenceToAxiom
239 | C.CurrentProof _ -> raise ReferenceToCurrentProof
240 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
241 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
242 | C.Variable (_,Some body,_) -> reduceaux context l body
244 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
245 | C.Sort _ as t -> t (* l should be empty *)
246 | C.Implicit as t -> t
248 C.Cast (reduceaux context l te, reduceaux context l ty)
249 | C.Prod (name,s,t) ->
252 reduceaux context [] s,
253 reduceaux ((Some (name,C.Decl s))::context) [] t)
254 | C.Lambda (name,s,t) ->
258 reduceaux context [] s,
259 reduceaux ((Some (name,C.Decl s))::context) [] t)
260 | he::tl -> reduceaux context tl (S.subst he t)
261 (* when name is Anonimous the substitution should be superfluous *)
264 reduceaux context l (S.subst (reduceaux context [] s) t)
266 let tl' = List.map (reduceaux context []) tl in
267 reduceaux context (tl'@l) he
268 | C.Appl [] -> raise (Impossible 1)
269 | C.Const (uri,cookingsno) as t ->
270 (match CicEnvironment.get_cooked_obj uri cookingsno with
271 C.Definition (_,body,_,_) -> reduceaux context l body
272 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
273 | C.Variable _ -> raise ReferenceToVariable
274 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
275 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
277 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
278 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
279 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
282 C.CoFix (i,fl) as t ->
284 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
286 let (_,_,body) = List.nth fl i in
288 let counter = ref (List.length fl) in
290 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
294 reduceaux (tys@context) [] body'
295 | C.Appl (C.CoFix (i,fl) :: tl) ->
297 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
299 let (_,_,body) = List.nth fl i in
301 let counter = ref (List.length fl) in
303 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
307 let tl' = List.map (reduceaux context []) tl in
308 reduceaux (tys@context) tl' body'
311 (match decofix (reduceaux context [] term) with
312 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
313 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
314 let (arity, r, num_ingredients) =
315 match CicEnvironment.get_obj mutind with
316 C.InductiveDefinition (tl,ingredients,r) ->
317 let (_,_,arity,_) = List.nth tl i
318 and num_ingredients =
321 if k < cookingsno then i + List.length l else i
324 (arity,r,num_ingredients)
325 | _ -> raise WrongUriToInductiveDefinition
328 let num_to_eat = r + num_ingredients in
332 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
333 | _ -> raise (Impossible 5)
335 eat_first (num_to_eat,tl)
337 reduceaux context (ts@l) (List.nth pl (j-1))
338 | C.Cast _ | C.Implicit ->
339 raise (Impossible 2) (* we don't trust our whd ;-) *)
341 let outtype' = reduceaux context [] outtype in
342 let term' = reduceaux context [] term in
343 let pl' = List.map (reduceaux context []) pl in
345 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
347 if l = [] then res else C.Appl (res::l)
351 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
356 (function (n,recindex,ty,bo) ->
357 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
362 let (_,recindex,_,body) = List.nth fl i in
365 Some (List.nth l recindex)
371 (match reduceaux context [] recparam with
373 | C.Appl ((C.MutConstruct _)::_) ->
375 let counter = ref (List.length fl) in
377 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
381 (* Possible optimization: substituting whd recparam in l*)
382 reduceaux context l body'
383 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
385 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
389 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
394 (function (n,ty,bo) ->
395 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
400 if l = [] then t' else C.Appl (t'::l)
405 exception WrongShape;;
406 exception AlreadySimplified;;
408 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
409 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
411 (*CSC: {foo [n,m:nat]:nat := *)
412 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
414 (* Takes a well-typed term and *)
415 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
416 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
417 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
418 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
419 (* is applied again to the new redex; Step 3) is applied to the result *)
420 (* of the recursive simplification. Otherwise, if the Fix can not be *)
421 (* reduced, than the delta-reductions fails and the delta-redex is *)
422 (* not reduced. Otherwise, if the delta-residual is not the *)
423 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
424 (* directly returned, without performing step 3). *)
425 (* 3) Folds the application of the constant to the arguments that did not *)
426 (* change in every iteration, i.e. to the actual arguments for the *)
427 (* lambda-abstractions that precede the Fix. *)
428 (*CSC: It does not perform simplification in a Case *)
430 (* reduceaux is equal to the reduceaux locally defined inside *)
431 (*reduce, but for the const case. *)
433 let rec reduceaux context l =
434 let module C = Cic in
435 let module S = CicSubstitution in
438 (match List.nth context (n-1) with
439 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
440 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
441 | None -> raise RelToHiddenHypothesis
444 (match CicEnvironment.get_cooked_obj uri 0 with
445 C.Definition _ -> raise ReferenceToDefinition
446 | C.Axiom _ -> raise ReferenceToAxiom
447 | C.CurrentProof _ -> raise ReferenceToCurrentProof
448 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
449 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
450 | C.Variable (_,Some body,_) -> reduceaux context l body
452 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
453 | C.Sort _ as t -> t (* l should be empty *)
454 | C.Implicit as t -> t
456 C.Cast (reduceaux context l te, reduceaux context l ty)
457 | C.Prod (name,s,t) ->
460 reduceaux context [] s,
461 reduceaux ((Some (name,C.Decl s))::context) [] t)
462 | C.Lambda (name,s,t) ->
466 reduceaux context [] s,
467 reduceaux ((Some (name,C.Decl s))::context) [] t)
468 | he::tl -> reduceaux context tl (S.subst he t)
469 (* when name is Anonimous the substitution should be superfluous *)
472 reduceaux context l (S.subst (reduceaux context [] s) t)
474 let tl' = List.map (reduceaux context []) tl in
475 reduceaux context (tl'@l) he
476 | C.Appl [] -> raise (Impossible 1)
477 | C.Const (uri,cookingsno) as t ->
478 (match CicEnvironment.get_cooked_obj uri cookingsno with
479 C.Definition (_,body,_,_) ->
483 let res,constant_args =
484 let rec aux rev_constant_args l =
486 C.Lambda (name,s,t) as t' ->
489 [] -> raise WrongShape
491 (* when name is Anonimous the substitution should be *)
493 aux (he::rev_constant_args) tl (S.subst he t)
496 aux rev_constant_args l (S.subst s t)
497 | C.Fix (i,fl) as t ->
499 List.map (function (name,_,ty,_) ->
500 Some (C.Name name, C.Decl ty)) fl
502 let (_,recindex,_,body) = List.nth fl i in
507 _ -> raise AlreadySimplified
509 (match CicReduction.whd context recparam with
511 | C.Appl ((C.MutConstruct _)::_) ->
513 let counter = ref (List.length fl) in
516 decr counter ; S.subst (C.Fix (!counter,fl))
519 (* Possible optimization: substituting whd *)
521 reduceaux (tys@context) l body',
522 List.rev rev_constant_args
523 | _ -> raise AlreadySimplified
525 | _ -> raise WrongShape
531 match constant_args with
532 [] -> C.Const (uri,cookingsno)
533 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
535 let reduced_term_to_fold = reduce context term_to_fold in
536 replace (=) reduced_term_to_fold term_to_fold res
539 (* The constant does not unfold to a Fix lambda-abstracted *)
540 (* w.r.t. zero or more variables. We just perform reduction. *)
541 reduceaux context l body
542 | AlreadySimplified ->
543 (* If we performed delta-reduction, we would find a Fix *)
544 (* not applied to a constructor. So, we refuse to perform *)
545 (* delta-reduction. *)
551 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
552 | C.Variable _ -> raise ReferenceToVariable
553 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
554 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
556 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
557 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
558 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
561 C.CoFix (i,fl) as t ->
563 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
564 let (_,_,body) = List.nth fl i in
566 let counter = ref (List.length fl) in
568 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
572 reduceaux (tys@context) [] body'
573 | C.Appl (C.CoFix (i,fl) :: tl) ->
575 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
576 let (_,_,body) = List.nth fl i in
578 let counter = ref (List.length fl) in
580 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
584 let tl' = List.map (reduceaux context []) tl in
585 reduceaux (tys@context) tl body'
588 (match decofix (reduceaux context [] term) with
589 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
590 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
591 let (arity, r, num_ingredients) =
592 match CicEnvironment.get_obj mutind with
593 C.InductiveDefinition (tl,ingredients,r) ->
594 let (_,_,arity,_) = List.nth tl i
595 and num_ingredients =
598 if k < cookingsno then i + List.length l else i
601 (arity,r,num_ingredients)
602 | _ -> raise WrongUriToInductiveDefinition
605 let num_to_eat = r + num_ingredients in
609 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
610 | _ -> raise (Impossible 5)
612 eat_first (num_to_eat,tl)
614 reduceaux context (ts@l) (List.nth pl (j-1))
615 | C.Cast _ | C.Implicit ->
616 raise (Impossible 2) (* we don't trust our whd ;-) *)
618 let outtype' = reduceaux context [] outtype in
619 let term' = reduceaux context [] term in
620 let pl' = List.map (reduceaux context []) pl in
622 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
624 if l = [] then res else C.Appl (res::l)
628 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
633 (function (n,recindex,ty,bo) ->
634 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
639 let (_,recindex,_,body) = List.nth fl i in
642 Some (List.nth l recindex)
648 (match reduceaux context [] recparam with
650 | C.Appl ((C.MutConstruct _)::_) ->
652 let counter = ref (List.length fl) in
654 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
658 (* Possible optimization: substituting whd recparam in l*)
659 reduceaux context l body'
660 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
662 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
666 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
671 (function (n,ty,bo) ->
672 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
677 if l = [] then t' else C.Appl (t'::l)