type world = int
type param = string
type var = string * int
datatype t = Eq of world * world
| And of t * t
| Imp of t * t
| All of param * t
| Ex of var * t
| Hole
There are formulas with holes, and I wanted to fill in a hole with another formula.
Since the fill function does the same thing for the binops and the quantifiers, I
lifted the logic out of the main function (binop and quant)
val fill : t * t -> t option =
fn (inp, x) =>
let
val rec find : t -> t option =
fn Hole => SOME x
| And t12 => binop And t12
| Imp t12 => binop Imp t12
| All xt => quant All xt
| Ex xt => quant Ex xt
| Eq _ => NONE
and binop: (t * t -> t) -> t * t -> t option =
fn con => fn (t1, t2) =>
case find t1 of
SOME t => SOME(con(t, t2))
| NONE => Option.map (fn t => con(t1, t)) (find t2)
and quant: ('a * t -> t) -> 'a * t -> t option =
fn con => fn (x, t) => Option.map (fn t => con(x, t)) (find t)
in
find inp
end
This didn't typecheck because quant was being called with 'a = var and also 'a = param.
Tom Murphy supplied the pretty workaround: quant gets an extra argument which is
an abstraction of 'find'. This breaks the mutual dependency, and shows that the function
is not really polymorphic-recursive.
val fill : t * t -> t option =
fn (inp, x) =>
let
val quant : (t -> t option) -> ('a * t -> t) -> 'a * t -> t option =
fn find => fn con => fn (x, t) => Option.map (fn t => con(x, t)) (find t)
val rec find : t -> t option =
fn Hole => SOME x
| And t12 => binop And t12
| Imp t12 => binop Imp t12
| All xt => quant find All xt
| Ex xt => quant find Ex xt
| Eq _ => NONE
and binop : (t * t -> t) -> t * t -> t option =
fn con => fn (t1, t2) =>
case find t1 of
SOME t => SOME(con(t, t2))
| NONE => Option.map (fn t => con(t1, t)) (find t2)
in
find inp
end
No comments:
Post a Comment