+let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
+ match cmd with
+ | GrafiteAst.Index(loc,key,uri) ->
+ let lexicon_status_ref = ref estatus in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let disambiguate_term_option metasenv =
+ function
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term metasenv t in
+ metasenv, Some t
+ in
+ let metasenv,key = disambiguate_term_option metasenv key in
+ !lexicon_status_ref,metasenv,GrafiteAst.Index(loc,key,uri)
+ | GrafiteAst.Select (loc,uri) ->
+ estatus, metasenv, GrafiteAst.Select(loc,uri)
+ | GrafiteAst.Pump(loc,i) ->
+ estatus, metasenv, GrafiteAst.Pump(loc,i)
+ | GrafiteAst.PreferCoercion (loc,t) ->
+ let lexicon_status_ref = ref estatus in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let metasenv,t = disambiguate_term metasenv t in
+ !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
+ | GrafiteAst.Coercion (loc,t,b,a,s) ->
+ let lexicon_status_ref = ref estatus in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let metasenv,t = disambiguate_term metasenv t in
+ !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
+ | GrafiteAst.Inverter (loc,n,indty,params) ->
+ let lexicon_status_ref = ref estatus in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let metasenv,indty = disambiguate_term metasenv indty in
+ !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
+ | GrafiteAst.Default _
+ | GrafiteAst.Drop _
+ | GrafiteAst.Include _
+ | GrafiteAst.Print _
+ | GrafiteAst.Qed _
+ | GrafiteAst.Set _ as cmd ->
+ estatus,metasenv,cmd
+ | GrafiteAst.Obj (loc,obj) ->
+ let estatus,metasenv,obj =
+ disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in
+ estatus, metasenv, GrafiteAst.Obj (loc,obj)
+ | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
+ let lexicon_status_ref = ref estatus in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let disambiguate_term_option metasenv =
+ function
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term metasenv t in
+ metasenv, Some t
+ in
+ let metasenv,a = disambiguate_term metasenv a in
+ let metasenv,aeq = disambiguate_term metasenv aeq in
+ let metasenv,refl = disambiguate_term_option metasenv refl in
+ let metasenv,sym = disambiguate_term_option metasenv sym in
+ let metasenv,trans = disambiguate_term_option metasenv trans in
+ !lexicon_status_ref, metasenv,
+ GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)