X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=8bdb409e923ed19387be8a66fb1b765492ceb582;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c33462f8fd90269eedabefac815c2af3f6c1c5c2;hpb=c12d08acf947823bbfd5909618b042c65ff107de;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index c33462f8f..8bdb409e9 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -29,14 +29,16 @@ open DisambiguateTypes open UriManager exception No_choices of domain_item -exception NoWellTypedInterpretation +exception NoWellTypedInterpretation of string Lazy.t list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) -exception Try_again +exception Try_again of string Lazy.t + +type aliases = bool * DisambiguateTypes.environment let debug = false -let debug_print = if debug then prerr_endline else ignore +let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* (** print benchmark information *) @@ -47,16 +49,6 @@ let domain_size = ref 0 let choices_avg = ref 0. *) -let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) - -let dummy_floc = floc_of_loc (-1, -1) - let descr_of_domain_item = function | Id s -> s | Symbol (s, _) -> s @@ -64,45 +56,42 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko - | Uncertain + | Ko of string Lazy.t + | Uncertain of string Lazy.t let refine_term metasenv context uri term ugraph = (* if benchmark then incr actual_refinements; *) assert (uri=None); - let metasenv, term = - CicMkImplicit.expand_implicits metasenv [] context term in - debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)); + debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = CicRefine.type_of_aux' metasenv context term ugraph in (Ok (term', metasenv')),ugraph1 with - | CicRefine.Uncertain s -> - debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ; - Uncertain,ugraph + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph | CicRefine.RefineFailure msg -> - debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) msg); - Ko,ugraph + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph let refine_obj metasenv context uri obj ugraph = assert (context = []); - let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in - debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj)); + debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; try let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in (Ok (obj', metasenv)),ugraph with - | CicRefine.Uncertain s -> - debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ; - Uncertain,ugraph + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph | CicRefine.RefineFailure msg -> - debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) msg); - Ko,ugraph + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (Lazy.force msg))) ; + Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph -let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = +let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args with Not_found -> @@ -110,7 +99,7 @@ let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = (DisambiguateTypes.string_of_domain_item item)) (* TODO move it to Cic *) -let find_in_environment name (context: Cic.name list) = +let find_in_context name (context: Cic.name list) = let rec aux acc = function | [] -> raise Not_found | Cic.Name hd :: tl when hd = name -> acc @@ -142,7 +131,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context None outtype in - let do_branch ((head, args), term) = + let do_branch ((head, _, args), term) = let rec do_branch' context = function | [] -> aux loc context term | (name, typ) :: tl -> @@ -159,22 +148,28 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = in let (indtype_uri, indtype_no) = match indty_ident with - | Some indty_ident -> - (match resolve env (Id indty_ident) () with + | Some (indty_ident, _) -> + (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) - | Cic.Implicit _ -> raise Try_again - | _ -> raise Invalid_choice) + | Cic.Implicit _ -> + raise (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) | None -> let fst_constructor = match branches with - | ((head, _), _) :: _ -> head - | [] -> raise Invalid_choice + | ((head, _, _), _) :: _ -> head + | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) in (match resolve env (Id fst_constructor) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) - | Cic.Implicit _ -> raise Try_again - | _ -> raise Invalid_choice) + | Cic.Implicit _ -> + raise (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -224,14 +219,37 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | `Inductive -> (fun (var, _, _, _) cic -> incr counter; - Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic)) + let fix = Cic.Fix (!counter,funs) in + match cic with + Cic.Rel 1 -> fix + | (Cic.Appl (Cic.Rel 1::l)) -> + (try + let l' = + List.map + (function t -> + let t',subst,metasenv = + CicMetaSubst.delift_rels [] [] 1 t + in + assert (subst=[]); + assert (metasenv=[]); + t') l + in + Cic.Appl (fix::l') + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + Cic.LetIn (Cic.Name var, fix, cic)) + | _ -> Cic.LetIn (Cic.Name var, fix, cic)) | `CoInductive -> let funs = List.map (fun (name, _, typ, body) -> (name, typ, body)) funs in (fun (var, _, _, _) cic -> incr counter; - Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) + let cofix = Cic.CoFix (!counter,funs) in + match cic with + Cic.Rel 1 -> cofix + | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (cofix::l) + | _ -> Cic.LetIn (Cic.Name var, cofix, cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body | CicNotationPt.Ident _ @@ -241,7 +259,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try if is_uri ast then raise Not_found;(* don't search the env for URIs *) - let index = find_in_environment name context in + let index = find_in_context name context in if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here"; Cic.Rel index @@ -266,7 +284,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = (try List.assoc s ids_to_uris, aux loc context term with Not_found -> - raise Invalid_choice)) + raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in @@ -300,20 +318,20 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = Cic.MutConstruct (uri, i, j, mk_subst uris) | Cic.Meta _ | Cic.Implicit _ as t -> (* - debug_print (sprintf + debug_print (lazy (sprintf "Warning: %s must be instantiated with _[%s] but we do not enforce it" (CicPp.ppterm t) (String.concat "; " (List.map (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term) - subst))); + subst)))); *) t | _ -> - raise Invalid_choice + raise (Invalid_choice (lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> - raise Invalid_choice)) + raise (Invalid_choice (lazy "Circular dependency in the environment")))) | CicNotationPt.Implicit -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () @@ -326,7 +344,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = Cic.Meta (index, cic_subst) | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set - | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) + | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () @@ -339,8 +357,8 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term | term -> aux dummy_floc context term -let interpretate_path ~context ~env path = - interpretate_term ~context ~env ~uri:None ~is_path:true path +let interpretate_path ~context path = + interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path let interpretate_obj ~context ~env ~uri ~is_path obj = assert (context = []); @@ -493,9 +511,9 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function let outtype_dom = domain_rev_of_term_option loc context outtype in let get_first_constructor = function | [] -> [] - | ((head, _), _) :: _ -> [ Id head ] + | ((head, _, _), _) :: _ -> [ Id head ] in - let do_branch ((head, args), term) = + let do_branch ((head, _, args), term) = let (term_context, args_domain) = List.fold_left (fun (cont, dom) (name, typ) -> @@ -513,7 +531,7 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function branches_dom @ outtype_dom @ term_dom @ (match indty_ident with | None -> get_first_constructor branches - | Some ident -> [ Id ident ]) + | Some (ident, _) -> [ Id ident ]) | CicNotationPt.Cast (term, ty) -> let term_dom = domain_rev_of_term ~loc context term in let ty_dom = domain_rev_of_term ~loc context ty in @@ -544,7 +562,7 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function where_dom @ defs_dom | CicNotationPt.Ident (name, subst) -> (try - let index = find_in_environment name context in + let index = find_in_context name context in if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here" else @@ -577,8 +595,7 @@ and domain_rev_of_term_option loc context = function | None -> [] | Some t -> domain_rev_of_term ~loc context t -let domain_of_term ~context ast = - rev_uniq (domain_rev_of_term context ast) +let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast) let domain_of_obj ~context ast = assert (context = []); @@ -639,26 +656,32 @@ let domain_diff dom1 dom2 = module type Disambiguator = sig val disambiguate_term : - dbd:Mysql.dbd -> + ?fresh_instances:bool -> + dbd:HMysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:environment -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term -> - (environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term* - CicUniv.universe_graph) list (* disambiguated term *) + CicUniv.universe_graph) list * (* disambiguated term *) + bool val disambiguate_obj : - dbd:Mysql.dbd -> - aliases:environment -> (* previous interpretation status *) + ?fresh_instances:bool -> + dbd:HMysql.dbd -> + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> - (environment * (* new interpretation status *) + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * - CicUniv.universe_graph) list (* disambiguated obj *) + CicUniv.universe_graph) list * (* disambiguated obj *) + bool end module Make (C: Callbacks) = @@ -686,54 +709,63 @@ module Make (C: Callbacks) = try CicUtil.term_of_uri uri with exn -> - debug_print (UriManager.string_of_uri uri); - debug_print (Printexc.to_string exn); + debug_print (lazy (UriManager.string_of_uri uri)); + debug_print (lazy (Printexc.to_string exn)); assert false in fun _ _ _ -> term)) uris +let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" + let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = - debug_print "NEW DISAMBIGUATE INPUT"; + debug_print (lazy "DISAMBIGUATE INPUT"); let disambiguate_context = (* cic context -> disambiguate context *) List.map (function None -> Cic.Anonymous | Some (name, _) -> name) context in - debug_print ("TERM IS: " ^ (pp_thing thing)); + debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); let thing_dom = domain_of_thing ~context:disambiguate_context thing in - debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" - (string_of_domain thing_dom)); + debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s" + (string_of_domain thing_dom))); +(* + debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" + (DisambiguatePp.pp_environment aliases))); + debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s" + (match universe with None -> "None" | Some _ -> "Some _"))); +*) let current_dom = - Environment.fold (fun item _ dom -> item :: dom) current_env [] + Environment.fold (fun item _ dom -> item :: dom) aliases [] in let todo_dom = domain_diff thing_dom current_dom in (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = let id_choices = Hashtbl.create 1023 in fun item -> - let choices = - match item with - | Id id -> - (try - Hashtbl.find id_choices id - with Not_found -> - let choices = choices_of_id dbd id in - Hashtbl.add id_choices id choices; - choices) - | Symbol (symb, _) -> - List.map DisambiguateChoices.mk_choice - (CicNotationRew.lookup_interpretations symb) -(* DisambiguateChoices.lookup_symbol_choices symb *) - | Num instance -> DisambiguateChoices.lookup_num_choices () - in - if choices = [] then raise (No_choices item); - choices + let choices = + let lookup_in_library () = + match item with + | Id id -> choices_of_id dbd id + | Symbol (symb, _) -> + List.map DisambiguateChoices.mk_choice + (CicNotationRew.lookup_interpretations symb) + | Num instance -> + DisambiguateChoices.lookup_num_choices () + in + match universe with + | None -> lookup_in_library () + | Some e -> + (try + Environment.find item e + with Not_found -> lookup_in_library ()) + in + if choices = [] then raise (No_choices item); + choices in - (* (* *) let _ = @@ -743,8 +775,8 @@ module Make (C: Callbacks) = (fun dom_item -> try let len = List.length (lookup_choices dom_item) in - debug_print (sprintf "BENCHMARK %s: %d" - (string_of_domain_item dom_item) len); + debug_print (lazy (sprintf "BENCHMARK %s: %d" + (string_of_domain_item dom_item) len)); len with No_choices _ -> 0) thing_dom @@ -761,7 +793,7 @@ module Make (C: Callbacks) = (* (3) test an interpretation filling with meta uninterpreted identifiers *) - let test_env current_env todo_dom ugraph = + let test_env aliases todo_dom ugraph = let filled_env = List.fold_left (fun env item -> @@ -770,70 +802,110 @@ module Make (C: Callbacks) = (match item with | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) - current_env todo_dom + aliases todo_dom in try let cic_thing = interpretate_thing ~context:disambiguate_context ~env:filled_env ~uri ~is_path:false thing in +let foo () = let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in (k , ugraph1 ) +in refine_profiler.HExtlib.profile foo () with - | Try_again -> Uncertain, ugraph - | Invalid_choice -> Ko, ugraph + | Try_again msg -> Uncertain msg, ugraph + | Invalid_choice msg -> Ko msg, ugraph in (* (4) build all possible interpretations *) - let rec aux current_env todo_dom base_univ = + let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in + let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = match todo_dom with | [] -> - (match test_env current_env [] base_univ with + assert (lookup_in_todo_dom = None); + (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ current_env, metasenv, thing, new_univ ] - | Ko,_ | Uncertain,_ -> []) + [ aliases, diff, metasenv, thing, new_univ ], [] + | Ko msg,_ | Uncertain msg,_ -> [],[msg]) | item :: remaining_dom -> - debug_print (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item)); - let choices = lookup_choices item in - let rec filter univ = function - | [] -> [] - | codomain_item :: tl -> - debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ; - let new_env = - Environment.add item codomain_item current_env - in - (match test_env new_env remaining_dom univ with - | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> [ new_env, metasenv, thing, new_univ ] - | _ -> aux new_env remaining_dom new_univ )@ - filter univ tl - | Uncertain,new_univ -> - (match remaining_dom with - | [] -> [] - | _ -> aux new_env remaining_dom new_univ )@ - filter univ tl - | Ko,_ -> filter univ tl) - in - filter base_univ choices + debug_print (lazy (sprintf "CHOOSED ITEM: %s" + (string_of_domain_item item))); + let choices = + match lookup_in_todo_dom with + None -> lookup_choices item + | Some choices -> choices in + match choices with + [] -> [], [lazy "No choices"] + | [codomain_item] -> + (* just one choice. We perform a one-step look-up and + if the next set of choices is also a singleton we + skip this refinement step *) + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + let lookup_in_todo_dom,next_choice_is_single = + match remaining_dom with + [] -> None,false + | he::_ -> + let choices = lookup_choices he in + Some choices,List.length choices = 1 + in + if next_choice_is_single then + aux new_env new_diff lookup_in_todo_dom remaining_dom + base_univ + else + (match test_env new_env remaining_dom base_univ with + | Ok (thing, metasenv),new_univ -> + (match remaining_dom with + | [] -> + [ new_env, new_diff, metasenv, thing, new_univ ], [] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Uncertain msg,new_univ -> + (match remaining_dom with + | [] -> [], [msg] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Ko msg,_ -> [], [msg]) + | _::_ -> + let rec filter univ = function + | [] -> [],[] + | codomain_item :: tl -> + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + (match test_env new_env remaining_dom univ with + | Ok (thing, metasenv),new_univ -> + (match remaining_dom with + | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], [] + | _ -> aux new_env new_diff None remaining_dom new_univ + ) @@ + filter univ tl + | Uncertain msg,new_univ -> + (match remaining_dom with + | [] -> [],[msg] + | _ -> aux new_env new_diff None remaining_dom new_univ + ) @@ + filter univ tl + | Ko msg,_ -> ([],[msg]) @@ filter univ tl) + in + filter base_univ choices in let base_univ = initial_ugraph in try let res = - match aux current_env todo_dom base_univ with - | [] -> raise NoWellTypedInterpretation - | [ e,me,t,u ] -> - debug_print "UNA SOLA SCELTA"; - (* Experimental: we forget the environment [e] since we are able - to recompute it. In this way we are forced to do more work - later (since we have less aliases), but we have more freedom - (since we have less aliases) in the future disambiguations. *) - [ current_env,me,t,u] - | l -> - debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); + match aux aliases [] None todo_dom base_univ with + | [],errors -> raise (NoWellTypedInterpretation errors) + | [_,diff,metasenv,t,ugraph],_ -> + debug_print (lazy "SINGLE INTERPRETATION"); + [diff,metasenv,t,ugraph], false + | l,_ -> + debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map - (fun (env, _, _, _) -> + (fun (env, _, _, _, _) -> List.map (fun domain_item -> let description = @@ -844,40 +916,40 @@ module Make (C: Callbacks) = l in let choosed = C.interactive_interpretation_choice choices in - List.map (List.nth l) choosed + (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed), + true in -(* - (if benchmark then - let res_size = List.length res in - 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 - !choices_avg - (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))); -*) - res + res with CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" - let disambiguate_term ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term + let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term = - disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases - ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term - ~interpretate_thing:interpretate_term ~refine_thing:refine_term term - - let disambiguate_obj ~dbd ~aliases ~uri obj = - disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri - ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj - ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj - obj + let term = + if fresh_instances then CicNotationUtil.freshen_term term else term + in + disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases + ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term + ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term + ~refine_thing:refine_term term + + let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri + obj + = + let obj = + if fresh_instances then CicNotationUtil.freshen_obj obj else obj + in + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri + ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj + ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj + obj end module Trivial = struct - exception Ambiguous_term of string + exception Ambiguous_term of string Lazy.t exception Exit module Callbacks = struct @@ -891,10 +963,12 @@ struct let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph ?(aliases = DisambiguateTypes.Environment.empty) term = - let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in + let ast = + CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term) + in try - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases - with Exit -> raise (Ambiguous_term term) + fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast + ?initial_ugraph ~aliases ~universe:None) + with Exit -> raise (Ambiguous_term (lazy term)) end