extensible Calculi

extensible_calculi.ml

type _ calculi_register = ..

type 'a c =
  | Core of 'a
  | Ext: 'b calculi_register *'b -> 'a c

type mixed_eval = { eval: 'a. 'a calculi_register -> 'a -> 'a c }

module type ext_calculus = sig
  type core
  type t = core c
  type _ calculi_register += R: core calculi_register
  val eval: (t->t) -> t -> t
end

module String = struct
  type core =
    | Str of string
    | Print of t
  and t = core c
  type _ calculi_register += R: core calculi_register


  let unwrap (type x) (w: x calculi_register) (y:x c): t = match y with
    | Core x -> Ext(w,x)
    | Ext (R,x) -> Core x
    | Ext (w,e) -> Ext (w,e)

  let rec core_eval global = function
    | Str _ as x -> x
    | Print t -> Print(eval global t)
  and eval global = function
    | Core x -> Core (core_eval global x)
    | Ext (R,x) -> Core (core_eval global x)
    | Ext (w,x) -> unwrap w (global.eval w x)

end


module Arith = struct
  type core =
    | Int of int
    | IfThenElse of t * t * t
  and t = core c
  type _ calculi_register += R: core calculi_register

  let unwrap (type x) (w: x calculi_register) (y:x c): t = match y with
    | Core x -> Ext(w,x)
    | Ext (R,x) -> Core x
    | Ext (w,e) -> Ext (w,e)

  let rec core_eval global = function
    | Int _ as x -> Core x
    | IfThenElse(t,then',else') ->
      begin match eval global t with
        | Core Int x ->
          if x = 0 then eval global then' else eval global else'
        | t -> Core (IfThenElse(t,then',else'))
      end
  and eval global = function
    | Core x -> core_eval global x
    | Ext (R,x) -> core_eval global x
    | Ext (w,x) -> unwrap w (global.eval w x)
end


let rec global_eval: type t. t calculi_register -> t -> t c = fun w x ->
  match w with
  | String.R -> Core (String.core_eval {eval=global_eval} x)
  | Arith.R -> Arith.core_eval {eval=global_eval} x
  | w -> Ext(w,x)

let global = { eval = global_eval }
open String
open Arith

let print x = String.Print x
let if_then_else x y z = IfThenElse(x,y,z)
let arith x = Ext(Arith.R,x)
let string x = Ext(String.R,x)
let int x = Core(Int x)
let str x = (Str x)

let t = print (arith @@ if_then_else (int 0) (string @@ str "Hello") (int 1));;
let t' = String.core_eval global t