Commit c16bc3be authored by POTTIER Francois's avatar POTTIER Francois

Early version of an advanced demo.

parent 0bc058cd
open AlphaLib
open Term
module T =
Toolbox.Make(Term)
TARGET := \
Main.native
OCAMLBUILD := \
ocamlbuild \
-use-ocamlfind \
-classic-display \
MLI := \
$(patsubst %.ml,%.inferred.mli,$(wildcard *.ml))
.PHONY: all test mli processed clean
all:
@ $(OCAMLBUILD) $(TARGET)
test: all
@ ./$(TARGET)
mli:
@ $(OCAMLBUILD) $(MLI)
include $(shell ocamlfind query visitors)/Makefile.preprocess
processed: Term.processed.ml
clean:
@ rm -f *~
@ rm -f *.processed.ml
@ $(OCAMLBUILD) -clean
open AlphaLib
open BindingForms
type ('bn, 'fn) tele =
| TeleNil
| TeleCons of 'bn binder * ('bn, 'fn) term outer * ('bn, 'fn) tele rebind
and ('bn, 'fn) 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
[@@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"] },
visitors { variety = "iter2"; ancestors = ["BindingForms.iter2"]; public = ["visit_term"] }]
true: \
debug, \
safe_string, \
warn(A-4-44), \
package(pprint), \
package(visitors.ppx), \
package(visitors.runtime), \
package(alphaLib)
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