X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateChoices.ml;h=368bc2f45f9a21911821ba9ffbd905a37c542ad7;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=aa203f8be3c4b9e6ac01c0673d8cd9c29cd364c4;hpb=6459acbd4bb69475cfaa0b37a9771ced94193667;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml
index aa203f8be..368bc2f45 100644
--- 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,18 @@ 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 _ =
+  add_binary_op "exists" "exists"
+    (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []));
+  add_symbol_choice "cast"
+    ("type cast",
+      (fun env _ args ->
+        let t1, t2 =
+          match args with 
+          | [t1; t2] -> t1, t2
+          | _ -> raise Invalid_choice
+        in
+        Cic.Cast (t1, t2)));
+