(* *)
(******************************************************************************)
+module T = MQGTypes
+module U = MQGUtil
+
type classification =
Backbone of int
| Branch of int
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
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
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
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
;;