Commit f53a41e7 authored by POTTIER Francois's avatar POTTIER Francois

The beginning of the System F demo.

parent 9f5c561d
B _build
PKG pprint
PKG visitors.ppx
PKG visitors.runtime
PKG alphaLib
open AlphaLib
open Abstraction
#include "AlphaLibMacros.cppo.ml"
(* In this demo, only type variables are handled via AlphaLib. Term variables
are represented as strings. *)
(* Types. *)
type ('fn, 'bn) typ =
| TyVar of 'fn
| TyArrow of ('fn, 'bn) typ * ('fn, 'bn) typ
| TyProduct of ('fn, 'bn) typ * ('fn, 'bn) typ
| TyForall of ('bn, ('fn, 'bn) typ) abstraction
| TyMu of ('bn, ('fn, 'bn) typ) abstraction
(* Term variables. *)
and var = (string[@opaque])
(* Terms. *)
and ('fn, 'bn) term =
| TeVar of var
| TeAbs of var * ('fn, 'bn) typ * ('fn, 'bn) term
| TeApp of ('fn, 'bn) term * ('fn, 'bn) term
| TeLet of var * ('fn, 'bn) term * ('fn, 'bn) term
| TeTyAbs of ('bn, ('fn, 'bn) term) abstraction
| TeTyApp of ('fn, 'bn) term * ('fn, 'bn) typ
| TePair of ('fn, 'bn) term * ('fn, 'bn) term
| Teroj of int * ('fn, 'bn) term
(* Visitor generation. *)
[@@deriving
visitors { variety = "iter"; public = ["visit_term"; "visit_typ"];
ancestors = ["Bn.iter"; "Abstraction.iter"] }
,
visitors { variety = "map"; public = ["visit_term"; "visit_typ"];
ancestors = ["Bn.map"; "Abstraction.map"] }
,
visitors { variety = "endo"; public = ["visit_term"; "visit_typ"];
ancestors = ["Bn.endo"; "Abstraction.endo"] }
,
visitors { variety = "reduce"; public = ["visit_term"; "visit_typ"];
ancestors = ["Bn.reduce"; "Abstraction.reduce"] }
,
visitors { variety = "iter2"; public = ["visit_term"; "visit_typ"];
ancestors = ["Bn.iter2"; "Abstraction.iter2"] }
]
(* Operations based on visitors. *)
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
__FA
FA(typ)
FA(term)
__FILTER
FILTER(typ)
FILTER(term)
__BA
BA(typ)
BA(term)
__COPY
COPY(typ)
COPY(term)
__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)
__SUBST(typ, TyVar)
SUBST(typ, typ)
SUBST(typ, term)
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))" \
# TEMPORARY cppo_I($(PWD)) should not be required
# TEMPORARY a dependency computation on .cppo.ml files should be carried out
MLI := \
$(patsubst %.ml,%.inferred.mli,$(shell ls *.ml | grep -v cppo | grep -v myocamlbuild)) \
$(patsubst %.cppo.ml,%.inferred.mli,$(shell ls *.cppo.ml)) \
.PHONY: all test mli processed clean
all:
@ $(OCAMLBUILD) $(TARGET)
test: all
@ ./$(TARGET)
mli:
@ $(OCAMLBUILD) $(MLI)
processed: all
make -C _build -f ../Makefile.preprocess F.processed.ml
clean:
@ rm -f *~
@ rm -f *.processed.ml
@ $(OCAMLBUILD) -clean
# This Makefile allows running visitors as a preprocessor,
# so as to inspect the generated code and possibly include
# it in a TeX document.
# This assumes the visitors package is installed.
# The rewriting command.
PPX := `ocamlfind query ppx_deriving`/ppx_deriving \
`ocamlfind query visitors`/ppx_deriving_visitors.cma
REWRITE := ocamlfind ppx_tools/rewriter -ppx '$(PPX)'
# Use GNU sed to extract the generated code.
# This requires GNU sed 3.95 or above, I am told.
SED := $(shell if command -v gsed >/dev/null ; then echo gsed ; else echo sed ; fi)
EXTRACT := $(SED) -e '/VISITORS.BEGIN/,/VISITORS.END/!d;//d'
# Use sed to fix some deficiencies of OCaml's code printer.
# 0. Force a space after a comma.
# 1. Replace multiple consecutive spaces with a single space.
# This will destroy indentation; we restore it afterwards.
# 2. Force a line break after [in].
# 3. Force a line break after [->].
# 4. (Ad hoc.) Force a line break between [= let],
# presumably at the beginning of a method definition.
# 5. Remove the line break between [=] and [object].
BEAUTIFY := \
| $(SED) -e 's/,/, /g' \
| $(SED) -e 's/ / /g' \
| $(SED) -e 's/ in / in\n/g' \
| $(SED) -e 's/ -> / ->\n/g' \
| $(SED) -e 's/= let /=\nlet /g' \
| perl -0777 -pe 's/=\n *object/= object/gs' \
# Use ocp-indent to beautify the generated code.
INDENT := ocp-indent --config=JaneStreet,match_clause=4
%.processed.ml: %.ml
$(REWRITE) $< $(BEAUTIFY) | $(INDENT) > $@
true: \
debug, \
safe_string, \
warn(A-4-44), \
package(pprint), \
package(visitors.ppx), \
package(visitors.runtime), \
package(alphaLib)
let () =
Ocamlbuild_plugin.dispatch (fun phase ->
Ocamlbuild_cppo.dispatcher phase
)
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