interp_with_binary_sums.ml

type symbol = string

module Env = Map.Make (String)

type binary_op = Add | Sub | Mul | Div

module Type = struct
  type t =
    | Unit | Int
    | Fun of t * t
    | Sum of t * t
end

module Term = struct
  type t =
    | Unit
    | Int of int

    | Var of symbol
    | Lam of symbol * Type.t * t
    | App of t * t

    | Inl of t * Type.t
    | Inr of t * Type.t
    | Case of t * symbol * t * symbol * t
end

module Value = struct
  type t =
    | Unit
    | Int of int
    | Inl of t
    | Inr of t
    | Clo of (t -> t)
end

exception Mismatch of Type.t * Type.t

let type_error msg = raise (Invalid_argument msg)

let type_mismatch a b = raise (Mismatch (a, b))

let check_equal a b =
  let open Type in
  let rec equal a b =
    match a, b with
    | Unit, Unit
    | Int, Int -> true
    | Fun (x1, y1), Fun (x2, y2)
    | Sum (x1, y1), Sum (x2, y2) -> equal x1 x2 && equal y1 y2
    | _, _ -> type_mismatch a b in
  ignore (equal a b)

let rec type_of env term =
  let module T = Term in
  match term with
  | T.Unit -> Type.Unit
  | T.Int _ -> Type.Int
  | T.Var name -> Env.find name env
  | T.Lam (arg_name, arg_ty, body) ->
    let body_type = type_of (Env.add arg_name arg_ty env) body in
    Type.Fun (arg_ty, body_type)
  | T.App (f, arg) ->
    (match type_of env f with
     | Type.Fun (a, b) ->
       check_equal a (type_of env arg);
       b
     | _ -> type_error "application of non-function")
  | T.Inl (term, ty) -> Type.Sum (type_of env term, ty)
  | T.Inr (term, ty) -> Type.Sum (ty, type_of env term)
  | T.Case (term, varl, terml, varr, termr) ->
    (match type_of env term with
     | Type.Sum (sl, sr) ->
       let typel = type_of (Env.add varl sl env) terml in
       let typer = type_of (Env.add varr sr env) termr in
       check_equal typel typer;
       typel
     | _ -> failwith "case of non-sum")

exception Exn of Value.t

let rec eval env term =
  let module T = Term in
  let module V = Value in
  match term with
  | T.Unit -> V.Unit
  | T.Int k -> V.Int k
  | T.Var name -> Env.find name env
  | T.Lam (arg_name, _, body) ->
    V.Clo (fun value -> eval (Env.add arg_name value env) body)
  | T.App (f, arg) ->
    (match eval env f with
     | V.Clo c -> c (eval env arg)
     | _ -> failwith "application of non-function")
  | T.Inl (term, _) -> V.Inl (eval env term)
  | T.Inr (term, _) -> V.Inr (eval env term)
  | T.Case (term, varl, terml, varr, termr) ->
    (match eval env term with
     | V.Inl x -> eval (Env.add varl x env) terml
     | V.Inr x -> eval (Env.add varr x env) termr
     | _ -> failwith "case of non-variant")

let term =
  Term.(App (Lam ("x", Type.(Sum (Int, Unit)),
                  Case (Var "x",
                        "y", Var "y",
                        "_", Int 0)),
             Inl (Int 1, Type.Unit)))
             (* Inr (Unit, Type.Int))) *)