(* Contexts *)
(* Author: Frank Pfenning *)
(*
Variables (represented by name) are mapped to
arbitrary values (normally propositions)
*)
signature CTX =
sig
(* Contexts -- defined via polymorphic data-type
NOTE : 'a is a type variable and we can think of 'a as a parameter
a more common example is the polymorphic definition of lists.
datatype 'a list = nil | :: of 'a * 'a list
this defines a list with elements of type 'a
instances of this datatype are for example,
int list -- a list with integers as elements
char list -- a list with char as elements
(int * char) list -- a list with tuples of integers and chars
etc.
*)
(* Contexts *)
(* Later declarations shadow earlier ones *)
(* example: the context x:A, y:B is represented as
Decl( Decl (Null, ("x", Prop.Atom "A")), ("y", Prop.Atom "B"))
*)
datatype 'a Ctx = (* G ::= *)
Null (* . *)
| Decl of 'a Ctx * (string * 'a) (* | G, x:A *)
(* lookup (G, x) = Option
if there exists a declaration x:A in G,
then we return SOME(A)
else NONE
NOTE: the option type is a built in data-type
which can be used for handling partial functions and optional values
you can think of it as the following data-type definition:
datatype 'a option =
NONE
| SOME of 'a
*)
val lookup : 'a Ctx * string -> 'a option
end; (* signature CTX *)
structure Ctx :> CTX =
struct
(* Contexts *)
(* Later declarations shadow earlier ones *)
datatype 'a Ctx = (* G ::= *)
Null (* . *)
| Decl of 'a Ctx * (string * 'a) (* | G, x:A *)
(* lookup (G, x) = NONE if x not declared in G
= SOME(A) if x:A is last declaration of x in G
*)
fun lookup (Null, x) = NONE
| lookup (Decl (G, (y, A)), x) =
if (x = y) then SOME(A)
else lookup (G, x)
end; (* structure Ctx *)
(* Global abbreviation *)
structure C = Ctx;