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
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
+ 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
?(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
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+ ?initial_ugraph ~aliases
with Exit -> raise (Ambiguous_term term)
end