feat: scope notations generated for LTS and ReductionSystem (#133)

Closes #124 and #120.

Author: chenson2018

Cslib/Foundations/Lint/Basic.lean

@@ -27,12 +27,6 @@ def topNamespace : Batteries.Tactic.Lint.Linter where
     if top.contains declName.components[0]! then
       return none
     else
-      let ty := env.find? declName |>.get! |>.type
-      /- TODO: this is a temporary allowance for unscoped notations generated
-         for `LTS` and `ReductionSystem`. -/
-      if ty == .const ``Lean.TrailingParserDescr [] then
-        return none
-      else
-        return m!"{declName} is not namespaced."
+      return m!"{declName} is not namespaced."
 
 end Cslib.Lint

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -719,17 +719,17 @@ elab "create_lts" lt:ident name:ident : command => do
   also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β»
   in the above example.
 -/
-syntax "lts_transition_notation" ident (str)? : command
+syntax attrKind "lts_transition_notation" ident (str)? : command
 macro_rules
-  | `(lts_transition_notation $lts $sym) =>
+  | `($kind:attrKind lts_transition_notation $lts $sym) =>
     `(
-      notation3 t:39 "["μ"]⭢" $sym:str t':39 => (LTS.Tr.toRelation $lts μ) t t'
-      notation3 t:39 "["μs"]↠" $sym:str t':39 => (LTS.MTr.toRelation $lts μs) t t'
+      $kind:attrKind notation3 t:39 "["μ"]⭢" $sym:str t':39 => (LTS.Tr.toRelation $lts μ) t t'
+      $kind:attrKind notation3 t:39 "["μs"]↠" $sym:str t':39 => (LTS.MTr.toRelation $lts μs) t t'
      )
-  | `(lts_transition_notation $lts) =>
+  | `($kind:attrKind lts_transition_notation $lts) =>
     `(
-      notation3 t:39 "["μ"]⭢" t':39 => (LTS.Tr.toRelation $lts μ) t t'
-      notation3 t:39 "["μs"]↠" t':39 => (LTS.MTr.toRelation $lts μs) t t'
+      $kind:attrKind notation3 t:39 "["μ"]⭢" t':39 => (LTS.Tr.toRelation $lts μ) t t'
+      $kind:attrKind notation3 t:39 "["μs"]↠" t':39 => (LTS.MTr.toRelation $lts μs) t t'
      )
 
 /-- This attribute calls the `lts_transition_notation` command for the annotated declaration. -/
@@ -746,11 +746,15 @@ initialize Lean.registerBuiltinAttribute {
           sym := Syntax.mkStrLit (sym.getString ++ " ")
         let lts := lts.getId.updatePrefix decl.getPrefix |> Lean.mkIdent
         liftCommandElabM <| Command.elabCommand (← `(create_lts $(mkIdent decl) $lts))
-        liftCommandElabM <| Command.elabCommand (← `(lts_transition_notation $lts $sym))
+        liftCommandElabM <| (do
+          modifyScope ({ · with currNamespace := decl.getPrefix })
+          Command.elabCommand (← `(scoped lts_transition_notation $lts $sym)))
     | `(attr | lts $lts) =>
         let lts := lts.getId.updatePrefix decl.getPrefix |> Lean.mkIdent
         liftCommandElabM <| Command.elabCommand (← `(create_lts $(mkIdent decl) $lts))
-        liftCommandElabM <| Command.elabCommand (← `(lts_transition_notation $lts))
+        liftCommandElabM <| (do
+          modifyScope ({ · with currNamespace := decl.getPrefix })
+          Command.elabCommand (← `(scoped lts_transition_notation $lts)))
     | _ => throwError "invalid syntax for 'lts' attribute"
 }
 

Cslib/Foundations/Semantics/ReductionSystem/Basic.lean

@@ -98,17 +98,17 @@ elab "create_reduction_sys" rel:ident name:ident : command => do
   also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β»
   in the above example.
 -/
-syntax "reduction_notation" ident (str)? : command
+syntax attrKind "reduction_notation" ident (str)? : command
 macro_rules
-  | `(reduction_notation $rs $sym) =>
+  | `($kind:attrKind reduction_notation $rs $sym) =>
     `(
-      notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red  $rs) t t'
-      notation3 t:39 " ↠" $sym:str t':39 => (ReductionSystem.MRed $rs) t t'
+      $kind:attrKind notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red  $rs) t t'
+      $kind:attrKind notation3 t:39 " ↠" $sym:str t':39 => (ReductionSystem.MRed $rs) t t'
      )
-  | `(reduction_notation $rs) =>
+  | `($kind:attrKind reduction_notation $rs) =>
     `(
-      notation3 t:39 " ⭢ " t':39 => (ReductionSystem.Red  $rs) t t'
-      notation3 t:39 " ↠ " t':39 => (ReductionSystem.MRed $rs) t t'
+      $kind:attrKind notation3 t:39 " ⭢ " t':39 => (ReductionSystem.Red  $rs) t t'
+      $kind:attrKind notation3 t:39 " ↠ " t':39 => (ReductionSystem.MRed $rs) t t'
      )
 
 
@@ -133,11 +133,15 @@ initialize Lean.registerBuiltinAttribute {
           sym := Syntax.mkStrLit (sym.getString ++ " ")
         let rs := rs.getId.updatePrefix decl.getPrefix |> Lean.mkIdent
         liftCommandElabM <| Command.elabCommand (← `(create_reduction_sys $(mkIdent decl) $rs))
-        liftCommandElabM <| Command.elabCommand (← `(reduction_notation $rs $sym))
+        liftCommandElabM <| (do
+          modifyScope ({ · with currNamespace := decl.getPrefix })
+          Command.elabCommand (← `(scoped reduction_notation $rs $sym)))
     | `(attr | reduction_sys $rs) =>
         let rs := rs.getId.updatePrefix decl.getPrefix |> Lean.mkIdent
         liftCommandElabM <| Command.elabCommand (← `(create_reduction_sys $(mkIdent decl) $rs))
-        liftCommandElabM <| Command.elabCommand (← `(reduction_notation $rs))
+        liftCommandElabM <| (do
+          modifyScope ({ · with currNamespace := decl.getPrefix })
+          Command.elabCommand (← `(scoped reduction_notation $rs)))
     | _ => throwError "invalid syntax for 'reduction_sys' attribute"
 }