(* 
<h1>Formal Specification using RSL</h1>
<P>
<pre> *)

(**********************************************************************

                   Ephram Requirements Specification
                         Objects and Operations

                               Jon Doyel
                               Fall 1994

For more infomation, please see the <A HREF="abstract.html> Ephram Abstract</A>.

***********************************************************************)


module Ephram;
    import BasicAppleData.Form, BasicAppleData.InfoChunk;

    define object attribute IconicRepresenationOf;

    obj foo =  InfoChunk;

    obj EphramWorld =
          ib:InfoBase and 
          rb:RuleBase and 
          ws:WorkSpace and
	         ase:AppleScriptEditor and 
          prefs:Preferences and 
          state:EmphramState;

    obj Preferences =
	summaries:Summary* and ...;

    obj Summary =  type:FormType and fnl:FieldNameList;
    obj Summaries =  Summary*;

    obj FormName =  string;

    obj WorkSpace =
          items:ItemsOfInterest and 
          actionss:Actions and
	         curitem:Item and 
          curaction:Action;


    obj ItemsOfInterest =  FormList;


    obj FormList =  Form*;
    obj FormSummary =  Form;

    obj Form =  ...;  (* Should have been expanded, presumably a lot *)

    obj EmphramState =
          regular:Regular or 
          teach:Teach;


    obj AppleScriptEditor =
          f:RecordationFunction and 
          as:AppleScript and
	       ib:InfoBase (* For recognizing changes during teach mode *);

    obj RecordationFunction =
          op(MacWorld)->(AppleScript);

    obj MacWorld;
	      (* The entire Macintosh environment in which a user may run.  The idea
	       * is that when the script editor is running, the user is at the
          * top-level of the Mac OS, and the editor is recording what goes on.
          * The result of the recording is an AppleScript record of what the
          * user did. *)



    obj FormIconList =
       FormIcon*;


    obj FormIcon =
       Form;
       (* A FormIcon is rep'd as a graphic icon on the screen, corresponding
        * to some form data.  See BasicAppleData.Form. *)


    obj ActionIconDisplay =  ActionIcon*;


    obj ActionIcon
       description:
       (* A Icon is rep'd as a graphic icon on the screen, corresponding
        * to some tool that performs an action, where the action is most
        * likely defined in AppleScript.  Need to confirm this. *);
    end ActionIcon;

    
    op CreateNewAction(ActionName,ActionIcon,Form,UserInteractionSequence)->
                      (Action, ActionIconDisplay, UserExplanation)
       description:
       (* This operation allows the end user to demonstrate the Action he wishes
        * the computer to perform with the current Form.  This demonstration is
        * accomplished by placing Ephram in a 'Teach' mode and watching what the
        * user does. These user actions are recorded internally as AppleScript
        * statements. *);
    end CreateNewAction;


    obj UserInteractionSequence =  UserGesturedAction* ;


    obj Action =  GeneratedAppleScriptCode ;


    obj UserExplanation
       description:
       (* An End-User oriented description of the Action's function. This should
        * not take the form of AppleScript, or any programming language, but 
        * rather should be a 'languageless' description of the code generated 
        * by Ephram. *);
    end UserExplanation;


    obj GeneratedAppleScriptCode =  AppleScriptProgram;
       (* This AppleScriptProgram may have been altered from the raw AppleScript
        * that was generated as a result of the users gestured actions.  The
        * alterations would come in the form of generalizations made to the 
        * AppleScript due to inferencing applied to the actions.  In this way
        * Ephram does not simply act as a 'macro recorder', but rather gains
        * a more 'intelligent' role in the user's world. *)


    obj UserGesturedAction =  AppleScriptStmtList;


    obj AppleScriptProgram;
       (* <A HREF="references.html#AppleScriptRef">See AppleScript syntax</A> *)


    op Display(ew:EphramWorld, f:Form)->Form; 


    op DisplaySummary(ew:EphramWorld, f:Form)->fs:FormSummary
        post: HasAllSignificantFeatures(ew, f, fs);
    end;

    function HasAllSignificantFeatures(ew: EphramWorld, 
                                       f:Form, 
                                       fs:FormSummary)->boolean = (
             let prefs = ew.prefs;
             let formprefs = FindPrefsForFormType(ew, f.type);
             forall (fn in formprefs)
                FindChunkByName(f,fn) iff FindChunkByName(fs,fn)
    );

    op FindPrefsForFormType(ew:EphramWorld,type:FormType)->FieldNameList =
	FindPrefsForFormTypeJr(ew.prefs.summaries,type);

    op FindPrefsForFormTypeJr(sums:Summaries,type:FormType)->FieldNameList =
	if sums[1].type = type then sums[1].fnl
	else FindPrefsForFormTypeJr(sums[2:#sums],type);


    obj FieldName =  string;


    obj FieldNameList =  FieldName*;



    (************************************************************
     * The following are the main, top-level Ephram operations.
     ************************************************************)

    op RecordViaAppleScriptEditor(ew:EphramWorld,
	                                 start:StartRecordingAppleEventAndFile)->
                                 (ew':EphramWorld)
      	description: 
         (* Tell the AppleScript Editor to run, recording whatever the user
	       * does.  We'll tell it to stop when the user comes back to Ephram and
	       * chooses 'Stop Recording'. *);
	   pre:
	    IsScriptable(ew.ase)
         (* Sorry, but this is now known to be false,
		    * so we need a fall back position.  No fooling
	   	 * here, we need to figure out how to make this
	   	 * happen. *)

	   	and

	    ew ?. teach;

	   post:
	    (* Everything in the output world is the same, except for the
	     * script ed component, which is simply whatever the input
	     * AppleScriptEditor produces inside itself, the actions of which
	     * are opaque to Ephram; and possibly the info base, which may have
	     * been modified during the running of the editor.  We should note
	     * that the info base could also be modified by backgrounding
	     * Ephram with the finder, but this is beyond the scope of this
	     * spec. *)
	    (ew'.ib = ew'.ase.ib) and
	    (ew'.rb = ew.ib) and
	    (ew'.ws = ew.ws) and	(* NOTE: the workspace is frozen in teach mode.*)
	    (ew'.prefs = ew.prefs) and
	    (ew'.state = ew.state) and
	    (ew'.ase = WhatItDo(ew.ase));
    end;


    function WhatItDo(ase:AppleScriptEditor)->(ase':AppleScriptEditor);
	    (* An apple script editor at play with the user.  Genuinely opaque to
	     * Ephram, until it's done playing.  Despite the flipancy here, is is
	     * actually a fundamentally important principle.  Viz., Eprham is not a
	     * recorder at the Mac World level.  Rather, lets the AppleScript
	     * editor do this, and then uses its output to work on. *)


    op TellAppleScriptEditorToQuitAndSaveItsWork(ew:EphramWorld,
		                                      StopRecordingAndSaveAppleEvent)->
                                           (ew':EphramWorld)
      	description: 
         (* After the users tells Ephram to stop, Ephram in turn tells AS Ed to
	       * stop, after which Ephram snags the the AppleScript that the Ed
	       * built from the file that Ephram originally told the Ed to record
	       * to. *);

    pre:
	    not (ew ?. teach);
	
    post:
	    as = ew.ase.as	
             (* This is the "snagging", given that the
				  * recording file has been abstracted out.
				  * Rather, we snag the script directly from the
				  * editor object, which concretely will be
				  * implemented as a file read. *)
		
      and

	    ew'.ib = Inference(ew.ase.as, ew.rb, nil);
					      (* ^^^ user assistance, which Ephram cant give to itself *)
    end;


    op Run(ew:EphramWorld, 
           mw:MacWorld)->
	         (mw':MacWorld, 
           hfur:HelpFromUserRequest)
      	description: 
         (* If the ew.rb finds a match for the situation in the ew.ws, then it
	       * gens the AppleScript to do what it should and runs it.  The user,
	       * of course, does not know or care that it's AppleScript running, but
	       * we include it here to reminda us what is going on. *);
	    pre:
	     not (ew ?. teach);	(* Prevents recursive teaching! *)

    	post:
       if  FindSituationMatch(ew.rb, ew.ws) != nil
	      then 
         mw' = RunAppleScript(mw, ew.ase, FindSituationMatch(ew.rb, ew.ws)) and
		       hfur = nil
	      else 
	       	(mw' = mw) and
	        (hfur = TeachMeDialog);
    end;


    val TeachMeDialog = "I dont understand, please help ...";
     (* Where Ephram asks for help, expecting the user to enter teach mode. *) 

    obj x;


    function FindSituationMatch(rb:RuleBase, 
                                ws:WorkSpace)->
	                              (as:AppleScript);
	    (* This function is the rule-based expert system running in action rule
	     * mode, where an action rule generates apple script, not more rules.
	     * Cf. the Inference function just below. *)


    function Inference(AppleScript,		(* Recorded by the AS Ed *)
	                      RuleBase,		(* Pre-inference rule base *)
	                      UserAssistance)->	(* Asked for when help is needed *)
	                     (RuleBase,		(* Post-inference rule base *)
	                      UserExplanations);(* As appropriate and/or asked for *)
	    (* This function is the rule-based expert system running in meta rule
	     * mode, where a meta rule generates more rules.  Cf. the
	     * FindSituationMatch function just above.
	     *
	     * It's honestly not clear if a formal logic spec would be useful here
	     * or not, given that this function will be implemented in some expert
	     * system, the logic of which is comparable to RSL.  Hence, we might
	     * consider the expert system to be the spec itself.  *)


    function RunAppleScript(mw:MacWorld, 
                            ase:AppleScriptEditor, 
                            as:AppleScript)->
                           (mw':MacWorld);
	    (* The ultimately opaque function -- it does in the Mac World what
	     * Ephram figured out should be done. *)

    end Ephram;

(* </pre> *)