Commit 5b8fa17f by Danny Willems

Lexer and parser. Ok on simple example. Fail with unboun variable on more_complex.inria

parent 782a8a5c
{
open Lexing
let next_line lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{
pos with pos_bol = lexbuf.Lexing.lex_curr_pos;
pos_lnum = pos.Lexing.pos_lnum + 1
}
}
let abstraction = "lambda"
let type_abstraction = "Lambda"
let for_all = "forall"
let projection = "proj" ['0'-'9']+
let white = [' ' '\t' '\r']
let newline = ['\n']
rule prog = parse
| white { prog lexbuf }
| newline { next_line lexbuf; prog lexbuf }
| ',' { Parser.COMMA }
| abstraction { Parser.ABSTRACTION }
| type_abstraction { Parser.TYPEABSTRACTION }
| "let" { Parser.LET }
| "in" { Parser.IN }
| for_all { Parser.FORALL }
| '[' { Parser.LSQUAREBRACKET }
| ']' { Parser.RSQUAREBRACKET }
| '(' { Parser.LPARENT }
| ')' { Parser.RPARENT }
| '=' { Parser.EQUAL }
| ':' { Parser.COLON }
| '.' { Parser.DOT }
| '*' { Parser.STAR }
| "->" { Parser.ARROW }
| projection as l {
let len = String.length l in
Parser.PROJECTION(int_of_string @@ String.sub l 4 (len - 4))
}
| ['a'-'z']+ as id {
Parser.VAR(id)
}
| ['A'-'Z']+ ['a'-'z' 'A'-'Z']* as id {
Parser.TYPEVAR(id)
}
| _ { failwith "Illegal character" }
| eof { Parser.EOF}
%token ARROW
%token COLON
%token COMMA
%token DOT
%token STAR /* For product */
%token LPARENT
%token RPARENT
%token LSQUAREBRACKET
%token RSQUAREBRACKET
%token EQUAL
%token FORALL
%token LET
%token IN
%token <string> TYPEVAR
%token <string> VAR
%token <int> PROJECTION
%token ABSTRACTION /* small lambda */
%token TYPEABSTRACTION /* capital lambda */
%token EOF
%start <F.raw_term> top_level
%%
(* A top level is a term. See that only terms are accepted as top level
expression. Type term like type application is not allowed.
Parenthesis is not mandatory for the top level expressions.
*)
top_level:
| t = term ; EOF { t }
term:
(* Simple variable *)
| id = VAR { F.TeVar(id) }
(* Term abstraction *)
| ABSTRACTION ;
bv = VAR ;
COLON ;
typevar = type_term ;
t = term {
F.TeAbs(bv, typevar, t)
}
(* Build a type application *)
| t1 = term ;
LSQUAREBRACKET ;
t2 = type_term ;
RSQUAREBRACKET {
F.TeTyApp(t1, t2)
}
(* Build a pair *)
| LPARENT ;
t1 = term ;
COMMA ;
t2 = term ;
RPARENT {
F.TePair(t1, t2)
}
(* Build a projection *)
| i = PROJECTION ;
t = term {
F.TeProj(i, t)
}
(* Build a term application. It must be surround by parenthesis: it avoids
conflicts between (id [A] x), (id [B] y) and id [A] (x, id [B] y)
By a previous rule, we can add as many parenthesis as we want.
*)
|
t1 = term ;
t2 = term {
F.TeApp(t1, t2)
}
(* Build a Let definition *)
| LET ;
bv = VAR ;
EQUAL ;
t1 = term ;
IN ;
t2 = term {
F.TeLet(bv, t1, t2)
}
(* Type abstraction *)
| TYPEABSTRACTION ;
id = TYPEVAR ;
t = term {
F.TeTyAbs(id, t)
}
(* Surround term with nested parentheses. Allow to add an infinite number of
parenthesis without modifying the meaning
*)
| LPARENT ;
t = term ;
RPARENT {
t
}
type_term:
| id = TYPEVAR { F.TyVar(id) }
| ty1 = type_term ; STAR ; ty2 = type_term { F.TyProduct(ty1, ty2) }
| t1 = type_term ; ARROW ; t2 = type_term { F.TyArrow(t1, t2) }
| FORALL ; id = TYPEVAR ; DOT ; t = type_term { F.TyForall(id, t) }
| LPARENT ; t = type_term ; RPARENT { t }
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment