Commit 2e8bb630 by POTTIER Francois

Merge branch 'lexer_parser' into 'master'

Lexer parser

See merge request !1
parents 36252ead 6fa100f6
......@@ -35,54 +35,17 @@ let check (t : raw_term) =
(* -------------------------------------------------------------------------- *)
(* Sample well-typed terms. *)
let identity =
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"))
let terms : raw_term list = [
identity;
TeTyAbs ("A", TeAbs ("x", TyVar "A",
TeApp (TeTyApp (identity, TyVar "A"), TeVar "x")
));
TeTyAbs ("A", TeAbs ("x", TyVar "A",
TeTyAbs ("B", TeAbs ("y", TyVar "B",
TeLet ("id", identity,
TePair (
TeApp (TeTyApp (TeVar "id", TyVar "A"), TeVar "x"),
TeApp (TeTyApp (TeVar "id", TyVar "B"), TeVar "y")
)
)
))));
]
let rec eval_file f =
try
check @@ Parser.top_level Lexer.prog f;
eval_file f
with End_of_file -> ()
let () =
List.iter check terms
(* -------------------------------------------------------------------------- *)
(* Sample ill-typed terms. *)
let ill_typed : raw_term list = [
TeTyAbs ("A", TeAbs ("x", TyVar "A", TeApp (TeVar "x", TeVar "x")));
TeProj (1, identity);
TeTyAbs ("A",
TeLet ("id", TeAbs ("x", TyVar "A", TeVar "x"),
TeTyApp (TeVar "id", TyVar "A")
)
);
]
let () =
List.iter check ill_typed
(* TEMPORARY report unbound term variables, with locations. *)
(* TEMPORARY report unbound type variables, with locations. *)
let argc = Array.length Sys.argv in
if argc > 1
then
let f = open_in @@ Array.get Sys.argv 1 in
eval_file (Lexing.from_channel f);
close_in f
else print_endline "You must give a file."
......@@ -5,6 +5,9 @@ open F
let arrow =
string "->"
let backslash =
string "\\"
let doublebackslash =
string "\\\\"
......@@ -14,7 +17,7 @@ let forall =
let rec typ0 ty =
match ty with
| TyVar x ->
string x
string x
| TyArrow _
| TyProduct _
| TyForall _ ->
......@@ -66,7 +69,7 @@ and term1 t =
and term2 t =
match t with
| TePair (t1, t2) ->
group (term1 t1 ^^ comma ^/^ term2 t2)
group (lparen ^^ term1 t1 ^^ comma ^/^ term2 t2 ^^ rparen)
| _ ->
term1 t
......@@ -74,8 +77,8 @@ and term3 t =
match t with
| TeAbs (x, ty, t) ->
block
(backslash ^^ string x ^^ spacecolon)
(break 1 ^^ typ ty)
(backslash ^^ string "(" ^^ string x ^^ spacecolon)
(break 1 ^^ typ ty ^^ string ")")
(break 1 ^^ dot)
^/^
term3 t
......
......@@ -5,4 +5,5 @@ true: \
package(pprint), \
package(visitors.ppx), \
package(visitors.runtime), \
package(alphaLib)
package(alphaLib), \
use_menhir
\ No newline at end of file
{
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 = "\\"
let type_abstraction = "\\\\"
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.SEMICOLON }
| '.' { 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 SEMICOLON
%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.
Parentheses are not mandatory for the top level expressions.
A top level expression must be ended with ;; to evaluate it (as in OCaml).
*)
top_level:
| t = term ; SEMICOLON ; SEMICOLON { t }
| EOF { raise End_of_file }
term:
(* Simple variable *)
| id = VAR { F.TeVar(id) }
(* Term abstraction *)
| ABSTRACTION ;
bv = VAR ;
COLON ;
typevar = type_term ;
DOT ;
t = term {
F.TeAbs(bv, typevar, t)
}
(* Build an abstraction. For ease of reading when the variable type is long,
parentheses are added around the variable and the type.
*)
| ABSTRACTION ;
LPARENT ;
bv = VAR ;
COLON ;
typevar = type_term ;
RPARENT ;
DOT ;
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. No parentheses are mandatory.
*)
|
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 ;
DOT ;
t = term {
F.TeTyAbs(id, t)
}
(* Surround term with nested parentheses. Allow to add an infinite number of
parentheses.
*)
| 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 }
\\B . \\A . \(x : A) . \(y : B) . proj1 (x, y);;
\\A . \\B . \(x : A) . \(y : B) . let p = (x, (y, (x, y))) in proj1 p;;
\\A . \\B . \(x : A) . \(y : B) . let p = (x, (y, (x, y))) in proj2 proj2 p;;
\\A . \(x : A) . \\B . \(y : B) . let id = \\A . \(x : A) . x in (id [A] x, id [B] y);;
\\A . \(x : A -> A) . \(y : A) . x y;;
\\A . \(x : A) . x;;
\\A . \\B . \(x : A) . \(y : B) . (x, y);;
\\A . \\B . \(x : A) . \(y : B) . let p = (x, y) in proj1 p;;
\\A . \(x : A) . (\\A . \(x : A) . x) [A] x;;
\\A . \\B . \(p : A * B) . proj1 p;;
\\A . \\B . \(p : A * B) . proj2 p;;
\ No newline at end of file
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