From 1469fd94659b3562ea7e3c180e0366194717a287 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 26 Jan 2008 17:26:14 -0500 Subject: Added simple expression constructors to Elab --- src/elab_env.sig | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'src/elab_env.sig') diff --git a/src/elab_env.sig b/src/elab_env.sig index c4e5ae5a..f24206ee 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -34,17 +34,27 @@ signature ELAB_ENV = sig exception UnboundRel of int exception UnboundNamed of int + datatype 'a var = + NotBound + | Rel of int * 'a + | Named of int * 'a + val pushCRel : env -> string -> Elab.kind -> env val lookupCRel : env -> int -> string * Elab.kind val pushCNamed : env -> string -> Elab.kind -> env * int val pushCNamedAs : env -> string -> int -> Elab.kind -> env val lookupCNamed : env -> int -> string * Elab.kind + + val lookupC : env -> string -> Elab.kind var + + val pushERel : env -> string -> Elab.con -> env + val lookupERel : env -> int -> string * Elab.con + + val pushENamed : env -> string -> Elab.con -> env * int + val pushENamedAs : env -> string -> int -> Elab.con -> env + val lookupENamed : env -> int -> string * Elab.con - datatype var = - CNotBound - | CRel of int * Elab.kind - | CNamed of int * Elab.kind - val lookupC : env -> string -> var + val lookupE : env -> string -> Elab.con var end -- cgit v1.2.3