* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception BaseUriNotSetYet
let singleton = function
| `Unfold (Some t) ->
let t = disambiguate_lazy_term lexicon_status_ref t in
`Unfold (Some t)
+ | `Demodulate
| `Normalize
| `Reduce
| `Simpl
lexicon_status, metasenv, cic
let disambiguate_command lexicon_status ~baseuri metasenv =
- function
+ function
| GrafiteAst.Coercion _
| GrafiteAst.Default _
| GrafiteAst.Drop _
let lexicon_status,metasenv,obj =
disambiguate_obj lexicon_status ~baseuri metasenv obj in
lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+
+let disambiguate_macro lexicon_status_ref metasenv context macro =
+ let disambiguate_term = disambiguate_term lexicon_status_ref in
+ match macro with
+ | GrafiteAst.WMatch (loc,term) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.WMatch (loc,term)
+ | GrafiteAst.WInstance (loc,term) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.WInstance (loc,term)
+ | GrafiteAst.WElim (loc,term) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.WElim (loc,term)
+ | GrafiteAst.WHint (loc,term) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.WHint (loc,term)
+ | GrafiteAst.Check (loc,term) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Check (loc,term)
+ | GrafiteAst.Hint _
+ | GrafiteAst.WLocate _ as macro ->
+ metasenv,macro
+ | GrafiteAst.Quit _
+ | GrafiteAst.Print _
+ | GrafiteAst.Search_pat _
+ | GrafiteAst.Search_term _ -> assert false