#!/usr/bin/perl

my $TYPE_T="mu(x.Variant(None:Unit, " 
                      . "Boolean:Unit, "
                      . "Nat:Unit, "
                      . "Arrow:Record(in:x, out:x)"
                      . "))";

my $TERM_T="mu(y.Variant(Tru:Unit, "
                      . "Fls:Unit, "
                      . "Zero:Unit, "
                      . "Var:Char, "
                      . "Abs:Record(var:Char, tp:$TYPE_T, t:y), "
                      . "App:Record(fun:y, arg:y), "
                      . "If:Record(cond:y, thn:y, els:y), "
                      . "Succ:y, "
                      . "Pred:y, "
                      . "IsZero:y, "
                      . "Fix: y, "
                      . "None:Unit "
                      . "))";

my $ENV_T = "->(Char,$TYPE_T)";

$temparea = "
=(app(f,project(v.cond)),
  tag(Boolean=Unit as $TYPE_T))
";

$iftest="  tag(If=record(cond=tag(Tru=# as $TERM_T),
                thn=tag(Zero=# as $TERM_T),
                els=tag(Zero=# as $TERM_T)) as $TERM_T)
            fi";
$succtest="        tag (Succ=tag (Zero=# as $TERM_T) as $TERM_T)";
$valtest="        tag (Zero=# as $TERM_T)";

$prog = "
app(app(fix(abs(f:->($ENV_T,->($TERM_T,$TYPE_T)).abs(env:$ENV_T.abs(tm:$TERM_T.case tm of
    Tru=v => tag(Boolean=# as $TYPE_T)
  | Fls=v => tag(Boolean=# as $TYPE_T)
  | Zero=v => tag(Nat=# as $TYPE_T)
  | Var=v => app(env, v)
  | Abs=v => ( case app(app(f,
                            app(app(app(extendEnv, env),project(v.var)),project(v.tp))
                        ), project(v.t)) of
                  Boolean=vv => tag (Arrow=record(fun=project(v.tp),
                                                  arg=tag(Boolean=# as $TYPE_T)) as $TYPE_T)
                | Nat=vv => tag (Arrow=record(fun=project(v.tp),
                                                  arg=tag(Nat=# as $TYPE_T)) as $TYPE_T)
                | Arrow=vv => tag (Arrow=record(fun=project(v.tp),
                                                  arg=tag(Arrow=vv as $TYPE_T)) as $TYPE_T)
                | None=vv => tag(None=# as $TYPE_T)
               esac
             )
  | App=v => ( case app(app(f,env), project(v.fun)) of
                    Arrow=vv => if =(project(vv.fun),
                                     app(app(f,env), project(v.arg)))
                                then project(vv.arg)
                                else tag(None=# as $TYPE_T)
                                fi
                  | Boolean=vv => tag(None=# as $TYPE_T)
                  | Nat=vv => tag(None=# as $TYPE_T)
                  | None=vv => tag(None=# as $TYPE_T)
               esac )
  | If=v => if =(app(app(f,env),project(v.cond)), tag(Boolean=# as $TYPE_T))
            then ( if =(app(app(f,env),project(v.thn)), app(f,project(v.els)))
                   then app(app(f,env),project(v.thn))
                   else tag(None=# as $TYPE_T)
                   fi )
            else tag(None=# as $TYPE_T)
            fi
  | Succ=v => if =(app(app(f,env),v), tag(Nat=# as $TYPE_T))
              then tag(Nat=# as $TYPE_T)
              else tag(None=# as $TYPE_T)
              fi
  | Pred=v => if =(app(app(f,env),v), tag(Nat=# as $TYPE_T))
              then tag(Nat=# as $TYPE_T)
              else tag(None=# as $TYPE_T)
              fi
  | Fix=v => ( case v of
                   Abs=v => if =(app(app(f,env), project(v.t)), project(v.tp))
                            then project(v.tp)
                            else tag(None=# as $TYPE_T)
                            fi
                 | Tru=v => tag(Nat=# as $TYPE_T)
                 | Fls=v => tag(Nat=# as $TYPE_T)
                 | Abs=v => tag(Nat=# as $TYPE_T)
                 | App=v => tag(Nat=# as $TYPE_T)
                 | If=v => tag(Nat=# as $TYPE_T)
                 | Succ=v => tag(Nat=# as $TYPE_T)
                 | Pred=v => tag(Nat=# as $TYPE_T)
                 | Fix=v => tag(Nat=# as $TYPE_T)
               esac )
  esac
   )))), 
   emptyEnv), 
        tag(App=record(fun=tag(Abs=record(var='a',
                                tp=tag(Nat=# as $TYPE_T), 
                                t=tag(Var='a' as $TERM_T)
                            ) as $TERM_T),
                        arg=tag(Zero=# as $TYPE_T))
            as $TYPE_T)
)
";

$testEnv = "
            app(
                app(
                    app(
                        app(
                            extendEnv,
                            app(app(app(extendEnv,emptyEnv),'c'), tag(Boolean=# as $TYPE_T))
                        ),
                        'd'
                    ),
                    tag(Nat=# as $TYPE_T)
                ),
                'b'
            )
";

$extendEnv = "
    app(
        abs(extendEnv:->(->(Char,$TYPE_T),->(Char,->($TYPE_T,->(Char,$TYPE_T)))).
            $prog
        ), 
        abs(oldEnv:->(Char,$TYPE_T).
            abs(s:Char.
                abs(n:$TYPE_T.
                    abs(sprime:Char.
                        if =(s,sprime) then n else app(oldEnv,sprime) fi
                    )
                )
            )
        )
    ) 
";
$emptyEnv = "
app(abs(emptyEnv:$ENV_T.
        $extendEnv
    ),
    abs(s:Char.tag(none = # as $TERM_T))
)
";

$_ = "
$emptyEnv
";

#print;
#print "\n-------------------------------------------------------\n\n";

s/\n/ /g;

$file = "5-programming.sml";
print "Writing code as $file...\n";
open (FILE, ">$file");
print FILE "\n val tc = \"".$_.'"

val tcm = ps tc
';
close (FILE);