Commit 8d9ca05b authored by POTTIER Francois's avatar POTTIER Francois

Introduced macros in Term.

parent d339979b
TARGET := \
Main.native
PWD := \
$(shell pwd)
ALPHALIB := \
`ocamlfind query alphaLib`
OCAMLBUILD := \
ocamlbuild \
-use-ocamlfind \
-classic-display \
-plugin-tag 'package(cppo_ocamlbuild)' \
-tag "cppo_I($(ALPHALIB))" \
-tag "cppo_I($(PWD))" \
MLI := \
$(patsubst %.ml,%.inferred.mli,$(wildcard *.ml))
......
open AlphaLib
open BindingForms
type ('bn, 'fn) tele =
#define tele ('bn, 'fn) tele
#define term ('bn, 'fn) term
type tele =
| TeleNil
| TeleCons of 'bn binder * ('bn, 'fn) term outer * ('bn, 'fn) tele rebind
| TeleCons of 'bn binder * term outer * tele rebind
and ('bn, 'fn) term =
and term =
| TVar of 'fn
| TPi of (('bn, 'fn) tele, ('bn, 'fn) term) bind
| TLam of (('bn, 'fn) tele, ('bn, 'fn) term) bind
| TApp of ('bn, 'fn) term * ('bn, 'fn) term list
| TPi of (tele, term) bind
| TLam of (tele, term) bind
| TApp of term * term list
[@@deriving visitors { variety = "iter"; ancestors = ["BindingForms.iter"]; public = ["visit_term"] },
visitors { variety = "map"; ancestors = ["BindingForms.map"]; public = ["visit_term"] },
visitors { variety = "endo"; ancestors = ["BindingForms.endo"]; public = ["visit_term"] },
......
let () =
Ocamlbuild_plugin.dispatch (fun phase ->
Ocamlbuild_cppo.dispatcher phase
)
......@@ -11,13 +11,14 @@ type tyvar =
(* Types. *)
#define TYP ('bn, 'fn) typ
#define typ ('bn, 'fn) typ
#define term ('bn, 'fn) term
type TYP =
type typ =
| TyVar of 'fn
| TyArrow of TYP * TYP
| TyProduct of TYP * TYP
| TyForall of ('bn, TYP) abs
| TyArrow of typ * typ
| TyProduct of typ * typ
| TyForall of ('bn, typ) abs
(* Term variables. *)
......@@ -25,17 +26,18 @@ and tevar = (string[@opaque])
(* Terms. *)
#define TERM ('bn, 'fn) term
and TERM =
and term =
| TeVar of tevar
| 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
| 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
#undef typ
#undef term
(* Visitor generation. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment