From b0f7c07bc4115c795f17ac319ee795a6d8118b22 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 1 Dec 2008 15:37:28 +0000 Subject: [PATCH] we start a kernel for the version "basic with reverse indexes and global references" --- helm/software/lambda-delta/.depend.opt | 2 ++ helm/software/lambda-delta/Makefile | 2 +- helm/software/lambda-delta/basic_rg/Make | 1 + helm/software/lambda-delta/basic_rg/brg.ml | 15 +++++++++++++++ 4 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 helm/software/lambda-delta/basic_rg/Make create mode 100644 helm/software/lambda-delta/basic_rg/brg.ml diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 60e0390bd..4ad04534d 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -8,6 +8,8 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: automath/autParser.cmi automath/autLexer.cmx: automath/autParser.cmx +basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx +basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 50f1a83b6..e7aa0ae76 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -1,6 +1,6 @@ MAIN = helena -DIRECTORIES = lib automath toplevel +DIRECTORIES = lib automath basic_rg toplevel REQUIRES = unix diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make new file mode 100644 index 000000000..be843055b --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/Make @@ -0,0 +1 @@ +brg diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml new file mode 100644 index 000000000..a3a32f8d0 --- /dev/null +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -0,0 +1,15 @@ +module U = NUri +module A = Aut + +type uri = U.uri +type id = A.id + +type binder = Abst | Abbr + +type term = Sort of int + | LRef of int + | GRef of uri + | Cast of term * term + | Appl of term * term + | Bind of id * binder * term * term + -- 2.39.2