assert (context = []);
assert (is_path = false);
match obj with
- | GrafiteAst.Inductive (params,tyl) ->
+ | CicNotationPt.Inductive (params,tyl) ->
let uri = match uri with Some uri -> uri | None -> assert false in
let context,params =
let context,res =
) tyl
in
Cic.InductiveDefinition (tyl,[],List.length params,[])
- | GrafiteAst.Record (params,name,ty,fields) ->
+ | CicNotationPt.Record (params,name,ty,fields) ->
let uri = match uri with Some uri -> uri | None -> assert false in
let context,params =
let context,res =
let field_names = List.map fst fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
- | GrafiteAst.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
(match bo with
assert (context = []);
let domain_rev =
match ast with
- | GrafiteAst.Theorem (_,_,ty,bo) ->
+ | CicNotationPt.Theorem (_,_,ty,bo) ->
(match bo with
None -> []
| Some bo -> domain_rev_of_term [] bo) @
domain_of_term [] ty
- | GrafiteAst.Inductive (params,tyl) ->
+ | CicNotationPt.Inductive (params,tyl) ->
let dom =
List.flatten (
List.rev_map
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_,_) -> name = Id name') tyl)
) dom
- | GrafiteAst.Record (params,_,ty,fields) ->
+ | CicNotationPt.Record (params,_,ty,fields) ->
let dom =
List.flatten
(List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
- GrafiteAst.obj ->
+ CicNotationPt.obj ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *
| Id id -> choices_of_id dbd id
| Symbol (symb, _) ->
List.map DisambiguateChoices.mk_choice
- (CicNotationRew.lookup_interpretations symb)
+ (TermAcicContent.lookup_interpretations symb)
| Num instance ->
DisambiguateChoices.lookup_num_choices ()
in
if fresh_instances then CicNotationUtil.freshen_obj obj else obj
in
disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
- ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
+ ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
obj
end