can parse trivial

h0nzZik · Apr 15, 2024 · a1c7683 · a1c7683
1 parent 6967304
commit a1c7683
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 10 deletions.
diff --git a/minuska/bin/lexer.mll b/minuska/bin/lexer.mll
@@ -13,17 +13,15 @@ let float = digit* frac? exp?
 
 let white = [' ' '\t']+
 let newline = '\r' | '\n' | "\r\n"
-let id = ['a'-'z'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
+let id = ['a'-'z'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '.']*
 let var = ['A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
 
 
 rule read =
   parse
   | white        { read lexbuf }
-  | int          { INT (int_of_string (Lexing.lexeme lexbuf)) }
-  | id           { ID (Lexing.lexeme lexbuf)  }
-  | var           { VAR (Lexing.lexeme lexbuf)  }
-
+  | newline  { Lexing.new_line lexbuf; read lexbuf }
+
   | '('          { BRACKET_ROUND_LEFT }
   | ')'          { BRACKET_ROUND_RIGHT }
   | '['          { BRACKET_SQUARE_LEFT }
@@ -42,5 +40,10 @@ rule read =
   | ":"          { COLON }
   | ':'          { COLON }
   | ','          { COMMA }
+
+  | int          { INT (int_of_string (Lexing.lexeme lexbuf)) }
+  | id           { ID (Lexing.lexeme lexbuf)  }
+  | var           { VAR (Lexing.lexeme lexbuf)  }
+
   | _            { raise (SyntaxError ("Unexpected char: " ^ Lexing.lexeme lexbuf)) }
   | eof          { EOF }
diff --git a/minuska/bin/parser.mly b/minuska/bin/parser.mly
@@ -29,7 +29,9 @@
 symbolsdecl:
   | KEYWORD_SYMBOLS
     COLON
+    BRACKET_SQUARE_LEFT
     v = separated_list(COMMA, ID)
+    BRACKET_SQUARE_RIGHT
     SEMICOLON
     { v }
   ;
@@ -50,29 +52,40 @@ strictnessone:
 strictnessall:
   | KEYWORD_STRICTNESS;
     COLON;
+    BRACKET_SQUARE_LEFT;
     ss = separated_list(COMMA, strictnessone);
+    BRACKET_SQUARE_RIGHT;
+    SEMICOLON;
     { ss }
   ;
 
 
 pattern:
   | x= VAR
     { `PVar (`Var x) }
-  | s= ID BRACKET_SQUARE_LEFT es= separated_list(COMMA, pattern) BRACKET_SQUARE_RIGHT
+  | s = ID
+    BRACKET_SQUARE_LEFT 
+    es = separated_list(COMMA, pattern)
+    BRACKET_SQUARE_RIGHT
     { `PTerm ((`Id s), es) }
   ;
 
 groundterm:
   | s = ID;
+    BRACKET_SQUARE_LEFT
     ts = separated_list(COMMA, groundterm)
+    BRACKET_SQUARE_RIGHT
     { `GTerm ((`Id s),ts)}
   ;  
 
 
 expr:
   | x = VAR
     { `EVar (`Var x) }
-  | g = groundterm
+  | 
+    BRACKET_SQUARE_LEFT
+    g = groundterm
+    BRACKET_SQUARE_RIGHT
     { `EGround g }
   | s = ID
     BRACKET_ROUND_LEFT
@@ -97,7 +110,9 @@ valuedecl:
     x = VAR 
     BRACKET_ROUND_RIGHT
     COLON 
+    BRACKET_ROUND_LEFT
     e = expr
+    BRACKET_ROUND_RIGHT
     SEMICOLON
     { (x,e) }
   ;

diff --git a/minuska/imp.m b/minuska/imp.m
@@ -1,10 +1,10 @@
-symbols: plus, minus, ite, while, unitValue ;
+symbols : plus, minus, ite, while, unitValue ;
 
-value(X): bool.or(Z.is(X), Bool.or(Bool.is(X), Symbol.is(unitValue, X))) ;
+value(X): bool.or(z.is(X), bool.or(bool.is(X), symbol.is(unitValue, X))) ;
 
 
 strictness: plus of arity 3 in [0,1] ;
-rule/simple plus-Z-Z: plus[X,Y] =>{a} Z.plus(X, Y) where bool.and(Z.is(X), Z.is(Y)) ;
+rule/simple plus-z-z: plus[X,Y] =>{a} z.plus(X, Y) where bool.and(z.is(X), z.is(Y)) ;
 
 rule/simple [stmt-ite-true]:
 	ite[B,X,Y] => X where B ;

diff --git a/minuska/trivial.m b/minuska/trivial.m
@@ -0,0 +1,8 @@
+symbols : [s] ;
+
+value(X): (bool.false() ) ;
+
+strictness: [] ;
+
+
+