(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);
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
try
snd (Environment.find item env) env num args
- with Not_found -> assert false
+ with Not_found ->
+ failwith ("Domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
let find_in_environment name context =
subst
| None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
in
- (* the try is for CicTypeChecker.typecheck *)
(try
match cic with
| Cic.Const (uri, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.Constant (_, _, _, uris) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.Variable (_, _, _, uris) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.InductiveDefinition (_, uris, _) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
| Cic.MutConstruct (uri, i, j, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.InductiveDefinition (_, uris, _) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
(*
uris
let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)
res
with
CicEnvironment.CircularDependency s ->
- raise (Failure "e chi la becca sta CircularDependency?");
+ 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
+