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_______________________________________________________________ *)
14 exception CircularDependency of string Lazy.t;;
15 exception ObjectNotFound of string Lazy.t;;
16 exception BadDependency of string Lazy.t;;
18 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
19 let set_typecheck_obj f =
29 let cache = NUri.UriHash.create 313;;
30 let frozen_list = ref [];;
32 exception Propagate of NUri.uri * exn;;
34 let get_checked_obj u =
35 if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
37 raise (CircularDependency (lazy (NUri.string_of_uri u)))
40 try NUri.UriHash.find cache u
43 let saved_frozen_list = !frozen_list in
46 try NCicLibrary.get_obj u
48 NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m)
50 frozen_list := (u,obj)::saved_frozen_list;
52 frozen_list := saved_frozen_list;
53 let obj = `WellTyped obj in
54 NUri.UriHash.add cache u obj;
58 frozen_list := saved_frozen_list;
60 | Propagate (u',_) as e' ->
61 frozen_list := saved_frozen_list;
62 let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
63 " depends (recursively) on " ^ NUri.string_of_uri u' ^
64 " which is not well-typed"))) in
65 NUri.UriHash.add cache u exn;
66 if saved_frozen_list = [] then
71 frozen_list := saved_frozen_list;
73 NUri.UriHash.add cache u exn;
74 if saved_frozen_list = [] then
77 raise (Propagate (u,e))
84 let get_checked_def = function
85 | NReference.Ref (_, uri, NReference.Def) ->
86 (match get_checked_obj uri with
87 | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
88 rlv,name,bo,ty,att,height
89 | _,_,_,_, NCic.Constant (_,_,None,_,_) ->
90 prerr_endline "get_checked_def on an axiom"; assert false
91 | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
92 | _ -> prerr_endline "get_checked_def on a non def"; assert false
95 let get_checked_indtys = function
96 | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
97 (match get_checked_obj uri with
98 | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
99 inductive,leftno,tys,att,n
100 | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
101 | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
104 let get_checked_fixes_or_cofixes = function
105 | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))->
106 (match get_checked_obj uri with
107 | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
109 | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
110 | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
113 let get_indty_leftno = function
114 | NReference.Ref (_, uri, NReference.Ind _)
115 | NReference.Ref (_, uri, NReference.Con _) ->
116 (match get_checked_obj uri with
117 | _,_,_,_, NCic.Inductive (_,left,_,_) -> left
118 | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false)
119 | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false
123 assert (!frozen_list = []);
124 NUri.UriHash.clear cache