-let disambiguate_tactic status = function
- | GrafiteAst.Apply (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Apply (loc, cic)
- | GrafiteAst.Absurd (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Absurd (loc, cic)
- | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *)
- | GrafiteAst.Change (loc, pattern, with_what) ->
- let status, with_what = disambiguate_term status with_what in
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Change (loc, pattern, with_what)
- | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id)
- | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id)
- | GrafiteAst.Compare (loc,term) ->
- let status, term = disambiguate_term status term in
- status, GrafiteAst.Compare (loc,term)
- | GrafiteAst.Constructor (loc,n) ->
- status, GrafiteAst.Constructor (loc,n)
- | GrafiteAst.Contradiction loc ->
- status, GrafiteAst.Contradiction loc
- | GrafiteAst.Cut (loc, ident, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.DecideEquality loc ->
- status, GrafiteAst.DecideEquality loc
- | GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate (status, types) = function
- | GrafiteAst.Type _ -> assert false
- | GrafiteAst.Ident id ->
- match disambiguate_term status (CicNotationPt.Ident (id, None)) with
- | status, Cic.MutInd (uri, tyno, _) ->
- status, (GrafiteAst.Type (uri, tyno) :: types)
- | _ ->
- raise Disambiguate.NoWellTypedInterpretation
- in
- let status, types = List.fold_left disambiguate (status, []) types in
- status, GrafiteAst.Decompose(loc, types, what, names)
- | GrafiteAst.Discriminate (loc,term) ->
- let status,term = disambiguate_term status term in
- status, GrafiteAst.Discriminate(loc,term)
- | GrafiteAst.Exact (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let status, what = disambiguate_term status what in
- let status, using = disambiguate_term status using in
- status, GrafiteAst.Elim (loc, what, Some using, depth, idents)
- | GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let status, what = disambiguate_term status what in
- status, GrafiteAst.Elim (loc, what, None, depth, idents)
- | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
- let status, what = disambiguate_term status what in
- let status, using = disambiguate_term status using in
- status, GrafiteAst.ElimType (loc, what, Some using, depth, idents)
- | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
- let status, what = disambiguate_term status what in
- status, GrafiteAst.ElimType (loc, what, None, depth, idents)
- | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc
- | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
- | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, term = disambiguate_term status term in
- let status, red_kind = disambiguate_reduction_kind status red_kind in
- status, GrafiteAst.Fold (loc,red_kind, term, pattern)
- | GrafiteAst.FwdSimpl (loc, hyp, names) ->
- status, GrafiteAst.FwdSimpl (loc, hyp, names)
- | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
- | GrafiteAst.Generalize (loc,pattern,ident) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Generalize(loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g)
- | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc
- | GrafiteAst.Injection (loc,term) ->
- let status, term = disambiguate_term status term in
- status, GrafiteAst.Injection (loc,term)
- | GrafiteAst.Intros (loc, num, names) ->
- status, GrafiteAst.Intros (loc, num, names)
- | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
- let f term (status, to_what) =
- let status, term = disambiguate_term status term in
- status, term :: to_what
- in
- let status, to_what = List.fold_right f to_what (status, []) in
- let status, what = disambiguate_term status what in
- status, GrafiteAst.LApply (loc, depth, to_what, what, ident)
- | GrafiteAst.Left loc -> status, GrafiteAst.Left loc
- | GrafiteAst.LetIn (loc, term, name) ->
- let status, term = disambiguate_term status term in
- status, GrafiteAst.LetIn (loc,term,name)
- | GrafiteAst.Reduce (loc, red_kind, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, red_kind = disambiguate_reduction_kind status red_kind in
- status, GrafiteAst.Reduce(loc, red_kind, pattern)
- | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
- | GrafiteAst.Replace (loc, pattern, with_what) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, with_what = disambiguate_term status with_what in
- status, GrafiteAst.Replace (loc, pattern, with_what)
- | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
- let status, term = disambiguate_term status t in
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Rewrite (loc, dir, term, pattern)
- | GrafiteAst.Right loc -> status, GrafiteAst.Right loc
- | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc
- | GrafiteAst.Split loc -> status, GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc
- | GrafiteAst.Transitivity (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Transitivity (loc, cic)
+let disambiguate_tactic status tactic =
+ let status_ref = ref status in
+ let tactic =
+ match tactic with
+ | GrafiteAst.Absurd (loc, term) ->
+ let cic = disambiguate_term status_ref term in
+ GrafiteAst.Absurd (loc, cic)
+ | GrafiteAst.Apply (loc, term) ->
+ let cic = disambiguate_term status_ref term in
+ GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
+ | GrafiteAst.Auto (loc,depth,width,paramodulation) ->
+ GrafiteAst.Auto (loc,depth,width,paramodulation)
+ | GrafiteAst.Change (loc, pattern, with_what) ->
+ let with_what = disambiguate_lazy_term status_ref with_what in
+ let pattern = disambiguate_pattern status_ref pattern in
+ GrafiteAst.Change (loc, pattern, with_what)
+ | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
+ | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
+ | GrafiteAst.Compare (loc,term) ->
+ let term = disambiguate_term status_ref term in
+ GrafiteAst.Compare (loc,term)
+ | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
+ | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
+ | GrafiteAst.Cut (loc, ident, term) ->
+ let cic = disambiguate_term status_ref term in
+ GrafiteAst.Cut (loc, ident, cic)
+ | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
+ | GrafiteAst.Decompose (loc, types, what, names) ->
+ let disambiguate types = function
+ | GrafiteAst.Type _ -> assert false
+ | GrafiteAst.Ident id ->
+ (match disambiguate_term status_ref (CicNotationPt.Ident (id, None)) with
+ | Cic.MutInd (uri, tyno, _) ->
+ (GrafiteAst.Type (uri, tyno) :: types)
+ | _ -> raise Disambiguate.NoWellTypedInterpretation)
+ in
+ let types = List.fold_left disambiguate [] types in
+ GrafiteAst.Decompose (loc, types, what, names)
+ | GrafiteAst.Discriminate (loc,term) ->
+ let term = disambiguate_term status_ref term in
+ GrafiteAst.Discriminate(loc,term)
+ | GrafiteAst.Exact (loc, term) ->
+ let cic = disambiguate_term status_ref term in
+ GrafiteAst.Exact (loc, cic)
+ | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
+ let what = disambiguate_term status_ref what in
+ let using = disambiguate_term status_ref using in
+ GrafiteAst.Elim (loc, what, Some using, depth, idents)
+ | GrafiteAst.Elim (loc, what, None, depth, idents) ->
+ let what = disambiguate_term status_ref what in
+ GrafiteAst.Elim (loc, what, None, depth, idents)
+ | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+ let what = disambiguate_term status_ref what in
+ let using = disambiguate_term status_ref using in
+ GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+ | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+ let what = disambiguate_term status_ref what in
+ GrafiteAst.ElimType (loc, what, None, depth, idents)
+ | GrafiteAst.Exists loc -> GrafiteAst.Exists loc
+ | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
+ | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ let term = disambiguate_lazy_term status_ref term in
+ let red_kind = disambiguate_reduction_kind status_ref red_kind in
+ GrafiteAst.Fold (loc, red_kind, term, pattern)
+ | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+ GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
+ | GrafiteAst.Generalize (loc,pattern,ident) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ GrafiteAst.Generalize (loc,pattern,ident)
+ | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
+ | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
+ | GrafiteAst.Injection (loc, term) ->
+ let term = disambiguate_term status_ref term in
+ GrafiteAst.Injection (loc,term)
+ | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+ | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term to_what =
+ let term = disambiguate_term status_ref term in
+ term :: to_what
+ in
+ let to_what = List.fold_right f to_what [] in
+ let what = disambiguate_term status_ref what in
+ GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ | GrafiteAst.Left loc -> GrafiteAst.Left loc
+ | GrafiteAst.LetIn (loc, term, name) ->
+ let term = disambiguate_term status_ref term in
+ GrafiteAst.LetIn (loc,term,name)
+ | GrafiteAst.Reduce (loc, red_kind, pattern) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ let red_kind = disambiguate_reduction_kind status_ref red_kind in
+ GrafiteAst.Reduce(loc, red_kind, pattern)
+ | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
+ | GrafiteAst.Replace (loc, pattern, with_what) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ let with_what = disambiguate_lazy_term status_ref with_what in
+ GrafiteAst.Replace (loc, pattern, with_what)
+ | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+ let term = disambiguate_term status_ref t in
+ let pattern = disambiguate_pattern status_ref pattern in
+ GrafiteAst.Rewrite (loc, dir, term, pattern)
+ | GrafiteAst.Right loc -> GrafiteAst.Right loc
+ | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
+ | GrafiteAst.Split loc -> GrafiteAst.Split loc
+ | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+ | GrafiteAst.Transitivity (loc, term) ->
+ let cic = disambiguate_term status_ref term in
+ GrafiteAst.Transitivity (loc, cic)
+ in
+ status_ref, tactic