1 (* Copyright (C) 2000, 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 (* Takes a well-typed term and fully reduces it. *)
150 (*CSC: It does not perform reduction in a Case *)
152 let rec reduceaux context l =
153 let module C = Cic in
154 let module S = CicSubstitution in
157 (match List.nth context (n-1) with
158 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
159 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
160 | None -> raise RelToHiddenHypothesis
163 (match CicEnvironment.get_cooked_obj uri 0 with
164 C.Definition _ -> raise ReferenceToDefinition
165 | C.Axiom _ -> raise ReferenceToAxiom
166 | C.CurrentProof _ -> raise ReferenceToCurrentProof
167 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
168 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
169 | C.Variable (_,Some body,_) -> reduceaux context l body
171 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
172 | C.Sort _ as t -> t (* l should be empty *)
173 | C.Implicit as t -> t
175 C.Cast (reduceaux context l te, reduceaux context l ty)
176 | C.Prod (name,s,t) ->
179 reduceaux context [] s,
180 reduceaux ((Some (name,C.Decl s))::context) [] t)
181 | C.Lambda (name,s,t) ->
185 reduceaux context [] s,
186 reduceaux ((Some (name,C.Decl s))::context) [] t)
187 | he::tl -> reduceaux context tl (S.subst he t)
188 (* when name is Anonimous the substitution should be superfluous *)
191 reduceaux context l (S.subst (reduceaux context [] s) t)
193 let tl' = List.map (reduceaux context []) tl in
194 reduceaux context (tl'@l) he
195 | C.Appl [] -> raise (Impossible 1)
196 | C.Const (uri,cookingsno) as t ->
197 (match CicEnvironment.get_cooked_obj uri cookingsno with
198 C.Definition (_,body,_,_) -> reduceaux context l body
199 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
200 | C.Variable _ -> raise ReferenceToVariable
201 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
202 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
204 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
205 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
206 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
209 C.CoFix (i,fl) as t ->
211 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
213 let (_,_,body) = List.nth fl i in
215 let counter = ref (List.length fl) in
217 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
221 reduceaux (tys@context) [] body'
222 | C.Appl (C.CoFix (i,fl) :: tl) ->
224 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
226 let (_,_,body) = List.nth fl i in
228 let counter = ref (List.length fl) in
230 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
234 let tl' = List.map (reduceaux context []) tl in
235 reduceaux (tys@context) tl' body'
238 (match decofix (reduceaux context [] term) with
239 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
240 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
241 let (arity, r, num_ingredients) =
242 match CicEnvironment.get_obj mutind with
243 C.InductiveDefinition (tl,ingredients,r) ->
244 let (_,_,arity,_) = List.nth tl i
245 and num_ingredients =
248 if k < cookingsno then i + List.length l else i
251 (arity,r,num_ingredients)
252 | _ -> raise WrongUriToInductiveDefinition
255 let num_to_eat = r + num_ingredients in
259 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
260 | _ -> raise (Impossible 5)
262 eat_first (num_to_eat,tl)
264 reduceaux context (ts@l) (List.nth pl (j-1))
265 | C.Cast _ | C.Implicit ->
266 raise (Impossible 2) (* we don't trust our whd ;-) *)
268 let outtype' = reduceaux context [] outtype in
269 let term' = reduceaux context [] term in
270 let pl' = List.map (reduceaux context []) pl in
272 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
274 if l = [] then res else C.Appl (res::l)
278 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
283 (function (n,recindex,ty,bo) ->
284 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
289 let (_,recindex,_,body) = List.nth fl i in
292 Some (List.nth l recindex)
298 (match reduceaux context [] recparam with
300 | C.Appl ((C.MutConstruct _)::_) ->
302 let counter = ref (List.length fl) in
304 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
308 (* Possible optimization: substituting whd recparam in l*)
309 reduceaux context l body'
310 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
312 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
316 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
321 (function (n,ty,bo) ->
322 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
327 if l = [] then t' else C.Appl (t'::l)
332 exception WrongShape;;
333 exception AlreadySimplified;;
334 exception WhatShouldIDo;;
336 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
337 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
339 (*CSC: {foo [n,m:nat]:nat := *)
340 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
342 (* Takes a well-typed term and *)
343 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
344 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
345 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
346 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
347 (* is applied again to the new redex; Step 3) is applied to the result *)
348 (* of the recursive simplification. Otherwise, if the Fix can not be *)
349 (* reduced, than the delta-reductions fails and the delta-redex is *)
350 (* not reduced. Otherwise, if the delta-residual is not the *)
351 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
352 (* directly returned, without performing step 3). *)
353 (* 3) Folds the application of the constant to the arguments that did not *)
354 (* change in every iteration, i.e. to the actual arguments for the *)
355 (* lambda-abstractions that precede the Fix. *)
356 (*CSC: It does not perform simplification in a Case *)
358 (* reduceaux is equal to the reduceaux locally defined inside *)
359 (*reduce, but for the const case. *)
361 let rec reduceaux context l =
362 let module C = Cic in
363 let module S = CicSubstitution in
366 (match List.nth context (n-1) with
367 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
368 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
369 | None -> raise RelToHiddenHypothesis
372 (match CicEnvironment.get_cooked_obj uri 0 with
373 C.Definition _ -> raise ReferenceToDefinition
374 | C.Axiom _ -> raise ReferenceToAxiom
375 | C.CurrentProof _ -> raise ReferenceToCurrentProof
376 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
377 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
378 | C.Variable (_,Some body,_) -> reduceaux context l body
380 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
381 | C.Sort _ as t -> t (* l should be empty *)
382 | C.Implicit as t -> t
384 C.Cast (reduceaux context l te, reduceaux context l ty)
385 | C.Prod (name,s,t) ->
388 reduceaux context [] s,
389 reduceaux ((Some (name,C.Decl s))::context) [] t)
390 | C.Lambda (name,s,t) ->
394 reduceaux context [] s,
395 reduceaux ((Some (name,C.Decl s))::context) [] t)
396 | he::tl -> reduceaux context tl (S.subst he t)
397 (* when name is Anonimous the substitution should be superfluous *)
400 reduceaux context l (S.subst (reduceaux context [] s) t)
402 let tl' = List.map (reduceaux context []) tl in
403 reduceaux context (tl'@l) he
404 | C.Appl [] -> raise (Impossible 1)
405 | C.Const (uri,cookingsno) as t ->
406 (match CicEnvironment.get_cooked_obj uri cookingsno with
407 C.Definition (_,body,_,_) ->
411 let res,constant_args =
412 let rec aux rev_constant_args l =
414 C.Lambda (name,s,t) as t' ->
417 [] -> raise WrongShape
419 (* when name is Anonimous the substitution should be *)
421 aux (he::rev_constant_args) tl (S.subst he t)
423 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
424 | C.Fix (i,fl) as t ->
426 List.map (function (name,_,ty,_) ->
427 Some (C.Name name, C.Decl ty)) fl
429 let (_,recindex,_,body) = List.nth fl i in
434 _ -> raise AlreadySimplified
436 (match CicReduction.whd context recparam with
438 | C.Appl ((C.MutConstruct _)::_) ->
440 let counter = ref (List.length fl) in
443 decr counter ; S.subst (C.Fix (!counter,fl))
446 (* Possible optimization: substituting whd *)
448 reduceaux (tys@context) l body',
449 List.rev rev_constant_args
450 | _ -> raise AlreadySimplified
452 | _ -> raise WrongShape
458 match constant_args with
459 [] -> C.Const (uri,cookingsno)
460 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
462 let reduced_term_to_fold = reduce context term_to_fold in
463 replace (=) reduced_term_to_fold term_to_fold res
466 (* The constant does not unfold to a Fix lambda-abstracted *)
467 (* w.r.t. zero or more variables. We just perform reduction. *)
468 reduceaux context l body
469 | AlreadySimplified ->
470 (* If we performed delta-reduction, we would find a Fix *)
471 (* not applied to a constructor. So, we refuse to perform *)
472 (* delta-reduction. *)
478 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
479 | C.Variable _ -> raise ReferenceToVariable
480 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
481 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
483 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
484 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
485 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
488 C.CoFix (i,fl) as t ->
490 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
491 let (_,_,body) = List.nth fl i in
493 let counter = ref (List.length fl) in
495 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
499 reduceaux (tys@context) [] body'
500 | C.Appl (C.CoFix (i,fl) :: tl) ->
502 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
503 let (_,_,body) = List.nth fl i in
505 let counter = ref (List.length fl) in
507 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
511 let tl' = List.map (reduceaux context []) tl in
512 reduceaux (tys@context) tl body'
515 (match decofix (reduceaux context [] term) with
516 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
517 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
518 let (arity, r, num_ingredients) =
519 match CicEnvironment.get_obj mutind with
520 C.InductiveDefinition (tl,ingredients,r) ->
521 let (_,_,arity,_) = List.nth tl i
522 and num_ingredients =
525 if k < cookingsno then i + List.length l else i
528 (arity,r,num_ingredients)
529 | _ -> raise WrongUriToInductiveDefinition
532 let num_to_eat = r + num_ingredients in
536 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
537 | _ -> raise (Impossible 5)
539 eat_first (num_to_eat,tl)
541 reduceaux context (ts@l) (List.nth pl (j-1))
542 | C.Cast _ | C.Implicit ->
543 raise (Impossible 2) (* we don't trust our whd ;-) *)
545 let outtype' = reduceaux context [] outtype in
546 let term' = reduceaux context [] term in
547 let pl' = List.map (reduceaux context []) pl in
549 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
551 if l = [] then res else C.Appl (res::l)
555 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
560 (function (n,recindex,ty,bo) ->
561 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
566 let (_,recindex,_,body) = List.nth fl i in
569 Some (List.nth l recindex)
575 (match reduceaux context [] recparam with
577 | C.Appl ((C.MutConstruct _)::_) ->
579 let counter = ref (List.length fl) in
581 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
585 (* Possible optimization: substituting whd recparam in l*)
586 reduceaux context l body'
587 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
589 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
593 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
598 (function (n,ty,bo) ->
599 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
604 if l = [] then t' else C.Appl (t'::l)