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 (* "textual" replacement of a subterm with another one *)
49 let replace ~equality ~what ~with_what ~where =
53 t when (equality t what) -> with_what
58 | C.Implicit as t -> t
59 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
60 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
61 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
62 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
64 (* Invariant enforced: no application of an application *)
65 (match List.map aux l with
66 (C.Appl l')::tl -> C.Appl (l'@tl)
70 | C.MutInd _ as t -> t
71 | C.MutConstruct _ as t -> t
72 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
73 C.MutCase (sp,cookingsno,i,aux outt, aux t,
78 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
81 C.Fix (i, substitutedfl)
85 (fun (name,ty,bo) -> (name, aux ty, aux bo))
88 C.CoFix (i, substitutedfl)
93 (* Takes a well-typed term and fully reduces it. *)
94 (*CSC: It does not perform reduction in a Case *)
96 let rec reduceaux context l =
98 let module S = CicSubstitution in
101 (match List.nth context (n-1) with
102 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
103 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
104 | None -> raise RelToHiddenHypothesis
107 (match CicEnvironment.get_cooked_obj uri 0 with
108 C.Definition _ -> raise ReferenceToDefinition
109 | C.Axiom _ -> raise ReferenceToAxiom
110 | C.CurrentProof _ -> raise ReferenceToCurrentProof
111 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
112 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
113 | C.Variable (_,Some body,_) -> reduceaux context l body
115 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
116 | C.Sort _ as t -> t (* l should be empty *)
117 | C.Implicit as t -> t
119 C.Cast (reduceaux context l te, reduceaux context l ty)
120 | C.Prod (name,s,t) ->
123 reduceaux context [] s,
124 reduceaux ((Some (name,C.Decl s))::context) [] t)
125 | C.Lambda (name,s,t) ->
129 reduceaux context [] s,
130 reduceaux ((Some (name,C.Decl s))::context) [] t)
131 | he::tl -> reduceaux context tl (S.subst he t)
132 (* when name is Anonimous the substitution should be superfluous *)
135 reduceaux context l (S.subst (reduceaux context [] s) t)
137 let tl' = List.map (reduceaux context []) tl in
138 reduceaux context (tl'@l) he
139 | C.Appl [] -> raise (Impossible 1)
140 | C.Const (uri,cookingsno) as t ->
141 (match CicEnvironment.get_cooked_obj uri cookingsno with
142 C.Definition (_,body,_,_) -> reduceaux context l body
143 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
144 | C.Variable _ -> raise ReferenceToVariable
145 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
146 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
148 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
149 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
150 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
151 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
154 C.CoFix (i,fl) as t ->
156 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
158 let (_,_,body) = List.nth fl i in
160 let counter = ref (List.length fl) in
162 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
166 reduceaux (tys@context) [] body'
167 | C.Appl (C.CoFix (i,fl) :: tl) ->
169 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
171 let (_,_,body) = List.nth fl i in
173 let counter = ref (List.length fl) in
175 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
179 let tl' = List.map (reduceaux context []) tl in
180 reduceaux (tys@context) tl' body'
183 (match decofix (reduceaux context [] term) with
184 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
185 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
186 let (arity, r, num_ingredients) =
187 match CicEnvironment.get_obj mutind with
188 C.InductiveDefinition (tl,ingredients,r) ->
189 let (_,_,arity,_) = List.nth tl i
190 and num_ingredients =
193 if k < cookingsno then i + List.length l else i
196 (arity,r,num_ingredients)
197 | _ -> raise WrongUriToInductiveDefinition
200 let num_to_eat = r + num_ingredients in
204 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
205 | _ -> raise (Impossible 5)
207 eat_first (num_to_eat,tl)
209 reduceaux context (ts@l) (List.nth pl (j-1))
210 | C.Abst _ | C.Cast _ | C.Implicit ->
211 raise (Impossible 2) (* we don't trust our whd ;-) *)
213 let outtype' = reduceaux context [] outtype in
214 let term' = reduceaux context [] term in
215 let pl' = List.map (reduceaux context []) pl in
217 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
219 if l = [] then res else C.Appl (res::l)
223 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
228 (function (n,recindex,ty,bo) ->
229 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
234 let (_,recindex,_,body) = List.nth fl i in
237 Some (List.nth l recindex)
243 (match reduceaux context [] recparam with
245 | C.Appl ((C.MutConstruct _)::_) ->
247 let counter = ref (List.length fl) in
249 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
253 (* Possible optimization: substituting whd recparam in l*)
254 reduceaux context l body'
255 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
257 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
261 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
266 (function (n,ty,bo) ->
267 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
272 if l = [] then t' else C.Appl (t'::l)
277 exception WrongShape;;
278 exception AlreadySimplified;;
279 exception WhatShouldIDo;;
281 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
282 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
284 (*CSC: {foo [n,m:nat]:nat := *)
285 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
287 (* Takes a well-typed term and *)
288 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
289 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
290 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
291 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
292 (* is applied again to the new redex; Step 3) is applied to the result *)
293 (* of the recursive simplification. Otherwise, if the Fix can not be *)
294 (* reduced, than the delta-reductions fails and the delta-redex is *)
295 (* not reduced. Otherwise, if the delta-residual is not the *)
296 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
297 (* directly returned, without performing step 3). *)
298 (* 3) Folds the application of the constant to the arguments that did not *)
299 (* change in every iteration, i.e. to the actual arguments for the *)
300 (* lambda-abstractions that precede the Fix. *)
301 (*CSC: It does not perform simplification in a Case *)
303 (* reduceaux is equal to the reduceaux locally defined inside *)
304 (*reduce, but for the const case. *)
306 let rec reduceaux context l =
307 let module C = Cic in
308 let module S = CicSubstitution in
311 (match List.nth context (n-1) with
312 Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
313 | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
314 | None -> raise RelToHiddenHypothesis
317 (match CicEnvironment.get_cooked_obj uri 0 with
318 C.Definition _ -> raise ReferenceToDefinition
319 | C.Axiom _ -> raise ReferenceToAxiom
320 | C.CurrentProof _ -> raise ReferenceToCurrentProof
321 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
322 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
323 | C.Variable (_,Some body,_) -> reduceaux context l body
325 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
326 | C.Sort _ as t -> t (* l should be empty *)
327 | C.Implicit as t -> t
329 C.Cast (reduceaux context l te, reduceaux context l ty)
330 | C.Prod (name,s,t) ->
333 reduceaux context [] s,
334 reduceaux ((Some (name,C.Decl s))::context) [] t)
335 | C.Lambda (name,s,t) ->
339 reduceaux context [] s,
340 reduceaux ((Some (name,C.Decl s))::context) [] t)
341 | he::tl -> reduceaux context tl (S.subst he t)
342 (* when name is Anonimous the substitution should be superfluous *)
345 reduceaux context l (S.subst (reduceaux context [] s) t)
347 let tl' = List.map (reduceaux context []) tl in
348 reduceaux context (tl'@l) he
349 | C.Appl [] -> raise (Impossible 1)
350 | C.Const (uri,cookingsno) as t ->
351 (match CicEnvironment.get_cooked_obj uri cookingsno with
352 C.Definition (_,body,_,_) ->
356 let res,constant_args =
357 let rec aux rev_constant_args l =
359 C.Lambda (name,s,t) as t' ->
362 [] -> raise WrongShape
364 (* when name is Anonimous the substitution should be *)
366 aux (he::rev_constant_args) tl (S.subst he t)
368 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
369 | C.Fix (i,fl) as t ->
371 List.map (function (name,_,ty,_) ->
372 Some (C.Name name, C.Decl ty)) fl
374 let (_,recindex,_,body) = List.nth fl i in
379 _ -> raise AlreadySimplified
381 (match CicReduction.whd context recparam with
383 | C.Appl ((C.MutConstruct _)::_) ->
385 let counter = ref (List.length fl) in
388 decr counter ; S.subst (C.Fix (!counter,fl))
391 (* Possible optimization: substituting whd *)
393 reduceaux (tys@context) l body',
394 List.rev rev_constant_args
395 | _ -> raise AlreadySimplified
397 | _ -> raise WrongShape
403 match constant_args with
404 [] -> C.Const (uri,cookingsno)
405 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
407 let reduced_term_to_fold = reduce context term_to_fold in
408 replace (=) reduced_term_to_fold term_to_fold res
411 (* The constant does not unfold to a Fix lambda-abstracted *)
412 (* w.r.t. zero or more variables. We just perform reduction. *)
413 reduceaux context l body
414 | AlreadySimplified ->
415 (* If we performed delta-reduction, we would find a Fix *)
416 (* not applied to a constructor. So, we refuse to perform *)
417 (* delta-reduction. *)
423 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
424 | C.Variable _ -> raise ReferenceToVariable
425 | C.CurrentProof (_,_,body,_) -> reduceaux context l body
426 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
428 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
429 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
430 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
431 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
434 C.CoFix (i,fl) as t ->
436 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
437 let (_,_,body) = List.nth fl i in
439 let counter = ref (List.length fl) in
441 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
445 reduceaux (tys@context) [] body'
446 | C.Appl (C.CoFix (i,fl) :: tl) ->
448 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
449 let (_,_,body) = List.nth fl i in
451 let counter = ref (List.length fl) in
453 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
457 let tl' = List.map (reduceaux context []) tl in
458 reduceaux (tys@context) tl body'
461 (match decofix (reduceaux context [] term) with
462 C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
463 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
464 let (arity, r, num_ingredients) =
465 match CicEnvironment.get_obj mutind with
466 C.InductiveDefinition (tl,ingredients,r) ->
467 let (_,_,arity,_) = List.nth tl i
468 and num_ingredients =
471 if k < cookingsno then i + List.length l else i
474 (arity,r,num_ingredients)
475 | _ -> raise WrongUriToInductiveDefinition
478 let num_to_eat = r + num_ingredients in
482 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
483 | _ -> raise (Impossible 5)
485 eat_first (num_to_eat,tl)
487 reduceaux context (ts@l) (List.nth pl (j-1))
488 | C.Abst _ | C.Cast _ | C.Implicit ->
489 raise (Impossible 2) (* we don't trust our whd ;-) *)
491 let outtype' = reduceaux context [] outtype in
492 let term' = reduceaux context [] term in
493 let pl' = List.map (reduceaux context []) pl in
495 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
497 if l = [] then res else C.Appl (res::l)
501 List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
506 (function (n,recindex,ty,bo) ->
507 (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
512 let (_,recindex,_,body) = List.nth fl i in
515 Some (List.nth l recindex)
521 (match reduceaux context [] recparam with
523 | C.Appl ((C.MutConstruct _)::_) ->
525 let counter = ref (List.length fl) in
527 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
531 (* Possible optimization: substituting whd recparam in l*)
532 reduceaux context l body'
533 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
535 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
539 List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
544 (function (n,ty,bo) ->
545 (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
550 if l = [] then t' else C.Appl (t'::l)