F.cppo.ml 1.82 KB
Newer Older
1
open AlphaLib
2
open BindingForms
3 4 5 6

(* In this demo, only type variables are handled via AlphaLib. Term variables
   are represented as strings. *)

POTTIER Francois's avatar
POTTIER Francois committed
7 8 9 10 11
(* Type variables. *)

type tyvar =
  Atom.t

12 13
(* Types. *)

14 15 16
#define TYP ('fn, 'bn) typ

type TYP =
17
  | TyVar of 'fn
18 19 20 21
  | TyArrow of TYP * TYP
  | TyProduct of TYP * TYP
  | TyForall of ('bn, TYP) abs
  | TyMu of ('bn, TYP) abs
22 23 24

(* Term variables. *)

POTTIER Francois's avatar
POTTIER Francois committed
25
and tevar = (string[@opaque])
26 27 28

(* Terms. *)

29 30 31
#define TERM ('fn, 'bn) term

and TERM =
POTTIER Francois's avatar
POTTIER Francois committed
32
  | TeVar of tevar
33 34 35 36 37 38 39
  | TeAbs of tevar * TYP * TERM
  | TeApp of TERM * TERM
  | TeLet of tevar * TERM * TERM
  | TeTyAbs of ('bn, TERM) abs
  | TeTyApp of TERM * TYP
  | TePair of TERM * TERM
  | TeProj of int * TERM
40 41 42

(* Visitor generation. *)

43
[@@deriving
44 45 46 47 48
  visitors { variety = "iter";   ancestors = ["BindingForms.iter"] },
  visitors { variety = "map";    ancestors = ["BindingForms.map"]  },
  visitors { variety = "endo";   ancestors = ["BindingForms.endo"] },
  visitors { variety = "reduce"; ancestors = ["BindingForms.reduce"] },
  visitors { variety = "iter2";  ancestors = ["BindingForms.iter2"] } ]
49

POTTIER Francois's avatar
POTTIER Francois committed
50
(* Type abbreviations. *)
51 52 53 54 55 56 57 58 59 60 61

type raw_typ =
  (string, string) typ
type nominal_typ =
  (Atom.t, Atom.t) typ

type raw_term =
  (string, string) term
type nominal_term =
  (Atom.t, Atom.t) term

POTTIER Francois's avatar
POTTIER Francois committed
62 63
(* Operations based on visitors. *)

POTTIER Francois's avatar
POTTIER Francois committed
64 65 66
(* We create more operations than we actually need in this demo.
   This is just a way of testing that everything works. *)

POTTIER Francois's avatar
POTTIER Francois committed
67 68
#include "AlphaLibMacros.cppo.ml"

69 70 71 72 73 74 75 76 77 78 79 80
__FA
FA(typ)
FA(term)

__FILTER
FILTER(typ)
FILTER(term)

__BA
BA(typ)
BA(term)

81 82 83 84
__GUQ
GUQ(typ)
GUQ(term)

85 86 87 88
__COPY
COPY(typ)
COPY(term)

POTTIER Francois's avatar
POTTIER Francois committed
89 90 91 92
__AVOID
AVOID(typ)
AVOID(term)

93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
__SHOW
SHOW(typ)
SHOW(term)

__IMPORT
IMPORT(typ)
IMPORT(term)

__EXPORT
EXPORT(typ)
EXPORT(term)

__SIZE
SIZE(typ)
SIZE(term)

__EQUIV
EQUIV(typ)
EQUIV(term)

113 114 115
__SUBST(TyVar)
SUBST(TyVar, typ)
SUBST(TyVar, term)