-- JunoExecImpl.mesa
-- June 6, 1983 2:09 pm Greg Nelson
-- Last Edited by: Gnelson, December 10, 1983 11:02 pm

DIRECTORY JunoSyntax, Lisp, JunoSolver, JunoBind, JunoExec, JunoLookup, JunoToCedar, Atom, Juno2Top, Rope;

JunoExecImpl: PROGRAM
IMPORTS JSolve:JunoSolver, JB: JunoBind, Lisp, JS: JunoSyntax,
JunoLookup, JunoToCedar, Juno2Top
EXPORTS JunoExec
= BEGIN OPEN Lisp;

Error: PROC[message: Rope.ROPE, env: JB.Alist, defs: REF] RETURNS [al: JB.Alist] = {
Juno2Top.Print2[LIST["Exception: "]];
Juno2Top.Print2[LIST[message]];
RETURN[Juno2Top.ReadEvalPrint["?- ", env, defs]]};

CedarCall: PROC[vl: JS.Varlist, tl: JS.Termlist, al2: JB.Alist, defs: REF]
RETURNS [al: JB.Alist] = {
{ul: LIST OF REF ANY ← OtherEvList[tl, al2, defs];
proc: REF JunoToCedar.Proc ← NARROW[ul.first];
-- ul = NIL => program contained Call[]
success: BOOL;
wl: LIST OF REF;
al ← al2;
[success, wl] ← JunoToCedar.Apply[proc^, ul.rest];
IF NOT success THEN RETURN[Error["invalid Cedar call", al, defs]];
WHILE wl # NIL AND vl # NIL DO
al ← JB.Bind[al, Car[vl], Car[wl]];
vl ← Cdr[vl];
wl ← wl.rest
ENDLOOP;
IF wl # NIL OR vl # NIL
THEN RETURN[Error["wrong number of results", al2, defs]]}};

Exec: PUBLIC PROC [c: JS.Command, env: JB.Alist, defs: REF] RETURNS [al: JB.Alist] =
{al ← env;
SELECT TRUE FROM

JS.IsSkip[c] => NULL;

JS.IsAbort[c] => al ← Error["Abort", env, defs];

JS.IsComposition[c] =>
{c1: JS.Command ← JS.LHSOfComposition[c];
c2: JS.Command ← JS.RHSOfComposition[c];
al ← Exec[c2, Exec[c1, al, defs], defs]};

JS.IsSuchthatCommand[c] =>
{vl: JS.Varlist ← JS.VarlistOfSuchthatCommand[c];
f: JS.Formula ← JS.PredOfSuchthatCommand[c];
rc: JSolve.ResultCode;
al2: JS.Alist;
[al2, rc] ← JSolve.Solve[f, vl, al, defs];
SELECT TRUE FROM
rc = $solved OR rc = $close => al ← JB.BindLoop[al, al2];
rc = $refuted =>
al ← Error["unsolvable constraint", env, defs];
rc = $stumped =>
al ← Error["stumped solver", env, defs]
ENDCASE => ERROR};

JS.IsAssignmentCommand[c] =>
{vl: JS.Varlist ← JS.VarlistOfAssignmentCommand[c];
tl: JS.Termlist ← JS.TermlistOfAssignmentCommand[c];
rc: JSolve.ResultCode;
al2: JB.Alist;
[al2, rc] ← EvList[tl, al, vl, defs];
SELECT TRUE FROM
rc = $solved OR rc = $close => al ← JB.BindLoop[al, al2];
rc= $refuted =>
al ← Error["undefined term", env, defs];
rc = $stumped =>
al ← Error["stumped solver", env, defs]
ENDCASE => ERROR};

JS.IsProcCall[c] =>
{vl: JS.Varlist ← JS.VarlistOfProcCall[c];
p: JS.ProcName ← JS.ProcOfProcCall[c];
tl: JS.Termlist ← JS.TermlistOfProcCall[c];
IF p = $Call THEN RETURN[CedarCall[vl, tl, env, defs]];
{pdef: JS.ProcDef ← JunoLookup.GetProcDef[p, defs];
xl: JS.Varlist ← JS.Varlist1OfProcDef[pdef];
yl: JS.Varlist ← JS.Varlist2OfProcDef[pdef];
b: JS.Command ← JS.BodyOfProcDef[pdef];
rc: JSolve.ResultCode;
al2: JB.Alist;
[al2, rc] ← EvList[Append[vl, tl], al, Append[xl, yl], defs];
SELECT TRUE FROM
rc = $solved OR rc = $close
=> {al2 ← Exec[b, al2, defs];
  WHILE xl # NIL DO
  {x: JS.Variable ← Car[xl];
  v: JS.Variable ← Car[vl];
  xl ← Cdr[xl];
  yl ← Cdr[yl];
  al ← JB.Bind[al, v, JB.Lookup[x, al2]]}
  ENDLOOP};
rc= $refuted =>
al ← Error["undefined term", env, defs];
rc = $stumped =>
al ← Error["stumped solver", env, defs]
ENDCASE => ERROR}};


JS.IsAlternatingCommand[c] =>
{gc: JS.GuardedCommand ← JS.BodyOfIterativeCommand[c];
rc: JSolve.ResultCode;
[al, rc] ← Fire[gc, al, defs];
SELECT TRUE FROM
rc = $solved => NULL;
rc = $refuted => RETURN[Error["all guards false in alternative command", env, defs]];
rc = $stumped => RETURN[Error["solver stumped in alternative command", env, defs]];
rc = $close => RETURN[Error["solver uncertain in alternative command", env, defs]]
ENDCASE => ERROR};

JS.IsIterativeCommand[c] =>
{gc: JS.GuardedCommand ← JS.BodyOfIterativeCommand[c];
rc: JSolve.ResultCode ← $solved;
WHILE rc = $solved DO [al, rc] ← Fire[gc, al, defs] ENDLOOP;
SELECT TRUE FROM
rc = $refuted => NULL;
rc = $stumped => al ← Error["solver stumped in iterative command", env, defs];
rc = $close => al ← Error["solver uncertain in iterative command", env, defs]
ENDCASE => ERROR};

ENDCASE => ERROR}; -- end of Exec

