| `Whd as kind -> kind
;;
-let disambiguate_tactic
+let rec disambiguate_tactic
lexicon_status_ref context metasenv (text,prefix_len,tactic)
=
let disambiguate_term =
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
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)
metasenv,GrafiteAst.ApplyS (loc, cic, params)
| GrafiteAst.Assumption loc ->
metasenv,GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,params) ->
- metasenv,GrafiteAst.Auto (loc,params)
+ | GrafiteAst.AutoBatch (loc,params) ->
+ 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)
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 ->
| GrafiteAst.Exact (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) ->
- let pattern = disambiguate_pattern pattern in
+ | 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
- metasenv,GrafiteAst.Elim (loc, pattern, Some using, depth, idents)
- | GrafiteAst.Elim (loc, pattern, None, depth, idents) ->
let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Elim (loc, pattern, None, depth, idents)
- | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+ 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, depth, idents)
- | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+ 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, depth, idents)
+ metasenv,GrafiteAst.ElimType (loc, what, None, specs)
| GrafiteAst.Exists loc ->
metasenv,GrafiteAst.Exists loc
| GrafiteAst.Fail loc ->
| GrafiteAst.Generalize (loc,pattern,ident) ->
let pattern = disambiguate_pattern pattern in
metasenv,GrafiteAst.Generalize (loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) ->
- metasenv,GrafiteAst.Goal (loc, g)
| GrafiteAst.IdTac loc ->
metasenv,GrafiteAst.IdTac loc
- | GrafiteAst.Intros (loc, num, names) ->
- metasenv,GrafiteAst.Intros (loc, num, names)
+ | 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)
`Auto _ as t -> metasenv,t
| `Term t ->
let metasenv,t = disambiguate_term context metasenv t in
- metasenv,`Term t in
+ metasenv,`Term t
+ | `Proof as t -> metasenv,t in
metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
| GrafiteAst.Check (loc,term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Check (loc,term)
+ | GrafiteAst.AutoInteractive _
| GrafiteAst.Hint _
| GrafiteAst.WLocate _
| GrafiteAst.Inline _ as macro ->