added a lot of notation: arithmetic operators, relational operators, ...

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

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index aa203f8be3c4b9e6ac01c0673d8cd9c29cd364c4..c74566f20861c4e030621d6b49c0cf642cb1726b 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
@@ -41,6 +41,24 @@ let add_symbol_choice symbol codomain_item =
   in
   Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices)
 
+let add_binary_op symbol dsc appl_head =
+  add_symbol_choice symbol
+    (dsc,
+      (fun env _ args ->
+        let t1, t2 =
+          match args with
+          | [t1; t2] -> t1, t2
+          | _ -> raise Invalid_choice
+        in
+        Cic.Appl [ appl_head; t1; t2 ]))
+
+let add_unary_op symbol dsc appl_head =
+  add_symbol_choice symbol
+    (dsc,
+      (fun env _ args ->
+        let t = match args with [t] -> t | _ -> raise Invalid_choice in
+        Cic.Appl [ appl_head; t ]))
+
 let add_num_choice choice = num_choices := choice :: !num_choices
 
 let lookup_symbol_choices symbol =
@@ -63,3 +81,13 @@ let lookup_num_by_dsc dsc =
     List.find (has_description dsc) !num_choices
   with Not_found -> raise (Choice_not_found ("Num with dsc " ^  dsc))
 
+  (** initial table contents *)
+
+let _ =
+  let uri s = UriManager.uri_of_string s in
+  let const s = Cic.Const (uri s, []) in
+  let mutind s = Cic.MutInd (uri s, 0, []) in
+  add_binary_op "exists" "exists" (mutind "cic:/Coq/Init/Logic/ex.ind");
+  add_binary_op "exists" "exists over terms with sort Type"
+    (mutind "cic:/Coq/Init/Logic_Type/exT.ind");
+