X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b2df644d261b087c60068ba971294a0d3894a7c2;hb=e9e00ee3e8d57c51e52fcfca9c642b8f366b8d0d;hp=827bbe2d4ea96af5ae8971588dee05d15d9035b9;hpb=aba014724c9ad08f80944ec3021c9fa3826dca4a;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 827bbe2d4..b2df644d2 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -23,61 +23,37 @@ * http://helm.cs.unibo.it/ *) -open Disambiguate_struct +open Printf + open Disambiguate_types +open UriManager -let debug = true -let debug_print = if debug then prerr_endline else ignore +exception Invalid_choice +exception No_choices of domain_item +exception NoWellTypedInterpretation -type interpretation_domain = Domain.t -type domain_and_interpretation = interpretation_domain * interpretation + (** raised when an environment is not enough informative to decide *) +exception Try_again -let string_of_interpretation_domain_item = function - | Id s -> "ID " ^ s - | Symbol (s, i) -> "SYMBOL " ^ s ^ " " ^ string_of_int i - | Num (s, i) -> "NUM " ^ s ^ " " ^ string_of_int i +let debug = true +let debug_print = if debug then prerr_endline else ignore let descr_of_domain_item = function | Id s -> s | Symbol (s, _) -> s - | Num (s, _) -> s - -let rec build_natural = - function - | 0 -> HelmLibraryObjects.Datatypes.zero - | n -> Cic.Appl [ HelmLibraryObjects.Datatypes.succ; (build_natural (n - 1)) ] - -exception Invalid_choice + | Num i -> string_of_int i -let symbol_choices: (string, interpretation_codomain_item list) Hashtbl.t = Hashtbl.create 1023 -let _ = - Hashtbl.add symbol_choices "eq" - [ ("Leibnitz's equality", - (fun interp args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise Invalid_choice - in - Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); - Cic.Implicit; t1; t2 - ])) ] -(* -let add_symbol_choice = Hashtbl.add symbol_choices -let add_symbol_choices symbol = List.iter (add_symbol_choice symbol) -*) -let num_choices = - ref [ - "natural number", - (fun num -> - let num = int_of_string num in - assert (num >= 0); - build_natural num) - ] +let symbol_choices = Hashtbl.create 1023 +let num_choices = ref [] -let add_num_choice choice = - num_choices := choice :: !num_choices +let add_symbol_choice symbol codomain_item = + let current_choices = + try + Hashtbl.find symbol_choices symbol + with Not_found -> [] + in + Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices) +let add_num_choice choice = num_choices := choice :: !num_choices type test_result = | Ok of Cic.term * Cic.metasenv @@ -86,6 +62,7 @@ type test_result = let refine metasenv context term = let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in + debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)); try let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in Ok (term', metasenv') @@ -93,9 +70,11 @@ let refine metasenv context term = | CicRefine.MutCaseFixAndCofixRefineNotImplemented -> (* TODO remove this case as soon as refine is fully implemented *) (try + debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term)); let term' = CicTypeChecker.type_of_aux' metasenv context term in Ok (term',metasenv) - with _ -> Ko) +(* with _ -> Ko) *) + with _ -> Uncertain) | CicRefine.Uncertain _ -> debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain @@ -103,10 +82,6 @@ let refine metasenv context term = debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; Ko -open Printf - -open UriManager - let indtyuri_of_uri uri = let index_sharp = String.index uri '#' in let index_num = index_sharp + 3 in @@ -146,181 +121,33 @@ let term_of_uri uri = with | Invalid_argument _ -> raise (UriManager.IllFormedUri uri) -module Make (C: Callbacks) = - struct - exception NoWellTypedInterpretation - - let choices_of_id mqi_handle id = - let query = MQueryGenerator.locate id in - let result = MQueryInterpreter.execute mqi_handle query in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri - ) result in - C.output_html (`Msg (`T "Locate query:")); - MQueryUtil.text_of_query - (fun s -> C.output_html ~append_NL:false (`Msg (`T s))) - "" query; - C.output_html (`Msg (`T "Result:")); - MQueryUtil.text_of_result - (fun s -> C.output_html (`Msg (`T s))) "" result; - let uris' = - match uris with - | [] -> - [UriManager.string_of_uri (C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown."))] - | [uri] -> [uri] - | _ -> - C.interactive_user_uri_choice ~selection_mode:`MULTIPLE - ~ok:"Try every selection." ~enable_button_for_non_vars:true - ~title:"Ambiguous input." ~id - ~msg: ("Ambiguous input \"" ^ id ^ - "\". Please, choose one or more interpretations:") - uris - in - List.map (fun uri -> (uri, term_of_uri uri)) uris' - - let disambiguate_input - mqi_handle context metasenv parser_dom parser_mk_term - (current_dom, current_interpretation) - = - debug_print "NEW DISAMBIGUATE INPUT"; - let todo_dom = Domain.diff parser_dom current_dom in - (* (1) for each item in todo_dom we get the associated list of choices *) - let id_choices = Hashtbl.create 1023 in - let _ = - Domain.iter - (function - | Id id -> - (* pairs *) - let choices = choices_of_id mqi_handle id in - debug_print (sprintf - "CHOICES_OF_ID di %s ha restituito %d scelte" - id (List.length choices)); - Hashtbl.add id_choices id choices - | _ -> assert false) - (Domain.filter (function Id _ -> true | _ -> false) todo_dom) - in - (* (2) lookup function for any item (Id/Symbol/Num) *) - let lookup_choices item = - try - (match item with - | Id id -> - let choices = Hashtbl.find id_choices id in - List.map (fun (descr, term) -> (descr, fun _ _ -> term)) choices - | Symbol (symb, _) -> Hashtbl.find symbol_choices symb - | Num (num, _) -> - List.map - (fun (descr, f) -> (descr, let term = f num in fun _ _ -> term)) - !num_choices) - with Not_found -> assert false - in - (* (3) test an interpretation filling with meta uninterpreted identifiers - *) - let test_interpretation current_interpretation todo_dom = - let filled_interpretation = - Domain.fold - (fun item' interpretation -> - fun item -> - if item = item' then - "Implicit", fun _ _ -> Cic.Implicit - else - interpretation item) - todo_dom current_interpretation - in - let term' = parser_mk_term filled_interpretation in - refine metasenv context term' - in - (* (4) build all possible interpretations *) - let rec aux current_interpretation todo_dom = - if Domain.is_empty todo_dom then - match test_interpretation current_interpretation Domain.empty with - | Ok (term, metasenv) -> [ current_interpretation, term, metasenv ] - | Ko | Uncertain -> [] - else - let item = Domain.choose todo_dom in - debug_print (sprintf "CHOOSED ITEM: %s" - (string_of_interpretation_domain_item item)); - let remaining_dom = Domain.remove item todo_dom in - let choices = lookup_choices item in - let rec filter = function - | [] -> [] - | codomain_item :: tl -> - let new_interpretation = - fun item' -> - if item' = item then - codomain_item - else - current_interpretation item' - in - (match test_interpretation new_interpretation remaining_dom with - | Ok (term, metasenv) -> - (if Domain.is_empty remaining_dom then - [ new_interpretation, term, metasenv ] - else - aux new_interpretation remaining_dom) - @ filter tl - | Uncertain -> - (if Domain.is_empty remaining_dom then - [] - else - aux new_interpretation remaining_dom) - @ filter tl - | Ko -> filter tl) - in - filter choices - in - let (choosed_interpretation, choosed_term, choosed_metasenv) = - match aux current_interpretation todo_dom with - | [] -> raise NoWellTypedInterpretation - | [ x ] -> - debug_print "UNA SOLA SCELTA"; - x - | l -> - debug_print "PIU' SCELTE"; - let choices = - List.map - (fun (interpretation, _, _) -> - List.map - (fun domain_item -> - let description = fst (interpretation domain_item) in -(* - match interpretation domain_item with - | None -> assert false - | Some (descr, _) -> descr - in -*) - (descr_of_domain_item domain_item, description)) - (Domain.elements parser_dom)) - l - in - let choosed = C.interactive_interpretation_choice choices in - List.nth l choosed - in - (Domain.union current_dom todo_dom, choosed_interpretation), - choosed_metasenv, choosed_term - - end +let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = + snd (Environment.find item env) env num args -let apply_interp (interp: interpretation) item = snd (interp item) +let find_in_environment name context = + let rec aux acc = function + | [] -> raise Not_found + | Cic.Name hd :: tl when hd = name -> acc + | _ :: tl -> aux (acc + 1) tl + in + aux 1 context -let interpretate ~context ~interp ast = +let interpretate ~context ~env ast = let rec aux loc context = function | Ast.LocatedTerm (loc, term) -> aux loc context term | Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms) - | Ast.Appl_symbol (symb, args) -> + | Ast.Appl_symbol (symb, i, args) -> let cic_args = List.map (aux loc context) args in - apply_interp interp (Symbol (symb, 0)) interp cic_args + resolve env (Symbol (symb, i)) ~args:cic_args () | Ast.Binder (binder_kind, var, typ, body) -> let cic_type = aux_option loc context typ in - let cic_body = aux loc (Some var :: context) body in + let cic_body = aux loc (var :: context) body in (match binder_kind with | `Lambda -> Cic.Lambda (var, cic_type, cic_body) | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body) | `Exists -> - apply_interp interp (Symbol ("exists", 0)) interp - [ cic_type; Cic.Lambda (var, cic_type, cic_body) ]) + resolve env (Symbol ("exists", 0)) + ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ()) | Ast.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context outtype in @@ -328,7 +155,7 @@ let interpretate ~context ~interp ast = let rec do_branch' context = function | [] -> aux loc context term | hd :: tl -> - let cic_body = do_branch' (Some (Cic.Name hd) :: context) tl in + let cic_body = do_branch' (Cic.Name hd :: context) tl in Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body) in match pat with @@ -336,20 +163,21 @@ let interpretate ~context ~interp ast = | [] -> assert false in let (indtype_uri, indtype_no) = - match apply_interp interp (Id indty_ident) interp [] with + match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> uri, tyno - | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident) + | Cic.Implicit -> raise Try_again + | _ -> raise Invalid_choice in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) | Ast.LetIn (var, def, body) -> let cic_def = aux loc context def in let name = Cic.Name var in - let cic_body = aux loc (Some name :: context) body in + let cic_body = aux loc (name :: context) body in Cic.LetIn (name, cic_def, cic_body) | Ast.LetRec (kind, defs, body) -> let context' = - List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc) + List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) context defs in let cic_body = aux loc context' body in @@ -380,19 +208,14 @@ let interpretate ~context ~interp ast = in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body | Ast.Ident (name, subst) -> - let rec find acc e = function - | [] -> raise Not_found - | Some (Cic.Name hd) :: tl when e = hd -> acc - | _ :: tl -> find (acc + 1) e tl - in + (* TODO hanlde explicit substitutions *) (try - let index = find 1 name context in + let index = find_in_environment name context in if subst <> [] then Parser.fail loc "Explicit substitutions not allowed here"; Cic.Rel index - with Not_found -> - apply_interp interp (Id name) interp []) - | Ast.Num num -> apply_interp interp (Num (num, 0)) interp [] + with Not_found -> resolve env (Id name) ()) + | Ast.Num (num, i) -> resolve env (Num i) ~num () | Ast.Meta (index, subst) -> let cic_subst = List.map @@ -412,3 +235,221 @@ let interpretate ~context ~interp ast = | Ast.LocatedTerm (loc, term) -> aux loc context term | _ -> assert false +let domain_of_term ~context ast = + let rec aux loc context = function + | Ast.LocatedTerm (_, term) -> aux loc context term + | Ast.Appl terms -> + List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) + Domain.empty terms + | Ast.Appl_symbol (symb, i, args) -> + List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) + (Domain.singleton (Symbol (symb, i))) args + | Ast.Binder (_, var, typ, body) -> + let type_dom = aux_option loc context typ in + let body_dom = aux loc (var :: context) body in + Domain.union type_dom body_dom + | Ast.Case (term, indty_ident, outtype, branches) -> + let term_dom = aux loc context term in + let outtype_dom = aux_option loc context outtype in + let do_branch (pat, term) = + match pat with + | _ :: tl -> + aux loc + (List.fold_left (fun acc var -> (Cic.Name var) :: acc) + context tl) + term + | [] -> assert false + in + let branches_dom = + List.fold_left (fun dom branch -> Domain.union dom (do_branch branch)) + Domain.empty branches + in + Domain.add (Id indty_ident) + (Domain.union outtype_dom (Domain.union term_dom branches_dom)) + | Ast.LetIn (var, body, where) -> + let body_dom = aux loc context body in + let where_dom = aux loc (Cic.Name var :: context) where in + Domain.union body_dom where_dom + | Ast.LetRec (kind, defs, where) -> + let context' = + List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) + context defs + in + let where_dom = aux loc context' where in + let defs_dom = + List.fold_left + (fun dom (_, body, typ, _) -> + Domain.union (aux loc context' body) (aux_option loc context typ)) + Domain.empty defs + in + Domain.union where_dom defs_dom + | Ast.Ident (name, subst) -> + (* TODO hanlde explicit substitutions *) + (try + let index = find_in_environment name context in + if subst <> [] then + Parser.fail loc "Explicit substitutions not allowed here"; + Domain.empty + with Not_found -> Domain.singleton (Id name)) + | Ast.Num (num, i) -> Domain.singleton (Num i) + | Ast.Meta (index, local_context) -> + List.fold_left + (fun dom term -> Domain.union dom (aux_option loc context term)) + Domain.empty local_context + | Ast.Sort _ -> Domain.empty + and aux_option loc context = function + | None -> Domain.empty + | Some t -> aux loc context t + in + match ast with + | Ast.LocatedTerm (loc, term) -> aux loc context term + | _ -> assert false + +module Make (C: Callbacks) = + struct + let choices_of_id mqi_handle id = + let query = MQueryGenerator.locate id in + let result = MQueryInterpreter.execute mqi_handle query in + let uris = + List.map + (function uri,_ -> + MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + C.output_html (`Msg (`T "Locate query:")); + MQueryUtil.text_of_query + (fun s -> C.output_html ~append_NL:false (`Msg (`T s))) + "" query; + C.output_html (`Msg (`T "Result:")); + MQueryUtil.text_of_result + (fun s -> C.output_html (`Msg (`T s))) "" result; + let uris' = + match uris with + | [] -> + [UriManager.string_of_uri (C.input_or_locate_uri + ~title:("URI matching \"" ^ id ^ "\" unknown."))] + | [uri] -> [uri] + | _ -> + C.interactive_user_uri_choice ~selection_mode:`MULTIPLE + ~ok:"Try every selection." ~enable_button_for_non_vars:true + ~title:"Ambiguous input." ~id + ~msg: ("Ambiguous input \"" ^ id ^ + "\". Please, choose one or more interpretations:") + uris + in + List.map + (fun uri -> (uri, let term = term_of_uri uri in fun _ _ _ -> term)) + uris' + + let disambiguate_term mqi_handle context metasenv term ~aliases:current_env + = + let current_dom = (* TODO temporary, remove ASAP *) + Environment.fold (fun item _ dom -> Domain.add item dom) + current_env Domain.empty + in + debug_print "NEW DISAMBIGUATE INPUT"; + let disambiguate_context = (* cic context -> disambiguate context *) + List.map + (function None -> Cic.Anonymous | Some (name, _) -> name) + context + in + let term_dom = domain_of_term ~context:disambiguate_context term in + debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" + (string_of_domain term_dom)); + let todo_dom = Domain.diff term_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 mqi_handle id in + Hashtbl.add id_choices id choices; + choices) + | Symbol (symb, _) -> + (try Hashtbl.find symbol_choices symb with Not_found -> []) + | Num instance -> !num_choices + in + if choices = [] then raise (No_choices item); + choices + in + (* (3) test an interpretation filling with meta uninterpreted identifiers + *) + let test_env current_env todo_dom = + let filled_env = + Domain.fold + (fun item env -> + Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env) + todo_dom current_env + in + try + let cic_term = + interpretate ~context:disambiguate_context ~env:filled_env term + in + refine metasenv context cic_term + with + | Try_again -> Uncertain + | Invalid_choice -> Ko + in + (* (4) build all possible interpretations *) + let rec aux current_env todo_dom = + if Domain.is_empty todo_dom then + match test_env current_env Domain.empty with + | Ok (term, metasenv) -> [ current_env, term, metasenv ] + | Ko | Uncertain -> [] + else + let item = Domain.choose todo_dom in + let remaining_dom = Domain.remove item todo_dom in + debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item)); + let choices = lookup_choices item in + let rec filter = function + | [] -> [] + | codomain_item :: tl -> + let new_env = Environment.add item codomain_item current_env in + (match test_env new_env remaining_dom with + | Ok (term, metasenv) -> + (if Domain.is_empty remaining_dom then + [ new_env, term, metasenv ] + else + aux new_env remaining_dom) + @ filter tl + | Uncertain -> + (if Domain.is_empty remaining_dom then + [] + else + aux new_env remaining_dom) + @ filter tl + | Ko -> filter tl) + in + filter choices + in + let (choosed_env, choosed_term, choosed_metasenv) = + match aux current_env todo_dom with + | [] -> raise NoWellTypedInterpretation + | [ x ] -> + debug_print "UNA SOLA SCELTA"; + x + | l -> + debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); + let choices = + List.map + (fun (env, _, _) -> + List.map + (fun domain_item -> + let description = + fst (Environment.find domain_item env) + in + (descr_of_domain_item domain_item, description)) + (Domain.elements term_dom)) + l + in + let choosed = C.interactive_interpretation_choice choices in + List.nth l choosed + in + (choosed_env, choosed_metasenv, choosed_term) + + end +