snapshot, almost working

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate_types.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.ml b/helm/ocaml/cic_disambiguation/disambiguate_types.ml
new file mode 100644 (file)
index 0000000..545099d
--- /dev/null
+++ b/helm/ocaml/cic_disambiguation/disambiguate_types.ml
@@ -0,0 +1,47 @@
+
+type domain_item =
+ | Id of string               (* literal *)
+ | Symbol of string * int     (* literal, instance num *)
+ | Num of int                 (* instance num *)
+
+module OrderedDomain =
+  struct
+    type t = domain_item
+    let compare = Pervasives.compare
+  end
+
+module Domain = Set.Make (OrderedDomain)
+module Environment = Map.Make (OrderedDomain)
+
+type codomain_item =
+  string *  (* description *)
+  (environment -> string -> Cic.term list -> Cic.term)
+    (* environment, literal number, arguments as needed *)
+
+and environment = codomain_item Environment.t
+
+module type Callbacks =
+  sig
+    val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
+    val interactive_user_uri_choice :
+      selection_mode:[`SINGLE | `MULTIPLE] ->
+      ?ok:string ->
+      ?enable_button_for_non_vars:bool ->
+      title:string -> msg:string -> id:string -> string list -> string list
+    val interactive_interpretation_choice :
+      (string * string) list list -> int
+    val input_or_locate_uri : title:string -> UriManager.uri
+  end
+
+let string_of_domain_item = function
+  | Id s -> Printf.sprintf "ID(%s)" s
+  | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
+  | Num i -> Printf.sprintf "NUM(instance %d)" i
+
+let string_of_domain dom =
+  let buf = Buffer.create 1024 in
+  Domain.iter
+    (fun item -> Buffer.add_string buf (string_of_domain_item item ^ "; "))
+    dom;
+  Buffer.contents buf
+