(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
+module Ref = NReference
+
let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;
struct
(* precedence, skel1, skel2, term *)
type t = int * NCic.term * NCic.term * NCic.term
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module EOT : Set.OrderedType
with type t = int * NCic.term =
struct
type t = int * NCic.term
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module HintSet = Set.Make(HOT)
method uhint_db = db
method set_uhint_db v = {< db = v >}
method set_unifhint_status
- : 'status. #g_status as 'status -> 'self
+ : 'status. (#g_status as 'status) -> 'self
= fun o -> {< db = o#uhint_db >}
end
-let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
+let dummy =
+ let uri = NUri.uri_of_string "cic:/matita/dummy/dec.con" in
+ NCic.Const (Ref.reference_of_spec uri Ref.Decl);;
+
let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
let index_hint status context t1 t2 precedence =
in
let n1 =
NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri
- u1 (NReference.Def h1)) :: mk_rels (List.length ctx))
+ u1 (Ref.Def h1)) :: mk_rels (List.length ctx))
in
let n2 =
NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri
- u2 (NReference.Def h2)) :: mk_rels (List.length ctx))
+ u2 (Ref.Def h2)) :: mk_rels (List.length ctx))
in
[ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2]
end else []
rc
in
let rc =
- List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
+ List.sort (fun (x,_,_,_) (y,_,_,_) -> Stdlib.compare x y) rc
in
let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
end
;;
-let pp_hint t p =
- let context, t =
+let pp_hint _t _p =
+(* let context, t =
let rec aux ctx = function
| NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
| t -> ctx, t
in
let buff = Buffer.create 100 in
let fmt = Format.formatter_of_buffer buff in
-(*
F.fprintf "@[<hov>"
F.fprintf "@[<hov>"
(* pp_ctx [] context *)
edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
(HintSet.elements dataset);
);
- List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
- List.iter (fun x, y, l, _, _ ->
+ List.iter (fun (x, l) -> Pp.node x ~attrs:["label",l] fmt) !nodes;
+ List.iter (fun (x, y, _l, _, _) ->
Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
!edges;
edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
- List.iter (fun x, y, _, p, l -> pp_hint l p) !edges;
+ List.iter (fun (_x, _y, _, p, l) -> pp_hint l p) !edges;
;;