gadt.ml

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"

gadtParser.mly

%{
  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 }