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.Abst _, C.Abst _ -> assert false
79 | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
80 UriManager.eq uri uri' && i = i'
81 | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
82 UriManager.eq uri uri' && i = i' && j = j'
83 | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
84 UriManager.eq sp sp' && i = i' &&
85 syntactic_equality outt outt' &&
86 syntactic_equality t t' &&
88 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
89 | C.Fix (i,fl), C.Fix (i',fl') ->
92 (fun b (name,i,ty,bo) (name',i',ty',bo') ->
93 b && name = name' && i = i' &&
94 syntactic_equality ty ty' &&
95 syntactic_equality bo bo') true fl fl'
96 | C.CoFix (i,fl), C.CoFix (i',fl') ->
99 (fun b (name,ty,bo) (name',ty',bo') ->
101 syntactic_equality ty ty' &&
102 syntactic_equality bo bo') true fl fl'
106 (* "textual" replacement of a subterm with another one *)
107 let replace ~equality ~what ~with_what ~where =
108 let module C = Cic in
111 t when (equality t what) -> with_what
116 | C.Implicit as t -> t
117 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
118 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
119 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
120 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
122 (* Invariant enforced: no application of an application *)
123 (match List.map aux l with
124 (C.Appl l')::tl -> C.Appl (l'@tl)
126 | C.Const _ as t -> t
128 | C.MutInd _ as t -> t
129 | C.MutConstruct _ as t -> t
130 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
131 C.MutCase (sp,cookingsno,i,aux outt, aux t,
136 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
139 C.Fix (i, substitutedfl)
143 (fun (name,ty,bo) -> (name, aux ty, aux bo))
146 C.CoFix (i, substitutedfl)
151 (* Takes a well-typed term and fully reduces it. *)
152 (*CSC: It does not perform reduction in a Case *)
154 let rec reduceaux context l =
155 let module C = Cic in
156 let module S = CicSubstitution in
159 (match List.nth context (n-1) with
160 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
161 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
162 | None -> raise RelToHiddenHypothesis
165 (match CicEnvironment.get_cooked_obj uri 0 with
166 C.Definition _ -> raise ReferenceToDefinition
167 | C.Axiom _ -> raise ReferenceToAxiom
168 | C.CurrentProof _ -> raise ReferenceToCurrentProof
169 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
170 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
171 | C.Variable (_,Some body,_) -> reduceaux context l body
173 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
174 | C.Sort _ as t -> t (* l should be empty *)
175 | C.Implicit as t -> t
177 C.Cast (reduceaux context l te, reduceaux context l ty)
178 | C.Prod (name,s,t) ->
181 reduceaux context [] s,
182 reduceaux ((Some (name,C.Decl s))::context) [] t)
183 | C.Lambda (name,s,t) ->
187 reduceaux context [] s,
188 reduceaux ((Some (name,C.Decl s))::context) [] t)
189 | he::tl -> reduceaux context tl (S.subst he t)
190 (* when name is Anonimous the substitution should be superfluous *)
193 reduceaux context l (S.subst (reduceaux context [] s) t)
195 let tl' = List.map (reduceaux context []) tl in
196 reduceaux context (tl'@l) he
197 | C.Appl [] -> raise (Impossible 1)
198 | C.Const (uri,cookingsno) as t ->
199 (match CicEnvironment.get_cooked_obj uri cookingsno with
200 C.Definition (_,body,_,_) -> reduceaux context l body
201 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
202 | C.Variable _ -> raise ReferenceToVariable
203 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
204 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
206 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
207 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
208 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
209 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
212 C.CoFix (i,fl) as t ->
214 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
216 let (_,_,body) = List.nth fl i in
218 let counter = ref (List.length fl) in
220 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
224 reduceaux (tys@context) [] body'
225 | C.Appl (C.CoFix (i,fl) :: tl) ->
227 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
229 let (_,_,body) = List.nth fl i in
231 let counter = ref (List.length fl) in
233 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
237 let tl' = List.map (reduceaux context []) tl in
238 reduceaux (tys@context) tl' body'
241 (match decofix (reduceaux context [] term) with
242 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
243 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
244 let (arity, r, num_ingredients) =
245 match CicEnvironment.get_obj mutind with
246 C.InductiveDefinition (tl,ingredients,r) ->
247 let (_,_,arity,_) = List.nth tl i
248 and num_ingredients =
251 if k < cookingsno then i + List.length l else i
254 (arity,r,num_ingredients)
255 | _ -> raise WrongUriToInductiveDefinition
258 let num_to_eat = r + num_ingredients in
262 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
263 | _ -> raise (Impossible 5)
265 eat_first (num_to_eat,tl)
267 reduceaux context (ts@l) (List.nth pl (j-1))
268 | C.Abst _ | C.Cast _ | C.Implicit ->
269 raise (Impossible 2) (* we don't trust our whd ;-) *)
271 let outtype' = reduceaux context [] outtype in
272 let term' = reduceaux context [] term in
273 let pl' = List.map (reduceaux context []) pl in
275 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
277 if l = [] then res else C.Appl (res::l)
281 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
286 (function (n,recindex,ty,bo) ->
287 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
292 let (_,recindex,_,body) = List.nth fl i in
295 Some (List.nth l recindex)
301 (match reduceaux context [] recparam with
303 | C.Appl ((C.MutConstruct _)::_) ->
305 let counter = ref (List.length fl) in
307 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
311 (* Possible optimization: substituting whd recparam in l*)
312 reduceaux context l body'
313 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
315 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
319 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
324 (function (n,ty,bo) ->
325 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
330 if l = [] then t' else C.Appl (t'::l)
335 exception WrongShape;;
336 exception AlreadySimplified;;
337 exception WhatShouldIDo;;
339 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
340 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
342 (*CSC: {foo [n,m:nat]:nat := *)
343 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
345 (* Takes a well-typed term and *)
346 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
347 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
348 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
349 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
350 (* is applied again to the new redex; Step 3) is applied to the result *)
351 (* of the recursive simplification. Otherwise, if the Fix can not be *)
352 (* reduced, than the delta-reductions fails and the delta-redex is *)
353 (* not reduced. Otherwise, if the delta-residual is not the *)
354 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
355 (* directly returned, without performing step 3). *)
356 (* 3) Folds the application of the constant to the arguments that did not *)
357 (* change in every iteration, i.e. to the actual arguments for the *)
358 (* lambda-abstractions that precede the Fix. *)
359 (*CSC: It does not perform simplification in a Case *)
361 (* reduceaux is equal to the reduceaux locally defined inside *)
362 (*reduce, but for the const case. *)
364 let rec reduceaux context l =
365 let module C = Cic in
366 let module S = CicSubstitution in
369 (match List.nth context (n-1) with
370 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
371 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
372 | None -> raise RelToHiddenHypothesis
375 (match CicEnvironment.get_cooked_obj uri 0 with
376 C.Definition _ -> raise ReferenceToDefinition
377 | C.Axiom _ -> raise ReferenceToAxiom
378 | C.CurrentProof _ -> raise ReferenceToCurrentProof
379 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
380 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
381 | C.Variable (_,Some body,_) -> reduceaux context l body
383 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
384 | C.Sort _ as t -> t (* l should be empty *)
385 | C.Implicit as t -> t
387 C.Cast (reduceaux context l te, reduceaux context l ty)
388 | C.Prod (name,s,t) ->
391 reduceaux context [] s,
392 reduceaux ((Some (name,C.Decl s))::context) [] t)
393 | C.Lambda (name,s,t) ->
397 reduceaux context [] s,
398 reduceaux ((Some (name,C.Decl s))::context) [] t)
399 | he::tl -> reduceaux context tl (S.subst he t)
400 (* when name is Anonimous the substitution should be superfluous *)
403 reduceaux context l (S.subst (reduceaux context [] s) t)
405 let tl' = List.map (reduceaux context []) tl in
406 reduceaux context (tl'@l) he
407 | C.Appl [] -> raise (Impossible 1)
408 | C.Const (uri,cookingsno) as t ->
409 (match CicEnvironment.get_cooked_obj uri cookingsno with
410 C.Definition (_,body,_,_) ->
414 let res,constant_args =
415 let rec aux rev_constant_args l =
417 C.Lambda (name,s,t) as t' ->
420 [] -> raise WrongShape
422 (* when name is Anonimous the substitution should be *)
424 aux (he::rev_constant_args) tl (S.subst he t)
426 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
427 | C.Fix (i,fl) as t ->
429 List.map (function (name,_,ty,_) ->
430 Some (C.Name name, C.Decl ty)) fl
432 let (_,recindex,_,body) = List.nth fl i in
437 _ -> raise AlreadySimplified
439 (match CicReduction.whd context recparam with
441 | C.Appl ((C.MutConstruct _)::_) ->
443 let counter = ref (List.length fl) in
446 decr counter ; S.subst (C.Fix (!counter,fl))
449 (* Possible optimization: substituting whd *)
451 reduceaux (tys@context) l body',
452 List.rev rev_constant_args
453 | _ -> raise AlreadySimplified
455 | _ -> raise WrongShape
461 match constant_args with
462 [] -> C.Const (uri,cookingsno)
463 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
465 let reduced_term_to_fold = reduce context term_to_fold in
466 replace (=) reduced_term_to_fold term_to_fold res
469 (* The constant does not unfold to a Fix lambda-abstracted *)
470 (* w.r.t. zero or more variables. We just perform reduction. *)
471 reduceaux context l body
472 | AlreadySimplified ->
473 (* If we performed delta-reduction, we would find a Fix *)
474 (* not applied to a constructor. So, we refuse to perform *)
475 (* delta-reduction. *)
481 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
482 | C.Variable _ -> raise ReferenceToVariable
483 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
484 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
486 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
487 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
488 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
489 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
492 C.CoFix (i,fl) as t ->
494 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
495 let (_,_,body) = List.nth fl i in
497 let counter = ref (List.length fl) in
499 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
503 reduceaux (tys@context) [] body'
504 | C.Appl (C.CoFix (i,fl) :: tl) ->
506 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
507 let (_,_,body) = List.nth fl i in
509 let counter = ref (List.length fl) in
511 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
515 let tl' = List.map (reduceaux context []) tl in
516 reduceaux (tys@context) tl body'
519 (match decofix (reduceaux context [] term) with
520 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
521 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
522 let (arity, r, num_ingredients) =
523 match CicEnvironment.get_obj mutind with
524 C.InductiveDefinition (tl,ingredients,r) ->
525 let (_,_,arity,_) = List.nth tl i
526 and num_ingredients =
529 if k < cookingsno then i + List.length l else i
532 (arity,r,num_ingredients)
533 | _ -> raise WrongUriToInductiveDefinition
536 let num_to_eat = r + num_ingredients in
540 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
541 | _ -> raise (Impossible 5)
543 eat_first (num_to_eat,tl)
545 reduceaux context (ts@l) (List.nth pl (j-1))
546 | C.Abst _ | C.Cast _ | C.Implicit ->
547 raise (Impossible 2) (* we don't trust our whd ;-) *)
549 let outtype' = reduceaux context [] outtype in
550 let term' = reduceaux context [] term in
551 let pl' = List.map (reduceaux context []) pl in
553 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
555 if l = [] then res else C.Appl (res::l)
559 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
564 (function (n,recindex,ty,bo) ->
565 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
570 let (_,recindex,_,body) = List.nth fl i in
573 Some (List.nth l recindex)
579 (match reduceaux context [] recparam with
581 | C.Appl ((C.MutConstruct _)::_) ->
583 let counter = ref (List.length fl) in
585 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
589 (* Possible optimization: substituting whd recparam in l*)
590 reduceaux context l body'
591 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
593 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
597 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
602 (function (n,ty,bo) ->
603 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
608 if l = [] then t' else C.Appl (t'::l)