F.cppo.ml 1.83 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. *)

7 8 9 10 11
(* Type variables. *)

type tyvar =
  Atom.t

12 13
(* Types. *)

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

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

(* Term variables. *)

24
and tevar = (string[@opaque])
25 26 27

(* Terms. *)

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

and TERM =
31
  | TeVar of tevar
32 33 34 35 36 37 38
  | 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
39 40 41

(* Visitor generation. *)

42
[@@deriving
43 44 45 46 47
  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"] } ]
48

49
(* Type abbreviations. *)
50 51 52 53 54 55 56 57 58 59 60

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

61 62
(* Operations based on visitors. *)

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

66 67
#include "AlphaLibMacros.cppo.ml"

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

__FILTER
FILTER(typ)
FILTER(term)

__BA
BA(typ)
BA(term)

80 81 82 83
__AVOIDS
AVOIDS(typ)
AVOIDS(term)

84 85 86 87
__GUQ
GUQ(typ)
GUQ(term)

88 89 90 91
__COPY
COPY(typ)
COPY(term)

POTTIER Francois's avatar
POTTIER Francois committed
92 93 94 95
__AVOID
AVOID(typ)
AVOID(term)

96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
__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)

116 117 118
__SUBST(TyVar)
SUBST(TyVar, typ)
SUBST(TyVar, term)