Minor type and transformation sketches

Author: d-plaindoux

README.md

@@ -29,7 +29,7 @@ occurrence   = ("*" | "+" | "?")
 additional   = "|" ? parser
 transform    = "->" '{' rust_code '}'
 atom         = alter? '(' parser? ')' | CHAR | STRING | ident
-alter        = ("^" | "!" | "#" | "/")
+alter        = ("^" | "!" | "#")
 ident        = [a..zA..Z][a..zA..Z0..9_] * - {"let"}
 ```
 
@@ -185,8 +185,8 @@ let stream = ParserStream::new( & tokenizer, CharStream::new("1 + 2"));
 let response = expr().and_left(eos()).parse(stream);
 
 match response {
-Success(v, _, _) => assert_eq!(v.eval(), 3),
-_ => assert_eq!(true, false),
+    Success(v, _, _) => assert_eq!(v.eval(), 3),
+    _ => assert_eq!(true, false),
 }
 ```
 

lang/v1/normalizer/src/ast.rs

@@ -20,32 +20,32 @@ pub enum ASTGrammar<A> {
     Bottom(),
     Var(String),
     Token(A),
-    TokenChar(char),
     Seq(Box<AST<A>>, Box<AST<A>>),
     Choice(Box<AST<A>>, Box<AST<A>>),
     Rec(String, Box<AST<A>>),
+    // Extension for capture and transformation
+    Bind(String, Box<AST<A>>),
+    Map(Box<AST<A>>, String),
+    // Negation for alternate paths
+    Not(Box<AST<A>>),
 }
 
 /*
-   PBind(String, Box<ASTParsec>),  // Variable
-   PMap(Box<ASTParsec>, String),   // Map
-   PNot(Box<ASTParsec>),           // Negation
-
-   -- Pre-normalization
-
+   PN : ASTParsec -> (string -> ASTParsec) -> string list -> ASTGrammar
    PN : ASTParsec -> (string -> ASTParsec) -> string list -> ASTGrammar
 
-                               / Var(n)               if n in l
-   PN[PIdent(n)]gl          = {
-                               \ mu(n,PN[g(n)]g(n::l) otherwise
-
+   PN[PIdent(n)]gl          = Var(n)               if n in l
+                            | mu(n,PN[g(n)]g(n::l) otherwise
    PN[PAtom(c)]gl           = TokenChar(c)
    PN[PAtoms([])]gl         = Epsilon()
-   PN[PAtoms(c::l)]gl       = Seq(TokenChar(v),PN[PAtoms(c::l)]gl)
+   PN[PAtoms(c::l)]gl       = Seq(Token(v),PN[PAtoms(c::l)]gl)
    PN[PEpsilon()]gl         = Epsilon()
    PN[PSequence(T1,T2]]gl   = Seq(PN[T1]gl,PN[T2]gl)
    PN[PChoice(T1,T2)]gl     = Choice(PN[T1]gl,PN[T2]gl)
-   PN[PRepeat(T)]gl         = PN[T]gl | mu(n,Choice(Seq(PN[T]gl,Var(n)),Epsilon()))
+   PN[PRepeat(T)]gl         = PN[T]gl|mu(n,Choice(Seq(PN[T]gl,Var(n)),Epsilon())) - fresh n not in l
    PN[PTry(T)gl]            = PN[T]gl
-   PN[PCheck(T]gl]          = PN[T]gl
+   PN[PCheck(T)gl]          = PN[T]gl
+   PN[PBind(s,T)]gl         = Bind(s,PN[T]gl)
+   PN[PMap(T,s)]gl          = Map(PN[T]gl,s)
+   PN[PNot(T)]gl            = Not(PN[T]gl)
 */

lang/v1/normalizer/src/dgnf.rs

@@ -27,11 +27,11 @@ Normalization of well-typed context-free expressions.
 (seq)       N 𝑔1·𝑔2 = 𝑛⇒{𝑛→𝑁1 𝑛2 |𝑛1 →𝑁1 ∈𝐺1 }∪𝐺1 ∪𝐺2
                       where N 𝑔1 = 𝑛1 ⇒𝐺1 ∧N 𝑔2 = 𝑛2 ⇒𝐺2
 (alt)       N 𝑔1∨𝑔2 = 𝑛⇒{𝑛→𝑁1 |𝑛1 →𝑁1 ∈𝐺1 }∪{𝑛→𝑁2 |𝑛2 →𝑁2 ∈𝐺2 }∪𝐺1 ∪𝐺2
-                       where N 𝑔1 = 𝑛1 ⇒𝐺1 ∧N 𝑔2 = 𝑛2 ⇒𝐺2
+                      where N 𝑔1 = 𝑛1 ⇒𝐺1 ∧N 𝑔2 = 𝑛2 ⇒𝐺2
 (fix)       N 𝜇𝛼.𝑔  = 𝛼 ⇒{𝛼 →𝑁 |𝑛→𝑁 ∈𝐺} (1)
                         ∪{𝑛′→𝑁 𝑛′|𝑛′→𝛼𝑛′∈𝐺∧𝑛→𝑁 ∈𝐺} (2)
                         ∪𝐺\𝑛′→𝛼 𝑛′ (3)
-                    where N 𝑔= 𝑛⇒𝐺
+                      where N 𝑔= 𝑛⇒𝐺
                         𝐺\𝑛′→𝛼 𝑛′ is 𝐺 with all 𝑛′→𝛼𝑛′removed for any 𝑛′and 𝑛′
 (var)       N 𝛼     = 𝑛⇒{𝑛→𝛼}