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' ->
76 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
77 | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
78 | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
79 UriManager.eq uri uri' && i = i'
80 | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
81 UriManager.eq uri uri' && i = i' && j = j'
82 | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
83 UriManager.eq sp sp' && i = i' &&
84 syntactic_equality outt outt' &&
85 syntactic_equality t t' &&
87 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
88 | C.Fix (i,fl), C.Fix (i',fl') ->
91 (fun b (name,i,ty,bo) (name',i',ty',bo') ->
92 b && name = name' && i = i' &&
93 syntactic_equality ty ty' &&
94 syntactic_equality bo bo') true fl fl'
95 | C.CoFix (i,fl), C.CoFix (i',fl') ->
98 (fun b (name,ty,bo) (name',ty',bo') ->
100 syntactic_equality ty ty' &&
101 syntactic_equality bo bo') true fl fl'
105 (* "textual" replacement of a subterm with another one *)
106 let replace ~equality ~what ~with_what ~where =
107 let module C = Cic in
110 t when (equality t what) -> with_what
115 | C.Implicit as t -> t
116 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
117 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
118 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
119 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
121 (* Invariant enforced: no application of an application *)
122 (match List.map aux l with
123 (C.Appl l')::tl -> C.Appl (l'@tl)
125 | C.Const _ as t -> t
126 | C.MutInd _ as t -> t
127 | C.MutConstruct _ as t -> t
128 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
129 C.MutCase (sp,cookingsno,i,aux outt, aux t,
134 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
137 C.Fix (i, substitutedfl)
141 (fun (name,ty,bo) -> (name, aux ty, aux bo))
144 C.CoFix (i, substitutedfl)
149 (* replaces in a term a term with another one. *)
150 (* Lifting are performed as usual. *)
151 let replace_lifting ~equality ~what ~with_what ~where =
153 let module C = Cic in
155 t when (equality t what) -> CicSubstitution.lift (k-1) with_what
156 | C.Rel n as t -> t (*CSC: ??? BUG ? *)
158 | C.Meta (i, l) as t ->
163 | Some t -> Some (substaux k t)
168 | C.Implicit as t -> t
169 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
170 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
171 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
172 | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
174 (* Invariant: no Appl applied to another Appl *)
175 let tl' = List.map (substaux k) tl in
177 match substaux k he with
178 C.Appl l -> C.Appl (l@tl')
179 | _ as he' -> C.Appl (he'::tl')
181 | C.Appl _ -> assert false
182 | C.Const _ as t -> t
183 | C.MutInd _ as t -> t
184 | C.MutConstruct _ as t -> t
185 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
186 C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
187 List.map (substaux k) pl)
189 let len = List.length fl in
192 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
195 C.Fix (i, substitutedfl)
197 let len = List.length fl in
200 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
203 C.CoFix (i, substitutedfl)
208 (* Takes a well-typed term and fully reduces it. *)
209 (*CSC: It does not perform reduction in a Case *)
211 let rec reduceaux context l =
212 let module C = Cic in
213 let module S = CicSubstitution in
216 (match List.nth context (n-1) with
217 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
218 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
219 | None -> raise RelToHiddenHypothesis
222 (match CicEnvironment.get_cooked_obj uri 0 with
223 C.Definition _ -> raise ReferenceToDefinition
224 | C.Axiom _ -> raise ReferenceToAxiom
225 | C.CurrentProof _ -> raise ReferenceToCurrentProof
226 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
227 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
228 | C.Variable (_,Some body,_) -> reduceaux context l body
230 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
231 | C.Sort _ as t -> t (* l should be empty *)
232 | C.Implicit as t -> t
234 C.Cast (reduceaux context l te, reduceaux context l ty)
235 | C.Prod (name,s,t) ->
238 reduceaux context [] s,
239 reduceaux ((Some (name,C.Decl s))::context) [] t)
240 | C.Lambda (name,s,t) ->
244 reduceaux context [] s,
245 reduceaux ((Some (name,C.Decl s))::context) [] t)
246 | he::tl -> reduceaux context tl (S.subst he t)
247 (* when name is Anonimous the substitution should be superfluous *)
250 reduceaux context l (S.subst (reduceaux context [] s) t)
252 let tl' = List.map (reduceaux context []) tl in
253 reduceaux context (tl'@l) he
254 | C.Appl [] -> raise (Impossible 1)
255 | C.Const (uri,cookingsno) as t ->
256 (match CicEnvironment.get_cooked_obj uri cookingsno with
257 C.Definition (_,body,_,_) -> reduceaux context l body
258 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
259 | C.Variable _ -> raise ReferenceToVariable
260 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
261 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
263 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
264 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
265 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
268 C.CoFix (i,fl) as t ->
270 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
272 let (_,_,body) = List.nth fl i in
274 let counter = ref (List.length fl) in
276 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
280 reduceaux (tys@context) [] body'
281 | C.Appl (C.CoFix (i,fl) :: tl) ->
283 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
285 let (_,_,body) = List.nth fl i in
287 let counter = ref (List.length fl) in
289 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
293 let tl' = List.map (reduceaux context []) tl in
294 reduceaux (tys@context) tl' body'
297 (match decofix (reduceaux context [] term) with
298 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
299 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
300 let (arity, r, num_ingredients) =
301 match CicEnvironment.get_obj mutind with
302 C.InductiveDefinition (tl,ingredients,r) ->
303 let (_,_,arity,_) = List.nth tl i
304 and num_ingredients =
307 if k < cookingsno then i + List.length l else i
310 (arity,r,num_ingredients)
311 | _ -> raise WrongUriToInductiveDefinition
314 let num_to_eat = r + num_ingredients in
318 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
319 | _ -> raise (Impossible 5)
321 eat_first (num_to_eat,tl)
323 reduceaux context (ts@l) (List.nth pl (j-1))
324 | C.Cast _ | C.Implicit ->
325 raise (Impossible 2) (* we don't trust our whd ;-) *)
327 let outtype' = reduceaux context [] outtype in
328 let term' = reduceaux context [] term in
329 let pl' = List.map (reduceaux context []) pl in
331 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
333 if l = [] then res else C.Appl (res::l)
337 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
342 (function (n,recindex,ty,bo) ->
343 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
348 let (_,recindex,_,body) = List.nth fl i in
351 Some (List.nth l recindex)
357 (match reduceaux context [] recparam with
359 | C.Appl ((C.MutConstruct _)::_) ->
361 let counter = ref (List.length fl) in
363 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
367 (* Possible optimization: substituting whd recparam in l*)
368 reduceaux context l body'
369 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
371 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
375 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
380 (function (n,ty,bo) ->
381 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
386 if l = [] then t' else C.Appl (t'::l)
391 exception WrongShape;;
392 exception AlreadySimplified;;
394 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
395 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
397 (*CSC: {foo [n,m:nat]:nat := *)
398 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
400 (* Takes a well-typed term and *)
401 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
402 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
403 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
404 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
405 (* is applied again to the new redex; Step 3) is applied to the result *)
406 (* of the recursive simplification. Otherwise, if the Fix can not be *)
407 (* reduced, than the delta-reductions fails and the delta-redex is *)
408 (* not reduced. Otherwise, if the delta-residual is not the *)
409 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
410 (* directly returned, without performing step 3). *)
411 (* 3) Folds the application of the constant to the arguments that did not *)
412 (* change in every iteration, i.e. to the actual arguments for the *)
413 (* lambda-abstractions that precede the Fix. *)
414 (*CSC: It does not perform simplification in a Case *)
416 (* reduceaux is equal to the reduceaux locally defined inside *)
417 (*reduce, but for the const case. *)
419 let rec reduceaux context l =
420 let module C = Cic in
421 let module S = CicSubstitution in
424 (match List.nth context (n-1) with
425 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
426 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
427 | None -> raise RelToHiddenHypothesis
430 (match CicEnvironment.get_cooked_obj uri 0 with
431 C.Definition _ -> raise ReferenceToDefinition
432 | C.Axiom _ -> raise ReferenceToAxiom
433 | C.CurrentProof _ -> raise ReferenceToCurrentProof
434 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
435 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
436 | C.Variable (_,Some body,_) -> reduceaux context l body
438 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
439 | C.Sort _ as t -> t (* l should be empty *)
440 | C.Implicit as t -> t
442 C.Cast (reduceaux context l te, reduceaux context l ty)
443 | C.Prod (name,s,t) ->
446 reduceaux context [] s,
447 reduceaux ((Some (name,C.Decl s))::context) [] t)
448 | C.Lambda (name,s,t) ->
452 reduceaux context [] s,
453 reduceaux ((Some (name,C.Decl s))::context) [] t)
454 | he::tl -> reduceaux context tl (S.subst he t)
455 (* when name is Anonimous the substitution should be superfluous *)
458 reduceaux context l (S.subst (reduceaux context [] s) t)
460 let tl' = List.map (reduceaux context []) tl in
461 reduceaux context (tl'@l) he
462 | C.Appl [] -> raise (Impossible 1)
463 | C.Const (uri,cookingsno) as t ->
464 (match CicEnvironment.get_cooked_obj uri cookingsno with
465 C.Definition (_,body,_,_) ->
469 let res,constant_args =
470 let rec aux rev_constant_args l =
472 C.Lambda (name,s,t) as t' ->
475 [] -> raise WrongShape
477 (* when name is Anonimous the substitution should be *)
479 aux (he::rev_constant_args) tl (S.subst he t)
482 aux rev_constant_args l (S.subst s t)
483 | C.Fix (i,fl) as t ->
485 List.map (function (name,_,ty,_) ->
486 Some (C.Name name, C.Decl ty)) fl
488 let (_,recindex,_,body) = List.nth fl i in
493 _ -> raise AlreadySimplified
495 (match CicReduction.whd context recparam with
497 | C.Appl ((C.MutConstruct _)::_) ->
499 let counter = ref (List.length fl) in
502 decr counter ; S.subst (C.Fix (!counter,fl))
505 (* Possible optimization: substituting whd *)
507 reduceaux (tys@context) l body',
508 List.rev rev_constant_args
509 | _ -> raise AlreadySimplified
511 | _ -> raise WrongShape
517 match constant_args with
518 [] -> C.Const (uri,cookingsno)
519 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
521 let reduced_term_to_fold = reduce context term_to_fold in
522 replace (=) reduced_term_to_fold term_to_fold res
525 (* The constant does not unfold to a Fix lambda-abstracted *)
526 (* w.r.t. zero or more variables. We just perform reduction. *)
527 reduceaux context l body
528 | AlreadySimplified ->
529 (* If we performed delta-reduction, we would find a Fix *)
530 (* not applied to a constructor. So, we refuse to perform *)
531 (* delta-reduction. *)
537 | C.Axiom _ -> 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,_,_) as t -> if l = [] then t else C.Appl (t::l)
543 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
544 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
547 C.CoFix (i,fl) as t ->
549 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
550 let (_,_,body) = List.nth fl i in
552 let counter = ref (List.length fl) in
554 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
558 reduceaux (tys@context) [] body'
559 | C.Appl (C.CoFix (i,fl) :: tl) ->
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 let tl' = List.map (reduceaux context []) tl in
571 reduceaux (tys@context) tl body'
574 (match decofix (reduceaux context [] term) with
575 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
576 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
577 let (arity, r, num_ingredients) =
578 match CicEnvironment.get_obj mutind with
579 C.InductiveDefinition (tl,ingredients,r) ->
580 let (_,_,arity,_) = List.nth tl i
581 and num_ingredients =
584 if k < cookingsno then i + List.length l else i
587 (arity,r,num_ingredients)
588 | _ -> raise WrongUriToInductiveDefinition
591 let num_to_eat = r + num_ingredients in
595 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
596 | _ -> raise (Impossible 5)
598 eat_first (num_to_eat,tl)
600 reduceaux context (ts@l) (List.nth pl (j-1))
601 | C.Cast _ | C.Implicit ->
602 raise (Impossible 2) (* we don't trust our whd ;-) *)
604 let outtype' = reduceaux context [] outtype in
605 let term' = reduceaux context [] term in
606 let pl' = List.map (reduceaux context []) pl in
608 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
610 if l = [] then res else C.Appl (res::l)
614 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
619 (function (n,recindex,ty,bo) ->
620 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
625 let (_,recindex,_,body) = List.nth fl i in
628 Some (List.nth l recindex)
634 (match reduceaux context [] recparam with
636 | C.Appl ((C.MutConstruct _)::_) ->
638 let counter = ref (List.length fl) in
640 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
644 (* Possible optimization: substituting whd recparam in l*)
645 reduceaux context l body'
646 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
648 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
652 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
657 (function (n,ty,bo) ->
658 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
663 if l = [] then t' else C.Appl (t'::l)