2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
15 module Ref = NReference
17 exception CircularDependency of string Lazy.t;;
18 exception ObjectNotFound of string Lazy.t;;
19 exception BadDependency of string Lazy.t * exn;;
20 exception BadConstraint of string Lazy.t;;
21 exception AlreadyDefined of string Lazy.t;;
24 [ `Obj of NUri.uri * NCic.obj
25 | `Constr of NCic.universe * NCic.universe ]
29 [ `WellTyped of NCic.obj
34 cache : obj_exn NUri.UriHash.t;
35 history : item list ref;
36 frozen_list : (NUri.uri * NCic.obj) list ref;
37 lt_constraints : (NUri.uri * NUri.uri) list ref;
38 universes : NUri.uri list ref
47 class virtual status uid =
49 inherit NCic.status uid
52 cache = NUri.UriHash.create 313;
55 lt_constraints = ref []; (* a,b := a < b *)
61 method set_env_db v = {< db = v >}
62 method set_env_status : 's.#g_status as 's -> 'self
63 = fun o -> {< db = o#env_db >}
67 let get_obj = ref (fun _ _ -> assert false);;
69 let set_get_obj = (:=) get_obj;;
71 let typechk_already_set = ref false;;
72 let typecheck_obj = ref (fun _ _ -> assert false);;
74 let set_typecheck_obj f =
75 if !typechk_already_set then
80 typechk_already_set := true
85 let rec ppsort f = function
86 | C.Prop -> F.fprintf f "Prop"
87 | (C.Type []) -> F.fprintf f "Type0"
88 | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
89 | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
90 | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
93 ppsort f ((C.Type [List.hd l]));
94 List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
98 let string_of_univ u =
99 let b = Buffer.create 100 in
100 let f = Format.formatter_of_buffer b in
101 ppsort f (NCic.Type u);
102 Format.fprintf f "@?";
106 let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
108 let max (l1:NCic.universe) (l2:NCic.universe) =
111 let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
112 x :: HExtlib.list_uniq ~eq:eq_univ
113 (List.sort (fun (b1,u1) (b2,u2) ->
114 let res = compare b1 b2 in
115 if res = 0 then NUri.compare u1 u2 else res)
120 | ((`Type|`Succ), _)::_ -> l1
121 | (`CProp, u)::tl -> (`Type, u)::tl
124 let rec lt_path_uri s avoid a b =
129 (not (List.exists (NUri.eq x) avoid) &&
130 lt_path_uri s (x::avoid) a x))
131 ) !(s#env_db.lt_constraints)
134 let lt_path s a b = lt_path_uri s [b] a b;;
136 let universe_eq a b =
138 | [(`Type|`CProp) as b1, u1], [(`Type|`CProp) as b2, u2] ->
139 b1 = b2 && NUri.eq u1 u2
140 | _, [(`Type|`CProp),_]
141 | [(`Type|`CProp),_],_ -> false
144 (lazy "trying to check if two inferred universes are equal"))
147 let universe_leq s a b =
149 | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
150 | l, [((`Type|`CProp),b)] ->
153 | `Succ,a -> lt_path s a b
154 | _, a -> NUri.eq a b || lt_path s a b) l
155 | _, ([] | [`Succ,_] | _::_::_) ->
156 raise (BadConstraint (lazy (
157 "trying to check if "^string_of_univ a^
158 " is leq than the inferred universe " ^ string_of_univ b)))
161 let are_sorts_convertible st ~test_eq_only s1 s2 =
163 | C.Type a, C.Type b when not test_eq_only -> universe_leq st a b
164 | C.Type a, C.Type b -> universe_eq a b
165 | C.Prop,C.Type _ -> (not test_eq_only)
166 | C.Prop, C.Prop -> true
170 let pp_constraint x y =
171 NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
174 let pp_constraints s =
175 String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y)
176 !(s#env_db.lt_constraints))
179 let get_universes s =
180 List.map (fun x -> [`Type,x]) !(s#env_db.universes) @
181 List.map (fun x -> [`CProp,x]) !(s#env_db.universes)
184 let is_declared s u =
186 | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !(s#env_db.universes)
190 exception UntypableSort of string Lazy.t
191 exception AssertFailure of string Lazy.t
193 let typeof_sort s = function
194 | C.Type ([(`Type|`CProp),u] as univ) ->
195 if is_declared s univ then (C.Type [`Succ, u])
197 let universes = !(s#env_db.universes) in
198 raise (UntypableSort (lazy ("undeclared universe " ^
199 NUri.string_of_uri u ^ "\ndeclared ones are: " ^
200 String.concat ", " (List.map NUri.string_of_uri universes)
203 raise (AssertFailure (lazy (
204 "Cannot type an inferred type: "^ string_of_univ t)))
205 | C.Prop -> (C.Type [])
208 let add_lt_constraint s a b =
210 | [`Type,a2],[`Type,b2] ->
211 if not (lt_path_uri s [] a2 b2) then (
212 if lt_path_uri s [] b2 a2 || NUri.eq a2 b2 then
213 (raise(BadConstraint(lazy("universe inconsistency adding "^
215 ^ " to:\n" ^ pp_constraints s))));
216 s#env_db.universes := a2 :: b2 ::
217 List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2))
218 !(s#env_db.universes);
219 s#env_db.lt_constraints := (a2,b2) :: !(s#env_db.lt_constraints));
220 s#env_db.history := (`Constr (a,b))::!(s#env_db.history);
221 | _ -> raise (BadConstraint
222 (lazy "trying to add a constraint on an inferred universe"));
225 let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
229 | [(`Type|`CProp),_] -> Some l
231 let bigger_than acc (s1,n1) =
233 (fun x -> lt_path_uri s [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc
235 let solutions = List.fold_left bigger_than !(s#env_db.universes) l in
236 let rec aux = function
239 if List.exists (fun x -> lt_path_uri s [] x u) solutions then aux tl
245 let sup s l = sup s (family_of l) l;;
247 let inf s ~strict fam l =
249 | [(`Type|`CProp),_] -> Some l
252 let smaller_than acc (_s1,n1) =
254 (fun x -> lt_path_uri s [] x n1 || (not strict && NUri.eq n1 x)) acc
256 let solutions = List.fold_left smaller_than !(s#env_db.universes) l in
257 let rec aux = function
260 if List.exists (lt_path_uri s [] u) solutions then aux tl
266 let inf s ~strict l = inf s ~strict (family_of l) l;;
268 let rec universe_lt s a b =
270 | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
271 | l, ([((`Type|`CProp),b)] as orig_b) ->
275 (match sup s [a] with
277 | Some x -> universe_lt s x orig_b)
278 | _, a -> lt_path s a b) l
279 | _, ([] | [`Succ,_] | _::_::_) ->
280 raise (BadConstraint (lazy (
281 "trying to check if "^string_of_univ a^
282 " is lt than the inferred universe " ^ string_of_univ b)))
286 let allowed_sort_elimination s1 s2 =
288 | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])
289 | C.Type _, C.Type ((`CProp,_)::_)
291 | C.Prop, C.Prop -> `Yes
293 | C.Type ((`CProp,_)::_), C.Type (((`Type|`Succ),_)::_ | [])
294 | C.Prop, C.Type _ -> `UnitOnly
297 (* CSC: old code that performs recursive invalidation; to be removed
298 * once we understand what we really want. Once we removed it, we can
299 * also remove the !history
300 let invalidate_item item =
303 | `Obj (u1,_), `Obj (u2,_) -> NUri.eq u1 u2
304 | `Constr _, `Constr _ -> a=b (* MAKE EFFICIENT *)
307 let rec aux to_be_deleted =
310 | item'::tl when item_eq item item' -> item'::to_be_deleted,tl
311 | item'::tl -> aux (item'::to_be_deleted) tl
313 let to_be_deleted,h = aux [] !history in
317 | `Obj (uri,_) -> NUri.UriHash.remove cache uri
318 | `Constr ([_,u1],[_,u2]) as c ->
320 if not(List.mem c !history) then
321 lt_constraints := List.filter ((<>) w) !lt_constraints;
322 | `Constr _ -> assert false
327 let invalidate_item s o =
329 | `Obj (uri,_) -> NUri.UriHash.remove s#env_db.cache uri
330 | `Constr ([_,u1],[_,u2]) ->
332 s#env_db.lt_constraints := List.filter ((<>) w) !(s#env_db.lt_constraints);
333 | `Constr _ -> assert false;
336 exception Propagate of NUri.uri * exn;;
344 let check_and_add_obj (status:#status) ((u,_,_,_,_) as obj) =
345 let saved_frozen_list = !(status#env_db.frozen_list) in
347 status#env_db.frozen_list := (u,obj)::saved_frozen_list;
348 HLog.warn ("Typechecking of " ^ NUri.string_of_uri u);
349 !typecheck_obj (status :> status) obj;
350 status#env_db.frozen_list := saved_frozen_list;
351 let obj' = `WellTyped obj in
352 NUri.UriHash.add status#env_db.cache u obj';
353 status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
357 status#env_db.frozen_list := saved_frozen_list;
359 | Propagate (u',old_exn) as e' ->
360 status#env_db.frozen_list := saved_frozen_list;
361 let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
362 " depends (recursively) on " ^ NUri.string_of_uri u' ^
363 " which is not well-typed"),
364 match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
365 NUri.UriHash.add status#env_db.cache u exn;
366 status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
367 if saved_frozen_list = [] then
372 status#env_db.frozen_list := saved_frozen_list;
374 NUri.UriHash.add status#env_db.cache u exn;
375 status#env_db.history := (`Obj (u,obj))::!(status#env_db.history);
376 if saved_frozen_list = [] then
379 raise (Propagate (u,e))
382 let get_checked_obj (status:#status) u =
383 if List.exists (fun (k,_) -> NUri.eq u k) !(status#env_db.frozen_list)
385 raise (CircularDependency (lazy (NUri.string_of_uri u)))
387 try NUri.UriHash.find status#env_db.cache u
389 (* XXX: to be checked carefully *)
390 check_and_add_obj status (!get_obj (status :> status) u)
393 let get_checked_obj status u = to_exn (get_checked_obj status) u;;
395 let check_and_add_obj status ((u,_,_,_,_) as obj) =
396 if NUri.UriHash.mem status#env_db.cache u then
397 raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
399 ignore (to_exn (check_and_add_obj status) obj)
402 let get_checked_decl status = function
403 | Ref.Ref (uri, Ref.Decl) ->
404 (match get_checked_obj status uri with
405 | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
406 rlv,name,ty,att,height
407 | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
408 prerr_endline "get_checked_decl on a definition"; assert false
409 | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
410 | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
413 let get_checked_def status = function
414 | Ref.Ref (uri, Ref.Def _) ->
415 (match get_checked_obj status uri with
416 | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
417 rlv,name,bo,ty,att,height
418 | _,_,_,_, C.Constant (_,_,None,_,_) ->
419 prerr_endline "get_checked_def on an axiom"; assert false
420 | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
421 | _ -> prerr_endline "get_checked_def on a non def"; assert false
424 let get_checked_indtys status = function
425 | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
426 (match get_checked_obj status uri with
427 | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
428 inductive,leftno,tys,att,n
429 | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
430 | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
433 let get_checked_fixes_or_cofixes status = function
434 | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
435 (match get_checked_obj status uri with
436 | _,height,_,_, C.Fixpoint (_,funcs,att) ->
438 | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
439 | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
442 let get_relevance status (Ref.Ref (_, infos) as r) =
444 Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def status r in res
445 | Ref.Decl -> let res,_,_,_,_ = get_checked_decl status r in res
447 let _,_,tl,_,n = get_checked_indtys status r in
448 let res,_,_,_ = List.nth tl n in
451 let _,_,tl,_,n = get_checked_indtys status r in
452 let _,_,_,cl = List.nth tl n in
453 let res,_,_ = List.nth cl (i - 1) in
455 | Ref.Fix (fixno,_,_)
457 let fl,_,_ = get_checked_fixes_or_cofixes status r in
458 let res,_,_,_,_ = List.nth fl fixno in
464 assert (!(s#env_db.frozen_list) = []);
465 NUri.UriHash.clear s#env_db.cache