Introducing grammar-free tactic notations.

7 files changed, 132 insertions, 31 deletions

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 40d8ff078e..1dd8410d2a 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -42,14 +42,14 @@ type tacdef = {
 }
 
 let perform_tacdef visibility ((sp, kn), def) =
-  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp kn in
+  let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp (TacConstant kn) in
   Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
 
 let load_tacdef i obj = perform_tacdef (Until i) obj
 let open_tacdef i obj = perform_tacdef (Exactly i) obj
 
 let cache_tacdef ((sp, kn), def) =
-  let () = Tac2env.push_ltac (Until 1) sp kn in
+  let () = Tac2env.push_ltac (Until 1) sp (TacConstant kn) in
   Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
 
 let subst_tacdef (subst, def) =
@@ -599,7 +599,43 @@ let inTac2Notation : synext -> obj =
      subst_function = subst_synext;
      classify_function = classify_synext}
 
-let register_notation ?(local = false) tkn lev body =
+type abbreviation = {
+  abbr_body : raw_tacexpr;
+}
+
+let perform_abbreviation visibility ((sp, kn), abbr) =
+  let () = Tac2env.push_ltac visibility sp (TacAlias kn) in
+  Tac2env.define_alias kn abbr.abbr_body
+
+let load_abbreviation i obj = perform_abbreviation (Until i) obj
+let open_abbreviation i obj = perform_abbreviation (Exactly i) obj
+
+let cache_abbreviation ((sp, kn), abbr) =
+  let () = Tac2env.push_ltac (Until 1) sp (TacAlias kn) in
+  Tac2env.define_alias kn abbr.abbr_body
+
+let subst_abbreviation (subst, abbr) =
+  let body' = subst_rawexpr subst abbr.abbr_body in
+  if body' == abbr.abbr_body then abbr
+  else { abbr_body = body' }
+
+let classify_abbreviation o = Substitute o
+
+let inTac2Abbreviation : abbreviation -> obj =
+  declare_object {(default_object "TAC2-ABBREVIATION") with
+     cache_function  = cache_abbreviation;
+     load_function   = load_abbreviation;
+     open_function   = open_abbreviation;
+     subst_function = subst_abbreviation;
+     classify_function = classify_abbreviation}
+
+let register_notation ?(local = false) tkn lev body = match tkn, lev with
+| [SexprRec (_, (_, Some id), [])], None ->
+  (** Tactic abbreviation *)
+  let body = Tac2intern.globalize Id.Set.empty body in
+  let abbr = { abbr_body = body } in
+  ignore (Lib.add_leaf id (inTac2Abbreviation abbr))
+| _ ->
   (** Check that the tokens make sense *)
   let entries = List.map ParseToken.parse_token tkn in
   let fold accu tok = match tok with
@@ -642,14 +678,18 @@ let print_ltac ref =
       try Tac2env.locate_ltac qid
       with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
     in
-    let (e, _, (_, t)) = Tac2env.interp_global kn in
-    let name = int_name () in
-    Feedback.msg_notice (
-      hov 0 (
-        hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ fnl () ++
-        hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e)
+    match kn with
+    | TacConstant kn ->
+      let (e, _, (_, t)) = Tac2env.interp_global kn in
+      let name = int_name () in
+      Feedback.msg_notice (
+        hov 0 (
+          hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ fnl () ++
+          hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e)
+        )
       )
-    )
+    | TacAlias kn ->
+      Feedback.msg_notice (str "Alias to ...")
 
 (** Calling tactics *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index a75500eae7..ac2bd5fc23 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -32,6 +32,7 @@ type ltac_state = {
   ltac_constructors : constructor_data KNmap.t;
   ltac_projections : projection_data KNmap.t;
   ltac_types : glb_quant_typedef KNmap.t;
+  ltac_aliases : raw_tacexpr KNmap.t;
 }
 
 let empty_state = {
@@ -39,6 +40,7 @@ let empty_state = {
   ltac_constructors = KNmap.empty;
   ltac_projections = KNmap.empty;
   ltac_types = KNmap.empty;
+  ltac_aliases = KNmap.empty;
 }
 
 let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
@@ -87,6 +89,12 @@ let define_type kn e =
 
 let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types
 
+let define_alias kn tac =
+  let state = !ltac_state in
+  ltac_state := { state with ltac_aliases = KNmap.add kn tac state.ltac_aliases }
+
+let interp_alias kn = KNmap.find kn ltac_state.contents.ltac_aliases
+
 module ML =
 struct
   type t = ml_tactic_name
@@ -115,11 +123,30 @@ struct
     id, (DirPath.repr dir)
 end
 
+type tacref = Tac2expr.tacref =
+| TacConstant of ltac_constant
+| TacAlias of ltac_alias
+
+module TacRef =
+struct
+type t = tacref
+let compare r1 r2 = match r1, r2 with
+| TacConstant c1, TacConstant c2 -> KerName.compare c1 c2
+| TacAlias c1, TacAlias c2 -> KerName.compare c1 c2
+| TacConstant _, TacAlias _ -> -1
+| TacAlias _, TacConstant _ -> 1
+
+let equal r1 r2 = compare r1 r2 == 0
+
+end
+
 module KnTab = Nametab.Make(FullPath)(KerName)
+module RfTab = Nametab.Make(FullPath)(TacRef)
+module RfMap = Map.Make(TacRef)
 
 type nametab = {
-  tab_ltac : KnTab.t;
-  tab_ltac_rev : full_path KNmap.t;
+  tab_ltac : RfTab.t;
+  tab_ltac_rev : full_path RfMap.t;
   tab_cstr : KnTab.t;
   tab_cstr_rev : full_path KNmap.t;
   tab_type : KnTab.t;
@@ -129,8 +156,8 @@ type nametab = {
 }
 
 let empty_nametab = {
-  tab_ltac = KnTab.empty;
-  tab_ltac_rev = KNmap.empty;
+  tab_ltac = RfTab.empty;
+  tab_ltac_rev = RfMap.empty;
   tab_cstr = KnTab.empty;
   tab_cstr_rev = KNmap.empty;
   tab_type = KnTab.empty;
@@ -143,22 +170,22 @@ let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab"
 
 let push_ltac vis sp kn =
   let tab = !nametab in
-  let tab_ltac = KnTab.push vis sp kn tab.tab_ltac in
-  let tab_ltac_rev = KNmap.add kn sp tab.tab_ltac_rev in
+  let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in
+  let tab_ltac_rev = RfMap.add kn sp tab.tab_ltac_rev in
   nametab := { tab with tab_ltac; tab_ltac_rev }
 
 let locate_ltac qid =
   let tab = !nametab in
-  KnTab.locate qid tab.tab_ltac
+  RfTab.locate qid tab.tab_ltac
 
 let locate_extended_all_ltac qid =
   let tab = !nametab in
-  KnTab.find_prefixes qid tab.tab_ltac
+  RfTab.find_prefixes qid tab.tab_ltac
 
 let shortest_qualid_of_ltac kn =
   let tab = !nametab in
-  let sp = KNmap.find kn tab.tab_ltac_rev in
-  KnTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
+  let sp = RfMap.find kn tab.tab_ltac_rev in
+  RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac
 
 let push_constructor vis sp kn =
   let tab = !nametab in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index fea03c4285..e4cc8387c5 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -61,12 +61,17 @@ type projection_data = {
 val define_projection : ltac_projection -> projection_data -> unit
 val interp_projection : ltac_projection -> projection_data
 
+(** {5 Toplevel definition of aliases} *)
+
+val define_alias : ltac_constant -> raw_tacexpr -> unit
+val interp_alias : ltac_constant -> raw_tacexpr
+
 (** {5 Name management} *)
 
-val push_ltac : visibility -> full_path -> ltac_constant -> unit
-val locate_ltac : qualid -> ltac_constant
-val locate_extended_all_ltac : qualid -> ltac_constant list
-val shortest_qualid_of_ltac : ltac_constant -> qualid
+val push_ltac : visibility -> full_path -> tacref -> unit
+val locate_ltac : qualid -> tacref
+val locate_extended_all_ltac : qualid -> tacref list
+val shortest_qualid_of_ltac : tacref -> qualid
 
 val push_constructor : visibility -> full_path -> ltac_constructor -> unit
 val locate_constructor : qualid -> ltac_constructor
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 10d8c1d421..7efb85cbb0 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -18,10 +18,15 @@ type lid = Id.t
 type uid = Id.t
 
 type ltac_constant = KerName.t
+type ltac_alias = KerName.t
 type ltac_constructor = KerName.t
 type ltac_projection = KerName.t
 type type_constant = KerName.t
 
+type tacref =
+| TacConstant of ltac_constant
+| TacAlias of ltac_alias
+
 type 'a or_relid =
 | RelId of qualid located
 | AbsKn of 'a
@@ -88,7 +93,7 @@ type raw_patexpr =
 
 type raw_tacexpr =
 | CTacAtm of atom located
-| CTacRef of ltac_constant or_relid
+| CTacRef of tacref or_relid
 | CTacCst of Loc.t * ltac_constructor or_tuple or_relid
 | CTacFun of Loc.t * (raw_patexpr * raw_typexpr option) list * raw_tacexpr
 | CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 32ed211ad0..2b1dde7553 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -654,6 +654,10 @@ let expand_pattern avoid bnd =
   let nas = List.rev_map (fun (na, _, _) -> na) bnd in
   (nas, expand)
 
+let is_alias env qid = match get_variable env qid with
+| ArgArg (TacAlias _) -> true
+| ArgVar _ | (ArgArg (TacConstant _)) -> false
+
 let rec intern_rec env = function
 | CTacAtm (_, atm) -> intern_atm env atm
 | CTacRef qid ->
@@ -661,9 +665,12 @@ let rec intern_rec env = function
   | ArgVar (_, id) ->
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
-  | ArgArg kn ->
+  | ArgArg (TacConstant kn) ->
     let (_, _, sch) = Tac2env.interp_global kn in
     (GTacRef kn, fresh_type_scheme env sch)
+  | ArgArg (TacAlias kn) ->
+    let e = Tac2env.interp_alias kn in
+    intern_rec env e
   end
 | CTacCst (loc, qid) ->
   let kn = get_constructor env qid in
@@ -682,6 +689,20 @@ let rec intern_rec env = function
 | CTacApp (loc, CTacCst (_, qid), args) ->
   let kn = get_constructor env qid in
   intern_constructor env loc kn args
+| CTacApp (loc, CTacRef qid, args) when is_alias env qid ->
+  let kn = match get_variable env qid with
+  | ArgArg (TacAlias kn) -> kn
+  | ArgVar _ | (ArgArg (TacConstant _)) -> assert false
+  in
+  let e = Tac2env.interp_alias kn in
+  let map arg =
+    (** Thunk alias arguments *)
+    let loc = loc_of_tacexpr arg in
+    let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Tuple 0), []))] in
+    CTacFun (loc, var, arg)
+  in
+  let args = List.map map args in
+  intern_rec env (CTacApp (loc, e, args))
 | CTacApp (loc, f, args) ->
   let loc = loc_of_tacexpr f in
   let (f, ft) = intern_rec env f in
@@ -1372,9 +1393,12 @@ let rec subst_rawtype subst t = match t with
 
 let subst_tacref subst ref = match ref with
 | RelId _ -> ref
-| AbsKn kn ->
+| AbsKn (TacConstant kn) ->
   let kn' = subst_kn subst kn in
-  if kn' == kn then ref else AbsKn kn'
+  if kn' == kn then ref else AbsKn (TacConstant kn')
+| AbsKn (TacAlias kn) ->
+  let kn' = subst_kn subst kn in
+  if kn' == kn then ref else AbsKn (TacAlias kn')
 
 let subst_projection subst prj = match prj with
 | RelId _ -> prj
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 28f9516f65..b679e030fd 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -143,7 +143,7 @@ let pr_glbexpr_gen lvl c =
   | GTacAtm atm -> pr_atom atm
   | GTacVar id -> Id.print id
   | GTacRef gr ->
-    let qid = shortest_qualid_of_ltac gr in
+    let qid = shortest_qualid_of_ltac (TacConstant gr) in
     Libnames.pr_qualid qid
   | GTacFun (nas, c) ->
     let nas = pr_sequence pr_name nas in
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 7d9c01f3f0..3e25e1cadb 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -229,10 +229,10 @@ let of_rewriting (loc, rew) =
 
 let of_hyp ?loc id =
   let loc = Option.default dummy_loc loc in
-  let hyp = CTacRef (AbsKn (control_core "hyp")) in
+  let hyp = CTacRef (AbsKn (TacConstant (control_core "hyp"))) in
   CTacApp (loc, hyp, [of_ident id])
 
 let of_exact_hyp ?loc id =
   let loc = Option.default dummy_loc loc in
-  let refine = CTacRef (AbsKn (control_core "refine")) in
+  let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in
   CTacApp (loc, refine, [thunk (of_hyp ~loc id)])