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

Builtin booleans

parent 599c2f93
...@@ -30,6 +30,12 @@ rule token = parse ...@@ -30,6 +30,12 @@ rule token = parse
| '.' { DOT } | '.' { DOT }
| "->" { ARR } | "->" { ARR }
| "λ" { LAMBDA } | "λ" { LAMBDA }
| "Bool" { BOOL }
| "true" { TRUE }
| "false" { FALSE }
| "if" { IF }
| "then" { THEN }
| "else" { ELSE }
| "type" { TYPE (Parsing.rhs_start_pos 1) } | "type" { TYPE (Parsing.rhs_start_pos 1) }
| "let" { VAR (Parsing.rhs_start_pos 1) } | "let" { VAR (Parsing.rhs_start_pos 1) }
| "check" { CHECK (Parsing.rhs_start_pos 1) } | "check" { CHECK (Parsing.rhs_start_pos 1) }
......
...@@ -27,7 +27,7 @@ ...@@ -27,7 +27,7 @@
%token <string> ID CID SELECT UPDATE FUPD STRING %token <string> ID CID SELECT UPDATE FUPD STRING
%token LBRACK RBRACK COLUMN SEMICOLUMN LPAR RPAR SIGMA EQUAL DEF DOT %token LBRACK RBRACK COLUMN SEMICOLUMN LPAR RPAR SIGMA EQUAL DEF DOT
%token LAMBDA ARR %token LAMBDA ARR BOOL TRUE FALSE IF THEN ELSE
%token <Lexing.position> TYPE VAR CHECK NORM PRINT %token <Lexing.position> TYPE VAR CHECK NORM PRINT
%right ARR %right ARR
...@@ -48,6 +48,8 @@ line: TYPE CID DEF ty DOT { ($1, Typedef (Cid ($2), $4)) } ...@@ -48,6 +48,8 @@ line: TYPE CID DEF ty DOT { ($1, Typedef (Cid ($2), $4)) }
ty: CID { Tcid (Cid ($1)) } ty: CID { Tcid (Cid ($1)) }
| LBRACK type_elems RBRACK { Tlist ($2) } | LBRACK type_elems RBRACK { Tlist ($2) }
| ty ARR ty { Tarr ($1, $3) } | ty ARR ty { Tarr ($1, $3) }
| LPAR ty RPAR { $2 }
| BOOL LPAR ty RPAR { Tbool ($3) }
; ;
type_elem: ID COLUMN ty { (label ($1), $3) }; type_elem: ID COLUMN ty { (label ($1), $3) };
...@@ -63,6 +65,8 @@ type_elems: /* empty */ { [] } ...@@ -63,6 +65,8 @@ type_elems: /* empty */ { [] }
obj: ID { Var (Id ($1)) } obj: ID { Var (Id ($1)) }
| LPAR term RPAR { Par ($2) } | LPAR term RPAR { Par ($2) }
| LBRACK obj_elems RBRACK { Obj ($2) } | LBRACK obj_elems RBRACK { Obj ($2) }
| TRUE LPAR ty RPAR { True ($3) }
| FALSE LPAR ty RPAR { False ($3) }
; ;
sterm: obj { $1 } sterm: obj { $1 }
...@@ -77,6 +81,7 @@ term: sterm app { apply $1 $2 } ...@@ -77,6 +81,7 @@ term: sterm app { apply $1 $2 }
| LAMBDA LPAR ID COLUMN ty RPAR term { Abst (Id ($3), $5, $7)} | LAMBDA LPAR ID COLUMN ty RPAR term { Abst (Id ($3), $5, $7)}
| obj UPDATE meth { Update ($1, label ($2), $3) } | obj UPDATE meth { Update ($1, label ($2), $3) }
| obj FUPD sterm { Field_update ($1, label ($2), $3) } | obj FUPD sterm { Field_update ($1, label ($2), $3) }
| IF term THEN term ELSE obj { If ($2, $4, $6) }
; ;
meth: SIGMA LPAR ID COLUMN ty RPAR term { Method (Id ($3), $5, $7) } meth: SIGMA LPAR ID COLUMN ty RPAR term { Method (Id ($3), $5, $7) }
......
type id = Id of string;; type id = Id of string
type cid = Cid of string;; type cid = Cid of string
type label = Label of string;; type label = Label of string
type stype = type stype =
| Tcid of cid | Tcid of cid
| Tlist of (label * stype) list | Tlist of (label * stype) list
| Tarr of stype * stype;; | Tarr of stype * stype
| Tbool of stype
type term = type term =
| Var of id | Var of id
| Par of term | Par of term
| App of term * term | App of term * term
| Abst of id * stype * term | Abst of id * stype * term
| True of stype
| False of stype
| If of term * term * term
| Obj of (label * meth) list | Obj of (label * meth) list
| Select of term * label | Select of term * label
| Update of term * label * meth | Update of term * label * meth
| Field_update of term * label * term | Field_update of term * label * term
and meth = Method of id * stype * term;; and meth = Method of id * stype * term
type line = type line =
| Typedef of cid * stype | Typedef of cid * stype
......
...@@ -32,6 +32,9 @@ let rec print_ty out_fmter = function ...@@ -32,6 +32,9 @@ let rec print_ty out_fmter = function
Format.fprintf out_fmter "@[<hov>dk_obj_examples.arrow@ %a@ %a@]" Format.fprintf out_fmter "@[<hov>dk_obj_examples.arrow@ %a@ %a@]"
print_par_ty ty1 print_par_ty ty1
print_par_ty ty2 print_par_ty ty2
| Stbool ty ->
Format.fprintf out_fmter "@[<hov>dk_obj_examples.boolT@ %a@]"
print_par_ty ty
and print_par_ty out_fmter = function and print_par_ty out_fmter = function
| Stcid _ | Stlist [] as ty -> print_ty out_fmter ty | Stcid _ | Stlist [] as ty -> print_ty out_fmter ty
| ty -> | ty ->
...@@ -57,6 +60,18 @@ let rec print_term out_fmter : tterm -> unit = function ...@@ -57,6 +60,18 @@ let rec print_term out_fmter : tterm -> unit = function
print_id x print_id x
print_par_ty ty print_par_ty ty
print_term body print_term body
| Ttrue ty ->
Format.fprintf out_fmter "@[<hov>dk_obj_examples.trueT@ %a@]"
print_par_ty ty
| Tfalse ty ->
Format.fprintf out_fmter "@[<hov>dk_obj_examples.falseT@ %a@]"
print_par_ty ty
| Tif (b, t, e, ty) ->
Format.fprintf out_fmter "@[<hov>dk_obj_examples.ifT@ %a@ %a@ %a@ %a@]"
print_par_ty ty
print_par_term b
print_par_term t
print_par_term e
| Tobj (ll, ty) -> | Tobj (ll, ty) ->
print_object ty out_fmter ll print_object ty out_fmter ll
| Tsel (t, l, ty) -> | Tsel (t, l, ty) ->
......
...@@ -7,6 +7,7 @@ type sty = ...@@ -7,6 +7,7 @@ type sty =
| Stcid of cid * sty | Stcid of cid * sty
| Stlist of (label * sty) list | Stlist of (label * sty) list
| Starr of sty * sty | Starr of sty * sty
| Stbool of sty
type sterm = type sterm =
| Svar of id * sty | Svar of id * sty
...@@ -14,6 +15,9 @@ type sterm = ...@@ -14,6 +15,9 @@ type sterm =
| Spar of sterm | Spar of sterm
| Sapp of sterm * sterm | Sapp of sterm * sterm
| Sabst of id * sty * sterm | Sabst of id * sty * sterm
| Strue of sty
| Sfalse of sty
| Sif of sterm * sterm * sterm
| Sobj of (label * smeth) list | Sobj of (label * smeth) list
| Ssel of sterm * label | Ssel of sterm * label
| Supd of sterm * label * smeth | Supd of sterm * label * smeth
...@@ -44,6 +48,7 @@ let rec scope_ty ty_env = function ...@@ -44,6 +48,7 @@ let rec scope_ty ty_env = function
| Tarr (ty1, ty2) -> | Tarr (ty1, ty2) ->
Starr (scope_ty ty_env ty1, Starr (scope_ty ty_env ty1,
scope_ty ty_env ty2) scope_ty ty_env ty2)
| Tbool ty -> Stbool (scope_ty ty_env ty)
let rec assoc3 v = function let rec assoc3 v = function
| [] -> raise Not_found | [] -> raise Not_found
...@@ -66,6 +71,11 @@ let rec scope_term ty_env const_env var_env : term -> sterm = function ...@@ -66,6 +71,11 @@ let rec scope_term ty_env const_env var_env : term -> sterm = function
| Abst (x, ty, body) -> | Abst (x, ty, body) ->
let sty = scope_ty ty_env ty in let sty = scope_ty ty_env ty in
Sabst (x, sty, scope_term ty_env const_env ((x, sty) :: var_env) body) Sabst (x, sty, scope_term ty_env const_env ((x, sty) :: var_env) body)
| True ty -> Strue (scope_ty ty_env ty)
| False ty -> Sfalse (scope_ty ty_env ty)
| If (b, t, e) -> Sif (scope_term ty_env const_env var_env b,
scope_term ty_env const_env var_env t,
scope_term ty_env const_env var_env e)
| Obj l -> | Obj l ->
Sobj (List.map (fun (l, m) -> (l, scope_method ty_env const_env var_env m)) l) Sobj (List.map (fun (l, m) -> (l, scope_method ty_env const_env var_env m)) l)
| Select (t, l) -> | Select (t, l) ->
...@@ -134,6 +144,9 @@ let rec string_of_sty = function ...@@ -134,6 +144,9 @@ let rec string_of_sty = function
Printf.sprintf "(%s -> %s)" Printf.sprintf "(%s -> %s)"
(string_of_sty sty1) (string_of_sty sty1)
(string_of_sty sty2) (string_of_sty sty2)
| Stbool sty ->
Printf.sprintf "(Bool %s)"
(string_of_sty sty)
let rec string_of_sterm = function let rec string_of_sterm = function
| Svar (id, sty) -> Printf.sprintf "%s {: %s}" | Svar (id, sty) -> Printf.sprintf "%s {: %s}"
...@@ -144,7 +157,11 @@ let rec string_of_sterm = function ...@@ -144,7 +157,11 @@ let rec string_of_sterm = function
| Sapp (sterm1, sterm2) -> Printf.sprintf "%s @ %s" | Sapp (sterm1, sterm2) -> Printf.sprintf "%s @ %s"
(string_of_sterm sterm1) (string_of_sterm sterm2) (string_of_sterm sterm1) (string_of_sterm sterm2)
| Sabst (id, sty, sterm) -> Printf.sprintf "λ(%s : %s) %s" | Sabst (id, sty, sterm) -> Printf.sprintf "λ(%s : %s) %s"
(string_of_id id) (string_of_sty sty) (string_of_sterm sterm) (string_of_id id) (string_of_sty sty) (string_of_sterm sterm)
| Strue sty -> Printf.sprintf "(true %s)" (string_of_sty sty)
| Sfalse sty -> Printf.sprintf "(false %s)" (string_of_sty sty)
| Sif (b, t, e) -> Printf.sprintf "(if %s then %s else %s)"
(string_of_sterm b) (string_of_sterm t) (string_of_sterm e)
| Sobj ll -> | Sobj ll ->
Printf.sprintf "[ %s ]" Printf.sprintf "[ %s ]"
(String.concat " ; " (String.concat " ; "
......
...@@ -7,6 +7,7 @@ type sty = ...@@ -7,6 +7,7 @@ type sty =
| Stcid of cid * sty | Stcid of cid * sty
| Stlist of (label * sty) list | Stlist of (label * sty) list
| Starr of sty * sty | Starr of sty * sty
| Stbool of sty
type sterm = type sterm =
| Svar of id * sty | Svar of id * sty
...@@ -14,6 +15,9 @@ type sterm = ...@@ -14,6 +15,9 @@ type sterm =
| Spar of sterm | Spar of sterm
| Sapp of sterm * sterm | Sapp of sterm * sterm
| Sabst of id * sty * sterm | Sabst of id * sty * sterm
| Strue of sty
| Sfalse of sty
| Sif of sterm * sterm * sterm
| Sobj of (label * smeth) list | Sobj of (label * smeth) list
| Ssel of sterm * label | Ssel of sterm * label
| Supd of sterm * label * smeth | Supd of sterm * label * smeth
......
...@@ -7,6 +7,9 @@ type tterm = ...@@ -7,6 +7,9 @@ type tterm =
| Tpar of tterm | Tpar of tterm
| Tapp of tterm * tterm * sty * sty | Tapp of tterm * tterm * sty * sty
| Tabst of id * sty * tterm * sty | Tabst of id * sty * tterm * sty
| Ttrue of sty
| Tfalse of sty
| Tif of tterm * tterm * tterm * sty
| Tobj of (label * tmeth) list * sty | Tobj of (label * tmeth) list * sty
| Tsel of tterm * label * sty | Tsel of tterm * label * sty
| Tupd of tterm * label * tmeth * sty | Tupd of tterm * label * tmeth * sty
......
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