Fire: PROC[gc: JS.GuardedCommand, env: JB.Alist, defs: REF]
RETURNS [al: JB.Alist, rc: JSolve.ResultCode]
= {al ← env;
SELECT TRUE FROM

JS.IsCompoundGuardedCommand[gc] =>
{gc1: JS.GuardedCommand ← JS.LHSOfCompoundGuardedCommand[gc];
gc2: JS.GuardedCommand ← JS.RHSOfCompoundGuardedCommand[gc];
[al, rc] ← Fire[gc1, al, defs];
IF rc = $refuted THEN [al, rc] ← Fire[gc2, al, defs]};

JS.IsSimpleGuardedCommand[gc] =>
{vl: JS.Varlist ← JS.VarlistOfSimpleGuardedCommand[gc];
f: JS.Formula ← JS.PredOfSimpleGuardedCommand[gc];
c: JS.Command ← JS.CommandOfSimpleCommand[gc];
[al, rc] ← Fire2[vl, f, c, al, defs]};

ENDCASE => ERROR}; -- end of Fire

Fire2: PROC[vl: JS.Varlist, f: JS.Formula, c: JS.Command, env: JS.Alist, defs: REF]
RETURNS [al: JS.Alist, rc: JSolve.ResultCode]
= {al2: JS.Alist;
al ← env;
[al2, rc] ← JSolve.Solve[f, vl, al, defs];
IF rc = $solved
THEN {al ← JB.Push[al];
al ← JB.Extend[al2, al];
al ← Exec[c, al, defs];
al ← JB.Pop[al]}}; -- end of Fire2

Eval: PUBLIC PROC[t: JS.Term, al: JB.Alist, defs: REF] RETURNS [v:Value, rc: JSolve.ResultCode]
= {IF JS.IsVar[t] THEN {v ← JB.Lookup[t, al]; rc ← $solved; RETURN};
{fn: JS.FunName ← JS.FunctionOfTerm[t];
args: JS.Termlist ← JS.TermlistOfTerm[t];
IF args = NIL THEN RETURN [fn, $solved]; -- numeric constant
IF Memq[fn, LIST[JS.plus, JS.minus, JS.times, JS.divide, JS.div, JS.cons, JS.car, JS.cdr]]
THEN {[v, rc] ← DirectApply[fn, OtherEvList[args, al, defs]]; RETURN};
{fndef: JS.FunDef ← JunoLookup.GetFunDef[fn, defs];
IF fndef = NIL THEN {al ← Error["undefined function", al, defs]; ERROR};
{fnformals: JS.Varlist ← JS.VarlistOfFunDef[fndef];
fnresult: JS.Variable ← JS.ResultnameOfFunDef[fndef];
fnbody: JS.Formula ← JS.BodyOfFunDef[fndef];
argvals: JB.Alist;
rc: JSolve.ResultCode;
[argvals, rc] ← EvList[args, al, fnformals, defs];
-- now argvals is an alist associating formals with actual values
SELECT TRUE FROM
rc = $refuted => {al ← Error["undefined term", al, defs]; ERROR};
rc = $stumped => {al ← Error["solver stumped", al, defs]; ERROR};
rc = $solved OR rc = $close =>
{al2: JB.Alist;
[al2, rc] ← JSolve.Solve[fnbody, Cons[fnresult, NIL], al, defs];
SELECT TRUE FROM
rc = $refuted => {al ← Error["undefined term", al, defs]; ERROR};
rc = $stumped => {al ← Error["solver stumped", al, defs]; ERROR};
rc = $solved OR rc = $close => v ← JB.Lookup[fnresult, al2]
ENDCASE => ERROR}
ENDCASE => ERROR}}}};

