X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=93795f96ebb780eba031192d03ac15a16561a774;hb=fd648e40eb2c9c5b29cfa4408459511a74898d1d;hp=f75941475563d0ec45e87f8f2dc25019f921430e;hpb=597bf5f989f410aea68d38ba6e32b9498493faf6;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index f75941475..93795f96e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -37,6 +37,15 @@ exception Try_again let debug = true let debug_print = if debug then prerr_endline else ignore +(* + (** print benchmark information *) +let benchmark = true +let max_refinements = ref 0 (* benchmarking is not thread safe *) +let actual_refinements = ref 0 +let domain_size = ref 0 +let choices_avg = ref 0. +*) + let descr_of_domain_item = function | Id s -> s | Symbol (s, _) -> s @@ -48,7 +57,8 @@ type test_result = | Uncertain let refine metasenv context term = - let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in +(* if benchmark then incr actual_refinements; *) + 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 @@ -57,13 +67,14 @@ let refine metasenv context term = | CicRefine.Uncertain _ -> debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain - | _ -> - (* TODO we should catch only the RefineFailure excecption *) + | CicRefine.RefineFailure _ -> debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; Ko let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = - snd (Environment.find item env) env num args + try + snd (Environment.find item env) env num args + with Not_found -> assert false (* TODO move it to Cic *) let find_in_environment name context = @@ -102,7 +113,7 @@ let interpretate ~context ~env ast = let cic_body = do_branch' (name :: context) tl in let typ = match typ with - | None -> Cic.Implicit + | None -> Cic.Implicit (Some `Type) | Some typ -> aux loc context typ in Cic.Lambda (name, typ, cic_body) @@ -110,10 +121,23 @@ let interpretate ~context ~env ast = do_branch' context args in let (indtype_uri, indtype_no) = - match resolve env (Id indty_ident) () with - | Cic.MutInd (uri, tyno, _) -> uri, tyno - | Cic.Implicit -> raise Try_again - | _ -> raise DisambiguateChoices.Invalid_choice + match 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 DisambiguateChoices.Invalid_choice) + | None -> + let fst_constructor = + match branches with + | ((head, _), _) :: _ -> head + | [] -> raise DisambiguateChoices.Invalid_choice + in + (match resolve env (Id fst_constructor) () with + | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> + (indtype_uri, indtype_no) + | Cic.Implicit _ -> raise Try_again + | _ -> raise DisambiguateChoices.Invalid_choice) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -167,15 +191,81 @@ let interpretate ~context ~env ast = in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body | CicAst.Ident (name, subst) -> - (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in - if subst <> [] then + if subst <> None then CicTextualParser2.fail loc "Explicit substitutions not allowed here"; Cic.Rel index - with Not_found -> resolve env (Id name) ()) - | CicAst.Implicit -> Cic.Implicit + with Not_found -> + let cic = resolve env (Id name) () in + let mk_subst uris = + let ids_to_uris = + List.map (fun uri -> UriManager.name_of_uri uri, uri) uris + in + (match subst with + | Some subst -> + List.map + (fun (s, term) -> + (try + List.assoc s ids_to_uris, aux loc context term + with Not_found -> + raise DisambiguateChoices.Invalid_choice)) + subst + | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) + in + (* the try is for CicTypeChecker.typecheck *) + (try + match cic with + | Cic.Const (uri, []) -> + let uris = + match CicEnvironment.get_obj uri with + (*match CicTypeChecker.typecheck uri with*) + | Cic.Constant (_, _, _, uris) -> uris + | _ -> assert false + in + Cic.Const (uri, mk_subst uris) + | Cic.Var (uri, []) -> + let uris = + match CicEnvironment.get_obj uri with + (*match CicTypeChecker.typecheck uri with*) + | Cic.Variable (_, _, _, uris) -> uris + | _ -> assert false + in + Cic.Var (uri, mk_subst uris) + | Cic.MutInd (uri, i, []) -> + let uris = + match CicEnvironment.get_obj uri with + (*match CicTypeChecker.typecheck uri with*) + | Cic.InductiveDefinition (_, uris, _) -> uris + | _ -> assert false + in + Cic.MutInd (uri, i, mk_subst uris) + | Cic.MutConstruct (uri, i, j, []) -> + let uris = + match CicEnvironment.get_obj uri with + (*match CicTypeChecker.typecheck uri with*) + | Cic.InductiveDefinition (_, uris, _) -> uris + | _ -> assert false + in + Cic.MutConstruct (uri, i, j, mk_subst uris) + | Cic.Meta _ | Cic.Implicit _ as t -> +(* + prerr_endline (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 ^ " := " ^ CicAstPp.pp_term term) + subst))); +*) + t + | _ -> + raise DisambiguateChoices.Invalid_choice + with + CicEnvironment.CircularDependency _ -> + raise DisambiguateChoices.Invalid_choice)) + | CicAst.Implicit -> Cic.Implicit None | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -186,12 +276,12 @@ let interpretate ~context ~env ast = Cic.Meta (index, cic_subst) | CicAst.Sort `Prop -> Cic.Sort Cic.Prop | CicAst.Sort `Set -> Cic.Sort Cic.Set - | CicAst.Sort `Type -> Cic.Sort Cic.Type + | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) | CicAst.Sort `CProp -> Cic.Sort Cic.CProp | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () and aux_option loc context = function - | None -> Cic.Implicit + | None -> Cic.Implicit (Some `Type) | Some term -> aux loc context term in match ast with @@ -207,10 +297,15 @@ let domain_of_term ~context ast = | CicAst.AttributedTerm (_, term) -> aux loc context term | CicAst.Appl terms -> List.fold_left (fun dom term -> aux loc context term @ dom) [] terms - | CicAst.Binder (_, (var, typ), body) -> + | CicAst.Binder (kind, (var, typ), body) -> + let kind_dom = + match kind with + | `Exists -> [ Symbol ("exists", 0) ] + | _ -> [] + in let type_dom = aux_option loc context typ in let body_dom = aux loc (var :: context) body in - body_dom @ type_dom + body_dom @ type_dom @ kind_dom | CicAst.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in @@ -229,7 +324,8 @@ let domain_of_term ~context ast = let branches_dom = List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches in - branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ] + branches_dom @ outtype_dom @ term_dom @ + (match indty_ident with None -> [] | Some ident -> [ Id ident ]) | CicAst.LetIn ((var, typ), body, where) -> let body_dom = aux loc context body in let type_dom = aux_option loc context typ in @@ -249,14 +345,22 @@ let domain_of_term ~context ast = in where_dom @ defs_dom | CicAst.Ident (name, subst) -> - (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in - if subst <> [] then + if subst <> None then CicTextualParser2.fail loc - "Explicit substitutions not allowed here"; - [] - with Not_found -> [ Id name ]) + "Explicit substitutions not allowed here" + else + [] + with Not_found -> + (match subst with + | None -> [Id name] + | Some subst -> + List.fold_left + (fun dom (_, term) -> + let dom' = aux loc context term in + dom' @ dom) + [Id name] subst)) | CicAst.Implicit -> [] | CicAst.Num (num, i) -> [ Num i ] | CicAst.Meta (index, local_context) -> @@ -318,18 +422,11 @@ module Make (C: Callbacks) = (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."))] + ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())] | [uri] -> [uri] | _ -> C.interactive_user_uri_choice ~selection_mode:`MULTIPLE @@ -384,79 +481,138 @@ module Make (C: Callbacks) = if choices = [] then raise (No_choices item); choices in + +(* + (* *) + let _ = + if benchmark then begin + let per_item_choices = + List.map + (fun dom_item -> + try + let len = List.length (lookup_choices dom_item) in + prerr_endline (sprintf "BENCHMARK %s: %d" + (string_of_domain_item dom_item) len); + len + with No_choices _ -> 0) + term_dom + in + max_refinements := List.fold_left ( * ) 1 per_item_choices; + actual_refinements := 0; + domain_size := List.length term_dom; + choices_avg := + (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size) + end + in + (* *) +*) + (* (3) test an interpretation filling with meta uninterpreted identifiers *) - let test_env current_env todo_dom = + let test_env current_env todo_dom univ = let filled_env = List.fold_left (fun env item -> - Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env) + Environment.add item + ("Implicit", + (match item with + | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) current_env todo_dom in try + CicUniv.set_working univ; let cic_term = interpretate ~context:disambiguate_context ~env:filled_env term in - refine metasenv context cic_term + let k = refine metasenv context cic_term in + let new_univ = CicUniv.get_working () in + (k , new_univ ) with - | Try_again -> Uncertain - | DisambiguateChoices.Invalid_choice -> Ko + | Try_again -> Uncertain,univ + | DisambiguateChoices.Invalid_choice -> Ko,univ in (* (4) build all possible interpretations *) - let rec aux current_env todo_dom = + let rec aux current_env todo_dom base_univ = match todo_dom with | [] -> - (match test_env current_env [] with - | Ok (term, metasenv) -> [ current_env, term, metasenv ] - | Ko | Uncertain -> []) + (match test_env current_env [] base_univ with + | Ok (term, metasenv),new_univ -> + [ current_env, metasenv, term, new_univ ] + | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item)); + (string_of_domain_item item)); let choices = lookup_choices item in - let rec filter = function + 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 with - | Ok (term, metasenv) -> + (match test_env new_env remaining_dom univ with + | Ok (term, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, term, metasenv ] - | _ -> aux new_env remaining_dom) @ filter tl - | Uncertain -> + | [] -> [ new_env, metasenv, term, new_univ ] + | _ -> aux new_env remaining_dom new_univ )@ + filter univ tl + | Uncertain,new_univ -> (match remaining_dom with | [] -> [] - | _ -> 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)) - term_dom) - l + | _ -> aux new_env remaining_dom new_univ )@ + filter univ tl + | Ko,_ -> filter univ tl) in - let choosed = C.interactive_interpretation_choice choices in - List.nth l choosed + filter base_univ choices in - (choosed_env, choosed_metasenv, choosed_term) - + let base_univ = CicUniv.get_working () in + try + let res = + match aux current_env todo_dom base_univ with + | [] -> raise NoWellTypedInterpretation + | [ e,me,t,u ] as l -> + debug_print "UNA SOLA SCELTA"; + CicUniv.set_working u; + [ e,me,t ] + | 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)) + term_dom) + l + in + let choosed = C.interactive_interpretation_choice choices in + let l' = List.map (List.nth l) choosed in + match l' with + [] -> assert false + | [e,me,t,u] -> + CicUniv.set_working u; + (*CicUniv.print_working_graph ();*) + [e,me,t] + | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *) + List.map (fun (e,me,t,u) -> (e,me,t)) l' + in +(* + (if benchmark then + let res_size = List.length res in + prerr_endline (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 + with + CicEnvironment.CircularDependency s -> + raise (Failure "e chi la becca sta CircularDependency?"); end