int *
((Stdpp.location list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Stdpp.location option * string Lazy.t * bool) list
+ (Stdpp.location * string) Lazy.t * bool) list
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
| Symbol (s, _) -> s
| Num i -> string_of_int i
-type ('a,'m) test_result =
- | Ok of 'a * 'm
- | Ko of Stdpp.location option * string Lazy.t
- | Uncertain of Stdpp.location option * string Lazy.t
+type ('term,'metasenv,'subst,'graph) test_result =
+ | Ok of 'term * 'metasenv * 'subst * 'graph
+ | Ko of (Stdpp.location * string) Lazy.t
+ | Uncertain of (Stdpp.location * string) Lazy.t
-let refine_term metasenv context uri term ugraph ~localization_tbl =
+let refine_term metasenv subst context uri term ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
try
let term', _, metasenv',ugraph1 =
CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
- (Ok (term', metasenv')),ugraph1
+ (Ok (term', metasenv',[],ugraph1))
with
exn ->
let rec process_exn loc =
function
- HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+ HExtlib.Localized (loc,exn) -> process_exn loc exn
| CicRefine.Uncertain msg ->
debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Uncertain (loc,msg),ugraph
+ Uncertain (lazy (loc,Lazy.force msg))
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
(CicPp.ppterm term) (Lazy.force msg)));
- Ko (loc,msg),ugraph
+ Ko (lazy (loc,Lazy.force msg))
| exn -> raise exn
in
- process_exn None exn
+ process_exn Stdpp.dummy_loc exn
-let refine_obj metasenv context uri obj ugraph ~localization_tbl =
- assert (context = []);
+let refine_obj metasenv subst context uri obj ugraph ~localization_tbl =
+ assert (context = []);
+ assert (metasenv = []);
+ assert (subst = []);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
try
let obj', metasenv,ugraph =
- CicRefine.typecheck metasenv uri obj ~localization_tbl
+ CicRefine.typecheck metasenv uri obj ~localization_tbl
in
- (Ok (obj', metasenv)),ugraph
+ (Ok (obj', metasenv,[],ugraph))
with
exn ->
let rec process_exn loc =
function
- HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+ HExtlib.Localized (loc,exn) -> process_exn loc exn
| CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
- Uncertain (loc,msg),ugraph
+ debug_print (lazy ("UNCERTAIN!!! [" ^
+ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
+ Uncertain (lazy (loc,Lazy.force msg))
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
(CicPp.ppobj obj) (Lazy.force msg))) ;
- Ko (loc,msg),ugraph
+ Ko (lazy (loc,Lazy.force msg))
| exn -> raise exn
in
- process_exn None exn
+ process_exn Stdpp.dummy_loc exn
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
try
raise (Try_again (lazy "The type of the term to be matched
is still unknown"))
| _ ->
- raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+ raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
| None ->
let rec fst_constructor =
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
- | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
+ | [] -> raise (Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")))
in
(match resolve env (Id (fst_constructor branches)) () with
| Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
raise (Try_again (lazy "The type of the term to be matched
is still unknown"))
| _ ->
- raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+ raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
in
let branches =
if create_dummy_ids then
(function
Ast.Wildcard,term -> ("wildcard",None,[]), term
| Ast.Pattern _,_ ->
- raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+ raise (Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\"")))
) branches
else
match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
[] ->
if unrecognized != [] then
raise (Invalid_choice
- (Some loc,
- lazy
+ (lazy (loc,
("Unrecognized constructors: " ^
- String.concat " " unrecognized)))
+ String.concat " " unrecognized))))
else if useless > 0 then
raise (Invalid_choice
- (Some loc,
- lazy
+ (lazy (loc,
("The last " ^ string_of_int useless ^
"case" ^ if useless > 1 then "s are" else " is" ^
- " unused")))
+ " unused"))))
else
[]
| (Ast.Wildcard,_)::tl when not unused ->
[] ->
raise
(Invalid_choice
- (Some loc, lazy ("Missing case: " ^ name)))
+ (lazy (loc, ("Missing case: " ^ name))))
| ((Ast.Wildcard, _) as branch :: _) as branches ->
branch, branches
| (Ast.Pattern (name',_,_),_) as branch :: tl
else
raise
(Invalid_choice
- (Some loc,
- lazy ("Wrong number of arguments for " ^ name)))
+ (lazy (loc,"Wrong number of arguments for " ^
+ name)))
| Ast.Wildcard,term ->
let rec mk_lambdas =
function
(try
List.assoc s ids_to_uris, aux ~localize loc context term
with Not_found ->
- raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+ raise (Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
subst
| None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
in
*)
t
| _ ->
- raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
+ raise (Invalid_choice (lazy (loc, "??? Can this happen?")))
with
CicEnvironment.CircularDependency _ ->
- raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
+ raise (Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
| CicNotationPt.Implicit -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
dbd:HSql.dbd ->
context:'context ->
metasenv:'metasenv ->
+ subst:'subst ->
initial_ugraph:'ugraph ->
hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
- (('refined_thing,'metasenv) test_result -> 'ugraph ->
- ('refined_thing,'metasenv) test_result * 'ugraph) ->
+ (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+ ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
universe:DisambiguateTypes.codomain_item list
DisambiguateTypes.Environment.t option ->
uri:'uri ->
is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
refine_thing:('metasenv ->
+ 'subst ->
'context ->
'uri ->
'raw_thing ->
- 'ugraph -> localization_tbl:'cichash -> ('refined_thing,
- 'metasenv) test_result * 'ugraph) ->
+ 'ugraph -> localization_tbl:'cichash ->
+ ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
- list * 'metasenv * 'refined_thing * 'ugraph)
+ list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
list * bool
val disambiguate_term :
?fresh_instances:bool ->
dbd:HSql.dbd ->
context:Cic.context ->
- metasenv:Cic.metasenv -> ?goal:int ->
+ metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
+ ?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
CicNotationPt.term disambiguator_input ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
+ Cic.substitution *
Cic.term*
CicUniv.universe_graph) list * (* disambiguated term *)
bool
CicNotationPt.term CicNotationPt.obj disambiguator_input ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
+ Cic.substitution *
Cic.obj *
CicUniv.universe_graph) list * (* disambiguated obj *)
bool
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
- let disambiguate_thing ~dbd ~context ~metasenv
- ~initial_ugraph ~hint
+ let disambiguate_thing ~dbd ~context ~metasenv ~subst
+ ~initial_ugraph:base_univ ~hint
~aliases ~universe
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~localization_tbl
in
let cic_thing = (fst hint) metasenv cic_thing in
let foo () =
- let k,ugraph1 =
- refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
+ let k =
+ refine_thing metasenv subst
+ context uri cic_thing ugraph ~localization_tbl
in
- let k, ugraph1 = (snd hint) k ugraph1 in
- (k , ugraph1 )
+ let k = (snd hint) k in
+ k
in refine_profiler.HExtlib.profile foo ()
with
- | Try_again msg -> Uncertain (None,msg), ugraph
- | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
+ | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+ | Invalid_choice loc_msg -> Ko loc_msg
in
(* (4) build all possible interpretations *)
let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
(* aux returns triples Ok/Uncertain/Ko *)
(* rem_dom is the concatenation of all the remainin domains *)
- let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
+ let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
match todo_dom with
| [] ->
assert (lookup_in_todo_dom = None);
(match test_env aliases rem_dom base_univ with
- | Ok (thing, metasenv),new_univ ->
- [ aliases, diff, metasenv, thing, new_univ ], [], []
- | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
- | Uncertain (loc,msg),new_univ ->
- [],[aliases,diff,loc,msg,new_univ],[])
+ | Ok (thing, metasenv,subst,new_univ) ->
+ [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
+ | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
+ | Uncertain loc_msg ->
+ [],[aliases,diff,loc_msg],[])
| Node (locs,item,inner_dom) :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
(string_of_domain_item item)));
match choices with
[] ->
[], [],
- [aliases, diff, Some (List.hd locs),
- lazy ("No choices for " ^ string_of_domain_item item),
+ [aliases, diff,
+ (lazy (List.hd locs,
+ "No choices for " ^ string_of_domain_item item)),
true]
(*
| [codomain_item] ->
| _::_ ->
let mark_not_significant failures =
List.map
- (fun (env, diff, loc, msg, _b) ->
- env, diff, loc, msg, false)
+ (fun (env, diff, loc_msg, _b) ->
+ env, diff, loc_msg, false)
failures in
let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
if ok_l <> [] || uncertain_l <> [] then
ok_l,uncertain_l,mark_not_significant error_l
else
outcome in
- let rec filter univ = function
+ let rec filter = function
| [] -> [],[],[]
| codomain_item :: tl ->
debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
let new_env = Environment.add item codomain_item aliases in
let new_diff = (item,codomain_item)::diff in
(match
- test_env new_env (inner_dom@remaining_dom@rem_dom) univ
+ test_env new_env
+ (inner_dom@remaining_dom@rem_dom) base_univ
with
- | Ok (thing, metasenv),new_univ ->
+ | Ok (thing, metasenv,subst,new_univ) ->
let res =
(match inner_dom with
| [] ->
- [new_env,new_diff,metasenv,thing,new_univ], [], []
+ [new_env,new_diff,metasenv,subst,thing,new_univ],
+ [], []
| _ ->
aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom) new_univ
+ (remaining_dom@rem_dom)
)
in
- res @@ filter univ tl
- | Uncertain (loc,msg),new_univ ->
+ res @@ filter tl
+ | Uncertain loc_msg ->
let res =
(match inner_dom with
- | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
+ | [] -> [],[new_env,new_diff,loc_msg],[]
| _ ->
aux new_env new_diff None inner_dom
- (remaining_dom@rem_dom) new_univ
+ (remaining_dom@rem_dom)
)
in
- res @@ filter univ tl
- | Ko (loc,msg),_ ->
- let res = [],[],[new_env,new_diff,loc,msg,true] in
- res @@ filter univ tl)
+ res @@ filter tl
+ | Ko loc_msg ->
+ let res = [],[],[new_env,new_diff,loc_msg,true] in
+ res @@ filter tl)
in
let ok_l,uncertain_l,error_l =
- classify_errors (filter base_univ choices)
+ classify_errors (filter choices)
in
let res_after_ok_l =
List.fold_right
- (fun (env,diff,_,_,univ) res ->
- aux env diff None remaining_dom rem_dom univ @@ res
+ (fun (env,diff,_,_,_,_) res ->
+ aux env diff None remaining_dom rem_dom @@ res
) ok_l ([],[],error_l)
in
List.fold_right
- (fun (env,diff,_,_,univ) res ->
- aux env diff None remaining_dom rem_dom univ @@ res
+ (fun (env,diff,_) res ->
+ aux env diff None remaining_dom rem_dom @@ res
) uncertain_l res_after_ok_l
in
- let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+ let aux' aliases diff lookup_in_todo_dom todo_dom =
match test_env aliases todo_dom base_univ with
- | Ok _,_
- | Uncertain _,_ ->
- aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
- | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
- let base_univ = initial_ugraph in
+ | Ok _
+ | Uncertain _ ->
+ aux aliases diff lookup_in_todo_dom todo_dom []
+ | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
try
let res =
- match aux' aliases [] None todo_dom base_univ with
+ match aux' aliases [] None todo_dom with
| [],uncertain,errors ->
let errors =
List.map
- (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
+ (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
) uncertain @ errors
in
let errors =
List.map
- (fun (env,diff,loc,msg,significant) ->
+ (fun (env,diff,loc_msg,significant) ->
let env' =
filter_map_domain
(fun locs domain_item ->
Not_found -> None)
thing_dom
in
- env',diff,loc,msg,significant
+ env',diff,loc_msg,significant
) errors
in
raise (NoWellTypedInterpretation (0,errors))
- | [_,diff,metasenv,t,ugraph],_,_ ->
+ | [_,diff,metasenv,subst,t,ugraph],_,_ ->
debug_print (lazy "SINGLE INTERPRETATION");
- [diff,metasenv,t,ugraph], false
+ [diff,metasenv,subst,t,ugraph], false
| l,_,_ ->
debug_print
(lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
let choices =
List.map
- (fun (env, _, _, _, _) ->
+ (fun (env, _, _, _, _, _) ->
map_domain
(fun locs domain_item ->
let description =
C.interactive_interpretation_choice
thing_txt thing_txt_prefix_len choices
in
- (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
+ (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
+ choosed),
true
in
res
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?goal
+ ~subst ?goal
?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
(text,prefix_len,term)
=
if fresh_instances then CicNotationUtil.freshen_term term else term
in
let hint = match goal with
- | None -> (fun _ x -> x), fun k u -> k, u
+ | None -> (fun _ x -> x), fun k -> k
| Some i ->
(fun metasenv t ->
let _,c,ty = CicUtil.lookup_meta i metasenv in
assert(c=context);
Cic.Cast(t,ty)),
function
- | Ok (t,m) -> fun ug ->
+ | Ok (t,m,s,ug) ->
(match t with
- | Cic.Cast(t,_) -> Ok (t,m), ug
+ | Cic.Cast(t,_) -> Ok (t,m,s,ug)
| _ -> assert false)
- | k -> fun ug -> k, ug
+ | k -> k
in
let localization_tbl = Cic.CicHash.create 503 in
- disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
+ disambiguate_thing ~dbd ~context ~metasenv ~subst
+ ~initial_ugraph ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
in
let hint =
(fun _ x -> x),
- fun k u -> k, u
+ fun k -> k
in
let localization_tbl = Cic.CicHash.create 503 in
- disambiguate_thing ~dbd ~context:[] ~metasenv:[]
+ disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[]
~aliases ~universe ~uri
~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
~initial_ugraph:CicUniv.empty_ugraph
projects / helm.git / blobdiff