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;;
47 (* "textual" replacement of a subterm with another one *)
48 let replace ~what ~with_what ~where =
52 t when t = what -> with_what
57 | C.Implicit as t -> t
58 | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
59 | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
60 | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
61 | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
63 (* Invariant enforced: no application of an application *)
64 (match List.map aux l with
65 (C.Appl l')::tl -> C.Appl (l'@tl)
69 | C.MutInd _ as t -> t
70 | C.MutConstruct _ as t -> t
71 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
72 C.MutCase (sp,cookingsno,i,aux outt, aux t,
77 (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
80 C.Fix (i, substitutedfl)
84 (fun (name,ty,bo) -> (name, aux ty, aux bo))
87 C.CoFix (i, substitutedfl)
92 (* Takes a well-typed term and fully reduces it. *)
93 (*CSC: It does not perform reduction in a Case *)
97 let module S = CicSubstitution in
99 C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
101 (match CicEnvironment.get_cooked_obj uri 0 with
102 C.Definition _ -> raise ReferenceToDefinition
103 | C.Axiom _ -> raise ReferenceToAxiom
104 | C.CurrentProof _ -> raise ReferenceToCurrentProof
105 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
106 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
107 | C.Variable (_,Some body,_) -> reduceaux l body
109 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
110 | C.Sort _ as t -> t (* l should be empty *)
111 | C.Implicit as t -> t
112 | C.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
113 | C.Prod (name,s,t) ->
115 C.Prod (name, reduceaux [] s, reduceaux [] t)
116 | C.Lambda (name,s,t) ->
118 [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
119 | he::tl -> reduceaux tl (S.subst he t)
120 (* when name is Anonimous the substitution should be superfluous *)
122 | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
124 let tl' = List.map (reduceaux []) tl in
126 | C.Appl [] -> raise (Impossible 1)
127 | C.Const (uri,cookingsno) as t ->
128 (match CicEnvironment.get_cooked_obj uri cookingsno with
129 C.Definition (_,body,_,_) -> reduceaux l body
130 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
131 | C.Variable _ -> raise ReferenceToVariable
132 | C.CurrentProof (_,_,body,_) -> reduceaux l body
133 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
135 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
136 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
137 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
138 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
141 C.CoFix (i,fl) as t ->
142 let (_,_,body) = List.nth fl i in
144 let counter = ref (List.length fl) in
146 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
151 | C.Appl (C.CoFix (i,fl) :: tl) ->
152 let (_,_,body) = List.nth fl i in
154 let counter = ref (List.length fl) in
156 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
160 let tl' = List.map (reduceaux []) tl in
164 (match decofix (reduceaux [] term) with
165 C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
166 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
167 let (arity, r, num_ingredients) =
168 match CicEnvironment.get_obj mutind with
169 C.InductiveDefinition (tl,ingredients,r) ->
170 let (_,_,arity,_) = List.nth tl i
171 and num_ingredients =
174 if k < cookingsno then i + List.length l else i
177 (arity,r,num_ingredients)
178 | _ -> raise WrongUriToInductiveDefinition
181 let num_to_eat = r + num_ingredients in
185 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
186 | _ -> raise (Impossible 5)
188 eat_first (num_to_eat,tl)
190 reduceaux (ts@l) (List.nth pl (j-1))
191 | C.Abst _ | C.Cast _ | C.Implicit ->
192 raise (Impossible 2) (* we don't trust our whd ;-) *)
194 let outtype' = reduceaux [] outtype in
195 let term' = reduceaux [] term in
196 let pl' = List.map (reduceaux []) pl in
198 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
200 if l = [] then res else C.Appl (res::l)
206 (function (n,recindex,ty,bo) ->
207 (n,recindex,reduceaux [] ty, reduceaux [] bo)
212 let (_,recindex,_,body) = List.nth fl i in
215 Some (List.nth l recindex)
221 (match reduceaux [] recparam with
223 | C.Appl ((C.MutConstruct _)::_) ->
225 let counter = ref (List.length fl) in
227 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
231 (* Possible optimization: substituting whd recparam in l *)
233 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
235 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
241 (function (n,ty,bo) ->
242 (n,reduceaux [] ty, reduceaux [] bo)
247 if l = [] then t' else C.Appl (t'::l)
252 exception WrongShape;;
253 exception AlreadySimplified;;
254 exception WhatShouldIDo;;
256 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
257 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
259 (*CSC: {foo [n,m:nat]:nat := *)
260 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
262 (* Takes a well-typed term and *)
263 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
264 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
265 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
266 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
267 (* is applied again to the new redex; Step 3) is applied to the result *)
268 (* of the recursive simplification. Otherwise, if the Fix can not be *)
269 (* reduced, than the delta-reductions fails and the delta-redex is *)
270 (* not reduced. Otherwise, if the delta-residual is not the *)
271 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
272 (* directly returned, without performing step 3). *)
273 (* 3) Folds the application of the constant to the arguments that did not *)
274 (* change in every iteration, i.e. to the actual arguments for the *)
275 (* lambda-abstractions that precede the Fix. *)
276 (*CSC: It does not perform simplification in a Case *)
278 (* reduceaux is equal to the reduceaux locally defined inside *)
279 (*reduce, but for the const case. *)
281 let rec reduceaux l =
282 let module C = Cic in
283 let module S = CicSubstitution in
285 C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
287 (match CicEnvironment.get_cooked_obj uri 0 with
288 C.Definition _ -> raise ReferenceToDefinition
289 | C.Axiom _ -> raise ReferenceToAxiom
290 | C.CurrentProof _ -> raise ReferenceToCurrentProof
291 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
292 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
293 | C.Variable (_,Some body,_) -> reduceaux l body
295 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
296 | C.Sort _ as t -> t (* l should be empty *)
297 | C.Implicit as t -> t
298 | C.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
299 | C.Prod (name,s,t) ->
301 C.Prod (name, reduceaux [] s, reduceaux [] t)
302 | C.Lambda (name,s,t) ->
304 [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
305 | he::tl -> reduceaux tl (S.subst he t)
306 (* when name is Anonimous the substitution should be superfluous *)
308 | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
310 let tl' = List.map (reduceaux []) tl in
312 | C.Appl [] -> raise (Impossible 1)
313 | C.Const (uri,cookingsno) as t ->
314 (match CicEnvironment.get_cooked_obj uri cookingsno with
315 C.Definition (_,body,_,_) ->
319 let res,constant_args =
320 let rec aux rev_constant_args l =
322 C.Lambda (name,s,t) as t' ->
325 [] -> raise WrongShape
327 (* when name is Anonimous the substitution should be *)
329 aux (he::rev_constant_args) tl (S.subst he t)
331 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
332 | C.Fix (i,fl) as t ->
333 let (_,recindex,_,body) = List.nth fl i in
338 _ -> raise AlreadySimplified
340 (match CicReduction.whd context recparam with
342 | C.Appl ((C.MutConstruct _)::_) ->
344 let counter = ref (List.length fl) in
347 decr counter ; S.subst (C.Fix (!counter,fl))
350 (* Possible optimization: substituting whd *)
352 reduceaux l body', List.rev rev_constant_args
353 | _ -> raise AlreadySimplified
355 | _ -> raise WrongShape
361 match constant_args with
362 [] -> C.Const (uri,cookingsno)
363 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
365 let reduced_term_to_fold = reduce context term_to_fold in
366 prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
367 prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
368 replace reduced_term_to_fold term_to_fold res
371 (* The constant does not unfold to a Fix lambda-abstracted *)
372 (* w.r.t. zero or more variables. We just perform reduction. *)
374 | AlreadySimplified ->
375 (* If we performed delta-reduction, we would find a Fix *)
376 (* not applied to a constructor. So, we refuse to perform *)
377 (* delta-reduction. *)
383 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
384 | C.Variable _ -> raise ReferenceToVariable
385 | C.CurrentProof (_,_,body,_) -> reduceaux l body
386 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
388 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
389 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
390 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
391 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
394 C.CoFix (i,fl) as t ->
395 let (_,_,body) = List.nth fl i in
397 let counter = ref (List.length fl) in
399 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
404 | C.Appl (C.CoFix (i,fl) :: tl) ->
405 let (_,_,body) = List.nth fl i in
407 let counter = ref (List.length fl) in
409 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
413 let tl' = List.map (reduceaux []) tl in
417 (match decofix (reduceaux [] term) with
418 C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
419 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
420 let (arity, r, num_ingredients) =
421 match CicEnvironment.get_obj mutind with
422 C.InductiveDefinition (tl,ingredients,r) ->
423 let (_,_,arity,_) = List.nth tl i
424 and num_ingredients =
427 if k < cookingsno then i + List.length l else i
430 (arity,r,num_ingredients)
431 | _ -> raise WrongUriToInductiveDefinition
434 let num_to_eat = r + num_ingredients in
438 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
439 | _ -> raise (Impossible 5)
441 eat_first (num_to_eat,tl)
443 reduceaux (ts@l) (List.nth pl (j-1))
444 | C.Abst _ | C.Cast _ | C.Implicit ->
445 raise (Impossible 2) (* we don't trust our whd ;-) *)
447 let outtype' = reduceaux [] outtype in
448 let term' = reduceaux [] term in
449 let pl' = List.map (reduceaux []) pl in
451 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
453 if l = [] then res else C.Appl (res::l)
459 (function (n,recindex,ty,bo) ->
460 (n,recindex,reduceaux [] ty, reduceaux [] bo)
465 let (_,recindex,_,body) = List.nth fl i in
468 Some (List.nth l recindex)
474 (match reduceaux [] recparam with
476 | C.Appl ((C.MutConstruct _)::_) ->
478 let counter = ref (List.length fl) in
480 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
484 (* Possible optimization: substituting whd recparam in l *)
486 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
488 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
494 (function (n,ty,bo) ->
495 (n,reduceaux [] ty, reduceaux [] bo)
500 if l = [] then t' else C.Appl (t'::l)