X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=2775aed3b97428354897113d441a2c48c69e0f50;hb=2eb1644f907fc2319957fad1511ad98dccc89209;hp=67b6d115c2cd908daac51084287ce958be60f0c6;hpb=a1bfef9d9930c9a136abe0593d8da457b4e21fc3;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 67b6d115c..2775aed3b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -66,18 +66,13 @@ let refine metasenv context term ugraph = CicRefine.type_of_aux' metasenv context term ugraph in (Ok (term', metasenv')),ugraph1 with - | CicRefine.Uncertain _ -> - debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; + | CicRefine.Uncertain s -> + debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ 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 @@ -255,7 +250,7 @@ let interpretate ~context ~env ast = Cic.MutConstruct (uri, i, j, mk_subst uris) | Cic.Meta _ | Cic.Implicit _ as t -> (* - prerr_endline (sprintf + debug_print (sprintf "Warning: %s must be instantiated with _[%s] but we do not enforce it" (CicPp.ppterm t) (String.concat "; " @@ -270,6 +265,8 @@ let interpretate ~context ~env ast = CicEnvironment.CircularDependency _ -> raise DisambiguateChoices.Invalid_choice)) | CicAst.Implicit -> Cic.Implicit None + | CicAst.UserInput -> Cic.Implicit (Some `Hole) +(* | CicAst.UserInput -> assert false*) | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -284,7 +281,6 @@ let interpretate ~context ~env ast = | CicAst.Sort `CProp -> Cic.Sort Cic.CProp | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () - | CicAst.UserInput -> assert false and aux_option loc context = function | None -> Cic.Implicit (Some `Type) | Some term -> aux loc context term @@ -314,6 +310,10 @@ let domain_of_term ~context ast = | CicAst.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in + let get_first_constructor = function + | [] -> [] + | ((head, _), _) :: _ -> [ Id head ] + in let do_branch ((head, args), term) = let (term_context, args_domain) = List.fold_left @@ -330,7 +330,9 @@ let domain_of_term ~context ast = List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches in branches_dom @ outtype_dom @ term_dom @ - (match indty_ident with None -> [] | Some ident -> [ Id ident ]) + (match indty_ident with + | None -> get_first_constructor branches + | Some ident -> [ Id ident ]) | CicAst.LetIn ((var, typ), body, where) -> let body_dom = aux loc context body in let type_dom = aux_option loc context typ in @@ -419,6 +421,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 = @@ -444,15 +461,16 @@ module Make (C: Callbacks) = try CicUtil.term_of_uri uri with exn -> - prerr_endline uri; - prerr_endline (Printexc.to_string exn); + debug_print uri; + debug_print (Printexc.to_string exn); assert false in fun _ _ _ -> term)) uris - let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term + 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 *) @@ -460,6 +478,7 @@ module Make (C: Callbacks) = (function None -> Cic.Anonymous | Some (name, _) -> name) context in + debug_print ("TERM IS: " ^ (CicAstPp.pp_term term)); let term_dom = domain_of_term ~context:disambiguate_context term in debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain term_dom)); @@ -496,7 +515,7 @@ module Make (C: Callbacks) = (fun dom_item -> try let len = List.length (lookup_choices dom_item) in - prerr_endline (sprintf "BENCHMARK %s: %d" + debug_print (sprintf "BENCHMARK %s: %d" (string_of_domain_item dom_item) len); len with No_choices _ -> 0) @@ -597,7 +616,7 @@ module Make (C: Callbacks) = (* (if benchmark then let res_size = List.length res in - prerr_endline (sprintf + debug_print (sprintf ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^ "BENCHMARK: estimated %.2f") !actual_refinements !max_refinements !domain_size res_size @@ -610,3 +629,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 +