1 exception WrongUriToConstant;;
2 exception WrongUriToInductiveDefinition;;
3 exception CircularDependency of string;;
7 type t = UriManager.uri
8 let compare (s1 : t) (s2 : t) =
9 (* library function for = *)
11 (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*)
15 let filename_of_uri uri =
16 let uri' = UriManager.string_of_uri uri in
17 let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in
21 (* quite inefficient coding of a set of strings: the only operations *)
22 (* performed are mem O(log n), and union O(n * log n?) *)
23 (* Perhaps a better implementation would be an array of bits or a map *)
24 (* from uri to booleans *)
25 module SetOfUris = Set.Make(OrderedUris);;
27 let (@@) = SetOfUris.union;;
29 let rec parameters_of te ty pparams=
30 let module S = SetOfUris in
35 | C.Var uri -> S.singleton uri
38 | C.Implicit -> S.empty
39 | C.Cast (te, ty) -> aux te @@ aux ty
40 | C.Prod (_, s, t) -> aux s @@ aux t
41 | C.Lambda (_, s, t) -> aux s @@ aux t
42 | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
44 (* the parameters could be not exact but only possible *)
45 fix_params uri (Some (filename_of_uri uri)) ;
46 (* now the parameters are surely possible *)
47 (match CicCache.get_obj uri with
48 C.Definition (_, _, _, params) ->
52 (fun x i -> S.singleton x @@ i) l i
54 | C.Axiom (_, _, params) ->
58 (fun x i -> S.singleton x @@ i) l i
60 | C.CurrentProof _ -> S.empty (*CSC wrong *)
61 | _ -> raise WrongUriToConstant
64 | C.MutInd (uri,_,_) ->
65 (match CicCache.get_obj uri with
66 C.InductiveDefinition (_, params, _) ->
70 (fun x i -> S.singleton x @@ i) l i
72 | _ -> raise WrongUriToInductiveDefinition
74 | C.MutConstruct (uri,_,_,_) ->
75 (match CicCache.get_obj uri with
76 C.InductiveDefinition (_, params, _) ->
80 (fun x i -> S.singleton x @@ i) l i
82 | _ -> raise WrongUriToInductiveDefinition
84 | C.MutCase (uri,_,_,outtype,term,patterns) ->
85 (*CSC cosa basta? Ci vuole anche uri? *)
86 (match CicCache.get_obj uri with
87 C.InductiveDefinition (_, params, _) ->
91 (fun x i -> S.singleton x @@ i) l i
93 | _ -> raise WrongUriToInductiveDefinition
94 ) @@ aux outtype @@ aux term @@
95 List.fold_right (fun x i -> aux x @@ i) patterns S.empty
98 (fun (_,_,ty,bo) i -> aux ty @@ aux bo @@ i)
102 (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
105 let actual_params = aux te @@ aux ty in
106 (* sort_actual_params wants in input the ordered list of possible params *)
107 let rec sort_actual_params2 =
110 | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
111 | _::tl -> sort_actual_params2 tl
113 let rec sort_actual_params =
116 | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
118 sort_actual_params pparams
120 and fix_params uri filename =
121 let module C = Cic in
122 let (ann, _, deann) = CicCache.get_annobj uri in
123 match ann, deann with
124 (C.ADefinition (xid, ann, id, te, ty, C.Possible pparams),
125 C.Definition (id', te', ty', _)) ->
126 (* let's freeze the object to avoid circular dependencies *)
127 CicCache.change_obj uri None ;
128 let real_params = parameters_of te' ty' pparams in
130 C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
132 Xml.pp (Cic2Xml.pp fixed uri) filename ;
133 (* unfreeze and fix the object *)
134 CicCache.change_obj uri
135 (Some (C.Definition (id', te', ty', real_params)))