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;;
23 let cache = NUri.UriHash.create 313;;
24 let history = ref [];;
25 let frozen_list = ref [];;
27 let get_obj = ref (fun _ -> assert false);;
28 let set_get_obj f = get_obj := f;;
34 let rec ppsort f = function
35 | C.Prop -> F.fprintf f "Prop"
36 | (C.Type []) -> F.fprintf f "Type0"
37 | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
38 | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
39 | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
42 ppsort f ((C.Type [List.hd l]));
43 List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
47 let string_of_univ u =
48 let b = Buffer.create 100 in
49 let f = Format.formatter_of_buffer b in
50 ppsort f (NCic.Type u);
51 Format.fprintf f "@?";
55 let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
57 let max (l1:NCic.universe) (l2:NCic.universe) =
60 let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
61 x :: HExtlib.list_uniq ~eq:eq_univ
62 (List.sort (fun (b1,u1) (b2,u2) ->
63 let res = compare b1 b2 in
64 if res = 0 then NUri.compare u1 u2 else res)
69 | ((`Type|`Succ), _)::_ -> l1
70 | (`CProp, u)::tl -> (`Type, u)::tl
73 let lt_constraints = ref [] (* a,b := a < b *)
75 let rec lt_path_uri avoid a b =
80 (not (List.exists (NUri.eq x) avoid) &&
81 lt_path_uri (x::avoid) a x))
85 let lt_path a b = lt_path_uri [b] a b;;
89 | [(`Type|`CProp) as b1, u1], [(`Type|`CProp) as b2, u2] ->
90 b1 = b2 && NUri.eq u1 u2
91 | _, [(`Type|`CProp),_]
92 | [(`Type|`CProp),_],_ -> false
95 (lazy "trying to check if two inferred universes are equal"))
98 let universe_leq a b =
100 | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
101 | l, [((`Type|`CProp),b)] ->
104 | `Succ,a -> lt_path a b
105 | _, a -> NUri.eq a b || lt_path a b) l
106 | _, ([] | [`Succ,_] | _::_::_) ->
107 raise (BadConstraint (lazy (
108 "trying to check if "^string_of_univ a^
109 " is leq than the inferred universe " ^ string_of_univ b)))
112 let are_sorts_convertible ~test_eq_only s1 s2 =
114 | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
115 | C.Type a, C.Type b -> universe_eq a b
116 | C.Prop,C.Type _ -> (not test_eq_only)
117 | C.Prop, C.Prop -> true
121 let pp_constraint x y =
122 NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
125 let pp_constraints () =
126 String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y) !lt_constraints)
129 let universes = ref [];;
131 let get_universes () =
132 List.map (fun x -> [`Type,x]) !universes @
133 List.map (fun x -> [`CProp,x]) !universes
138 | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !universes
142 exception UntypableSort of string Lazy.t
143 exception AssertFailure of string Lazy.t
145 let typeof_sort = function
146 | C.Type ([(`Type|`CProp),u] as univ) ->
147 if is_declared univ then (C.Type [`Succ, u])
149 raise (UntypableSort (lazy ("undeclared universe " ^
150 NUri.string_of_uri u ^ "\ndeclared ones are: " ^
151 String.concat ", " (List.map NUri.string_of_uri !universes)
154 raise (AssertFailure (lazy (
155 "Cannot type an inferred type: "^ string_of_univ t)))
156 | C.Prop -> (C.Type type0)
159 let add_lt_constraint a b =
161 | [`Type,a2],[`Type,b2] ->
162 if not (lt_path_uri [] a2 b2) then (
163 if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
164 (raise(BadConstraint(lazy("universe inconsistency adding "^
166 ^ " to:\n" ^ pp_constraints ()))));
167 universes := a2 :: b2 ::
168 List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
169 lt_constraints := (a2,b2) :: !lt_constraints);
170 history := (`Constr (a,b))::!history;
171 | _ -> raise (BadConstraint
172 (lazy "trying to add a constraint on an inferred universe"))
177 | [(`Type|`CProp),_] -> Some l
179 let bigger_than acc (_s1,n1) =
180 List.filter (fun x -> lt_path_uri [] n1 x || NUri.eq n1 x) acc
182 let solutions = List.fold_left bigger_than !universes l in
183 let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in
184 let rec aux = function
187 if List.exists (fun x -> lt_path_uri [] x u) solutions then aux tl
193 let allowed_sort_elimination s1 s2 =
195 | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])
196 | C.Type _, C.Type ((`CProp,_)::_)
198 | C.Prop, C.Prop -> `Yes
200 | C.Type ((`CProp,_)::_), C.Type (((`Type|`Succ),_)::_ | [])
201 | C.Prop, C.Type _ -> `UnitOnly
204 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
205 let set_typecheck_obj f =
215 let invalidate_item item =
218 | `Obj (u1,_), `Obj (u2,_) -> NUri.eq u1 u2
219 | `Constr _, `Constr _ -> a=b (* MAKE EFFICIENT *)
222 let rec aux to_be_deleted =
225 | item'::tl when item_eq item item' -> item'::to_be_deleted,tl
226 | item'::tl -> aux (item'::to_be_deleted) tl
228 let to_be_deleted,h = aux [] !history in
232 | `Obj (uri,_) -> NUri.UriHash.remove cache uri
233 | `Constr ([_,u1],[_,u2]) as c ->
235 if not(List.mem c !history) then
236 lt_constraints := List.filter ((<>) w) !lt_constraints;
237 | `Constr _ -> assert false
241 exception Propagate of NUri.uri * exn;;
249 let check_and_add_obj ((u,_,_,_,_) as obj) =
250 let saved_frozen_list = !frozen_list in
252 frozen_list := (u,obj)::saved_frozen_list;
254 frozen_list := saved_frozen_list;
255 let obj' = `WellTyped obj in
256 NUri.UriHash.add cache u obj';
257 history := (`Obj (u,obj))::!history;
261 frozen_list := saved_frozen_list;
263 | Propagate (u',old_exn) as e' ->
264 frozen_list := saved_frozen_list;
265 let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
266 " depends (recursively) on " ^ NUri.string_of_uri u' ^
267 " which is not well-typed"),
268 match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
269 NUri.UriHash.add cache u exn;
270 history := (`Obj (u,obj))::!history;
271 if saved_frozen_list = [] then
276 frozen_list := saved_frozen_list;
278 NUri.UriHash.add cache u exn;
279 history := (`Obj (u,obj))::!history;
280 if saved_frozen_list = [] then
283 raise (Propagate (u,e))
286 let get_checked_obj u =
287 if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
289 raise (CircularDependency (lazy (NUri.string_of_uri u)))
291 try NUri.UriHash.find cache u
292 with Not_found -> check_and_add_obj (!get_obj u)
295 let get_checked_obj u = to_exn get_checked_obj u;;
297 let check_and_add_obj ((u,_,_,_,_) as obj) =
298 if NUri.UriHash.mem cache u then
299 raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
301 ignore (to_exn check_and_add_obj obj)
304 let get_checked_decl = function
305 | Ref.Ref (uri, Ref.Decl) ->
306 (match get_checked_obj uri with
307 | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
308 rlv,name,ty,att,height
309 | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
310 prerr_endline "get_checked_decl on a definition"; assert false
311 | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
312 | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
315 let get_checked_def = function
316 | Ref.Ref (uri, Ref.Def _) ->
317 (match get_checked_obj uri with
318 | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
319 rlv,name,bo,ty,att,height
320 | _,_,_,_, C.Constant (_,_,None,_,_) ->
321 prerr_endline "get_checked_def on an axiom"; assert false
322 | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
323 | _ -> prerr_endline "get_checked_def on a non def"; assert false
326 let get_checked_indtys = function
327 | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
328 (match get_checked_obj uri with
329 | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
330 inductive,leftno,tys,att,n
331 | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
332 | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
335 let get_checked_fixes_or_cofixes = function
336 | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
337 (match get_checked_obj uri with
338 | _,height,_,_, C.Fixpoint (_,funcs,att) ->
340 | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
341 | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
344 let get_relevance (Ref.Ref (_, infos) as r) =
346 Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
347 | Ref.Decl -> let res,_,_,_,_ = get_checked_decl r in res
349 let _,_,tl,_,n = get_checked_indtys r in
350 let res,_,_,_ = List.nth tl n in
353 let _,_,tl,_,n = get_checked_indtys r in
354 let _,_,_,cl = List.nth tl n in
355 let res,_,_ = List.nth cl (i - 1) in
357 | Ref.Fix (fixno,_,_)
359 let fl,_,_ = get_checked_fixes_or_cofixes r in
360 let res,_,_,_,_ = List.nth fl fixno in
366 assert (!frozen_list = []);
367 NUri.UriHash.clear cache