(* $Id$ *)
-exception BaseUriNotSetYet
+class type g_status =
+ object
+ inherit LexiconTypes.g_status
+ end
+
+class status =
+ object (self)
+ inherit LexiconTypes.status
+ method set_grafite_disambiguate_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> (self#set_lexicon_engine_status o)
+ end
-type tactic =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
-type lazy_tactic =
- (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
- GrafiteAst.tactic
+exception BaseUriNotSetYet
let singleton msg = function
| [x], _ -> x
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
-let ncic_mk_choice = function
- | LexiconAst.Symbol_alias (name, _, dsc) ->
+let ncic_mk_choice status = function
+ | GrafiteAst.Symbol_alias (name, _, dsc) ->
if name = __Implicit then
dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
else if name = __Closed_Implicit then
dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
else
- DisambiguateChoices.lookup_symbol_by_dsc
+ DisambiguateChoices.lookup_symbol_by_dsc status
~mk_implicit:(function
| true -> NCic.Implicit `Closed
| false -> NCic.Implicit `Term)
~mk_appl:(function
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_uri:(fun _ -> assert false)
~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
- | LexiconAst.Number_alias (_, dsc) ->
+ | GrafiteAst.Number_alias (_, dsc) ->
let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
desc, `Num_interp
(fun num -> match f with `Num_interp f -> f num | _ -> assert false)
- | LexiconAst.Ident_alias (name, uri) ->
+ | GrafiteAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
- try
- let nref = NReference.reference_of_string uri in
- NCic.Const nref
- with
- NReference.IllFormedReference _ ->
- let uri = UriManager.uri_of_string uri in
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ let nref = NReference.reference_of_string uri in
+ NCic.Const nref)
;;
let mk_implicit b =
match b with
| false ->
- LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+ GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
| true ->
- LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
+ GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
;;
let nlookup_in_library
(try
let references = NCicLibrary.resolve id in
List.map
- (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
+ (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
) references
with
NCicEnvironment.ObjectNotFound _ -> [])
DisambiguateTypes.Symbol (_,n) ->
List.map
(function
- LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d)
+ GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
| _ -> assert false
) l
| DisambiguateTypes.Num n ->
List.map
(function
- LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d)
+ GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
| _ -> assert false
) l
| DisambiguateTypes.Id _ -> l
singleton "first"
(NCicDisambiguate.disambiguate_term
~rdb:estatus
- ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~aliases:estatus#lstatus.LexiconTypes.aliases
~expty
- ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
~lookup_in_library:nlookup_in_library
- ~mk_choice:ncic_mk_choice
+ ~mk_choice:(ncic_mk_choice estatus)
~mk_implicit ~fix_instance
- ~description_of_alias:LexiconAst.description_of_alias
+ ~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing)
in
- let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ let estatus =
+ LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+ GrafiteAst.WithPreferences diff
+ in
metasenv, subst, estatus, cic
;;
type pattern =
- CicNotationPt.term Disambiguate.disambiguator_input option *
+ NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
in
let name =
match obj with
- | CicNotationPt.Inductive (_,(name,_,_,_)::_)
- | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
- | CicNotationPt.Inductive _ -> assert false
+ | NotationPt.Inductive (_,(name,_,_,_)::_)
+ | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Inductive _ -> assert false
in
- UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ NUri.uri_of_string (baseuri ^ "/" ^ name)
in
let diff, _, _, cic =
singleton "third"
(NCicDisambiguate.disambiguate_obj
~lookup_in_library:nlookup_in_library
- ~description_of_alias:LexiconAst.description_of_alias
- ~mk_choice:ncic_mk_choice
+ ~description_of_alias:GrafiteAst.description_of_alias
+ ~mk_choice:(ncic_mk_choice estatus)
~mk_implicit ~fix_instance
- ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~uri
~rdb:estatus
- ~aliases:estatus#lstatus.LexiconEngine.aliases
- ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ ~aliases:estatus#lstatus.LexiconTypes.aliases
+ ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases)
(text,prefix_len,obj)) in
- let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ let estatus =
+ LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true
+ GrafiteAst.WithPreferences diff
+ in
estatus, cic
;;
-let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
- match cmd with
- | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Select (loc,uri) ->
- estatus, GrafiteAst.Select(loc,uri)
- | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Default _
- | GrafiteAst.Drop _
- | GrafiteAst.Include _
- | GrafiteAst.Print _
- | GrafiteAst.Qed _
- | GrafiteAst.Set _ as cmd ->
- estatus,cmd
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false
projects / helm.git / blobdiff