(** raised when an environment is not enough informative to decide *)
exception Try_again
-let debug = true
+let debug = false
let debug_print = if debug then prerr_endline else ignore
(*
| 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
+ | 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 =
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
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 ->
(*
| CicAst.Sort `CProp -> Cic.Sort Cic.CProp
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
+ | CicAst.UserInput -> assert false
and aux_option loc context = function
| None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term
in
match ast with
| CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
- | term -> aux (-1, -1) context term
+ | term -> aux CicAst.dummy_floc context term
let domain_of_term ~context ast =
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
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) ->
local_context
| CicAst.Sort _ -> []
| CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+ | CicAst.UserInput -> assert false
and aux_option loc context = function
| None -> []
rev_uniq
(match ast with
| CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
- | term -> aux (-1, -1) context term)
+ | term -> aux CicAst.dummy_floc context term)
(* dom1 \ dom2 *)
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
- let uris' =
+ let choices_of_id dbd id =
+ let uris = MetadataQuery.locate ~dbd id in
+ let uris =
match uris with
| [] ->
[UriManager.string_of_uri (C.input_or_locate_uri
(uri,
let term =
try
- HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
- with _ -> assert false
+ CicUtil.term_of_uri uri
+ with exn ->
+ prerr_endline uri;
+ prerr_endline (Printexc.to_string exn);
+ assert false
in
fun _ _ _ -> term))
- uris'
+ uris
- let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
+ let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)
(try
Hashtbl.find id_choices id
with Not_found ->
- let choices = choices_of_id mqi_handle id in
+ let choices = choices_of_id dbd id in
Hashtbl.add id_choices id choices;
choices)
| Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
(* (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 =
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 =
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
res
with
CicEnvironment.CircularDependency s ->
- raise (Failure "e chi la becca sta CircularDependency?");
+ failwith "Disambiguate: circular dependency"
end
projects / helm.git / blobdiff