* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open DisambiguateTypes
-exception Invalid_choice
-exception Choice_not_found of string
+exception Choice_not_found of string Lazy.t
let num_choices = ref []
let lookup_num_by_dsc dsc =
try
List.find (has_description dsc) !num_choices
- with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc))
+ with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
let mk_choice (dsc, args, appl_pattern) =
dsc,
in
try
List.combine names cic_args
- with Invalid_argument _ -> raise Invalid_choice
+ with Invalid_argument _ ->
+ raise (Invalid_choice (lazy "The notation expects a different number of arguments"))
in
- CicNotationFwd.instantiate_appl_pattern env' appl_pattern)
+ TermAcicContent.instantiate_appl_pattern env' appl_pattern)
let lookup_symbol_by_dsc symbol dsc =
try
mk_choice
(List.find
(fun (dsc', _, _) -> dsc = dsc')
- (CicNotationRew.lookup_interpretations symbol))
- with CicNotationRew.Interpretation_not_found | Not_found ->
- raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symbol dsc))
+ (TermAcicContent.lookup_interpretations symbol))
+ with TermAcicContent.Interpretation_not_found | Not_found ->
+ raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))