X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=f203e6d790edc4b2cc6e413afa8e1c40c6935964;hb=b96b712d43bda14914a9d563712db88f24f3276a;hp=b66e12d5e4c15909c2a7badc1d454666168086d2;hpb=9d27c7d2161dae5283a9121c206b9184e100c2b5;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b66e12d5e..f203e6d79 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -62,8 +62,6 @@ type 'a test_result = 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 (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = @@ -71,27 +69,26 @@ let refine_term metasenv context uri term ugraph = (Ok (term', metasenv')),ugraph1 with | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term)) ; + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (CicRefine.explain_error msg))); + (CicPp.ppterm term) (Lazy.force msg))); Ko,ugraph let refine_obj metasenv context uri obj ugraph = assert (context = []); - let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in 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 (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj)) ; + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (CicRefine.explain_error msg))) ; + (CicPp.ppobj obj) (Lazy.force msg))) ; Ko,ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = @@ -318,7 +315,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)) () @@ -631,14 +628,14 @@ module type Disambiguator = sig val disambiguate_term : ?fresh_instances:bool -> - dbd:Mysql.dbd -> + dbd:HMysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> 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 *) @@ -646,12 +643,12 @@ sig val disambiguate_obj : ?fresh_instances:bool -> - dbd:Mysql.dbd -> + 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 *) @@ -690,7 +687,7 @@ module Make (C: Callbacks) = fun _ _ _ -> term)) uris -let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing" +let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe @@ -706,10 +703,12 @@ let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing" let thing_dom = domain_of_thing ~context:disambiguate_context thing in 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) aliases [] in @@ -784,56 +783,98 @@ let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing" let foo () = let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in (k , ugraph1 ) -in refine_profiler.CicUtil.profile foo () +in refine_profiler.HExtlib.profile foo () with | Try_again -> Uncertain, ugraph | Invalid_choice -> Ko, ugraph in (* (4) build all possible interpretations *) - let rec aux aliases todo_dom base_univ = + let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = match todo_dom with | [] -> + assert (lookup_in_todo_dom = None); (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ aliases, metasenv, thing, new_univ ] + [ aliases, diff, metasenv, thing, new_univ ] | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (lazy (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 (lazy (sprintf "%s CHOSEN" (fst codomain_item))) ; - let new_env = Environment.add item codomain_item aliases 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 + let choices = + match lookup_in_todo_dom with + None -> lookup_choices item + | Some choices -> choices in + match choices with + [] -> [] + | [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,new_univ -> + (match remaining_dom with + | [] -> [] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Ko,_ -> []) + | _::_ -> + 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,new_univ -> + (match remaining_dom with + | [] -> [] + | _ -> aux new_env new_diff None remaining_dom new_univ + ) @ + filter univ tl + | Ko,_ -> filter univ tl) + in + filter base_univ choices in let base_univ = initial_ugraph in try let res = - match aux aliases todo_dom base_univ with + match aux aliases [] None todo_dom base_univ with | [] -> raise NoWellTypedInterpretation - | [ e,me,t,u ] -> + | [_,diff,metasenv,t,ugraph] -> debug_print (lazy "SINGLE INTERPRETATION"); - [ e,me,t,u ], false + [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,19 +885,10 @@ in refine_profiler.CicUtil.profile foo () l in let choosed = C.interactive_interpretation_choice choices in - (List.map (List.nth l) choosed), true + (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 (lazy (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" @@ -886,7 +918,7 @@ in refine_profiler.CicUtil.profile foo () module Trivial = struct - exception Ambiguous_term of string + exception Ambiguous_term of string Lazy.t exception Exit module Callbacks = struct @@ -906,6 +938,6 @@ struct try fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast ?initial_ugraph ~aliases ~universe:None) - with Exit -> raise (Ambiguous_term term) + with Exit -> raise (Ambiguous_term (lazy term)) end