Commit bc968c1b authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Field update

parent bedb2e0d
......@@ -16,7 +16,8 @@ rule token = parse
| ')' { RPAR }
| "ς" { SIGMA }
| '=' { EQUAL }
| ":=" { DEF }
| "::=" { DEF }
| ":=" { FUPD }
| '.' { DOT }
| "->" { ARR }
| "λ" { LAMBDA }
......
......@@ -12,7 +12,7 @@
%}
%token <string> ID CID SELECT UPDATE
%token LBRACK RBRACK COLUMN SEMICOLUMN LPAR RPAR SIGMA EQUAL DEF DOT
%token LBRACK RBRACK COLUMN SEMICOLUMN LPAR RPAR SIGMA EQUAL DEF DOT FUPD
%token LAMBDA ARR
%token <Lexing.position> TYPE VAR CHECK NORM
......@@ -40,11 +40,17 @@ type_elems: /* empty */ { [] }
term: ID { Var (Id ($1)) }
| LPAR term RPAR { Par ($2) }
obj: ID { Var (Id ($1)) }
| LPAR term RPAR { Par ($2) }
| LBRACK obj_elems RBRACK { Obj ($2) }
;
term: obj { $1 }
/* | term term { App ($1, $2) } */
| LAMBDA LPAR ID COLUMN ty RPAR term { Abst (Id ($3), $5, $7)}
| LBRACK obj_elems RBRACK { Obj ($2) }
| term SELECT { Select ($1, Label ($2)) }
| term UPDATE meth { Update ($1, Label ($2), $3) }
| LAMBDA LPAR ID COLUMN ty RPAR obj { Abst (Id ($3), $5, $7)}
| obj SELECT { Select ($1, label ($2)) }
| obj UPDATE meth { Update ($1, label ($2), $3) }
| obj DOT ID FUPD term { Field_update ($1, label ($3), $5) }
;
meth: SIGMA LPAR ID COLUMN ty RPAR term { Method (Id ($3), $5, $7) }
......
......@@ -18,11 +18,12 @@ type term =
| Obj of (label * meth) list
| Select of term * label
| Update of term * label * meth
| Field_update of term * label * term
and meth = Method of id * stype * term;;
type line =
| Typedef of cid * cid list * stype
| Typedef of cid * stype
| Vardef of id * stype * term
| Check of term * stype
| Norm of term
......
......@@ -17,6 +17,7 @@ type sterm =
| Sobj of (label * smeth) list
| Ssel of sterm * label
| Supd of sterm * label * smeth
| Sfupd of sterm * label * sterm
and smeth =
| Smeth of id * sty * sterm
......@@ -71,6 +72,10 @@ let rec scope_term ty_env const_env var_env : term -> sterm = function
Supd (scope_term ty_env const_env var_env t,
l,
scope_method ty_env const_env var_env m)
| Field_update (t1, l, t2) ->
Sfupd (scope_term ty_env const_env var_env t1,
l,
scope_term ty_env const_env var_env t2)
and scope_method ty_env const_env var_env (Method (id, ty, body)) =
let sty = scope_ty ty_env ty in
Smeth (id, sty, scope_term ty_env const_env ((id, sty) :: var_env) body)
......
......@@ -14,6 +14,7 @@ type sterm =
| Sobj of (label * smeth) list
| Ssel of sterm * label
| Supd of sterm * label * smeth
| Sfupd of sterm * label * sterm
and smeth =
| Smeth of id * sty * sterm
......
type A := [].
var a : A := [].
check a : [].
norm a.
type
\ No newline at end of file
type A ::= [ a : [] ].
type Bool ::= [ if : A ; then : A ; else : A ].
var true : Bool ::= [ if = ς(x : Bool) x.then ;
then = ς(x : Bool) x.then ;
else = ς(x : Bool) x.else ].
var false : Bool ::= [ if = ς(x : Bool) x.else ;
then = ς(x : Bool) x.then ;
else = ς(x : Bool) x.else ].
var if : Bool -> A -> A -> A ::=
λ(b : Bool) λ(t : A) λ(e : A) ((b.then := t).else := e).if.
type Nat ::= [ iszero : Bool ;
pred : A ].
var 0 : Nat ::= [ iszero = ς(x : Nat) true ;
pred = ς(x : Nat) x.pred ].
......@@ -82,7 +82,21 @@ let rec type_term env : sterm -> tterm = function
Tsel (tt, l, sty_assoc l ty)
| Supd (t, l, m) ->
let tt = type_term env t in
Tupd (tt, l, type_meth env m, infer tt)
let tty = infer tt in
let Tmeth (_, ty, _, rty) = type_meth env m in
let expected_rty = sty_assoc l ty in
if subtype tty ty then (
if subtype rty expected_rty then
Tupd (tt, l, type_meth env m, tty)
else
raise (Subtype_checking_error (rty, expected_rty)))
else
raise (Subtype_checking_error (tty, ty))
| Sfupd (t1, l, t2) ->
let tt1 = type_term env t1 in
let tty1 = infer tt1 in
let tt2 = type_term env t2 in
Tupd (tt1, l, Tmeth (dummy_var, tty1, tt2, infer tt2), tty1)
and type_meth env (Smeth (x, ty, body)) =
let tbody = type_term ((x, ty) :: env) body in
(Tmeth (x, ty, tbody, infer tbody))
......
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