; ------------- SORTS -------------------------------

TYPE
  ExpertSys :: F: FBase
               R: RBase;
  FBase = Fact-set;
  RBase = Rname -> Rule;
  Rname = STR;
  Fact = STR;
  Rule :: Ifs  : FBase
          Thens: FBase;
ENDTYPE

; ------------- STATE -------------------------------
; ES : ExpertSys

; ------------- FUNCTIONS ---------------------------

FUNC  TestIf(rn:Rname,fb:FBase,rb:RBase):Bool
PRE   rn in dom(rb)
RETURNS  subset(Ifs(rb[rn]),fb); 

FUNC  UseThen(rn:Rname,fb:FBase,rb:RBase) : FBase
PRE   rn in dom(rb)
RETURNS  fb U Thens(rb[rn]);


FUNC  TryRule(rn:Rname,fb:FBase,rb:RBase) : FBase
RETURNS  if TestIf(rn,fb,rb) then UseThen(rn,fb,rb) else fb;

FUNC  StepForward(fb:FBase,rb:RBase) : FBase
RETURNS  UNION({TryRule(rn,fb,rb) | rn <- dom(rb)});


FUNC  ForwardChain(fb:FBase, rb:RBase) : FBase
RETURNS  let ( facts = StepForward(fb,rb) )
         in  if (facts == fb)
             then  fb
             else  ForwardChain(fb U facts, rb);
 

FUNC  Deduce() :
STATE  let ( NewFacts = ForwardChain(F(ES),R(ES)),
             OldRules = R(ES) )
       in ES <- ExpertSys(NewFacts,OldRules);
  



FUNC  BackwardChain(f:Fact,fb:FBase,rb:RBase) : Bool 
STATE if (f in fb) then X <-"mmmm"
RETURNS   (f in fb)  
         ||
;          all( r <- ran(rb) : if (f in Thens(r)) then Testify(r,fb,rb) 
;                                 else true);
          exist( r <- ran(rb) : (f in Thens(r)) && Testify(r,fb,rb) ); 


FUNC  Testify(r:Rule,fb:FBase,rb:RBase) : Bool 
RETURNS   subset(Ifs(r),fb) 
         ||
          all( f <- Ifs(r) : BackwardChain(f,fb,rb) ); 

FUNC  Verify(f:Fact) : Bool 
RETURNS  BackwardChain(f,F(ES),R(ES));

FUNC  Init() : 
STATE  ES <- ExpertSys({},[]);

FUNC  AddFact(f:Fact) :
STATE  ES <- ExpertSys({f} U F(ES),R(ES));

FUNC  RemFact(f:Fact) :
STATE  ES <- ExpertSys({f} - F(ES),R(ES));

FUNC  AddRule(rn:Rname,r:Rule) :
PRE   ~(rn in dom(R(ES)))
STATE  ES <- ExpertSys(F(ES), [rn -> r] + R(ES));

FUNC  RemRule(rn:Rname) :
PRE   rn in dom(R(ES))
STATE  ES <- ExpertSys(F(ES), R(ES)\{rn});

;test

Init();
AddFact("peter plays tennis");
AddFact("paul plays golf");
AddFact("peter studies algebra");
AddFact("paul studies algebra");
AddFact("mary likes poetry");
AddRule("r1",Rule({"peter plays tennis"},{"he is doing CS"}));
AddRule("r2",Rule({"he is doing CS"},{"he reads poetry"}));
AddRule("r3",Rule({"peter studies algebra","he reads poetry"},{"mary loves peter"}));