-- JunoSolverImpl.mesa
-- June 11, 1983 12:05 am
-- GNelson
-- Last Edited by: Gnelson, December 11, 1983 10:10 pm

DIRECTORY SolverCommon, JunoSolver, JunoSyntax, RealSolver, 
               PairSolver, JunoBind, Lisp, JunoLookup, LinearSolver;

JunoSolverImpl: PROGRAM
  IMPORTS SolverCommon, JunoSyntax, RealSolver, PairSolver, 
              JunoBind, Lisp, JunoLookup, LinearSolver
  EXPORTS JunoSolver 
= BEGIN OPEN SolverCommon, JunoSolver, Lisp, JS: JunoSyntax, JB: JunoBind;

Solve: PUBLIC PROC [f: JS.Formula, vl: JS.Varlist, al: JunoBind.Alist, defs: REF]
        RETURNS [al2: JunoBind.Alist, rc: ResultCode]
= {g: JS.Formula; 
   vl2: JS.Varlist;
   rcon: RealSolver.Context;
   lcon: PairSolver.Context;
   eq: Value;
   [g, vl2] _ Normalize[f, defs];
   al2 _ JB.EmptyBinding[];
   {vll: JS.Varlist _ vl; 
     WHILE vll # NIL DO
       {temp: Solvee _ NewSolvee[Car[vll]]; 
        al2 _ JB.NewBind[al2, Car[vll], temp];
        vll _ Cdr[vll]}
     ENDLOOP};
   rc _ $solved;
   [eq, rcon, lcon] _ SetUp[al2, vl2, al, g ! ExplicitOccurrenceOfFalse => rc _ $refuted];
   IF rc = $refuted THEN RETURN;
   rc _ SolveLoop[eq, rcon, lcon];
   SELECT TRUE FROM
     rc = $refuted OR rc = $stumped => NULL;
     rc = $solved OR rc = $close => al2 _ ConstructSolution[vl, al2, rcon, lcon]
   ENDCASE => ERROR};

ExplicitOccurrenceOfFalse: SIGNAL = CODE;

SetUp: PROC [al2: JS.Alist, vl2: JS.Varlist, al: JS.Alist, g: JS.Formula] 
		 RETURNS [eq: Value, rcon: RealSolver.Context, lcon: PairSolver.Context]
= {rcon _ RealSolver.NewContext[];
   lcon _ PairSolver.NewContext[];
   al2 _ JB.Push[al2];
   eq _ NIL;
   WHILE g # NIL DO
     {f: JS.Formula _ Car[g];
      pred: JS.PredName _ JS.PredOfAtomicFormula[f];
      args: JS.Varlist _ JS.TermlistOfAtomicFormula[f];
      ndl: Value;
      g _ Cdr[g];
      [ndl, al2] _ VarlistToNodeList[args, al2, vl2, al, rcon, lcon];
      SELECT TRUE FROM
        pred = JS.true => NULL;
        pred = JS.false => SIGNAL ExplicitOccurrenceOfFalse;
        pred = JS.eq => eq _ Cons[ndl, eq];
        pred = JS.neq => lcon.neq _ Cons[ndl, lcon.neq];
        pred = JS.isPairOf => lcon.pa _ Cons[ndl, lcon.pa];
        pred = JS.isSumOf => rcon.su _ Cons[ndl, rcon.su];
        pred = JS.isPositive => rcon.po _ Cons[ndl, rcon.po];
        pred = JS.isProductOf => rcon.pr _ Cons[ndl, rcon.pr];
        Pair[pred] AND Car[pred] = JS.constant AND
         (ISTYPE[Cadr[pred], REF INT] OR ISTYPE[Cadr[pred], REF REAL])
          => rcon.b _ Cons[Cons[Cadr[pred], ndl], rcon.b];
        Pair[pred] AND Car[pred] = JS.constant AND ISTYPE[Cadr[pred], ATOM] 
          => lcon.b _ Cons[Cons[Cadr[pred], ndl], lcon.b]
      ENDCASE => ERROR}
    ENDLOOP;
    al2 _ JB.Pop[al2]};

VarlistToNodeList: PROC [args: JS.Varlist, 
    					       al2: JB.Alist, 
    					       vl2: JS.Varlist, 
    					       al: JB.Alist,
    					       rcon: RealSolver.Context,
    					       lcon: PairSolver.Context]
					   RETURNS [ndl: Value, newal2: JB.Alist]
