X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=05a15691eb3d478e7e8a0e986babac1adb7640db;hb=24320a56c9cc9e92c0a03475e529b4a54f5d4e14;hp=b9aa8f844fe76a10754a088c2cc2810f3e1d7bd8;hpb=8539d00ff2ed0ffd9b7a08ac8e62376e88987960;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b9aa8f844..05a15691e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -38,7 +38,7 @@ exception Try_again 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 *) @@ -64,34 +64,34 @@ let refine_term metasenv context uri term ugraph = 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) ; + debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term)) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> - debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) msg); + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (CicRefine.explain_error 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 (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) ; + debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj)) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> - debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) msg); + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (CicRefine.explain_error msg))) ; Ko,ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = @@ -102,7 +102,7 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ? (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 @@ -233,7 +233,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 @@ -292,13 +292,13 @@ 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 | _ -> @@ -318,7 +318,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)) () @@ -536,7 +536,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 @@ -631,14 +631,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 +646,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 *) @@ -683,31 +683,33 @@ 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 ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = - debug_print "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 (sprintf "DISAMBIGUATION ENVIRONMENT: %s" - (DisambiguatePp.pp_environment aliases)); - debug_print (sprintf "DISAMBIGUATION UNIVERSE: %s" - (match universe with None -> "None" | Some _ -> "Some _")); + 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 @@ -745,8 +747,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 @@ -779,41 +781,42 @@ module Make (C: Callbacks) = 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 in (* (4) build all possible interpretations *) - let rec aux aliases todo_dom base_univ = + let rec aux aliases diff todo_dom base_univ = match todo_dom with | [] -> (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 (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item)); + 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 (sprintf "%s CHOSEN" (fst codomain_item)) ; - let new_env = - Environment.add item codomain_item aliases - in + 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, metasenv, thing, new_univ ] - | _ -> aux new_env remaining_dom new_univ )@ + | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] + | _ -> aux new_env new_diff remaining_dom new_univ )@ filter univ tl | Uncertain,new_univ -> (match remaining_dom with | [] -> [] - | _ -> aux new_env remaining_dom new_univ )@ + | _ -> aux new_env new_diff remaining_dom new_univ )@ filter univ tl | Ko,_ -> filter univ tl) in @@ -822,16 +825,16 @@ module Make (C: Callbacks) = let base_univ = initial_ugraph in try let res = - match aux aliases todo_dom base_univ with + match aux aliases [] todo_dom base_univ with | [] -> raise NoWellTypedInterpretation - | [ e,me,t,u ] -> - debug_print "SINGLE INTERPRETATION"; - [ e,me,t,u ], false + | [_,diff,metasenv,t,ugraph] -> + debug_print (lazy "SINGLE INTERPRETATION"); + [diff,metasenv,t,ugraph], false | l -> - debug_print (sprintf "MANY INTERPRETATIONS (%d)" (List.length 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 = @@ -842,25 +845,10 @@ module Make (C: Callbacks) = 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 (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))); -*) - let choices, b = res in - (List.map - (fun (env, metasenv, t, ugraph) -> - Environment.fold Environment.add env aliases, - metasenv, t, ugraph) - choices), - b + res with CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" @@ -904,7 +892,9 @@ 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 fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast ?initial_ugraph ~aliases ~universe:None)