dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ poly
Poly/ML RTS version PPC-4.2.0 (04:54:44 Nov 16 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
Mapping /Applications/polyml/ML_dbase
Poly/ML 4.2.0 Release
> datatype Prop = Atom of string
| /\  of Prop * Prop
| \/  of Prop * Prop
| ==>  of Prop * Prop
| ~   of Prop;

infix 3 \/;
infix 4 /\;
infix 5 ==>;
infix 6 <=>;

val A = Atom "a";
val B = Atom "b";
val C = Atom "c";
val D = Atom "d";

fun rmImp (x ==> y) = ~(rmImp x) \/ (rmImp y)
| rmImp (~x) = ~(rmImp x)
| rmImp (x /\ y) = (rmImp x) /\ (rmImp y)
| rmImp (x \/ y) = (rmImp x) \/ (rmImp y)
| rmImp x = x;

fun pushNeg (~(~x)) = pushNeg x
| pushNeg (~(x /\ y)) = pushNeg (~x) \/ pushNeg (~y)
| pushNeg (~(x \/ y)) = pushNeg (~x) /\ pushNeg (~y)
| pushNeg (x /\ y) = (pushNeg x) /\ (pushNeg y)
| pushNeg (x \/ y) = (pushNeg x) \/ (pushNeg y)
| pushNeg x = x;

fun distr (x \/ (y /\ z)) = (distr(x \/ y) /\ distr(x \/ z))
| distr x = x;
fun distl ((y /\ z) \/ x) = (distl(y \/ x) /\ distl(z \/ x))
| distl x = x;

fun dist x = distr(distl x);

fun cnf (x /\ y) = (cnf x) /\ (cnf y)
|   cnf (x \/ y) = dist ((cnf x) \/ (cnf y))
|   cnf x = x;

fun cnf_test x = cnf (pushNeg (rmImp x));

# # # # datatype
  Prop =
      /\ of Prop * Prop
    | ==> of Prop * Prop
    | Atom of string
    | \/ of Prop * Prop
    | ~ of Prop
> > infix 3 \/
> infix 4 /\
> infix 5 ==>
> infix 6 <=>
> > val A = Atom "a" : Prop
> val B = Atom "b" : Prop
> val C = Atom "c" : Prop
> val D = Atom "d" : Prop
> > # # # # val rmImp = fn : Prop -> Prop
> > # # # # # val pushNeg = fn : Prop -> Prop
> > # val distr = fn : Prop -> Prop
> # val distl = fn : Prop -> Prop
> > val dist = fn : Prop -> Prop
> > # # val cnf = fn : Prop -> Prop
> > val cnf_test = fn : Prop -> Prop
> >   C-c C-c
=>q
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ 
dhcp-219-185:~/Documents/Informatics/web/teaching/courses/propm/ML mfourman$ poly
Poly/ML RTS version PPC-4.2.0 (04:54:44 Nov 16 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
Mapping /Applications/polyml/ML_dbase
Poly/ML 4.2.0 Release
> 1;
val it = 1 : int
> "fred";
val it = "fred" : string
> 2 * 30;
val it = 60 : int
> val a = 42;
val a = 42 : int
> a + a;
val it = 84 : int
> fun twice x = x + x;
val twice = fn : int -> int
> twice 30;
val it = 60 : int
> fun atimes x = a * x;
val atimes = fn : int -> int
> atimes 2;
val it = 84 : int
> val a = 30;
val a = 30 : int
> atimes x;
Error: Value or constructor (x) has not been declared   Found near atimes(x)

Static errors (pass2)
> > xtimes 2;
Error:
Value or constructor (xtimes) has not been declared   Found near xtimes(2)

Static errors (pass2)
> > atimes 2;
val it = 84 : int
> fun times x y = x * y;
val times = fn : int -> int -> int
> times 2 3;
val it = 6 : int
> times 30;
val it = fn : int -> int
> it 4;
val it = 120 : int
> 
> 
> 
> 
> datatype Answer = Yes | No | Maybe;
datatype Answer = Maybe | No | Yes
> Yes;
val it = Yes : Answer
> fun decide Maybe = No | Decide x = x;
Error:
In clausal function one clause defines Decide and another defines decide
Found near Decide(x)

Static errors (pass2)
> > fun decide Maybe = No | decide x = x;
val decide = fn : Answer -> Answer
> Decide Yes;
Error:
Value or constructor (Decide) has not been declared   Found near Decide(Yes)

Static errors (pass2)
> > decide Yes;
val it = Yes : Answer
> decide Maybe;
val it = No : Answer
> fun bigger x y = if x > y then Yes else if x < y then No else Maybe;
val bigger = fn : int -> int -> Answer
> bigger 2 1;
val it = Yes : Answer
> bigger 1 1;
val it = Maybe : Answer
> datatype Weight = KG of int | LB of int;
datatype Weight = KG of int | LB of int
> KG 50;
val it = KG 50 : Weight
> datatype Weight = KG of real | LB of real;
datatype Weight = KG of real | LB of real
> KG 50.0;
val it = KG 50.0 : Weight
> fun tolb (KG x) = LB (x * 2.2)| tolb x = x;
val tolb = fn : Weight -> Weight
> tolb it;
val it = LB 110.0 : Weight
> datatype Prop = Atom of string
| /\  of Prop * Prop
| \/  of Prop * Prop
| ==>  of Prop * Prop
| ~   of Prop;

# # # # datatype
  Prop =
      /\ of Prop * Prop
    | ==> of Prop * Prop
    | Atom of string
    | \/ of Prop * Prop
    | ~ of Prop
> > 
infix 3 \/;
infix 4 /\;
infix 5 ==>;
infix 6 <=>;

val A = Atom "a";
val B = Atom "b";
val C = Atom "c";
val D = Atom "d";

> infix 3 \/
> infix 4 /\
> infix 5 ==>
> infix 6 <=>
> > val A = Atom "a" : Prop
> val B = Atom "b" : Prop
> val C = Atom "c" : Prop
> val D = Atom "d" : Prop
> > A /\ B;
val it = Atom "a" /\ Atom "b" : Prop
> fun pp (Atom x) = x;
Warning: Matches are not exhaustive.   Found near fun pp(Atom(x)) = x

val pp = fn : Prop -> string
> pp A;
val it = "a" : string
> fun pp (Atom x) = x
| pp ( x /\ y) = pp x ^ "/\" pp y;


# # Error: no matching quote found on this line

# # 
# 
# 
# ;
Static errors (pass 1)
> > 
fun pp (Atom x) = x
| pp ( x /\ y) = pp x ^ "/\\" pp y;

> # Error:
Can't unify string with (Prop -> string) -> 'a (Incompatible types)
   Found near ^( pp(x), ("/\\")(pp)(y))

Static errors (pass2)
> > 
fun pp (Atom x) = x
| pp ( x /\ y) = pp x ^ "/\\" ^ pp y;


> # Warning:
Matches are not exhaustive.
Found near fun pp(Atom(x)) = x | pp(......) = ^( ...)

val pp = fn : Prop -> string
> > > pp(A /\ B);
val it = "a/\\b" : string
> 
fun rmImp (x ==> y) = ~(rmImp x) \/ (rmImp y)
| rmImp (~x) = ~(rmImp x)
| rmImp (x /\ y) = (rmImp x) /\ (rmImp y)
| rmImp (x \/ y) = (rmImp x) \/ (rmImp y)
| rmImp x = x;

> # # # # val rmImp = fn : Prop -> Prop
> > rmImp (A /\ B);
val it = Atom "a" /\ Atom "b" : Prop
> rmImp (A ==> (B ==> C));
val it = ~ (Atom "a") \/ (~ (Atom "b") \/ Atom "c") : Prop
> rmImp ((A ==> B) ==> C);
val it = ~ (~ (Atom "a") \/ Atom "b") \/ Atom "c" : Prop
> 
fun pushNeg (~(~x)) = pushNeg x
| pushNeg (~(x /\ y)) = pushNeg (~x) \/ pushNeg (~y)
| pushNeg (~(x \/ y)) = pushNeg (~x) /\ pushNeg (~y)
| pushNeg (x /\ y) = (pushNeg x) /\ (pushNeg y)
| pushNeg (x \/ y) = (pushNeg x) \/ (pushNeg y)
| pushNeg x = x;

> # # # # # val pushNeg = fn : Prop -> Prop
> > pushNeg it;
val it = Atom "a" /\ ~ (Atom "b") \/ Atom "c" : Prop
>