-- 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.
       
��!�J��8J�����+.+U