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 test_result =
- | Ok of 'a * Cic.metasenv
- | 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
in
aux 1 context
-let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
- let rec aux ~localize loc (context: Cic.name list) = function
+ let rec aux ~localize loc context = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
let res = aux ~localize loc context term in
if localize then Cic.CicHash.add localization_tbl res loc;
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
if localize then
match body with
CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+ (* since we avoid the letin, the context has no
+ * recfuns in it *)
let l' = List.map (aux ~localize loc context) l in
`AvoidLetIn (n,l')
| _ -> assert false
(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 ()
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
- | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+ | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
- and aux_option ~localize loc (context: Cic.name list) annotation = function
+ and aux_option ~localize loc context annotation = function
| None -> Cic.Implicit annotation
| Some term -> aux ~localize loc context term
in
| Some bo,_ ->
let bo' = Some (interpretate_term [] env None false bo) in
Cic.Constant (name,bo',ty',[],attrs))
+;;
+
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
+ ~localization_tbl
+=
+ let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
+interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
+~localization_tbl
+;;
+
let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
| Ast.AttributedTerm (`Loc loc, term) ->
uniq_domain (domain_of_term ~context term)
let domain_of_obj ~context ast =
+ let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
assert (context = []);
match ast with
| Ast.Theorem (_,_,ty,bo) ->
let domain_of_obj ~context obj =
uniq_domain (domain_of_obj ~context obj)
+let domain_of_ast_term = domain_of_term;;
+
+let domain_of_term ~context term =
+ let context =
+ List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
+ in
+ domain_of_term ~context term
+
(* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
module type Disambiguator =
sig
+ val disambiguate_thing:
+ dbd:HSql.dbd ->
+ context:'context ->
+ metasenv:'metasenv ->
+ subst:'subst ->
+ initial_ugraph:'ugraph ->
+ hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
+ (('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 ->
+ pp_thing:('ast_thing -> string) ->
+ domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+ interpretate_thing:(context:'context ->
+ env:DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ 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,'subst,'ugraph) test_result) ->
+ localization_tbl:'cichash ->
+ string * int * 'ast_thing ->
+ ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
+ list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
+ list * bool
+
val disambiguate_term :
?fresh_instances:bool ->
dbd:HSql.dbd ->
context:Cic.context ->
- metasenv:Cic.metasenv ->
+ 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 = CicUniv.oblivion_ugraph) ~aliases ~universe
+ 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
(thing_txt,thing_txt_prefix_len,thing)
=
debug_print (lazy "DISAMBIGUATE INPUT");
- let disambiguate_context = (* cic context -> disambiguate context *)
- List.map
- (function None -> Cic.Anonymous | Some (name, _) -> name)
- context
- in
debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
- let thing_dom = domain_of_thing ~context:disambiguate_context thing in
+ let thing_dom = domain_of_thing ~context thing in
debug_print
(lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
(*
aux (aux env l) tl in
let filled_env = aux aliases todo_dom in
try
- let localization_tbl = Cic.CicHash.create 503 in
let cic_thing =
- interpretate_thing ~context:disambiguate_context ~env:filled_env
+ interpretate_thing ~context ~env:filled_env
~uri ~is_path:false 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
- (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
CicEnvironment.CircularDependency s ->
failwith "Disambiguate: circular dependency"
- let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
+ let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
+ ~subst ?goal
?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
(text,prefix_len,term)
=
let term =
if fresh_instances then CicNotationUtil.freshen_term term else term
in
- disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
+ let hint = match goal with
+ | 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,s,ug) ->
+ (match t with
+ | Cic.Cast(t,_) -> Ok (t,m,s,ug)
+ | _ -> assert false)
+ | k -> k
+ in
+ let localization_tbl = Cic.CicHash.create 503 in
+ 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))
~refine_thing:refine_term (text,prefix_len,term)
+ ~localization_tbl
+ ~hint
let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
(text,prefix_len,obj)
let obj =
if fresh_instances then CicNotationUtil.freshen_obj obj else obj
in
- disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
+ let hint =
+ (fun _ x -> x),
+ fun k -> k
+ in
+ let localization_tbl = Cic.CicHash.create 503 in
+ 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
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
+ ~localization_tbl
+ ~hint
(text,prefix_len,obj)
+
end
+
projects / helm.git / blobdiff