= {ndl _ NIL;
   WHILE args # NIL DO
      {arg: Value _ Car[args];
       args _ Cdr[args];
       SELECT TRUE FROM
         
         ~JB.InDomain[arg, al2] AND ~ Memq[arg, vl2] =>
           {u: Value _ JB.Lookup[arg, al];
            temp: Solvee _ NewSolvee[arg];
            ndl _ Cons[temp, ndl];
            IF Pair[u]
              THEN lcon.b _ Cons[Cons[u, temp], lcon.b]
              ELSE rcon.b _ Cons[Cons[u, temp], rcon.b]};
         
         JB.InDomain[arg, al2] =>
           ndl _ Cons[JB.Lookup[arg, al2], ndl];
         
         ~JB.InDomain[arg, al2] AND Memq[arg, vl2] =>
           {temp: Solvee _ NewSolvee[arg];
            al2 _ JB.NewBind[al2, arg, temp];
            ndl _ Cons[temp, ndl]}
         
       ENDCASE => ERROR};
     ENDLOOP;
     ndl _ Reverse[ndl];
     newal2 _ al2};


SolveLoop: PROC [eq: Value, rcon: RealSolver.Context, lcon: PairSolver.Context] 
             RETURNS [rc: ResultCode]
= {rc _ $solved;
DO SELECT TRUE FROM

rc # $refuted AND eq # NIL =>
{x: Solvee = NARROW[Car[Car[eq]]];
 y: Solvee = NARROW[Cadr[Car[eq]]];
 eq _ Cdr[eq];
 [eq, rc] _ PairSolver.Merge[x, y, eq, lcon];
 [eq, rc] _ RealSolver.Merge[x, y, eq, rcon]};

rc # $refuted AND lcon.b # NIL =>
 {u: Value _ Car[Car[lcon.b]];
  x: Solvee _ NARROW[Cadr[Car[lcon.b]]];
  lcon.b _ Cdr[lcon.b];
  [eq, rc] _ PairSolver.Fix[u, x, eq, lcon]};

rc # $refuted AND lcon.neq # NIL =>
 {x: Solvee _ NARROW[Car[Car[lcon.neq]]];
  y: Solvee _ NARROW[Cadr[Car[lcon.neq]]];
  lcon.neq _ Cdr[lcon.neq];
  rc _ PairSolver.Neq[x, y, lcon]};

rc # $refuted AND rcon.b # NIL =>
 {u: Value _ Car[Car[rcon.b]];
  x: Solvee _ NARROW[Cadr[Car[rcon.b]]];
  rcon.b _ Cdr[rcon.b];
  [eq, rc] _ RealSolver.Fix[u, x, eq, rcon]};

rc # $refuted AND lcon.pa # NIL =>
 {x: Solvee _ NARROW[Car[Car[lcon.pa]]];
  y: Solvee _ NARROW[Cadr[Car[lcon.pa]]];
  z: Solvee _ NARROW[Caddr[Car[lcon.pa]]];
  lcon.pa _ Cdr[lcon.pa];
  [eq, rc] _ PairSolver.IsPairOf[x, y, z, eq, lcon]};

rc # $refuted AND rcon.su # NIL =>
 {x: Solvee _ NARROW[Car[Car[rcon.su]]];
  y: Solvee _ NARROW[Cadr[Car[rcon.su]]];
  z: Solvee _ NARROW[Caddr[Car[rcon.su]]];
  rcon.su _ Cdr[rcon.su];
  [eq, rc] _ RealSolver.IsSumOf[x, y, z, eq, rcon]};

rc # $refuted AND rcon.po # NIL =>
  {x: Solvee _ NARROW[Car[Car[rcon.po]]];
   rcon.po _ Cdr[rcon.po];
   [eq, rc] _ RealSolver.IsPositive[x, rcon, eq]}

ENDCASE => EXIT ENDLOOP;

IF rc # $refuted AND rcon.pr # NIL 
THEN {rc _ $close; NewtonRaphson[]}}; --end of SolveLoop

NewtonRaphson: PROC;

