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)
249 function t -> let res =
250 prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
252 t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
255 exception WrongShape;;
256 exception AlreadySimplified;;
257 exception WhatShouldIDo;;
259 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
260 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
262 (*CSC: {foo [n,m:nat]:nat := *)
263 (*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
265 (* Takes a well-typed term and *)
266 (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
267 (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
268 (* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
269 (* is reduced, the delta-reduction is succesfull and the whole algorithm *)
270 (* is applied again to the new redex; Step 3) is applied to the result *)
271 (* of the recursive simplification. Otherwise, if the Fix can not be *)
272 (* reduced, than the delta-reductions fails and the delta-redex is *)
273 (* not reduced. Otherwise, if the delta-residual is not the *)
274 (* lambda-abstraction of a Fix, then it is reduced and the result is *)
275 (* directly returned, without performing step 3). *)
276 (* 3) Folds the application of the constant to the arguments that did not *)
277 (* change in every iteration, i.e. to the actual arguments for the *)
278 (* lambda-abstractions that precede the Fix. *)
279 (*CSC: It does not perform simplification in a Case *)
281 (* reduceaux is equal to the reduceaux locally defined inside *)
282 (*reduce, but for the const case. *)
284 let rec reduceaux l =
285 let module C = Cic in
286 let module S = CicSubstitution in
288 C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
290 (match CicEnvironment.get_cooked_obj uri 0 with
291 C.Definition _ -> raise ReferenceToDefinition
292 | C.Axiom _ -> raise ReferenceToAxiom
293 | C.CurrentProof _ -> raise ReferenceToCurrentProof
294 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
295 | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
296 | C.Variable (_,Some body,_) -> reduceaux l body
298 | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
299 | C.Sort _ as t -> t (* l should be empty *)
300 | C.Implicit as t -> t
301 | C.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
302 | C.Prod (name,s,t) ->
304 C.Prod (name, reduceaux [] s, reduceaux [] t)
305 | C.Lambda (name,s,t) ->
307 [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
308 | he::tl -> reduceaux tl (S.subst he t)
309 (* when name is Anonimous the substitution should be superfluous *)
311 | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
313 let tl' = List.map (reduceaux []) tl in
315 | C.Appl [] -> raise (Impossible 1)
316 | C.Const (uri,cookingsno) as t ->
317 (match CicEnvironment.get_cooked_obj uri cookingsno with
318 C.Definition (_,body,_,_) ->
322 let res,constant_args =
323 let rec aux rev_constant_args l =
325 C.Lambda (name,s,t) as t' ->
328 [] -> raise WrongShape
330 (* when name is Anonimous the substitution should be *)
332 aux (he::rev_constant_args) tl (S.subst he t)
334 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
335 | C.Fix (i,fl) as t ->
336 let (_,recindex,_,body) = List.nth fl i in
341 _ -> raise AlreadySimplified
343 (match CicReduction.whd recparam with
345 | C.Appl ((C.MutConstruct _)::_) ->
347 let counter = ref (List.length fl) in
350 decr counter ; S.subst (C.Fix (!counter,fl))
353 (* Possible optimization: substituting whd *)
355 reduceaux l body', List.rev rev_constant_args
356 | _ -> raise AlreadySimplified
358 | _ -> raise WrongShape
364 match constant_args with
365 [] -> C.Const (uri,cookingsno)
366 | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
368 let reduced_term_to_fold = reduce term_to_fold in
369 prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
370 prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
371 replace reduced_term_to_fold term_to_fold res
374 (* The constant does not unfold to a Fix lambda-abstracted *)
375 (* w.r.t. zero or more variables. We just perform reduction. *)
377 | AlreadySimplified ->
378 (* If we performed delta-reduction, we would find a Fix *)
379 (* not applied to a constructor. So, we refuse to perform *)
380 (* delta-reduction. *)
386 | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
387 | C.Variable _ -> raise ReferenceToVariable
388 | C.CurrentProof (_,_,body,_) -> reduceaux l body
389 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
391 | C.Abst _ as t -> t (*CSC l should be empty ????? *)
392 | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
393 | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
394 | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
397 C.CoFix (i,fl) as t ->
398 let (_,_,body) = List.nth fl i in
400 let counter = ref (List.length fl) in
402 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
407 | C.Appl (C.CoFix (i,fl) :: tl) ->
408 let (_,_,body) = List.nth fl i in
410 let counter = ref (List.length fl) in
412 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
416 let tl' = List.map (reduceaux []) tl in
420 (match decofix (reduceaux [] term) with
421 C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
422 | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
423 let (arity, r, num_ingredients) =
424 match CicEnvironment.get_obj mutind with
425 C.InductiveDefinition (tl,ingredients,r) ->
426 let (_,_,arity,_) = List.nth tl i
427 and num_ingredients =
430 if k < cookingsno then i + List.length l else i
433 (arity,r,num_ingredients)
434 | _ -> raise WrongUriToInductiveDefinition
437 let num_to_eat = r + num_ingredients in
441 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
442 | _ -> raise (Impossible 5)
444 eat_first (num_to_eat,tl)
446 reduceaux (ts@l) (List.nth pl (j-1))
447 | C.Abst _ | C.Cast _ | C.Implicit ->
448 raise (Impossible 2) (* we don't trust our whd ;-) *)
450 let outtype' = reduceaux [] outtype in
451 let term' = reduceaux [] term in
452 let pl' = List.map (reduceaux []) pl in
454 C.MutCase (mutind,cookingsno,i,outtype',term',pl')
456 if l = [] then res else C.Appl (res::l)
462 (function (n,recindex,ty,bo) ->
463 (n,recindex,reduceaux [] ty, reduceaux [] bo)
468 let (_,recindex,_,body) = List.nth fl i in
471 Some (List.nth l recindex)
477 (match reduceaux [] recparam with
479 | C.Appl ((C.MutConstruct _)::_) ->
481 let counter = ref (List.length fl) in
483 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
487 (* Possible optimization: substituting whd recparam in l *)
489 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
491 | None -> if l = [] then t' () else C.Appl ((t' ())::l)
497 (function (n,ty,bo) ->
498 (n,reduceaux [] ty, reduceaux [] bo)
503 if l = [] then t' else C.Appl (t'::l)