Commit 0a129b04 authored by Danny Willems's avatar Danny Willems

Allow multiple expression with ;;. Add new examples.

parent dd19e2e5
......@@ -33,11 +33,17 @@ let check (t : raw_term) =
(* -------------------------------------------------------------------------- *)
let rec eval_file f =
try
check @@ Parser.top_level Lexer.prog f;
eval_file f
with End_of_file -> ()
let () =
let argc = Array.length Sys.argv in
if argc > 1 then
if argc > 1
then
let f = open_in @@ Array.get Sys.argv 1 in
check @@ Parser.top_level Lexer.prog (Lexing.from_channel f);
eval_file (Lexing.from_channel f);
close_in f
else print_endline "You must give a file."
......@@ -11,8 +11,8 @@
}
let abstraction = "lambda"
let type_abstraction = "Lambda"
let abstraction = "\\"
let type_abstraction = "\\\\"
let for_all = "forall"
let projection = "proj" ['0'-'9']+
......@@ -34,6 +34,7 @@ rule prog = parse
| ')' { Parser.RPARENT }
| '=' { Parser.EQUAL }
| ':' { Parser.COLON }
| ';' { Parser.SEMICOLON }
| '.' { Parser.DOT }
| '*' { Parser.STAR }
| "->" { Parser.ARROW }
......
......@@ -3,6 +3,7 @@
%token COMMA
%token DOT
%token STAR /* For product */
%token SEMICOLON
%token LPARENT
%token RPARENT
......@@ -35,7 +36,8 @@
Parenthesis is not mandatory for the top level expressions.
*)
top_level:
| t = term ; EOF { t }
| t = term ; SEMICOLON ; SEMICOLON { t }
| EOF { raise End_of_file }
term:
(* Simple variable *)
......@@ -45,6 +47,17 @@ term:
bv = VAR ;
COLON ;
typevar = type_term ;
DOT ;
t = term {
F.TeAbs(bv, typevar, t)
}
| ABSTRACTION ;
LPARENT ;
bv = VAR ;
COLON ;
typevar = type_term ;
RPARENT ;
DOT ;
t = term {
F.TeAbs(bv, typevar, t)
}
......@@ -90,6 +103,7 @@ term:
(* Type abstraction *)
| TYPEABSTRACTION ;
id = TYPEVAR ;
DOT ;
t = term {
F.TeTyAbs(id, t)
}
......
Lambda B
(lambda y : B
let id = Lambda A (lambda x : A x) in
(id [A] x, id [B] y)
)
\\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 . \(x : A) . (\\A . \(x : A) . x) [A] x;;
\ No newline at end of file
Lambda A (lambda x : A (Lambda A lambda x : A x) [A] x)
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