Raw text file

(* Section 4 *)

(* Type of variables and type variables. We make them concrete
   for some examples below *)
type tvar = string
type var = string

let print_var = print_string

let rec print_list sep f = function
  | [] -> ()
  | e :: q -> f e ; print_string sep; print_list sep f q

(*********************************************************************)

(* Ground values *)
type ground_ct = [ `Int of int | `Bool of bool ]
(* All the constants of the language *)
type ct = [ ground_ct | `IfTE | `OpPlus | `OpEq | `OpFix ]


(* Type constructors for ground values *)
type ground_typeconstr = [ `TInt | `TBool ]
(* And for the all the constants *)
type typeconstr = [
  | ground_typeconstr
  | `TVar of tvar
  | `TArrow of typeconstr * typeconstr
]

(* Constants and their type *)
let type_ifte : typeconstr =
  `TArrow (`TBool, `TArrow (`TVar "a",`TArrow (`TVar "a", `TVar "a")))
let ct_if = `IfTE, type_ifte
let type_plus : typeconstr = `TArrow (`TInt, `TArrow (`TInt, `TInt))
let ct_plus = `OpPlus, type_plus
let type_eq : typeconstr = `TArrow (`TVar "a", `TArrow (`TVar "a", `TBool))
let ct_eq = `OpEq, type_eq
let type_fix : typeconstr = `TArrow (`TArrow (`TVar "a", `TVar "a"), `TVar "a")
let ct_fix = `OpFix, type_fix


(* Auxiliary declarations for let constructions *)
type nonrec = [ `NonRec ]
type recnonrec = [ `Rec | nonrec ]
type ('rec_, 'expr) let_aux = [ `Let of 'rec_ * (var * 'expr) * 'expr ]


(* Constructions shared between the two ASTs *)
type 'expr common = [ `Var of var | `Uple of 'expr list ]

(* Constructions in only one of the ASTs, or exactly shared between the two *)
type 'expr source_aux = [
  | 'expr common
  | `SeqApp of 'expr * 'expr list
  | `SeqAbs of var list * 'expr
  | `Plus of 'expr * 'expr | `Eq of 'expr * 'expr
  | `If of 'expr * 'expr * 'expr ]
type 'expr dest_aux = [
  | 'expr common
  | `App of 'expr * 'expr
  | `Abs of var * 'expr ]

(* The two ASTs, obtained by closing the recursion *)
type source = [
  | source source_aux
  | (recnonrec, source) let_aux
  | `Ct of ground_ct * ground_typeconstr ]
type dest = [
  | dest dest_aux
  | (nonrec, dest) let_aux
  | `Ct of ct * typeconstr ]

(* Desugaring function *)
let rec desugar : source -> dest = function
  | `Var _ as v -> v
  | `Uple l -> `Uple (List.map desugar l)
  | `SeqApp (e, l) -> desugar_seq_app (desugar e) l
  | `SeqAbs ([], e) -> desugar e
  | `SeqAbs (v  :: q, e) -> `Abs (v, desugar (`SeqAbs (q, e)))
  | `Ct (c, t) -> `Ct ((c :> ct), (t :> typeconstr))
  | `If (c, e1, e2) -> desugar_seq_app (`Ct ct_if) [c;e1;e2]
  | `Plus (e1, e2) -> desugar_seq_app (`Ct ct_plus) [e1;e2]
  | `Eq (e1, e2) -> desugar_seq_app (`Ct ct_eq) [e1;e2]
  | `Let (`NonRec, (v, e1), e2) -> `Let (`NonRec, (v, desugar e1), desugar e2)
  | `Let (`Rec, (v, e1), e2) ->
      let e1' = `App (`Ct ct_fix, `Abs (v, desugar e1)) in
      `Let (`NonRec, (v, e1'), desugar e2)
and desugar_seq_app e = function
  | [] -> e
  | e' :: q -> desugar_seq_app (`App (e, desugar e')) q



(* Extensible pretty-printers needed for the destination langage *)
let print_common print : _ common -> unit = function
  | `Var v -> print_var v
  | `Uple l -> print_string "(" ; print_list ", " print l ; print_string ")"

let print_dest_aux print : _ dest_aux -> unit = function
  | #common as e -> print_common print e
  | `App (e, e') ->
      print_string "("; print e  ; print_string ")"; print_string " ";
      print_string "("; print e' ; print_string ")";
  | `Abs (v, e) ->
      print_string "fun "; print_var v; print_string " -> ";
      print_string "("; print e ; print_string ")"

let print_let print : ([< recnonrec], _) let_aux -> unit = function
  | `Let (annot, (v, e), e') ->
      print_string "let "; if annot <> `NonRec then print_string "rec ";
      print_var v; print_string " = ";
      print_string "("; print e  ; print_string ")"; print_string " in ";
      print_string "("; print e' ; print_string ")"

let print_ct = function
  | `Int i -> print_int i
  | `Bool true -> print_string "true"
  | `Bool false -> print_string "false"
  | `IfTE -> print_string "#If"
  | `OpFix -> print_string "#Fix"
  | `OpEq -> print_string "#="
  | `OpPlus -> print_string "#+"

let rec print_dest : dest -> unit = function
  | #dest_aux as e -> print_dest_aux print_dest e
  | #let_aux as l -> print_let print_dest l
  | `Ct (c, _) -> print_ct c



(* Least supertype of the two ASTs *)
type all_expr = [
  | all_expr source_aux
  | all_expr dest_aux
  | (recnonrec, all_expr) let_aux
  | `Ct of ct * typeconstr ]

(* Coercion from the two ASTs to the supertype *)
let coerce_source e = (e : source :> all_expr)
let coerce_dest   e = (e : dest :> all_expr)


(* Skeleton for a pretty-printer for the supertype *)
let rec print_all : all_expr -> unit = function
  | `App (e, e') -> print_all e ; print_all e'
(* [...] All other cases *)
  | _ -> failwith "Not implemented"

(* Pretty-printers for the ASTs, by coercing the values to the supertype *)
let print_source e = print_all (coerce_source e)
let print_dest e = print_all (coerce_dest e)

This document was generated using caml2html