exception Try_again
let debug = false
-let debug = true
let debug_print = if debug then prerr_endline else ignore
(*
(Ok (term', metasenv')),ugraph1
with
| CicRefine.Uncertain _ ->
- debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
Uncertain,ugraph
- | CicRefine.RefineFailure _ ->
- debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
+ | CicRefine.RefineFailure msg ->
+ debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) msg);
Ko,ugraph
- | CicUnification.UnificationFailure s ->
- prerr_endline ("PASSADI QUI: " ^ s);
- raise ( CicUnification.UnificationFailure s )
+ | CicUniv.UniverseInconsistency s ->
+ prerr_endline (
+ "INTERPRETAZIONE FALLITA PER UNIVERSE INCONSISTENCY:\n" ^ s);
+ (* non mi e' chiaro se debba essere wrappata dal typechecker o dal
+ * refiner, in ogni caso non andrebbe qui
+ *)
+ Ko, ugraph
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
try
in
List.filter (fun elt -> not (is_in_dom2 elt)) dom1
+module type Disambiguator =
+sig
+ val disambiguate_term :
+ dbd:Mysql.dbd ->
+ context:Cic.context ->
+ metasenv:Cic.metasenv ->
+ ?initial_ugraph:CicUniv.universe_graph ->
+ aliases:environment -> (* previous interpretation status *)
+ CicAst.term ->
+ (environment * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term*
+ CicUniv.universe_graph) list (* disambiguated term *)
+end
+
module Make (C: Callbacks) =
struct
let choices_of_id dbd id =
fun _ _ _ -> term))
uris
- let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+ let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+ term
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)
failwith "Disambiguate: circular dependency"
end
+module Trivial =
+struct
+ exception Ambiguous_term of string
+ exception Exit
+ module Callbacks =
+ struct
+ let interactive_user_uri_choice ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
+ raise Exit
+ let interactive_interpretation_choice interp = raise Exit
+ let input_or_locate_uri ~(title:string) ?id = raise Exit
+ end
+ module Disambiguator = Make (Callbacks)
+ let disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph
+ ?(aliases=DisambiguateTypes.Environment.empty) term =
+ let ast = CicTextualParser2.parse_term (Stream.of_string term) in
+ try
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+ ?initial_ugraph ~aliases
+ with Exit -> raise (Ambiguous_term term)
+end
+