X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=570ab894e434e7b9f45b5444e854c14b09fda6fe;hb=0ef18c2aaa95d86b3bcdac35d4a14cd4a0cf0fdd;hp=aafbeb7777d85689fab91712b412761119476ed2;hpb=ec339d7f6bcb3442f3aa816addc6a85f6adf5553;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index aafbeb777..570ab894e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -67,17 +67,12 @@ let refine metasenv context term ugraph = (Ok (term', metasenv')),ugraph1 with | CicRefine.Uncertain _ -> - debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; + debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> - debug_print ( - (sprintf ("%%%%%% PRUNED!!!\n<>\n" ^^ - "%s\n<>\n<>\n%s\n<>") - msg (CicPp.ppterm term))); + 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 ) let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -419,6 +414,21 @@ let domain_diff dom1 dom2 = 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 = @@ -451,8 +461,9 @@ module Make (C: Callbacks) = 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 *) @@ -610,3 +621,25 @@ module Make (C: Callbacks) = 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 +