DirectApply: PROC[fn:JS.FunName, u: LIST OF REF]
RETURNS [v:Value, rc: JSolve.ResultCode] = {
rc ← $solved;
SELECT TRUE FROM
fn = JS.plus AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ + NARROW[Cadr[u], REF REAL]^];
fn = JS.plus AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ + NARROW[Cadr[u], REF INT]^];
fn = JS.plus AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF INT]^ + NARROW[Cadr[u], REF REAL]^];
fn = JS.plus AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[INT ← NARROW[Car[u], REF INT]^ + NARROW[Cadr[u], REF INT]^];
fn = JS.minus AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ - NARROW[Cadr[u], REF REAL]^];
fn = JS.minus AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ - NARROW[Cadr[u], REF INT]^];
fn = JS.minus AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF INT]^ - NARROW[Cadr[u], REF REAL]^];
fn = JS.minus AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[INT ← NARROW[Car[u], REF INT]^ - NARROW[Cadr[u], REF INT]^];
fn = JS.times AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ * NARROW[Cadr[u], REF REAL]^];
fn = JS.times AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ * NARROW[Cadr[u], REF INT]^];
fn = JS.times AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF INT]^ * NARROW[Cadr[u], REF REAL]^];
fn = JS.times AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[INT ← NARROW[Car[u], REF INT]^ * NARROW[Cadr[u], REF INT]^];
fn = JS.divide AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ / NARROW[Cadr[u], REF REAL]^];
fn = JS.divide AND ISTYPE[Car[u], REF REAL] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[REAL ← NARROW[Car[u], REF REAL]^ / NARROW[Cadr[u], REF INT]^];
fn = JS.divide AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF REAL]
=> v ← NEW[REAL ← NARROW[Car[u], REF INT]^ / NARROW[Cadr[u], REF REAL]^];
fn = JS.divide AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[REAL ← (NARROW[Car[u], REF INT]^ + 0.) / NARROW[Cadr[u], REF INT]^];
fn = JS.div AND ISTYPE[Car[u], REF INT] AND ISTYPE[Cadr[u], REF INT]
=> v ← NEW[INT ← NARROW[Car[u], REF INT]^ / NARROW[Cadr[u], REF INT]^];
fn = JS.cons => v ← Cons[Car[u], Cadr[u]];
fn = JS.car => v ← Car[Car[u]];
fn = JS.cdr => v ← Cdr[Car[u]];
ENDCASE => rc ← $refuted};


EvList: PUBLIC PROC [tl: JS.Termlist, al:JS.Alist, vl: JS.Varlist, defs:REF]
RETURNS [al2: JB.Alist, rc: JSolve.ResultCode]
= {al2 ← JB.EmptyBinding[];
rc ← $solved;
WHILE tl # NIL AND rc = $solved DO
{u: Value;
v: JS.Variable ← Car[vl];
t: JS.Term ← Car[tl];
tl ← Cdr[tl];
vl ← Cdr[vl];
[u, rc] ← Eval[t, al, defs];
al2 ← JB.NewBind[al2, v, u]}
ENDLOOP};

OtherEvList: PROC [tl: JS.Termlist, al: JS.Alist, defs: REF]
RETURNS [LIST OF REF] =
{IF tl = NIL THEN RETURN [NIL];
{v: Value;
rc: JSolve.ResultCode;
[v, rc] ← Eval[Car[tl], al, defs];
SELECT TRUE FROM
rc = $refuted => {al ← Error["undefined term", al, defs]; ERROR};
rc = $stumped => {al ← Error["solver stumped", al, defs]; ERROR};
rc = $solved OR rc = $close =>
RETURN [CONS[v, OtherEvList[Cdr[tl], al, defs]]]
ENDCASE => ERROR}};

END.