* http://helm.cs.unibo.it/
*)
-type main_position = [ `MainConclusion | `MainHypothesis ]
+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"