X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=5096789d964eccc1560d05fe46ce68d92c4846c7;hb=13494c7c3ca9fde61c7476d0be6109b33c64b3a7;hp=026f9ebd1ee238ad6e7b7de248fa2f4f415bec30;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 026f9ebd1..5096789d9 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -35,6 +35,8 @@ exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again +type aliases = bool * DisambiguateTypes.environment + let debug = false let debug_print = if debug then prerr_endline else ignore @@ -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 @@ -102,7 +94,7 @@ let refine_obj metasenv context uri obj ugraph = (CicPp.ppobj obj) msg); Ko,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 -> @@ -142,7 +134,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,7 +151,7 @@ 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 -> + | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> raise Try_again @@ -167,7 +159,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | None -> let fst_constructor = match branches with - | ((head, _), _) :: _ -> head + | ((head, _, _), _) :: _ -> head | [] -> raise Invalid_choice in (match resolve env (Id fst_constructor) () with @@ -339,8 +331,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 = []); @@ -367,7 +359,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = (fun (i,res) (name,_,_,_) -> i + 1,(name,name,Cic.MutInd (uri,i,[]))::res ) (0,[]) tyl) in - let con_env = DisambiguateTypes.env_of_list name_to_uris env in + let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in let undebrujin t = snd (List.fold_right @@ -493,9 +485,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 +505,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 @@ -577,8 +569,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 +630,30 @@ let domain_diff dom1 dom2 = module type Disambiguator = sig val disambiguate_term : + ?fresh_instances:bool -> dbd:Mysql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:environment -> (* previous interpretation status *) + aliases:aliases -> (* previous interpretation status *) CicNotationPt.term -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term* - CicUniv.universe_graph) list (* disambiguated term *) + CicUniv.universe_graph) list * (* disambiguated term *) + bool val disambiguate_obj : + ?fresh_instances:bool -> dbd:Mysql.dbd -> - aliases:environment -> (* previous interpretation status *) + aliases:aliases -> (* previous interpretation status *) uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.obj * - CicUniv.universe_graph) list (* disambiguated obj *) + CicUniv.universe_graph) list * (* disambiguated obj *) + bool end module Make (C: Callbacks) = @@ -694,10 +689,15 @@ module Make (C: Callbacks) = uris let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = - debug_print "NEW DISAMBIGUATE INPUT"; + debug_print "DISAMBIGUATE INPUT"; + let current_env, multi_aliases_env = + match aliases with + | false, e -> Environment.hd e, None + | true, e -> Environment.empty, Some e + in let disambiguate_context = (* cic context -> disambiguate context *) List.map (function None -> Cic.Anonymous | Some (name, _) -> name) @@ -707,6 +707,8 @@ module Make (C: Callbacks) = 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 (snd aliases))); let current_dom = Environment.fold (fun item _ dom -> item :: dom) current_env [] in @@ -715,25 +717,26 @@ module Make (C: Callbacks) = 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 multi_aliases_env 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 _ = @@ -822,11 +825,11 @@ module Make (C: Callbacks) = let res = match aux current_env todo_dom base_univ with | [] -> raise NoWellTypedInterpretation - | [ e,me,t,u ] as l -> - debug_print "UNA SOLA SCELTA"; - [ e,me,t,u] + | [ e,me,t,u ] -> + debug_print "SINGLE INTERPRETATION"; + [ e,me,t,u ], false | l -> - debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); + debug_print (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)); let choices = List.map (fun (env, _, _, _) -> @@ -840,7 +843,7 @@ module Make (C: Callbacks) = l in let choosed = C.interactive_interpretation_choice choices in - List.map (List.nth l) choosed + (List.map (List.nth l) choosed), true in (* (if benchmark then @@ -852,23 +855,36 @@ module Make (C: Callbacks) = !choices_avg (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))); *) - res + let choices, b = res in + (List.map + (fun (env, metasenv, t, ugraph) -> + Environment.fold Environment.cons env (snd aliases), + metasenv, t, ugraph) + choices), + b with CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" - let disambiguate_term ~dbd ~context ~metasenv + let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases 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 + ~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 ~uri obj = + let obj = + if fresh_instances then CicNotationUtil.freshen_obj obj else obj + in + 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 end module Trivial = @@ -889,8 +905,8 @@ struct = let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in try - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases + fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast + ?initial_ugraph ~aliases:(false, aliases)) with Exit -> raise (Ambiguous_term term) end