(* ------------------------------------------------------------------------ *) (* Types for patterns, values, environments, expressions. *) type tag = | Left | Right type pattern binds = | PWildcard | PVar of atom | PAnd of p1: pattern * p2: pattern where bound(p1) # bound(p2) | POr of p1: pattern * p2: pattern where bound(p1) == bound(p2) | PUnit | PPair of p1: pattern * p2: pattern where bound(p1) # bound(p2) | PSum of inner tag * pattern type value = | VUnit | VPair of value * value | VSum of tag * value | VClosure of < env: env * x: atom * inner body: expression > where bound(env) # free(x) and free(body) <= bound(env) U free(x) and outer(env) == empty (* TEMPORARY *) type env binds = | SNil | SCons of s: env * x: atom * outer v: value where bound(s) # free(x) and free(v) == empty type expression = | EVar of atom | ELam of < atom * inner expression > | EApp of expression * expression | EUnit | EPair of expression * expression | ESum of tag * expression | ECase of expression * branches type branches = | BNil | BCons of < pattern * inner expression > * branches (* TEMPORARY on devrait pouvoir prouver tous seuls que, pour tout env, outer(env) = empty *) (* TEMPORARY en fait ce outer v devrait être neutral v *) (* ------------------------------------------------------------------------ *) (* Concatenation of environments. *) fun concat accepts env1, env2 where bound(env1) # bound(env2) produces s where bound(s) == bound(env1) U bound(env2) and outer(s) == outer(env1) U outer(env2) (* TEMPORARY *) = case env2 of | SNil -> env1 | SCons (tail, x, v) -> SCons (concat (env1, tail), x, v) end (* ------------------------------------------------------------------------ *) (* Matching a value against a pattern. *) (* This piece of code is interesting because it can fail. At the moment, the language does not have exceptions. We cannot use an option type, because we would then not be able to express the function's postcondition -- that would require either parameterizing the type with a set or defining a separate set function. The current solution (a hack) is to use a Boolean success flag. *) fun filter accepts p, v where free(v) == empty produces successful, env where successful -> bound(env) == bound(p) outer(env) == empty (* TEMPORARY *) = case p, v of | PWildcard, _ -> true, SNil | PVar (x), _ -> true, SCons (SNil, x, v) | PAnd (p1, p2), _ -> let successful1, env1 = filter (p1, v) in let successful2, env2 = filter (p2, v) in successful1 and successful2, concat (env1, env2) | POr (p1, p2), _ -> let successful1, env1 = filter (p1, v) in if successful1 then successful1, env1 else filter (p2, v) end | PUnit, VUnit -> true, SNil | PPair (p1, p2), VPair (v1, v2) -> let successful1, env1 = filter (p1, v1) in let successful2, env2 = filter (p2, v2) in successful1 and successful2, concat (env1, env2) | PSum (Left, p), VSum (Left, v) -> filter (p, v) | PSum (Right, p), VSum (Right, v) -> filter (p, v) | _, _ -> false, SNil (* dummy *) end (* ------------------------------------------------------------------------ *) (* Environment lookup. *) fun find accepts env, x where free(x) <= bound(env) produces v where free(v) == empty = case env of | SNil -> absurd | SCons (tail, y, v) -> if x == y then v else find (tail, x) end end (* ------------------------------------------------------------------------ *) (* Evaluation. *) fun eval accepts env, e where free(e) <= bound(env) and outer(env) == empty (* TEMPORARY *) produces v where free(v) == empty = case e of | EVar (x) -> find (env, x) | ELam (x, body) -> VClosure (env, x, body) | EApp (e1, e2) -> let v1 = eval (env, e1) in let v2 = eval (env, e2) in case v1 of | VClosure (env, x, body) -> eval (SCons (env, x, v2), body) end | EUnit -> VUnit | EPair (e1, e2) -> VPair (eval (env, e1), eval (env, e2)) | ESum (tag, e) -> VSum (tag, eval (env, e)) | ECase (e, branches) -> let v = eval (env, e) in eval_branches (v, env, branches) end fun eval_branches accepts v, env, bs where free(v) == empty and free(bs) <= bound(env) and outer(env) == empty (* TEMPORARY *) produces w where free(w) == empty = case bs of | BCons (p, e, more) -> let successful, fragment = filter (p, v) in if successful then eval (concat (env, fragment), e) else eval_branches (v, env, more) end end (* ------------------------------------------------------------------------ *) (* Evaluation of a closed expression. *) fun eval_closed accepts e where free(e) == empty produces v = eval (SNil, e)