mathql_generator: new constraint format (more type safe)

[helm.git] / helm / ocaml / mathql_generator / mQueryLevels2.ml

diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.ml b/helm/ocaml/mathql_generator/mQueryLevels2.ml
index d9e9e5359276095df3633f055abe48c507daaa6b..60633f897e722f988990d7157506ce178b052e34 100644 (file)
--- a/helm/ocaml/mathql_generator/mQueryLevels2.ml
+++ b/helm/ocaml/mathql_generator/mQueryLevels2.ml
@@ -34,6 +34,9 @@
 (*                                                                            *)
 (******************************************************************************)
 
+module T = MQGTypes
+module U = MQGUtil
+
 type classification =
    Backbone of int
  | Branch of int
@@ -50,16 +53,20 @@ let soften_classification =
 
 let (!!) =
  function
-    Backbone n ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
-  | Branch n ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
-  | InConclusion ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
-  | InHypothesis ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
+    Backbone n -> `MainConclusion (Some n)
+  | Branch n -> `MainHypothesis (Some n)
+  | _        -> assert false
+;;
+
+let (!!!) =
+ function
+    Backbone n -> `MainConclusion (Some n)
+  | Branch n -> `MainHypothesis (Some n)
+  | InConclusion -> `InConclusion
+  | InHypothesis -> `InHypothesis
 ;;
 
+
 let (@@) (l1,l2,l3) (l1',l2',l3') =
  let merge l1 l2 =
   List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
@@ -73,28 +80,24 @@ let get_constraints term =
   let rec process_type_aux kind =
    function
       C.Var (uri,expl_named_subst) ->
-       let kind',depth = !!kind in
-        ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
-          (process_type_aux_expl_named_subst kind expl_named_subst)
+       ([!!!kind, UriManager.string_of_uri uri],[],[]) @@
+         (process_type_aux_expl_named_subst kind expl_named_subst)
     | C.Rel _ ->
-       let kind',depth = !!kind in
-        (match depth with
-            None -> [],[],[]
-          | Some d -> [],[kind',Some d],[])
+       (match kind with
+         | InConclusion 
+         | InHypothesis -> [],[],[] 
+         | _            -> [],[!!kind],[])
     | C.Sort s ->
        (match kind with
            Backbone _
          | Branch _ ->
             let s' =
              match s with
-                Cic.Prop -> "Prop"
-              | Cic.Set -> "Set"
-              | Cic.Type -> "Type"
+                Cic.Prop -> T.Prop
+              | Cic.Set -> T.Set
+              | Cic.Type -> T.Type
             in
-             let kind',depth = !!kind in
-              (match depth with
-                  None -> assert false
-                | Some d -> [],[],[kind',Some d,s'])
+            [],[],[!!kind,s']
          | _ -> [],[],[])
     | C.Meta _
     | C.Implicit -> assert false
@@ -124,18 +127,15 @@ let get_constraints term =
         List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
     | C.Appl _ -> assert false
     | C.Const (uri,_) ->
-       let kind',depth = !!kind in
-        [UriManager.string_of_uri uri,kind',depth],[],[]
+       [!!!kind, UriManager.string_of_uri uri],[],[]
     | C.MutInd (uri,typeno,expl_named_subst) ->
-       let kind',depth = !!kind in
-       ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
-          ")", kind', depth],[],[]) @@
+       ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ 
+        string_of_int (typeno + 1) ^ ")"],[],[]) @@
          (process_type_aux_expl_named_subst kind expl_named_subst)
     | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
-       let kind',depth = !!kind in
-        ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
-          "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
-          (process_type_aux_expl_named_subst kind expl_named_subst)
+        ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
+        string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[])
+         @@ (process_type_aux_expl_named_subst kind expl_named_subst)
     | C.MutCase (_,_,_,term,patterns) ->
        (* outtype ignored *)
        let kind' = soften_classification kind in
@@ -173,25 +173,17 @@ in
 let get_constraints term =
  let res = get_constraints term in
  let (objs,rels,sorts) = res in
+  let text_of_pos p =
+    U.text_of_position p ^ " " ^ U.text_of_depth p "NULL"
+  in
   prerr_endline "Constraints on objs:" ;
   List.iter
-   (function (s1,s2,n) ->
-     prerr_endline
-      (s1 ^ " " ^ s2 ^ " " ^
-        match n with None -> "NULL" | Some n -> string_of_int n)
-   ) objs ;
+   (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ;
   prerr_endline "Constraints on Rels:" ;
-  List.iter
-   (function (s,n) ->
-     prerr_endline
-      (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
-   ) rels ;
+  List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ;
   prerr_endline "Constraints on Sorts:" ;
   List.iter
-   (function (s1,n,s2) ->
-     prerr_endline
-      (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
-        " " ^ s2)
+   (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s)
    ) sorts ;
   res
 ;;