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 exception CicReductionInternalError;;
27 exception WrongUriToInductiveDefinition;;
28 exception Impossible of int;;
29 exception ReferenceToConstant;;
30 exception ReferenceToVariable;;
31 exception ReferenceToCurrentProof;;
32 exception ReferenceToInductiveDefinition;;
36 let rec debug_aux t i =
38 let module U = UriManager in
39 CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
43 print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
48 type env = Cic.term list;;
49 type stack = Cic.term list;;
51 int * env * Cic.term Cic.explicit_named_substitution * Cic.term * stack;;
55 (* k is the length of the environment e *)
56 (* m is the current depth inside the term *)
57 let unwind' m k e ens t =
59 let module S = CicSubstitution in
60 if k = 0 && ens = [] then
63 let rec unwind_aux m =
69 Some (List.nth e (n-m-1))
74 if m = 0 then t' else S.lift m t'
77 | C.Var (uri,exp_named_subst) ->
79 prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
81 if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
82 CicSubstitution.lift m (List.assq uri ens)
85 (match CicEnvironment.get_cooked_obj uri with
86 C.Constant _ -> raise ReferenceToConstant
87 | C.Variable (_,_,_,params) -> params
88 | C.CurrentProof _ -> raise ReferenceToCurrentProof
89 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
92 let exp_named_subst' =
93 substaux_in_exp_named_subst params exp_named_subst m
95 C.Var (uri,exp_named_subst')
101 | Some t -> Some (unwind_aux m t)
106 | C.Implicit as t -> t
107 | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *)
108 | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
109 | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
110 | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
111 | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
112 | C.Const (uri,exp_named_subst) ->
114 (match CicEnvironment.get_cooked_obj uri with
115 C.Constant (_,_,_,params) -> params
116 | C.Variable _ -> raise ReferenceToVariable
117 | C.CurrentProof (_,_,_,_,params) -> params
118 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
121 let exp_named_subst' =
122 substaux_in_exp_named_subst params exp_named_subst m
124 C.Const (uri,exp_named_subst')
125 | C.MutInd (uri,i,exp_named_subst) ->
127 (match CicEnvironment.get_cooked_obj uri with
128 C.Constant _ -> raise ReferenceToConstant
129 | C.Variable _ -> raise ReferenceToVariable
130 | C.CurrentProof _ -> raise ReferenceToCurrentProof
131 | C.InductiveDefinition (_,params,_) -> params
134 let exp_named_subst' =
135 substaux_in_exp_named_subst params exp_named_subst m
137 C.MutInd (uri,i,exp_named_subst')
138 | C.MutConstruct (uri,i,j,exp_named_subst) ->
140 (match CicEnvironment.get_cooked_obj uri with
141 C.Constant _ -> raise ReferenceToConstant
142 | C.Variable _ -> raise ReferenceToVariable
143 | C.CurrentProof _ -> raise ReferenceToCurrentProof
144 | C.InductiveDefinition (_,params,_) -> params
147 let exp_named_subst' =
148 substaux_in_exp_named_subst params exp_named_subst m
150 C.MutConstruct (uri,i,j,exp_named_subst')
151 | C.MutCase (sp,i,outt,t,pl) ->
152 C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
153 List.map (unwind_aux m) pl)
155 let len = List.length fl in
158 (fun (name,i,ty,bo) ->
159 (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
162 C.Fix (i, substitutedfl)
164 let len = List.length fl in
167 (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
170 C.CoFix (i, substitutedfl)
171 and substaux_in_exp_named_subst params exp_named_subst' m =
172 (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
174 List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
175 (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
176 List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
178 let rec filter_and_lift =
182 let r = filter_and_lift tl in
184 (uri,(List.assq uri ens'))::r
189 filter_and_lift params
192 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
193 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
195 (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
196 (*CSC: codice altamente inefficiente *)
197 let rec filter_and_lift already_instantiated =
202 (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
204 not (List.mem uri already_instantiated)
208 (uri,CicSubstitution.lift m t) ::
209 (filter_and_lift (uri::already_instantiated) tl)
210 | _::tl -> filter_and_lift already_instantiated tl
213 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
214 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
215 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
216 if List.mem uri params then prerr_endline "---- OK2" ;
220 List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
221 (filter_and_lift [] (List.rev ens))
230 let reduce context : config -> Cic.term =
231 let module C = Cic in
232 let module S = CicSubstitution in
235 (k, e, _, (C.Rel n as t), s) ->
238 Some (List.nth e (n-1))
243 match List.nth context (n - 1 - k) with
245 | Some (_,C.Decl _) -> None
246 | Some (_,C.Def x) -> Some (S.lift (n - k) x)
252 Some t' -> reduce (0,[],[],t',s)
256 else C.Appl (C.Rel (n-k)::s)
258 | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
259 if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
260 reduce (0, [], [], List.assq uri ens, s)
262 (match CicEnvironment.get_cooked_obj uri with
263 C.Constant _ -> raise ReferenceToConstant
264 | C.CurrentProof _ -> raise ReferenceToCurrentProof
265 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
266 | C.Variable (_,None,_,_) ->
267 let t' = unwind k e ens t in
268 if s = [] then t' else C.Appl (t'::s)
269 | C.Variable (_,Some body,_,_) ->
270 let ens' = push_exp_named_subst k e ens exp_named_subst in
271 reduce (0, [], ens', body, s)
273 | (k, e, ens, (C.Meta _ as t), s) ->
274 let t' = unwind k e ens t in
275 if s = [] then t' else C.Appl (t'::s)
276 | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
277 | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *)
278 | (k, e, ens, (C.Cast (te,ty) as t), s) ->
279 reduce (k, e, ens, te, s) (* s should be empty *)
280 | (k, e, ens, (C.Prod _ as t), s) -> unwind k e ens t (* s should be empty *)
281 | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
282 | (k, e, ens, C.Lambda (_,_,t), p::s) ->
283 reduce (k+1, p::e, ens, t,s)
285 | (k, e, ens, (C.LetIn (_,m,t) as t'), s) when lazily ->
286 let m' = unwind k e ens m in reduce (k+1, m'::e, ens, t, s)
288 | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
289 let m' = reduce (k,e,ens,m,[]) in reduce (k+1,m'::e,ens,t,s)
290 | (_, _, _, C.Appl [], _) -> raise (Impossible 1)
292 | (k, e, ens, C.Appl (he::tl), s) when lazily ->
293 let tl' = List.map (unwind k e ens) tl in
294 reduce (k, e, ens, he, (List.append tl' s))
295 (* strict, but constants are NOT unfolded *)
296 | (k, e, ens, C.Appl (he::tl), s) ->
297 (* constants are NOT unfolded *)
300 C.Const _ as t -> unwind k e ens t
301 | t -> reduce (k,e,ens,t,[])
303 let tl' = List.map red tl in
304 reduce (k, e, ens, he , List.append tl' s)
306 | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
307 | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
308 | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
309 | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
310 (* strict evaluation, but constants are NOT unfolded *)
313 C.Const _ as t -> unwind k e ens t
314 | t -> reduce (k,e,ens,t,[])
316 let tl' = List.map red tl in
317 reduce (k, e, ens, he , List.append tl' s)
318 | (k, e, ens, C.Appl l, s) ->
319 C.Appl (List.append (List.map (unwind k e ens) l) s)
321 | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
322 (match CicEnvironment.get_cooked_obj uri with
323 C.Constant (_,Some body,_,_) ->
324 let ens' = push_exp_named_subst k e ens exp_named_subst in
325 (* constants are closed *)
326 reduce (0, [], ens', body, s)
327 | C.Constant (_,None,_,_) ->
328 let t' = unwind k e ens t in
329 if s = [] then t' else C.Appl (t'::s)
330 | C.Variable _ -> raise ReferenceToVariable
331 | C.CurrentProof (_,_,body,_,_) ->
332 let ens' = push_exp_named_subst k e ens exp_named_subst in
333 (* constants are closed *)
334 reduce (0, [], ens', body, s)
335 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
337 | (k, e, ens, (C.MutInd _ as t),s) ->
338 let t' = unwind k e ens t in
339 if s = [] then t' else C.Appl (t'::s)
340 | (k, e, ens, (C.MutConstruct _ as t),s) ->
341 let t' = unwind k e ens t in
342 if s = [] then t' else C.Appl (t'::s)
343 | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
346 C.CoFix (i,fl) as t ->
347 let (_,_,body) = List.nth fl i in
349 let counter = ref (List.length fl) in
351 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
355 (* the term is the result of a reduction; *)
356 (* so it is already unwinded. *)
357 reduce (0,[],[],body',[])
358 | C.Appl (C.CoFix (i,fl) :: tl) ->
359 let (_,_,body) = List.nth fl i in
361 let counter = ref (List.length fl) in
363 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
367 (* the term is the result of a reduction; *)
368 (* so it is already unwinded. *)
369 reduce (0,[],[],body',tl)
372 (match decofix (reduce (k,e,ens,term,[])) with
373 C.MutConstruct (_,_,j,_) ->
374 reduce (k, e, ens, (List.nth pl (j-1)), s)
375 | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
377 match CicEnvironment.get_obj mutind with
378 C.InductiveDefinition (tl,ingredients,r) ->
379 let (_,_,arity,_) = List.nth tl i in
381 | _ -> raise WrongUriToInductiveDefinition
384 let num_to_eat = r in
388 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
389 | _ -> raise (Impossible 5)
391 eat_first (num_to_eat,tl)
393 (* ts are already unwinded because they are a sublist of tl *)
394 reduce (k, e, ens, (List.nth pl (j-1)),(ts@s))
395 | C.Cast _ | C.Implicit ->
396 raise (Impossible 2) (* we don't trust our whd ;-) *)
398 let t' = unwind k e ens t in
399 if s = [] then t' else C.Appl (t'::s)
401 | (k, e, ens, (C.Fix (i,fl) as t), s) ->
402 let (_,recindex,_,body) = List.nth fl i in
405 Some (List.nth s recindex)
411 (match reduce (0,[],[],recparam,[]) with
412 (* match recparam with *)
414 | C.Appl ((C.MutConstruct _)::_) ->
417 let counter = ref (List.length fl) in
419 (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
423 reduce (k, e, ens, body', s) *)
425 let leng = List.length fl in
427 let unwind_fl (name,recindex,typ,body) =
428 (name,recindex,unwind k e ens typ,
429 unwind' leng k e ens body)
431 List.map unwind_fl fl
434 let counter = ref 0 in
435 let rec build_env e =
436 if !counter = leng then e
438 (incr counter ; build_env ((C.Fix (!counter -1, fl'))::e))
442 reduce (k+leng, new_env, ens, body, s)
444 let t' = unwind k e ens t in
445 if s = [] then t' else C.Appl (t'::s)
448 let t' = unwind k e ens t in
449 if s = [] then t' else C.Appl (t'::s)
451 | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
452 let t' = unwind k e ens t in
453 if s = [] then t' else C.Appl (t'::s)
454 and push_exp_named_subst k e ens =
457 | (uri,t)::tl -> push_exp_named_subst k e ((uri,unwind k e ens t)::ens) tl
462 let rec whd context t = reduce context (0, [], [], t, []);;
466 let res = whd context t in
467 let rescsc = CicReductionNaif.whd context t in
468 if not (CicReductionNaif.are_convertible context res rescsc) then
470 prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
472 prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
474 prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
476 CicReductionNaif.fdebug := 0 ;
477 let _ = CicReductionNaif.are_convertible context res rescsc in
486 (* t1, t2 must be well-typed *)
487 let are_convertible =
488 let module U = UriManager in
489 let rec aux context t1 t2 =
491 (* this trivial euristic cuts down the total time of about five times ;-) *)
492 (* this because most of the time t1 and t2 are "sintactically" the same *)
497 let module C = Cic in
499 (C.Rel n1, C.Rel n2) -> n1 = n2
500 | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
504 (fun (uri1,x) (uri2,y) b ->
505 U.eq uri1 uri2 && aux context x y && b
506 ) exp_named_subst1 exp_named_subst2 true
508 Invalid_argument _ -> false
510 | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
518 | Some t1',Some t2' -> aux context t1' t2'
520 | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
521 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
522 aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
523 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
524 aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
525 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
526 aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
527 | (C.Appl l1, C.Appl l2) ->
529 List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true
531 Invalid_argument _ -> false
533 | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
537 (fun (uri1,x) (uri2,y) b ->
538 U.eq uri1 uri2 && aux context x y && b
539 ) exp_named_subst1 exp_named_subst2 true
541 Invalid_argument _ -> false
543 | (C.MutInd (uri1,i1,exp_named_subst1),
544 C.MutInd (uri2,i2,exp_named_subst2)
546 U.eq uri1 uri2 && i1 = i2 &&
549 (fun (uri1,x) (uri2,y) b ->
550 U.eq uri1 uri2 && aux context x y && b
551 ) exp_named_subst1 exp_named_subst2 true
553 Invalid_argument _ -> false
555 | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
556 C.MutConstruct (uri2,i2,j2,exp_named_subst2)
558 U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
561 (fun (uri1,x) (uri2,y) b ->
562 U.eq uri1 uri2 && aux context x y && b
563 ) exp_named_subst1 exp_named_subst2 true
565 Invalid_argument _ -> false
567 | (C.MutCase (uri1,i1,outtype1,term1,pl1),
568 C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
569 U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 &&
570 aux context term1 term2 &&
571 List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true
572 | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
574 List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
578 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
579 b && recindex1 = recindex2 && aux context ty1 ty2 &&
580 aux (tys@context) bo1 bo2)
582 | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
584 List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
588 (fun (_,ty1,bo1) (_,ty2,bo2) b ->
589 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
591 | (C.Cast _, _) | (_, C.Cast _)
592 | (C.Implicit, _) | (_, C.Implicit) ->
593 raise (Impossible 3) (* we don't trust our whd ;-) *)
597 if aux2 t1 t2 then true
600 debug t1 [t2] "PREWHD";
601 let t1' = whd context t1
602 and t2' = whd context t2 in
603 debug t1' [t2'] "POSTWHD";