Initial revision

[helm.git] / helm / interface / cicFindParameters.ml

diff --git a/helm/interface/cicFindParameters.ml b/helm/interface/cicFindParameters.ml
new file mode 100644 (file)
index 0000000..607dd52
--- /dev/null
+++ b/helm/interface/cicFindParameters.ml
@@ -0,0 +1,137 @@
+exception WrongUriToConstant;;
+exception WrongUriToInductiveDefinition;;
+exception CircularDependency of string;;
+
+module OrderedUris =
+ struct
+  type t = UriManager.uri
+  let compare (s1 : t) (s2 : t) =
+   (* library function for = *)
+   compare s1 s2
+   (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*)
+ end
+;;
+
+let filename_of_uri uri =
+ let uri' = UriManager.string_of_uri uri in
+  let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in
+   fn ^ ".xml"
+;;
+
+(* quite inefficient coding of a set of strings: the only operations  *)
+(* performed are mem O(log n), and union O(n * log n?)                *)
+(* Perhaps a better implementation would be an array of bits or a map *)
+(* from uri to booleans                                               *)
+module SetOfUris = Set.Make(OrderedUris);;
+
+let (@@) = SetOfUris.union;;
+
+let rec parameters_of te ty pparams=
+ let module S = SetOfUris in
+ let module C = Cic in
+   let rec aux =
+    function
+       C.Rel _ -> S.empty
+     | C.Var uri -> S.singleton uri
+     | C.Meta _ -> S.empty
+     | C.Sort _ -> S.empty
+     | C.Implicit -> S.empty
+     | C.Cast (te, ty) -> aux te @@ aux ty
+     | C.Prod (_, s, t) -> aux s @@ aux t
+     | C.Lambda (_, s, t) -> aux s @@ aux t
+     | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
+     | C.Const (uri,_) ->
+        (* the parameters could be not exact but only possible *)
+        fix_params uri (Some (filename_of_uri uri)) ;
+        (* now the parameters are surely possible *)
+        (match CicCache.get_obj uri with
+            C.Definition (_, _, _, params) ->
+              List.fold_right
+               (fun (_,l) i ->
+                 List.fold_right
+                  (fun x i -> S.singleton x @@ i) l i
+               ) params S.empty
+          | C.Axiom (_, _, params) ->
+             List.fold_right
+              (fun (_,l) i ->
+                List.fold_right
+                 (fun x i -> S.singleton x @@ i) l i
+              ) params S.empty
+          | C.CurrentProof _ -> S.empty (*CSC wrong *)
+          | _ -> raise WrongUriToConstant
+        )
+     | C.Abst _ -> S.empty
+     | C.MutInd (uri,_,_) ->
+        (match CicCache.get_obj uri with
+            C.InductiveDefinition (_, params, _) ->
+             List.fold_right
+              (fun (_,l) i ->
+                List.fold_right
+                 (fun x i -> S.singleton x @@ i) l i
+              ) params S.empty
+          | _ -> raise WrongUriToInductiveDefinition
+        )
+     | C.MutConstruct (uri,_,_,_) ->
+        (match CicCache.get_obj uri with
+            C.InductiveDefinition (_, params, _) ->
+             List.fold_right
+              (fun (_,l) i ->
+                List.fold_right
+                 (fun x i -> S.singleton x @@ i) l i
+              ) params S.empty
+          | _ -> raise WrongUriToInductiveDefinition
+        )
+     | C.MutCase (uri,_,_,outtype,term,patterns) ->
+        (*CSC cosa basta? Ci vuole anche uri? *)
+        (match CicCache.get_obj uri with
+            C.InductiveDefinition (_, params, _) ->
+            List.fold_right
+             (fun (_,l) i ->
+               List.fold_right
+                (fun x i -> S.singleton x @@ i) l i
+             ) params S.empty
+          | _ -> raise WrongUriToInductiveDefinition
+        ) @@ aux outtype @@ aux term @@
+         List.fold_right (fun x i -> aux x @@ i) patterns S.empty
+     | C.Fix (_,fl) ->
+        List.fold_right
+         (fun (_,_,ty,bo) i  -> aux ty @@ aux bo @@ i)
+         fl S.empty
+     | C.CoFix (_,fl) ->
+        List.fold_right
+         (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
+         fl S.empty
+ in
+  let actual_params = aux te @@ aux ty in
+   (* sort_actual_params wants in input the ordered list of possible params *)
+   let rec sort_actual_params2 =
+    function
+       [] -> []
+     | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
+     | _::tl -> sort_actual_params2 tl
+   in
+    let rec sort_actual_params =
+     function
+        [] -> []
+      | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
+    in
+     sort_actual_params pparams
+
+and fix_params uri filename =
+ let module C = Cic in
+  let (ann, _, deann) = CicCache.get_annobj uri in
+   match ann, deann with
+      (C.ADefinition (xid, ann, id, te, ty, C.Possible pparams),
+       C.Definition (id', te', ty', _)) ->
+        (* let's freeze the object to avoid circular dependencies *)
+        CicCache.change_obj uri None ;
+        let real_params = parameters_of te' ty' pparams in
+         let fixed =
+          C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
+         in
+          Xml.pp (Cic2Xml.pp fixed uri) filename ;
+          (* unfreeze and fix the object *)
+          CicCache.change_obj uri
+           (Some (C.Definition (id', te', ty', real_params)))
+    | _ -> ()
+;;