--- /dev/null
+(*
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+exception BaseUriNotSetYet
+
+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
+
+let singleton msg = function
+ | [x], _ -> x
+ | l, _ ->
+ let debug =
+ Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
+ msg (List.length l)
+ in
+ HLog.debug debug; assert false
+
+ (** @param term not meaningful when context is given *)
+let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
+ let lexicon_status = !lexicon_status_ref in
+ let (diff, metasenv, cic, _) =
+ singleton "first"
+ (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~context ~metasenv (text,prefix_len,term))
+ in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status_ref := lexicon_status;
+ metasenv,cic
+;;
+
+ (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
+ * rationale: lazy_term will be invoked in different context to obtain a term,
+ * each invocation will disambiguate the term and can add aliases. Once all
+ * disambiguations have been performed, the first returned function can be
+ * used to obtain the resulting aliases *)
+let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
+ (fun context metasenv ugraph ->
+ let lexicon_status = !lexicon_status_ref in
+ 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
+ (text,prefix_len,term)) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status_ref := lexicon_status;
+ cic, metasenv, ugraph)
+;;
+
+let disambiguate_pattern
+ text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path)
+=
+ let interp path = Disambiguate.interpretate_path [] path in
+ let goal_path = HExtlib.map_option interp goal_path in
+ let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+ let wanted =
+ match wanted with
+ None -> None
+ | Some wanted ->
+ let wanted =
+ disambiguate_lazy_term text prefix_len lexicon_status_ref wanted
+ in
+ Some wanted
+ in
+ (wanted, hyp_paths, goal_path)
+;;
+
+let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
+ | `Unfold (Some t) ->
+ let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
+ `Unfold (Some t)
+ | `Normalize
+ | `Simpl
+ | `Unfold None
+ | `Whd as kind -> kind
+;;
+
+let disambiguate_auto_params
+ disambiguate_term metasenv context (terms, params)
+=
+ let metasenv, terms =
+ List.fold_right
+ (fun t (metasenv, terms) ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,t::terms) terms (metasenv, [])
+ in
+ metasenv, (terms, params)
+;;
+
+let rec disambiguate_tactic
+ lexicon_status_ref context metasenv (text,prefix_len,tactic)
+=
+ let disambiguate_term =
+ disambiguate_term text prefix_len lexicon_status_ref in
+ let disambiguate_pattern =
+ disambiguate_pattern text prefix_len lexicon_status_ref in
+ let disambiguate_reduction_kind =
+ disambiguate_reduction_kind text prefix_len lexicon_status_ref in
+ let disambiguate_lazy_term =
+ disambiguate_lazy_term text prefix_len lexicon_status_ref in
+ let disambiguate_tactic metasenv tac =
+ disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac)
+ in
+ let disambiguate_auto_params m p =
+ disambiguate_auto_params disambiguate_term m context p
+ in
+ match tactic with
+ (* Higher order tactics *)
+ | GrafiteAst.Progress (loc,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Progress (loc,tac)
+ | GrafiteAst.Solve (loc,tacl) ->
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.Solve (loc,tacl)
+ | GrafiteAst.Try (loc,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Try (loc,tac)
+ | GrafiteAst.First (loc,tacl) ->
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.First (loc,tacl)
+ | GrafiteAst.Seq (loc,tacl) ->
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.Seq (loc,tacl)
+ | GrafiteAst.Repeat (loc,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Repeat (loc,tac)
+ | GrafiteAst.Do (loc,n,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Do (loc,n,tac)
+ | GrafiteAst.Then (loc,tac,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.Then (loc,tac,tacl)
+ (* First order tactics *)
+ | GrafiteAst.Absurd (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Absurd (loc, cic)
+ | GrafiteAst.Apply (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.ApplyS (loc, term, params) ->
+ let metasenv, params = disambiguate_auto_params metasenv params in
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.ApplyS (loc, cic, params)
+ | GrafiteAst.Assumption loc ->
+ metasenv,GrafiteAst.Assumption loc
+ | GrafiteAst.AutoBatch (loc,params) ->
+ let metasenv, params = disambiguate_auto_params metasenv params in
+ metasenv,GrafiteAst.AutoBatch (loc,params)
+ | GrafiteAst.Cases (loc, what, idents) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.Cases (loc, what, idents)
+ | GrafiteAst.Change (loc, pattern, with_what) ->
+ let with_what = disambiguate_lazy_term with_what in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Change (loc, pattern, with_what)
+ | GrafiteAst.Clear (loc,id) ->
+ metasenv,GrafiteAst.Clear (loc,id)
+ | GrafiteAst.ClearBody (loc,id) ->
+ metasenv,GrafiteAst.ClearBody (loc,id)
+ | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
+ let metasenv,t1 = disambiguate_term context metasenv t1 in
+ let metasenv,t2 =
+ match t2 with
+ | None -> metasenv, None
+ | Some t2 ->
+ let m, t2 = disambiguate_term context metasenv t2 in
+ m, Some t2
+ in
+ metasenv, GrafiteAst.Compose (loc, t1, t2, times, spec)
+ | GrafiteAst.Constructor (loc,n) ->
+ metasenv,GrafiteAst.Constructor (loc,n)
+ | GrafiteAst.Contradiction loc ->
+ metasenv,GrafiteAst.Contradiction loc
+ | GrafiteAst.Cut (loc, ident, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Cut (loc, ident, cic)
+ | GrafiteAst.Decompose (loc, names) ->
+ metasenv,GrafiteAst.Decompose (loc, names)
+ | GrafiteAst.Demodulate (loc, params) ->
+ let metasenv, params = disambiguate_auto_params metasenv params in
+ metasenv,GrafiteAst.Demodulate (loc, params)
+ | GrafiteAst.Destruct (loc, Some terms) ->
+ let map term (metasenv, terms) =
+ let metasenv, term = disambiguate_term context metasenv term in
+ metasenv, term :: terms
+ in
+ let metasenv, terms = List.fold_right map terms (metasenv, []) in
+ metasenv, GrafiteAst.Destruct(loc, Some terms)
+ | GrafiteAst.Destruct (loc, None) ->
+ metasenv,GrafiteAst.Destruct(loc,None)
+ | GrafiteAst.Exact (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Exact (loc, cic)
+ | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ let metasenv,using = disambiguate_term context metasenv using in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
+ | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
+ | GrafiteAst.ElimType (loc, what, Some using, specs) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ let metasenv,using = disambiguate_term context metasenv using in
+ metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
+ | GrafiteAst.ElimType (loc, what, None, specs) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.ElimType (loc, what, None, specs)
+ | GrafiteAst.Exists loc ->
+ metasenv,GrafiteAst.Exists loc
+ | GrafiteAst.Fail loc ->
+ metasenv,GrafiteAst.Fail loc
+ | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
+ let pattern = disambiguate_pattern pattern in
+ let term = disambiguate_lazy_term term in
+ let red_kind = disambiguate_reduction_kind red_kind in
+ metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
+ | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+ metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc ->
+ metasenv,GrafiteAst.Fourier loc
+ | GrafiteAst.Generalize (loc,pattern,ident) ->
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Generalize (loc,pattern,ident)
+ | GrafiteAst.IdTac loc ->
+ metasenv,GrafiteAst.IdTac loc
+ | GrafiteAst.Intros (loc, specs) ->
+ metasenv,GrafiteAst.Intros (loc, specs)
+ | GrafiteAst.Inversion (loc, term) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Inversion (loc, term)
+ | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
+ let f term (metasenv, to_what) =
+ let metasenv, term = disambiguate_term context metasenv term in
+ metasenv, term :: to_what
+ in
+ let metasenv, to_what = List.fold_right f to_what (metasenv, []) in
+ let metasenv, what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
+ | GrafiteAst.Left loc ->
+ metasenv,GrafiteAst.Left loc
+ | GrafiteAst.LetIn (loc, term, name) ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.LetIn (loc,term,name)
+ | GrafiteAst.Reduce (loc, red_kind, pattern) ->
+ let pattern = disambiguate_pattern pattern in
+ let red_kind = disambiguate_reduction_kind red_kind in
+ metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
+ | GrafiteAst.Reflexivity loc ->
+ metasenv,GrafiteAst.Reflexivity loc
+ | GrafiteAst.Replace (loc, pattern, with_what) ->
+ let pattern = disambiguate_pattern pattern in
+ let with_what = disambiguate_lazy_term with_what in
+ metasenv,GrafiteAst.Replace (loc, pattern, with_what)
+ | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
+ let metasenv,term = disambiguate_term context metasenv t in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
+ | GrafiteAst.Right loc ->
+ metasenv,GrafiteAst.Right loc
+ | GrafiteAst.Ring loc ->
+ metasenv,GrafiteAst.Ring loc
+ | GrafiteAst.Split loc ->
+ metasenv,GrafiteAst.Split loc
+ | GrafiteAst.Symmetry loc ->
+ metasenv,GrafiteAst.Symmetry loc
+ | GrafiteAst.Transitivity (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Transitivity (loc, cic)
+ (* Nuovi casi *)
+ | GrafiteAst.Assume (loc, id, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Assume (loc, id, cic)
+ | GrafiteAst.Suppose (loc, term, id, term') ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' =
+ match term' with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
+ | GrafiteAst.Bydone (loc,term) ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ |Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.Bydone (loc, cic)
+ | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' =
+ match term' with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
+ | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ let metasenv,cic'' =
+ match term'' with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
+ | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
+ | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
+ | GrafiteAst.Byinduction (loc, term, id) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Byinduction(loc, cic, id)
+ | GrafiteAst.Thesisbecomes (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Thesisbecomes (loc, cic)
+ | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ let metasenv,cic' = disambiguate_term context metasenv term1 in
+ let cic''= disambiguate_lazy_term term2 in
+ metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
+ | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic'= disambiguate_term context metasenv term1 in
+ let metasenv,cic''= disambiguate_term context metasenv term2 in
+ metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')
+ | GrafiteAst.Case (loc, id, params) ->
+ let metasenv,params' =
+ List.fold_right
+ (fun (id,term) (metasenv,params) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,(id,cic)::params
+ ) params (metasenv,[])
+ in
+ metasenv,GrafiteAst.Case(loc, id, params')
+ | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
+ let metasenv,cic =
+ match term1 with
+ None -> metasenv,None
+ | Some (start,t) ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some (start,t) in
+ let metasenv,cic'= disambiguate_term context metasenv term2 in
+ let metasenv,cic'' =
+ match term3 with
+ | `SolveWith term ->
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv, `SolveWith term
+ | `Auto params ->
+ let metasenv, params = disambiguate_auto_params metasenv params in
+ metasenv,`Auto params
+ | `Term t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,`Term t
+ | `Proof as t -> metasenv,t in
+ metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
+
+
+let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
+ let uri =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) ->
+ (match baseuri with
+ | Some baseuri ->
+ Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
+ | None -> raise BaseUriNotSetYet)
+ | CicNotationPt.Inductive _ -> assert false
+ | CicNotationPt.Theorem _ -> None in
+ let (diff, metasenv, cic, _) =
+ singleton "third"
+ (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
+ (text,prefix_len,obj)) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status, metasenv, cic
+
+let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
+ match cmd with
+ | GrafiteAst.Index(loc,key,uri) ->
+ let lexicon_status_ref = ref lexicon_status in
+ let disambiguate_term =
+ disambiguate_term 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.Coercion _
+ | GrafiteAst.Default _
+ | GrafiteAst.Drop _
+ | GrafiteAst.Include _
+ | GrafiteAst.Print _
+ | GrafiteAst.Qed _
+ | GrafiteAst.Set _ as cmd ->
+ lexicon_status,metasenv,cmd
+ | GrafiteAst.Obj (loc,obj) ->
+ let lexicon_status,metasenv,obj =
+ disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
+ lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+ | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
+ let lexicon_status_ref = ref lexicon_status in
+ let disambiguate_term =
+ disambiguate_term 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)
+
+let disambiguate_macro
+ lexicon_status_ref metasenv context (text,prefix_len, macro)
+=
+ let disambiguate_term = disambiguate_term text prefix_len 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.AutoInteractive (loc, params) ->
+ let metasenv, params =
+ disambiguate_auto_params disambiguate_term metasenv context params in
+ metasenv, GrafiteAst.AutoInteractive (loc, params)
+ | GrafiteAst.Hint _
+ | GrafiteAst.WLocate _
+ | GrafiteAst.Inline _ as macro ->
+ metasenv,macro
projects / helm.git / blobdiff