* http://helm.cs.unibo.it/
*)
-type main_position = [ `MainConclusion | `MainHypothesis ]
+let position_prefix = "http://www.cs.unibo.it/helm/schemas/schema-helm#"
+(* let position_prefix = "" *)
+
+let inconcl_pos = position_prefix ^ "InConclusion"
+let mainconcl_pos = position_prefix ^ "MainConclusion"
+let mainhyp_pos = position_prefix ^ "MainHypothesis"
+let inhyp_pos = position_prefix ^ "InHypothesis"
+let inbody_pos = position_prefix ^ "InBody"
+
+type main_position =
+ [ `MainConclusion of int option (* Pi depth *)
+ | `MainHypothesis of int option (* Pi depth *)
+ ]
type position =
[ main_position
type pi_depth = int
type metadata =
- [ `Sort of Cic.sort * main_position * pi_depth
- | `Rel of main_position * pi_depth
- | `Obj of string * position * pi_depth option
+ [ `Sort of Cic.sort * main_position
+ | `Rel of main_position
+ | `Obj of string * position
]
+type constr =
+ [ `Sort of Cic.sort * main_position list
+ | `Rel of main_position list
+ | `Obj of string * position list
+ ]
+
+let constr_of_metadata: metadata -> constr = function
+ | `Sort (sort, pos) -> `Sort (sort, [pos])
+ | `Rel pos -> `Rel [pos]
+ | `Obj (uri, pos) -> `Obj (uri, [pos])
+
let sort_tbl = "refSort"
let rel_tbl = "refRel"
let obj_tbl = "refObj"