X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b71e908856ba017df051a5d244f7ab39a1fd9035;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=0c57754f6f4ddbb85e8c6a8eace5a048eb819c11;hpb=1e89c2701ceb5c6d91d966dfb264a15098fcf51c;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 0c57754f6..b71e90885 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -56,25 +56,30 @@ type test_result = | Ko | Uncertain -let refine metasenv context term = +let refine metasenv context term ugraph = (* 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 - Ok (term', metasenv') - with - | CicRefine.Uncertain _ -> - debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; - Uncertain - | CicRefine.RefineFailure _ -> - debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; - Ko + let metasenv, term = + CicMkImplicit.expand_implicits metasenv [] context term in + debug_print (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 _ -> + debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ; + Uncertain,ugraph + | CicRefine.RefineFailure msg -> + debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) msg); + Ko,ugraph let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args - with Not_found -> assert false + with Not_found -> + failwith ("Domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)) (* TODO move it to Cic *) let find_in_environment name context = @@ -190,15 +195,26 @@ let interpretate ~context ~env ast = Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body - | CicAst.Ident (name, subst) -> + | CicAst.Ident (name, subst) + | CicAst.Uri (name, subst) as ast -> + let is_uri = function CicAst.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 if subst <> None then CicTextualParser2.fail loc "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> - let cic = resolve env (Id name) () in + let cic = + if is_uri ast then (* we have the URI, build the term out of it *) + try + CicUtil.term_of_uri name + with UriManager.IllFormedUri _ -> + CicTextualParser2.fail loc "Ill formed URI" + else + resolve env (Id name) () + in let mk_subst uris = let ids_to_uris = List.map (fun uri -> UriManager.name_of_uri uri, uri) uris @@ -214,44 +230,27 @@ let interpretate ~context ~env ast = 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 + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o 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 + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o 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 + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o 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 + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o in Cic.MutConstruct (uri, i, j, mk_subst uris) | Cic.Meta _ | Cic.Implicit _ as t -> (* - prerr_endline (sprintf + debug_print (sprintf "Warning: %s must be instantiated with _[%s] but we do not enforce it" (CicPp.ppterm t) (String.concat "; " @@ -266,6 +265,8 @@ let interpretate ~context ~env ast = CicEnvironment.CircularDependency _ -> raise DisambiguateChoices.Invalid_choice)) | CicAst.Implicit -> Cic.Implicit None + | CicAst.UserInput -> Cic.Implicit (Some `Hole) +(* | CicAst.UserInput -> assert false*) | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -309,6 +310,10 @@ let domain_of_term ~context ast = | CicAst.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in + let get_first_constructor = function + | [] -> [] + | ((head, _), _) :: _ -> [ Id head ] + in let do_branch ((head, args), term) = let (term_context, args_domain) = List.fold_left @@ -325,7 +330,9 @@ let domain_of_term ~context ast = List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches in branches_dom @ outtype_dom @ term_dom @ - (match indty_ident with None -> [] | Some ident -> [ Id ident ]) + (match indty_ident with + | None -> get_first_constructor branches + | 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 @@ -361,6 +368,7 @@ let domain_of_term ~context ast = let dom' = aux loc context term in dom' @ dom) [Id name] subst)) + | CicAst.Uri _ -> [] | CicAst.Implicit -> [] | CicAst.Num (num, i) -> [ Num i ] | CicAst.Meta (index, local_context) -> @@ -368,6 +376,7 @@ let domain_of_term ~context ast = local_context | CicAst.Sort _ -> [] | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + | CicAst.UserInput -> assert false and aux_option loc context = function | None -> [] @@ -402,6 +411,7 @@ let domain_of_term ~context ast = | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term | term -> aux CicAst.dummy_floc context term) + (* dom1 \ dom2 *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) @@ -411,6 +421,21 @@ let domain_diff dom1 dom2 = in List.filter (fun elt -> not (is_in_dom2 elt)) dom1 +module type Disambiguator = +sig + val disambiguate_term : + dbd:Mysql.dbd -> + context:Cic.context -> + metasenv:Cic.metasenv -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:environment -> (* previous interpretation status *) + CicAst.term -> + (environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term* + CicUniv.universe_graph) list (* disambiguated term *) +end + module Make (C: Callbacks) = struct let choices_of_id dbd id = @@ -436,15 +461,16 @@ module Make (C: Callbacks) = try CicUtil.term_of_uri uri with exn -> - prerr_endline uri; - prerr_endline (Printexc.to_string exn); + debug_print uri; + debug_print (Printexc.to_string exn); assert false in fun _ _ _ -> term)) uris - let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term - ~aliases:current_env + let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env + term = debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) @@ -452,6 +478,7 @@ module Make (C: Callbacks) = (function None -> Cic.Anonymous | Some (name, _) -> name) context in + debug_print ("TERM IS: " ^ (CicAstPp.pp_term term)); let term_dom = domain_of_term ~context:disambiguate_context term in debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain term_dom)); @@ -488,7 +515,7 @@ module Make (C: Callbacks) = (fun dom_item -> try let len = List.length (lookup_choices dom_item) in - prerr_endline (sprintf "BENCHMARK %s: %d" + debug_print (sprintf "BENCHMARK %s: %d" (string_of_domain_item dom_item) len); len with No_choices _ -> 0) @@ -506,28 +533,26 @@ module Make (C: Callbacks) = (* (3) test an interpretation filling with meta uninterpreted identifiers *) - let test_env current_env todo_dom univ = + let test_env current_env todo_dom ugraph = let filled_env = List.fold_left (fun env item -> - Environment.add item - ("Implicit", + Environment.add item + ("Implicit", (match item with - | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) - | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) + | 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 - let k = refine metasenv context cic_term in - let new_univ = CicUniv.get_working () in - (k , new_univ ) + let k,ugraph1 = refine metasenv context cic_term ugraph in + (k , ugraph1 ) with - | Try_again -> Uncertain,univ - | DisambiguateChoices.Invalid_choice -> Ko,univ + | Try_again -> Uncertain,ugraph + | DisambiguateChoices.Invalid_choice -> Ko,ugraph in (* (4) build all possible interpretations *) let rec aux current_env todo_dom base_univ = @@ -563,15 +588,14 @@ module Make (C: Callbacks) = in filter base_univ choices in - let base_univ = CicUniv.get_working () in + let base_univ = initial_ugraph 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 ] + [ e,me,t,u] | l -> debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); let choices = @@ -587,20 +611,12 @@ module Make (C: Callbacks) = 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' + List.map (List.nth l) choosed in (* (if benchmark then let res_size = List.length res in - prerr_endline (sprintf + 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 @@ -610,6 +626,28 @@ module Make (C: Callbacks) = res with CicEnvironment.CircularDependency s -> - raise (Failure "e chi la becca sta CircularDependency?"); + failwith "Disambiguate: circular dependency" + end + +module Trivial = +struct + exception Ambiguous_term of string + exception Exit + module Callbacks = + struct + let interactive_user_uri_choice ~selection_mode ?ok + ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = + raise Exit + let interactive_interpretation_choice interp = raise Exit + let input_or_locate_uri ~(title:string) ?id = raise Exit end + module Disambiguator = Make (Callbacks) + let disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph + ?(aliases=DisambiguateTypes.Environment.empty) term = + let ast = CicTextualParser2.parse_term (Stream.of_string term) in + try + Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast + ?initial_ugraph ~aliases + with Exit -> raise (Ambiguous_term term) +end