X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=637636e0b8b8146d62964eb8710cd7947f7bbc75;hb=3289eda62f4b44bc5043abd2acff602f7a8e5f26;hp=bc78f55eddc0888d80dba682c7b3a6edeeef27bf;hpb=dccf88890f1f9f8c8139f67aa7a26f8339b13502;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index bc78f55ed..637636e0b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -57,8 +57,7 @@ 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 @@ -182,10 +181,9 @@ 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 @@ -195,55 +193,67 @@ let interpretate ~context ~env ast = let ids_to_uris = List.map (fun uri -> UriManager.name_of_uri uri, uri) uris in - List.map - (fun (s, term) -> - (try - List.assoc s ids_to_uris, aux loc context term - with Not_found -> raise DisambiguateChoices.Invalid_choice)) - subst + (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 - (match cic with - | Cic.Const (uri, []) -> - let uris = - match CicEnvironment.get_obj 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 - | 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 - | 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 - | Cic.InductiveDefinition (_, uris, _) -> uris - | _ -> assert false - in - Cic.MutConstruct (uri, i, j, mk_subst uris) - | Cic.Meta _ | Cic.Implicit _ as t -> + (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))); + 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)) + 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) -> @@ -255,7 +265,7 @@ 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)) () @@ -324,19 +334,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"; - [] + "Explicit substitutions not allowed here" + else + [] with Not_found -> - List.fold_left - (fun dom (_, term) -> - let dom' = aux loc context term in - dom' @ dom) - [ Id name ] subst) + (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) -> @@ -398,18 +411,11 @@ module Make (C: Callbacks) = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in - HelmLogger.log (`Msg (`T "Locate query:")); - MQueryUtil.text_of_query - (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s))) - "" query; - HelmLogger.log (`Msg (`T "Result:")); - MQueryUtil.text_of_result - (fun s -> HelmLogger.log (`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 @@ -466,7 +472,7 @@ module Make (C: Callbacks) = 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 -> @@ -478,55 +484,64 @@ module Make (C: Callbacks) = 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, metasenv, term ] - | 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, metasenv, term ] - | _ -> 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) + | _ -> aux new_env remaining_dom new_univ )@ + filter univ tl + | Ko,_ -> filter univ tl) in - filter choices + filter base_univ choices in - match aux current_env todo_dom with + let base_univ = CicUniv.get_working () in + try + match aux current_env todo_dom base_univ with | [] -> raise NoWellTypedInterpretation - | [ _ ] as l -> + | [ e,me,t,u ] as l -> debug_print "UNA SOLA SCELTA"; - l + CicUniv.set_working u; + [ e,me,t ] | l -> debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); let choices = List.map - (fun (env, _, _) -> + (fun (env, _, _, _) -> List.map (fun domain_item -> let description = @@ -537,7 +552,17 @@ module Make (C: Callbacks) = l in let choosed = C.interactive_interpretation_choice choices in - List.map (List.nth l) choosed - + 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' + with + CicEnvironment.CircularDependency s -> + raise (Failure "e chi la becca sta CircularDependency?"); end