Permalink
Browse files

Process integers.

  • Loading branch information...
xlq committed Aug 25, 2012
1 parent be65496 commit 79cea3466a05433abf16c49518ea233e5821ff06
Showing with 97 additions and 27 deletions.
  1. +1 −1 Makefile
  2. +2 −0 icode.ml
  3. +17 −11 lexer.mll
  4. +1 −0 parse_tree.mli
  5. +13 −4 parser.mly
  6. +25 −3 solving.ml
  7. +16 −3 symbols.ml
  8. +4 −1 symbols.mli
  9. +5 −1 translation.ml
  10. +13 −3 type_checking.ml
@@ -2,7 +2,7 @@
all:
ocamlbuild main.d.byte -cflags -w,-8 -libs nums
# ocamlbuild main.d.byte -libs nums
@# ocamlbuild main.d.byte -libs nums
clean:
ocamlbuild -clean main.d.byte
@@ -126,6 +126,8 @@ let calculate_free_names (blocks: block list): unit =
(* x is not bound - it was live at the start of this block. *)
Symbols.Sets.add x free
end
| Operation(op, lhs, rhs) ->
esearch (esearch free bound lhs) bound rhs
in
block.bl_free <- search Symbols.Sets.empty Symbols.Sets.empty
(unsome block.bl_body)
@@ -47,17 +47,23 @@ rule scan = parse
with Not_found -> IDENT(id)
}
| ['0'-'9']+ as value { INTEGER(big_int_of_string value) }
| '(' { LPAREN }
| ')' { RPAREN }
| '[' { LBRACKET }
| ']' { RBRACKET }
| '{' { LBRACE }
| '}' { RBRACE }
| ':' { COLON }
| ';' { SEMICOLON }
| '.' { DOT }
| ',' { COMMA }
| '(' { LPAREN }
| ')' { RPAREN }
| '[' { LBRACKET }
| ']' { RBRACKET }
| '{' { LBRACE }
| '}' { RBRACE }
| ':' { COLON }
| ';' { SEMICOLON }
| '.' { DOT }
| ',' { COMMA }
| ":=" { ASSIGN }
| ".." { DOTDOT }
| "=>" { RARROW }
| eof { EOF }
| '=' { EQ }
| "<>" { NE }
| '<' { LT }
| '>' { GT }
| "<=" { LE }
| ">=" { GE }
| eof { EOF }
@@ -47,3 +47,4 @@ and expr =
| Name of loc * dotted_name
| Boolean_literal of loc * bool
| Integer_literal of loc * big_int
| Operation of loc * Symbols.operator * expr * expr
@@ -30,10 +30,13 @@ let check_end (pos1, name1) (pos2, name2) =
/* Punctuation */
%token COLON SEMICOLON DOT DOTDOT COMMA ASSIGN RARROW
%token LPAREN RPAREN LBRACKET RBRACKET LBRACE RBRACE
%token EQ NE LT LE GT GE
/* Other */
%token EOF
%nonassoc EQ NE LT LE GT GE
%start subprogram
%type <Parse_tree.subprogram> subprogram
@@ -120,7 +123,13 @@ while_loop:
{ While_loop(pos (), $2, $4, $8) }
expr:
| dotted_name { Name(pos (), $1) }
| INTEGER { Integer_literal(pos (), $1) }
| TRUE { Boolean_literal(pos (), true) }
| FALSE { Boolean_literal(pos (), false) }
| dotted_name { Name(pos (), $1) }
| INTEGER { Integer_literal(pos (), $1) }
| TRUE { Boolean_literal(pos (), true) }
| FALSE { Boolean_literal(pos (), false) }
| expr EQ expr { Operation(rhs_end_pos 2, Symbols.EQ, $1, $3) }
| expr NE expr { Operation(rhs_end_pos 2, Symbols.NE, $1, $3) }
| expr LT expr { Operation(rhs_end_pos 2, Symbols.LT, $1, $3) }
| expr GT expr { Operation(rhs_end_pos 2, Symbols.GT, $1, $3) }
| expr LE expr { Operation(rhs_end_pos 2, Symbols.LE, $1, $3) }
| expr GE expr { Operation(rhs_end_pos 2, Symbols.GE, $1, $3) }
@@ -17,7 +17,7 @@ let rec subst (x_sym, x_version) replacement m =
| Integer_literal _ -> m
| Var_version(x,v) when (x == x_sym) && (v = x_version) -> replacement
| Var_version _ -> m
| Equal(i,j) -> Equal(r i, r j)
| Operation(op,i,j) -> Operation(op, r i, r j)
| For_all(x,v,n) when (x == x_sym) && (v = x_version) -> m
| For_all(x,v,n) -> For_all(x,v,r n)
| Conjunction p -> Conjunction (List.map r p)
@@ -35,12 +35,34 @@ let convert (constr: expr): inequality list =
| Var_version(x,v) ->
(* Must be boolean *)
(pos, (Var_version(x,v))::neg)
| Operation(EQ, m, Boolean_literal(true))
| Operation(EQ, Boolean_literal(true), m)
| Operation(NE, m, Boolean_literal(false))
| Operation(NE, Boolean_literal(false), m) ->
(pos, m::neg)
| Operation(EQ, m, Boolean_literal(false))
| Operation(EQ, Boolean_literal(false), m)
| Operation(NE, m, Boolean_literal(true))
| Operation(NE, Boolean_literal(true), m) ->
(m::pos, neg)
| Operation((LT|GT|LE|GE), lhs, rhs) as m ->
(pos, m::neg)
and positive (pos, neg) = function
| Equal(i,j) ->
(Equal(i,j)::pos, neg)
| Conjunction p ->
List.fold_left (fun ax p -> positive ax p) (pos, neg) p
| Operation(EQ, m, Boolean_literal(true))
| Operation(EQ, Boolean_literal(true), m)
| Operation(NE, m, Boolean_literal(false))
| Operation(NE, Boolean_literal(false), m) ->
(m::pos, neg)
| Operation(EQ, m, Boolean_literal(false))
| Operation(EQ, Boolean_literal(false), m)
| Operation(NE, m, Boolean_literal(true))
| Operation(NE, Boolean_literal(true), m) ->
(pos, m::neg)
| Operation((LT|GT|LE|GE), lhs, rhs) as m ->
(m::pos, neg)
in
let pos, neg = negative ([], []) constr in
@@ -3,6 +3,9 @@ open Misc
type version = int
type operator =
| EQ | NE | LT | GT | LE | GE
type ttype =
| Unknown_type of unknown
| Unit_type
@@ -19,7 +22,7 @@ and expr =
| Integer_literal of big_int
| Var of symbol
| Var_version of symbol * version
| Equal of expr * expr
| Operation of operator * expr * expr
| For_all of symbol * version * expr
| Conjunction of expr list
| Implication of expr * expr
@@ -71,14 +74,24 @@ let rec full_name sym =
let full_name_with_version sym version =
full_name sym ^ "#" ^ string_of_int version
let string_of_op = function
| EQ -> "="
| NE -> "<>"
| LT -> "<"
| GT -> ">"
| LE -> "<="
| GE -> ">="
let rec string_of_expr = function
| Boolean_literal true -> "True"
| Boolean_literal false -> "False"
| Integer_literal i -> string_of_big_int i
| Var sym -> full_name sym
| Var_version(sym,version) -> full_name_with_version sym version
| Equal(m,n) ->
string_of_expr m ^ " = " ^ string_of_expr n
| Operation(op,m,n) ->
string_of_expr m ^ " "
^ string_of_op op ^ " "
^ string_of_expr n
| For_all(a,aver,m) ->
"{" ^ full_name_with_version a aver ^ "} " ^ string_of_expr m
| Conjunction p ->
@@ -1,6 +1,9 @@
open Big_int
type version
type operator =
| EQ | NE | LT | GT | LE | GE
type ttype =
(* Unknown_type means the compiler hasn't decided yet,
@@ -26,7 +29,7 @@ and expr =
| Integer_literal of big_int
| Var of symbol
| Var_version of symbol * version
| Equal of expr * expr
| Operation of operator * expr * expr
| For_all of symbol * version * expr
| Conjunction of expr list
| Implication of expr * expr
@@ -59,7 +59,7 @@ let rec translate_type
("Undefined type `" ^ String.concat "." name ^ "'.");
raise Bail_out
let translate_expr
let rec translate_expr
(context: context)
(expression: Parse_tree.expr): expr
=
@@ -77,6 +77,10 @@ let translate_expr
end
| Parse_tree.Boolean_literal(loc, b) -> Boolean_literal(b)
| Parse_tree.Integer_literal(loc, i) -> Integer_literal(i)
| Parse_tree.Operation(loc, op, lhs, rhs) ->
Operation(op,
translate_expr context lhs,
translate_expr context rhs)
let translate_lvalue
(context: context)
@@ -46,7 +46,8 @@ let rec coerce context t1 t2: constraints * ttype =
match t1, t2 with
| Unit_type, Unit_type ->
no_constraints, Unit_type
| Boolean_type, Boolean_type ->
| Boolean_type, Boolean_type
| Integer_type, Integer_type ->
no_constraints, t1
| Unknown_type(unk), t2 ->
begin match context.tc_pass with
@@ -94,6 +95,15 @@ let rec type_check_expr
let t, version = Symbols.Maps.find x context.tc_vars in
let constr, t = got_type context t in
Var_version(x, version), constr, t
| Operation((EQ|NE|LT|GT|LE|GE) as op, lhs, rhs) ->
let operand_context = {context with tc_expected = None} in
let lhs, lhs_c, lhs_t = type_check_expr operand_context lhs in
let rhs, rhs_c, rhs_t = type_check_expr operand_context rhs in
let _ = coerce context lhs_t rhs_t in
let constr, result_t = got_type context Boolean_type in
(Operation(op, lhs, rhs),
Conjunction [lhs_c; rhs_c; constr],
result_t)
let rec type_check
(context: context)
@@ -138,10 +148,10 @@ let rec type_check
(Conjunction [
condition_constr;
Implication(
Equal(condition, Boolean_literal true),
Operation(EQ, condition, Boolean_literal true),
true_part_constr);
Implication(
Equal(condition, Boolean_literal false),
Operation(EQ, condition, Boolean_literal false),
false_part_constr)
]), Unit_type
| Jump_term(jmp) ->

0 comments on commit 79cea34

Please sign in to comment.