]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguateChoices.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_disambiguation / disambiguateChoices.mli
index 3a6e92f558de819af9b780967d10d4e2e5d3a96e..0ad498106456a50d50ed4962a530e597b7d1a08f 100644 (file)
 
 open DisambiguateTypes
 
-(** {2 Choice registration interface} *)
-
-  (** to be raised when a choice is invalid due to some given parameter (e.g.
-   * wrong number of Cic.term arguments received) *)
-exception Invalid_choice
+(** {2 Choice registration low-level interface} *)
 
   (** raised by lookup_XXXX below *)
-exception Choice_not_found of string
-
-  (** register a new symbol choice *)
-val add_symbol_choice: string -> codomain_item -> unit
+exception Choice_not_found of string Lazy.t
 
   (** register a new number choice *)
 val add_num_choice: codomain_item -> unit
@@ -43,16 +36,18 @@ val add_num_choice: codomain_item -> unit
 (** {2 Choices lookup}
  * for user defined aliases *)
 
-  (** @param symbol symbol as per AST *)
-val lookup_symbol_choices: string -> codomain_item list
-
 val lookup_num_choices: unit -> codomain_item list
 
+  (** @param dsc description (1st component of codomain_item) *)
+val lookup_num_by_dsc: string -> codomain_item
+
   (** @param symbol symbol as per AST
    * @param dsc description (1st component of codomain_item)
    *)
 val lookup_symbol_by_dsc: string -> string -> codomain_item
 
-  (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> codomain_item
+val mk_choice:
+  string * CicNotationPt.argument_pattern list *
+  CicNotationPt.cic_appl_pattern ->
+    codomain_item