structure MinML = struct
datatype oper
= OpPlus
| OpTimes
| OpMinus
type var = string
datatype exp
= ExInt of int
| ExOp of exp * oper * exp
| ExBool of bool
| ExIf of exp * exp * exp
| ExAbs of var * exp
| ExApp of exp * exp
| ExPair of exp * exp
| ExFst of exp
| ExSnd of exp
| ExLet of var * exp * exp
| ExVar of var
(* Designates which terms should be type-generalized *)
(* Note: could be generalized to "valuable" *)
fun value (ExInt _ | ExBool _ | ExAbs _ | ExVar _) = true
| value (ExOp _ | ExIf _ | ExApp _ | ExLet _) = false
| value (ExPair (e1, e2)) = value e1 andalso value e2
| value (ExFst _ | ExSnd _) = false
val value : exp -> bool = value
end
infixr 5 >>
infix 5 <<
structure Cons = struct
datatype 'a list = Nil | >> of 'a * 'a list
fun exists f Nil = false
| exists f (x >> xs) = if f x then true else exists f xs
fun map f Nil = Nil
| map f (x >> xs) = f x >> map f xs
end
structure Snoc = struct
datatype 'a list = Lin | << of 'a list * 'a
fun all f Lin = true
| all f (xs << x) = if f x then all f xs else false
end
open Cons
open Snoc
structure Examples = struct
local open MinML in
val polyid =
ExLet ("id", ExAbs ("x", ExVar "x"),
ExPair (ExApp (ExVar "id", ExInt 0),
ExApp (ExVar "id", ExBool true)))
(* should fail: id fails to be generalized *)
val notpolyid =
ExLet ("id", ExApp (ExAbs ("x", ExVar "x"), ExAbs ("x", ExVar "x")),
ExPair (ExApp (ExVar "id", ExInt 0),
ExApp (ExVar "id", ExBool true)))
val wrapnotpolyid =
ExLet ("id",
ExAbs ("y",
(* this one's not generalized, but the outer one is *)
ExApp (ExLet ("f", ExApp (ExAbs ("x", ExVar "x"),
ExAbs ("x", ExVar "x")),
ExVar "f"),
ExVar "y")),
ExPair (ExApp (ExVar "id", ExInt 0),
ExApp (ExVar "id", ExBool true)))
end
end