Skip to content

Instantly share code, notes, and snippets.

@vrotaru
Last active Aug 29, 2015
Embed
What would you like to do?
type _ ty =
| TBool : bool ty
| TInt : int ty
type _ value =
| Bool : bool -> bool value
| Int : int -> int value
type _ expr =
| Value : 'a value -> 'a expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
| Eq : 'a expr * 'a expr -> bool expr
| Lt : int expr * int expr -> bool expr
let rec eval : type a. a expr -> a = function
| Value (Bool b) -> b
| Value (Int n) -> n
| If (b, l, r) -> if eval b then eval l else eval r
| Eq (a, b) -> (eval a) = (eval b)
| Lt (a, b) -> (eval a) < (eval b)
type any =
| Any : _ expr -> any
let rec ty_from_expr : type a. a expr -> a ty = function
| Value(Bool _) -> TBool
| Value(Int _) -> TInt
| Eq(_, _) -> TBool
| Lt(_, _) -> TBool
| If(_, e, _) -> ty_from_expr e
let rec expr_from_any : type a. a ty -> any -> a expr =
fun ty any -> match ty, any with
| TBool, Any(Value(Bool _) as e) -> e
| TInt, Any(Value(Int _) as e) -> e
| TBool, Any(Eq(_, _) as e) -> e
| TBool, Any(Lt(_, _) as e) -> e
| t, Any(If(c, l, r)) ->
let l' = expr_from_any t (Any l) in
let r' = expr_from_any t (Any r) in
If(c, l', r')
| _ -> failwith "Type mismatch"
type tag = B | I
and t_expr = tag * any
let t_int n = (I, Any(Value(Int n)))
let t_bool b = (B, Any(Value(Bool b)))
let t_eq t t' = match t, t' with
| (B, a), (B, a') -> (B, Any(Eq(expr_from_any TBool a, expr_from_any TBool a')))
| (I, a), (I, a') -> (B, Any(Eq(expr_from_any TInt a, expr_from_any TInt a')))
| _ -> failwith "Type mismatch"
let t_lt t t' = match t, t' with
| (I, a), (I, a') -> (B, Any(Eq(expr_from_any TInt a, expr_from_any TInt a')))
| _ -> failwith "Type mismatch"
let t_if t t' t'' = match t, t', t'' with
| (B, a), (B, a'), (B, a'') -> (B, Any(If(expr_from_any TBool a, expr_from_any TBool a', expr_from_any TBool a'')))
| (B, a), (I, a'), (I, a'') -> (B, Any(If(expr_from_any TBool a, expr_from_any TInt a', expr_from_any TInt a'')))
| _ -> failwith "Type mismatch"
%{
open Gadt
%}
%token <int> NUM
%token <bool> BOOL
%token IF
%token THEN
%token ELSE
%token END
%token EQ
%token LT
%token LPAREN
%token RPAREN
%token EOF
%left EQ
%nonassoc LT
%start <Gadt.t_expr> parse
%%
parse:
e = exp EOF { e }
exp:
| n = NUM { t_int n }
| b = BOOL { t_bool b }
| IF c = exp THEN t = exp ELSE f = exp END
{ t_if c t f }
| l = exp EQ r = exp
{ t_eq l r }
| l = exp LT r = exp
{ t_lt l r }
| LPAREN e = exp RPAREN
{ e }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment