exception NotFound of string;; type 'a map = string -> 'a let lookup (m: 'a map) (key: string) : 'a = m key let insert (m: 'a map) (key: string) (v: 'a) : 'a map = fun k -> if k=key then v else m k let empty : 'a map = fun k -> raise (NotFound k) let m1 : int map = insert (insert empty "cat" 1) "dog" 2 let one = lookup m1 "cat" let two = lookup m1 "dog" let boom = lookup m1 "mouse" (** Theorem: lookup (insert m k v) k = v. Theorem: k<>k' -> lookup (insert m k v) k' = lookup m k'. Theorem: lookup empty k "=" NotFound See sf/LF/Maps.v or sf/plf/Maps.v or sf/VFA/Maps.v *) type 'a tree = Node of string * 'a * 'a tree * 'a tree | Leaf;; let rec insert (t: 'a tree) (key: string) (value: 'a) = match t with Node (k,v,l,r) -> if key k then Node (k,v,l, insert r key value) else Node (key,value,l,r) | Leaf -> Node(key,value,Leaf,Leaf);; let rec look (t: 'a tree) (key: string) : 'a = match t with Node(k,v,l,r) -> if key k then look r key else v | Leaf -> raise (NotFound key);; type env = int tree;; let empty_env = Leaf;; type var = string;; type exp = NUM of int | VAR of var | PLUS of exp * exp | LET of var * exp * exp;; (* Environment-based interpreter *) let rec interp (e: exp) (rho: env) : int = match e with NUM i -> i | VAR v -> look rho v | PLUS(e1,e2) -> interp e1 rho + interp e2 rho | LET(v,e1,e2) -> interp e2 (insert rho v (interp e1 rho));; let exp1 = LET("y",PLUS(NUM 3, NUM 4), PLUS(VAR "y", VAR "y"));; let exp2 = LET("y",PLUS(NUM 3, NUM 4), VAR "z");; let val1 = interp exp1 empty_env;; (* Denotational semantics *) let rec denot (e: exp) : env -> int = match e with NUM i -> fun rho -> i | VAR v -> fun rho -> look rho v | PLUS(e1,e2) -> fun rho -> denot e1 rho + denot e2 rho | LET(v,e1,e2) -> fun rho -> denot e2 (insert rho v (denot e1 rho));; let rec denot (e: exp) : env -> int = match e with NUM i -> fun rho -> i | VAR v -> fun rho -> look rho v | PLUS(e1,e2) -> let d1 = denot e1 and d2 = denot e2 in fun rho -> d1 rho + d2 rho | LET(v,e1,e2) -> let d1 = denot e1 and d2 = denot e2 in fun rho -> d2 (insert rho v (d1 rho));; (* Substitution *) let subst (e: exp) (v: var) : exp -> exp = let rec f (e2: exp) : exp = match e2 with | VAR w -> if v=w then e else e2 | NUM i -> e2 | PLUS(e1,e2) -> PLUS(f e1, f e2) | LET(w,e1,e2) -> LET(w, f e1, if v=w then e2 else f e2) in f;; (* Reduction *) let rec reduce (strategy: bool) (e: exp) : exp = match e with | PLUS(e1, e2) -> (match (reduce strategy e1, reduce strategy e2) with (NUM i, NUM j) -> NUM(i+j) | (e1',e2') -> PLUS(e1',e2') ) | NUM i -> e | VAR _ -> e | LET(w,e1,e2) -> if strategy then reduce strategy (subst e1 w e2) else reduce strategy (subst (reduce strategy e1) w e2);; (* Higher-Order Abstract Syntax (HOAS) *) type exp' = NUM of int | PLUS of exp' * exp' | LET of exp' * (exp' -> exp');; let rec interp' (e: exp') : int = match e with NUM i -> i | PLUS(e1,e2) -> interp' e1 + interp' e2 | LET(e1,e2) -> interp' (e2 e1);; let exp1' = LET(PLUS(NUM 3, NUM 4), fun y -> PLUS(y, y));; let rec plusses (e: exp') : int = match e with NUM i -> 0 | PLUS(e1,e2) -> 1 + plusses e1 + plusses e2 | LET(e1,e2) -> plusses e1 + plusses (e2 (NUM 0));; let rec optzero (e: exp') : exp' = match e with PLUS (e1, NUM 0) -> optzero e1 | NUM i -> e | PLUS(e1,e2) -> PLUS(optzero e1, optzero e2) | LET(e1,e2) -> LET(optzero e1, fun x -> optzero(e2 x));; (* A language with side effects and control flow *) type cmd = SET of var * exp | SEQ of cmd * cmd | IF of exp * cmd * cmd | WHILE of exp * cmd;; let rec cinterp c rho = match c with SET(v,e) -> insert rho v (interp e rho) | SEQ(c1,c2) -> cinterp c2 (cinterp c1 rho) | IF(e,c1,c2) -> if interp e rho <> 0 then cinterp c1 rho else cinterp c2 rho | WHILE(e,c) -> if interp e rho <> 0 then let rho1 = cinterp c rho in cinterp (WHILE(e,c)) rho1 else rho let cmd1 = SEQ(SET("s", NUM 0), SEQ(SET("i", NUM 6), WHILE(VAR "i", SEQ(SET("s", PLUS(VAR"s",VAR"i")), SET("i", PLUS(VAR"i",NUM (-1)))))));;