CicRefine.type_of_aux' metasenv context term ugraph in
(Ok (term', metasenv')),ugraph1
with
- | CicRefine.Uncertain _ ->
- debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ | CicRefine.Uncertain s ->
+ debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
Uncertain,ugraph
- | CicRefine.RefineFailure _ ->
- debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
+ | 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 =
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 =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o 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 =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o 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 =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o 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 =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o 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 "; "
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 =
| 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
| 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
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
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 =
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
- ?(initial_ugraph = CicUniv.empty_ugraph) ~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 *)
(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));
(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)
(*
(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
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
+