X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=67b6d115c2cd908daac51084287ce958be60f0c6;hb=a1bfef9d9930c9a136abe0593d8da457b4e21fc3;hp=055630971ee5edd3f5ca29b1aea0260c12429c89;hpb=cbe0302d6b0d2bca6657fa7479a62d0004665612;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 055630971..67b6d115c 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -56,25 +56,35 @@ 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!!!\n<>\n" ^^ + "%s\n<>\n<>\n%s\n<>") + msg (CicPp.ppterm term))); + Ko,ugraph + | CicUnification.UnificationFailure s -> + prerr_endline ("PASSADI QUI: " ^ s); + raise ( CicUnification.UnificationFailure s ) 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 +200,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,40 +235,23 @@ 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 -> (* @@ -362,6 +366,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) -> @@ -404,6 +409,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 *) @@ -446,7 +452,7 @@ module Make (C: Callbacks) = uris let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term - ~aliases:current_env + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env = debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) @@ -508,28 +514,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 = @@ -565,15 +569,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 = @@ -589,15 +592,7 @@ 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 @@ -612,6 +607,6 @@ module Make (C: Callbacks) = res with CicEnvironment.CircularDependency s -> - raise (Failure "e chi la becca sta CircularDependency?"); + failwith "Disambiguate: circular dependency" end