| Symbol (s, _) -> s
| Num i -> string_of_int i
-type ('a,'m) test_result =
- | Ok of 'a * 'm
+type ('term,'metasenv,'subst,'graph) test_result =
+ | Ok of 'term * 'metasenv * 'subst * 'graph
| Ko of Stdpp.location option * string Lazy.t
| Uncertain of Stdpp.location option * 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 =
HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
| CicRefine.Uncertain msg ->
debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Uncertain (loc,msg),ugraph
+ Uncertain (loc,msg)
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
(CicPp.ppterm term) (Lazy.force msg)));
- Ko (loc,msg),ugraph
+ Ko (loc,msg)
| exn -> raise exn
in
process_exn None 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
| 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 (loc,msg)
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
(CicPp.ppobj obj) (Lazy.force msg))) ;
- Ko (loc,msg),ugraph
+ Ko (loc,msg)
| exn -> raise exn
in
process_exn None exn
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 (None,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)));
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),_ ->
+ res @@ filter tl
+ | Ko (loc,msg) ->
let res = [],[],[new_env,new_diff,loc,msg,true] in
- res @@ filter univ tl)
+ 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 =
) 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
type domain = domain_tree list
and domain_tree =
Node of Stdpp.location list * DisambiguateTypes.domain_item * domain
-type ('a,'m) test_result =
- | Ok of 'a * 'm
+
+type ('term,'metasenv,'subst,'graph) test_result =
+ | Ok of 'term * 'metasenv * 'subst * 'graph
| Ko of Stdpp.location option * string Lazy.t
| Uncertain of Stdpp.location option * string Lazy.t
+
exception Try_again of string Lazy.t
val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
val disambiguate_thing:
dbd:HSql.dbd ->
context:'context ->
- metasenv:'metasenv ->
+ 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 ->
env:DisambiguateTypes.codomain_item
DisambiguateTypes.Environment.t ->
uri:'uri ->
- is_path:bool ->
- 'ast_thing ->
- localization_tbl:'cichash -> 'raw_thing) ->
+ 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
- (** @param fresh_instances when set to true fresh instances will be generated
- * for each number _and_ symbol in the disambiguation domain. Instances of the
- * input AST will be ignored. Defaults to false. *)
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.term *
+ Cic.substitution *
+ Cic.term*
CicUniv.universe_graph) list * (* disambiguated term *)
- bool (* has interactive_interpretation_choice been invoked? *)
+ bool
- (** @param fresh_instances as per disambiguate_term *)
val disambiguate_obj :
?fresh_instances:bool ->
dbd:HSql.dbd ->
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 (* has interactive_interpretation_choice been invoked? *)
-
+ bool
end
module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
HLog.debug debug; assert false
(** @param term not meaningful when context is given *)
-let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv term =
+let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+term =
let lexicon_status = !lexicon_status_ref in
- let (diff, metasenv, cic, _) =
+ let (diff, metasenv, subst, cic, _) =
singleton "first"
(GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
~aliases:lexicon_status.LexiconEngine.aliases
?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~context ~metasenv (text,prefix_len,term))
+ ~context ~metasenv ~subst:[] (text,prefix_len,term))
in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status_ref := lexicon_status;
- metasenv,cic
+ metasenv,(*subst,*) cic
;;
(** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
(fun context metasenv ugraph ->
let lexicon_status = !lexicon_status_ref in
- let (diff, metasenv, cic, ugraph) =
+ let (diff, metasenv, _, cic, ugraph) =
singleton "second"
(GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~context ~metasenv ?goal
+ ~context ~metasenv ~subst:[] ?goal
(text,prefix_len,term)) in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status_ref := lexicon_status;
| None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
- let (diff, metasenv, cic, _) =
+ let (diff, metasenv, _, cic, _) =
singleton "third"
(GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
~aliases:lexicon_status.LexiconEngine.aliases
in
aux d
in
- (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
+ (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
user_asked
let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
+ (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
user_asked
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?goal ?initial_ugraph
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
~aliases ~universe term
=
assert (fresh_instances = None);
let f =
- Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?goal ?initial_ugraph
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
in
disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff term
let debug_print _ = ();;
-let refine_term metasenv context uri term ugraph ~localization_tbl =
-(* if benchmark then incr actual_refinements; *)
+let refine_term metasenv subst context uri term ugraph ~localization_tbl =
assert (uri=None);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
- try
- let term', _, metasenv',ugraph1 =
- NCicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
- (Disambiguate.Ok (term', metasenv')),ugraph1
- with
- exn ->
- let rec process_exn loc =
- function
- HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Disambiguate.Uncertain (loc,msg),ugraph
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (Lazy.force msg)));
- Disambiguate.Ko (loc,msg),ugraph
- | exn -> raise exn
- in
- process_exn None exn
+ debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
+ (NCicPp.ppterm ~metasenv ~subst ~context term)));
+ try
+ let localise t =
+ try NCic.NCicHash.find localization_tbl t
+ with Not_found -> assert false
+ in
+ let metasenv, subst, term, ty =
+ NCicRefine.typeof metasenv subst context term None ~localise
+ in
+ Disambiguate.Ok (term, metasenv, subst, ())
+ with
+ | NCicRefine.Uncertain (loc, msg) ->
+ debug_print (lazy ("UNCERTAIN: [" ^ Lazy.force msg ^ "] " ^
+ NCicPp.ppterm ~metasenv ~subst ~context term)) ;
+ Disambiguate.Uncertain (loc,msg,())
+ | NCicRefine.RefineFailure (loc,msg) ->
+ debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
+ (NCicPp.ppterm ~metasenv ~subst ~context term) (Lazy.force msg)));
+ Disambiguate.Ko (loc,msg,())
+;;
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
try
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | Cic.Name hd :: tl when hd = name -> acc
+ | Cic.Name hd :: _ when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+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 = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
let res = aux ~localize loc context term in
- if localize then Cic.CicHash.add localization_tbl res loc;
+ if localize then NCic.NCicHash.add localization_tbl res loc;
res
| CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
| CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
resolve env (Symbol (symb, i)) ~args:cic_args ()
| CicNotationPt.Appl terms ->
- Cic.Appl (List.map (aux ~localize loc context) terms)
+ NCic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
let cic_type = aux_option ~localize loc context (Some `Type) typ in
let cic_name = CicNotationUtil.cic_name_of_name var in
let cic_body = aux ~localize loc (cic_name :: context) body in
(match binder_kind with
- | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
+ | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
| `Pi
- | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
+ | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
resolve env (Symbol ("exists", 0))
- ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
+ ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let cic_outtype = aux_option ~localize loc context None outtype in
- let do_branch ((head, _, args), term) =
+ let do_branch ((_, _, args), term) =
let rec do_branch' context = function
| [] -> aux ~localize loc context term
| (name, typ) :: tl ->
let cic_body = do_branch' (cic_name :: context) tl in
let typ =
match typ with
- | None -> Cic.Implicit (Some `Type)
+ | None -> NCic.Implicit (Some `Type)
| Some typ -> aux ~localize loc context typ
in
- Cic.Lambda (cic_name, typ, cic_body)
+ NCic.Lambda (cic_name, typ, cic_body)
in
do_branch' context args
in
match indty_ident with
| Some (indty_ident, _) ->
(match resolve env (Id indty_ident) () with
- | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
- | Cic.Implicit _ ->
+ | NCic.MutInd (uri, tyno, _) -> (uri, tyno)
+ | NCic.Implicit _ ->
raise (Disambiguate.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 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, _, _) ->
+ | NCic.MutConstruct (indtype_uri, indtype_no, _, _) ->
(indtype_uri, indtype_no)
- | Cic.Implicit _ ->
+ | NCic.Implicit _ ->
raise (Disambiguate.Try_again (lazy "The type of the term to be matched
is still unknown"))
| _ ->
) branches
else
match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
- Cic.InductiveDefinition (il,_,leftsno,_) ->
+ NCic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
List.nth il indtype_no
in
let rec count_prod t =
match CicReduction.whd [] t with
- Cic.Prod (_, _, t) -> 1 + (count_prod t)
+ NCic.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0
in
let rec sort branches cl =
sort branches cl
| _ -> assert false
in
- Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
+ NCic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
(List.map do_branch branches))
| CicNotationPt.Cast (t1, t2) ->
let cic_t1 = aux ~localize loc context t1 in
let cic_t2 = aux ~localize loc context t2 in
- Cic.Cast (cic_t1, cic_t2)
+ NCic.Cast (cic_t1, cic_t2)
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
let cic_typ =
match typ with
- | None -> Cic.Implicit (Some `Type)
+ | None -> NCic.Implicit (Some `Type)
| Some t -> aux ~localize loc context t
in
let cic_body = aux ~localize loc (cic_name :: context) body in
- Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
+ NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
| CicNotationPt.LetRec (kind, defs, body) ->
let context' =
List.fold_left
let cic_body =
let unlocalized_body = aux ~localize:false loc context' body in
match unlocalized_body with
- Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
- | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
+ NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
+ | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
(try
let l' =
List.map
(HExtlib.map_option (add_binders `Pi) typ) in
let name =
match CicNotationUtil.cic_name_of_name name with
- | Cic.Anonymous ->
+ | NCic.Anonymous ->
CicNotationPt.fail loc
"Recursive functions cannot be anonymous"
- | Cic.Name name -> name
+ | NCic.Name name -> name
in
(name, decr_idx, cic_type, cic_body))
defs
in
let fix_or_cofix n =
match kind with
- `Inductive -> Cic.Fix (n,inductiveFuns)
+ `Inductive -> NCic.Fix (n,inductiveFuns)
| `CoInductive ->
let coinductiveFuns =
List.map
(fun (name, _, typ, body) -> name, typ, body)
inductiveFuns
in
- Cic.CoFix (n,coinductiveFuns)
+ NCic.CoFix (n,coinductiveFuns)
in
let counter = ref ~-1 in
- let build_term funs (var,_,ty,_) t =
+ let build_term _ (var,_,ty,_) t =
incr counter;
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
+ NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
in
(match cic_body with
`AvoidLetInNoAppl n ->
fix_or_cofix n'
| `AvoidLetIn (n,l) ->
let n' = List.length inductiveFuns - n in
- Cic.Appl (fix_or_cofix n'::l)
+ NCic.Appl (fix_or_cofix n'::l)
| `AddLetIn cic_body ->
List.fold_right (build_term inductiveFuns) inductiveFuns
cic_body)
let index = find_in_context name context in
if subst <> None then
CicNotationPt.fail loc "Explicit substitutions not allowed here";
- Cic.Rel index
+ NCic.Rel index
with Not_found ->
let cic =
if is_uri ast then (* we have the URI, build the term out of it *)
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"))))
subst
- | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
+ | None -> List.map (fun uri -> uri, NCic.Implicit None) uris)
in
(try
match cic with
- | Cic.Const (uri, []) ->
+ | NCic.Const (uri, []) ->
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
- Cic.Const (uri, mk_subst uris)
- | Cic.Var (uri, []) ->
+ NCic.Const (uri, mk_subst uris)
+ | NCic.Var (uri, []) ->
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
- Cic.Var (uri, mk_subst uris)
- | Cic.MutInd (uri, i, []) ->
+ NCic.Var (uri, mk_subst uris)
+ | NCic.MutInd (uri, i, []) ->
(try
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
- Cic.MutInd (uri, i, mk_subst uris)
+ NCic.MutInd (uri, i, mk_subst uris)
with
CicEnvironment.Object_not_found _ ->
(* if we are here it is probably the case that during the
However, the inductive type is not yet in the environment
*)
(*here the explicit_named_substituion is assumed to be of length 0 *)
- Cic.MutInd (uri,i,[]))
- | Cic.MutConstruct (uri, i, j, []) ->
+ NCic.MutInd (uri,i,[]))
+ | NCic.MutConstruct (uri, i, j, []) ->
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_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 ->
+ NCic.MutConstruct (uri, i, j, mk_subst uris)
+ | NCic.Meta _ | NCic.Implicit _ as t ->
(*
debug_print (lazy (sprintf
"Warning: %s must be instantiated with _[%s] but we do not enforce it"
with
CicEnvironment.CircularDependency _ ->
raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
- | CicNotationPt.Implicit -> Cic.Implicit None
- | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
+ | CicNotationPt.Implicit -> NCic.Implicit None
+ | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
| Some term -> Some (aux ~localize loc context term))
subst
in
- Cic.Meta (index, cic_subst)
- | 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 u) -> Cic.Sort (Cic.CProp u)
+ NCic.Meta (index, cic_subst)
+ | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
+ | CicNotationPt.Sort `Set -> NCic.Sort NCic.Set
+ | CicNotationPt.Sort (`Type u) -> NCic.Sort (NCic.Type u)
+ | CicNotationPt.Sort (`CProp u) -> NCic.Sort (NCic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
- | None -> Cic.Implicit annotation
+ | None -> NCic.Implicit annotation
| Some term -> aux ~localize loc context term
in
aux ~localize:true HExtlib.dummy_floc context ast
=
assert false
(*
- let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
+ let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in
interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
~localization_tbl
*)
;;
let domain_of_term ~context =
- let context = List.map (fun x -> Cic.Name (fst x)) context in
+ let context = List.map (fun x -> NCic.Name (fst x)) context in
Disambiguate.domain_of_ast_term ~context
;;
module Disambiguator = Disambiguate.Make(C)
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
- (text,prefix_len,term) =
- let term =
- if fresh_instances then CicNotationUtil.freshen_term term else term
- in
- let localization_tbl = Cic.CicHash.create 503 in
- Disambiguator.disambiguate_thing
+ ?(initial_ugraph = ()) ~aliases ~universe
+ (text,prefix_len,term)
+ =
+ let term =
+ if fresh_instances then CicNotationUtil.freshen_term term else term
+ in
+ let localization_tbl = NCic.NCicHash.create 503 in
+ Disambiguator.disambiguate_thing
~dbd ~context ~metasenv ~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
+ ~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
;;
end
(* $Id$ *)
-exception RefineFailure of (Stdpp.location * string) Lazy.t;;
-exception Uncertain of (Stdpp.location * string) Lazy.t;;
+exception RefineFailure of Stdpp.location * (string Lazy.t);;
+exception Uncertain of Stdpp.location * (string Lazy.t);;
exception AssertFailure of string Lazy.t;;
val typeof :
projects / helm.git / commitdiff