Normalize: PROC [f: JS.Formula, defs:REF] RETURNS [g: Value, vl: JS.Varlist]
= {h: Value _ NIL;
   g _ NIL;
   vl _ NIL;
   
   -- h and g are lists of formulas; vl is a list of variables.
   -- h contains conjuncts of f that remain to be normalized;
   -- g contains the normalization as it is built up.
   
   DO SELECT TRUE FROM
   
   -- invariant:  Let f0 be the original formula f.  Then f0 is equivalent to
   -- 
   --         (E vl: f and g and h),
   --
   -- wherein the formula lists h and g represent the conjunctions of their elements.  
   -- Also, all formulas on g are atomic predicates applied to variables.  At the conclusion
   -- if the loop we will have h = nil and f is an atomic predicate applied to variables,
   -- hence the postcondition is established after the loop by g _ Cons[f, g].
   -- The variables on vl are all created by gensym, so we have f0 = (E vl: f0).
   
   JS.IsConjunction[f] =>
     {h _ Cons[JS.LHSOfConjunction[f], h];
      f _ JS.RHSOfConjunction[f]};
   
   -- (f1 and f2) and g and h == f2 and g and (f1 and h)
   
   JS.IsParenthesized[f] => f _ JS.ContentsOfParentheses[f]; 
   
   -- (f1) == f1
   
   JS.IsQuantification[f] AND JS.QuantifierOfQuantification[f] = JS.ex =>
   {vl2: JS.Varlist _ JS.QuantifierVarlistOfQuantification[f];
    f _ JS.QuantifieeOfQuantification[f];
    WHILE vl2 # NIL DO
      {temp: JS.Variable _ JS.Gensym[];
       vl _ Cons[temp, vl];
       f _ Subst[f, Car[vl2], temp];
       vl2 _ Cdr[vl2]}
    ENDLOOP};
    
    --     (E vl: (E vl2: f) and g and h) 
    -- == {if gl2 is a list of distinct symbols of the same length as vl2}
    --     (E vl: (E gl2: f(vl2:gl2)) and g and h)
    -- == {if no var in gl2 is free in g or h
    --     (E vl, gl2: f(vl2:gl2) and g and h)
    --
    -- The loop above constructs the concatenation of  gl2  and  vl  by repeated conses
    -- and simultaneously constructs  f(vl2:gl2)  by repeated substitutions.
    
    JS.IsAtomicFormula[f] AND JS.PredOfAtomicFormula[f] = JS.eq AND
      JS.IsVar[Car[JS.TermlistOfAtomicFormula[f]]] AND 
      LevelOneTerm[Cadr[JS.TermlistOfAtomicFormula[f]]]  AND
      NOT JS.IsConstant[Cadr[JS.TermlistOfAtomicFormula[f]]] =>
      -- I.e., if f is an equality between a variable and a function applied to a list of variables
    {lhs: JS.Variable = Car[JS.TermlistOfAtomicFormula[f]];
     rhs: JS.Term = Cadr[JS.TermlistOfAtomicFormula[f]];
     fun: JS.FunName = JS.FunctionOfTerm[rhs];
     args: JS.Termlist = JS.TermlistOfTerm[rhs];
     def: JS.FunDef = JunoLookup.GetFunDef[fun, defs];
     formals: JS.Varlist _ JS.VarlistOfFunDef[def];
     result: JS.Variable _ JS.ResultnameOfFunDef[def];
     body: JS.Formula _ JS.BodyOfFunDef[def];
     f _ MapSubst[body, Cons[result, formals], Cons[lhs, args]]};
     
     -- with f defined by  f(formals) = result == body , we have
     --
     --    lhs = f(args) == body(result, formals  :  lhs, args).
     --
     -- Note that the guard is stronger than logically necessary: we do not
     -- use this operation unless  args  is a list of variables.  This is to
     -- guarantee that the substitution does not blow up the size of  body .
    
    JS.IsAtomicFormula[f] AND JS.PredOfAtomicFormula[f] = JS.eq AND
      JS.IsVar[Cadr[JS.TermlistOfAtomicFormula[f]]] AND 
      LevelOneTerm[Car[JS.TermlistOfAtomicFormula[f]]] AND
      NOT JS.IsConstant[Car[JS.TermlistOfAtomicFormula[f]]]  =>    
     {tl: JS.Termlist _ JS.TermlistOfAtomicFormula[f];
      newtl: JS.Termlist _ Cons[Cadr[tl], Cons[Car[tl], NIL]];
      -- newtl = reverse(tl)
      f _ JS.MakeAtomicFormula[JS.eq, newtl]};
      
    -- f(varlist) = x   ==   x = f(varlist)
   
    -- termination of this loop depends on the next cases being below the two above
    
    JS.IsAtomicFormula[f] AND (NOT IsVarlist[JS.TermlistOfAtomicFormula[f]]) =>
    {temp: JS.Variable _ JS.Gensym[];
     t: JS.Term;
     pred: JS.PredName _ JS.PredOfAtomicFormula[f];
     tl: JS.Termlist _ JS.TermlistOfAtomicFormula[f];
     [tl, t] _ SwapVarForProperTerm[tl, temp];
     -- this finds the first non-variable in tl, replaces it by temp,
     -- sets tl to be the new list, and t to be the term that was replaced.
     f _ JS.MakeAtomicFormula[pred, tl];
     IF JS.IsConstant[t] 
     THEN h _ Cons[LIST[LIST[JS.constant, t], temp], h]
     ELSE  h _ Cons[JS.MakeAtomicFormula[JS.eq, Cons[temp, Cons[t, NIL]]], h];
     vl _ Cons[temp, vl]};
     
     -- pred(... t ...) == (E temp: pred(... temp ...) and temp = t)
    
    JS.IsAtomicFormula[f] AND IsVarlist[JS.TermlistOfAtomicFormula[f]]
    AND NOT JS.KernelPredicate[JS.PredOfAtomicFormula[f]] =>
    {def: JS.PredDef _ JunoLookup.GetPredDef[Car[f], defs];
     parameters: JS.Varlist _ JS.VarlistOfPredDef[def];
     body: JS.Formula _ JS.BodyOfPredDef[def];
     f _ MapSubst[body, parameters, JS.TermlistOfAtomicFormula[f]]};
    
    -- With p defined by  p(parameters) = body , we have  p(tl) == body(parameters: tl).
   
   JS.IsAtomicFormula[f] AND IsVarlist[JS.TermlistOfAtomicFormula[f]]
   AND JS.KernelPredicate[JS.PredOfAtomicFormula[f]] AND h # NIL =>
   {g _ Cons[f, g]; f _ Car[h]; h _ Cdr[h]};
   
   -- g and f and (h1 and h2) == (g and f) and h1 and h2
   
 ENDCASE => EXIT ENDLOOP;
 
 -- At this point f is an application of a Kernel predicate to a list of Level Zero terms,
 -- and h is NIL.  f may also be a constant predicate T or F. 
 
 IF f # JS.true 
 AND f # JS.false 
 AND NOT (JS.IsAtomicFormula[f] AND IsVarlist[JS.TermlistOfAtomicFormula[f]] AND h = NIL)
 THEN ERROR;
 
 g _ Cons[f, g]}; -- end of Normalize
 
 LevelOneTerm: PROC [t: JS.Term] RETURNS [BOOLEAN] 
 = {RETURN[IsVarlist[JS.TermlistOfTerm[t]]]};
 
IsVarlist: PROC [tl: JS.Termlist] RETURNS [BOOLEAN]
 = {WHILE tl # NIL AND JS.IsVar[Car[tl]] DO tl _ Cdr[tl] ENDLOOP;
     RETURN [tl = NIL]};
    
SwapVarForProperTerm: PROC[f:JS.Termlist, v: JS.Variable] 
   						 RETURNS [g: JS.Termlist, t: JS.Term] =
{l: JS.Termlist _ NIL;
 WHILE JS.IsVar[Car[f]] DO l _ Cons[Car[f], l]; f _ Cdr[f] ENDLOOP;
 t _ Car[f];
 f _ Cons[v, Cdr[f]];
 WHILE l # NIL DO f _ Cons[Car[l], f]; l _ Cdr[l] ENDLOOP;
 g _ f};
 
 ConstructSolution: 
  PROC[vl: JS.Varlist, alin: JB.Alist, rcon: RealSolver.Context, lcon: PairSolver.Context]
  RETURNS [alout: JB.Alist] = 
    {alout _ JB.EmptyBinding[];
     WHILE vl # NIL DO
       temp: LinearSolver.Unknown = NARROW[JB.Lookup[Car[vl], alin], Solvee].tableau;
       alout _ JB.NewBind[
                 alout,
                 Car[vl],
                 SELECT TRUE FROM 
                   temp = NIL => NIL, 
                   temp # NIL => NEW[REAL _ LinearSolver.Solution[temp]]
                 ENDCASE => ERROR];
       vl _ Cdr[vl]
     ENDLOOP    
    };

END.