1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc/java-sml.tex	Thu Apr 17 18:01:02 2003 +0200
     1.3 @@ -0,0 +1,162 @@
     1.4 +\documentclass[11pt,a4paper]{article}
     1.5 +\usepackage{latexsym}
     1.6 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}\:$}
     1.7 +\title{\isac Interfaces\\
     1.8 +        Frontend --- Kernel --- Frontend}
     1.9 +\author{Walther Neuper}
    1.10 +
    1.11 +\begin{document}
    1.12 +\maketitle
    1.13 +
    1.14 +\def\pow{\;\;\widehat{ }\;\;\widehat{ }\;\;\widehat{ }}
    1.15 +
    1.16 +In the Backus-Naur-Form used below the symbols of the meta language
    1.17 +are $\; ::= \;\; | \;\; ( \;\; ) \;\; ^* \;\; ^+ \;\;\epsilon\;\;$ as usual, whereas
    1.18 +italic parenthesis {\it (} {\it )}, braces {\it\{} {\it\}} and
    1.19 +brackets {\it[} {\it]} belong to the object language. Terminal symbols
    1.20 +start with an upper-case letter (reminding of SML datatype
    1.21 +constructors), non-terminals start with a lower-case letter. The
    1.22 +nonterminals {\it int} and {\it string} are as defined in SML (in
    1.23 +particular: negative numbers are $\tilde{ }\,1,\cdots$ and not $-1,\cdots$, strings are quoted by ''$\;$''), {\it digit} has the obvious
    1.24 +meaning, and {\it MAT} is being defined elsewhere. Inserted comments {\it (* \dots *)} do not belong to the object-language.
    1.25 +
    1.26 +
    1.27 +
    1.28 +\begin{tabbing}
    1.29 +123\={\it pro}\={\it ofID} \=cmd \=123\=123\=123\=123451234512345\=\kill
    1.30 +{\it FE-KE ::= }\\
    1.31 +\>\>$\:\;${\it StdinSML 0 0 0 0 New\_User ; cr}\\
    1.32 +\>\>$|\;${\it StdinSML userID 0 0 0 End\_User ; cr}\\
    1.33 +\>\>$|\;${\it StdinSML userID proofID acellID cellID dataFK ; cr}\\
    1.34 +
    1.35 +\>{\it userID} \>\>::= {\it int}\\
    1.36 +\>{\it proofID}\>\>::= {\it int}\\
    1.37 +\>{\it acellID}\>\>::= {\it cellID}\\
    1.38 +\>{\it cellID} \>\>::= {\it int}\\
    1.39 +\>{\it cr} \>\>::= {\it carriage-return}\\
    1.40 +\\
    1.41 +\>{\it dataFK}\>\>::= {\it New\_Proof}  $\:|\:$ {\it End\_Proof}\\
    1.42 +\>\>\>$\:|\:$ {\it Command user\_cmd}\\
    1.43 +\>\>\>$\:|\:$ {\it RuleFK rule}\\
    1.44 +\>\>\>$\:|\:$ {\it FormFK MAT}\\
    1.45 +\>\>\>$\:|\:$ {\it PpcFK ( mat\_ppc} )\`\\
    1.46 +\\
    1.47 +\>\>{\it user\_cmd} ::= 
    1.48 +                {\it Accept} $\:|\:$ {\it NotAccept} $\:|\:$ {\it Example}\\
    1.49 +\>\>\>\>$\:|\:$ {\it YourTurn} $\:|\:$ {\it Rules} $\:|\:$ {\it DontKnow}\\
    1.50 +\>\>\>\>$\:|\:$ {\it Undo} $\:|\:$ {\it Auto} $\:|\:$ {\it Details}\`\\
    1.51 +\>\>\>\>$\:|\:$ {\it ActivePlus} $\:|\:$ {\it ActiveMinus}\`\\
    1.52 +\>\>\>\>$\:|\:$ {\it StepwidthPlus} $\:|\:$ {\it StepwidthMinus}\`\\
    1.53 +\\
    1.54 +\>\>{\it rule} ::= {\it Init\_Proof\_Hid ( dialogmode , mat\_list , spec )}\\
    1.55 +\>\>\>$|\:$ {\it Init\_Proof }\>\>\>\>\>$|\:$ {\it
    1.56 +Specify\_Domain domID} \\
    1.57 +\>\>\>$|\:$ {\it Specify\_Problem pblID}\>\>\>\>\>$|\:$ {\it
    1.58 +Specify\_Method metID} \\
    1.59 +
    1.60 +\>\>\>$|\:$ {\it Add\_Given MAT}\>\>\>\>\>$|\:$ {\it Del\_Given MAT}\\
    1.61 +\>\>\>$|\:$ {\it Add\_Find MAT}\>\>\>\>\>$|\:$ {\it Del\_Find MAT}\\
    1.62 +\>\>\>$|\:$ {\it Add\_Relation MAT}\>\>\>\>\>$|\:$ {\it Del\_Relation MAT}\\
    1.63 +      
    1.64 +\>\>\>$|\:$ {\it Refine pblID}\>\>\>\>\>$|\:$ {\it Apply\_Method metID}\\
    1.65 +\>\>\>$|\:$ {\it Check\_Postcond pblID}\>\>\>\>\>$|\:$ {\it Free\_Solve}\\
    1.66 +\\    
    1.67 +\>\>\>$|\:$ {\it Rewrite\_Inst subs thm}
    1.68 +                              \>\>\>\>\>$|\:$ {\it Rewrite thm}\\
    1.69 +\>\>\>$|\:$ {\it Rewrite\_Set\_Inst ( subs , rls )}
    1.70 +                              \>\>\>\>\>$|\:$ {\it Rewrite\_Set rls}\`\\
    1.71 +\>\>\>$|\:$ {\it End\_Ruleset}\>\>\>\>\>$|\:$ {\it Calculate op}\\
    1.72 +\>\>\>$|\:$ {\it Rewrite\_Asm thm}\`\\
    1.73 +\\    
    1.74 +\>\>\>$|\:$ {\it Substitute subs}\>\>\>\>\>$|\:$ {\it Apply\_Assumption preds}\\
    1.75 +\>\>\>$|\:$ {\it Take term} \>\>\>\>\>$|\:$ {\it Take\_Inst term}\\
    1.76 +\>\>\>$|\:$ {\it Group ( con , int\_list )}\\
    1.77 +\>\>\>$|\:$ {\it Subproblem ( spec , mat\_list )}
    1.78 +                              \>\>\>\>\>$|\:$ {\it CAScmd term}\\
    1.79 +\\    
    1.80 +\>\>\>$|\:$ {\it Split\_And}  \>\>\>\>\>$|\:$ {\it Conclude\_And} \\
    1.81 +\>\>\>$|\:$ {\it Split\_Or}   \>\>\>\>\>$|\:$ {\it Conclude\_Or} \\
    1.82 +\>\>\>$|\:$ {\it Begin\_Trans}\>\>\>\>\>$|\:$ {\it End\_Trans} \\
    1.83 +\>\>\>$|\:$ {\it Begin\_Sequ} \>\>\>\>   \\
    1.84 +\>\>\>$|\:$ {\it Intersect}   \>\>\>\>\>$|\:$ {\it End\_Intersect} \\
    1.85 +\>\>\>$|\:$ {\it Check\_elementwise pred}
    1.86 +                             \>\>\>\>\>$|\:$ {\it Collect\_Trues}\`\\
    1.87 +\>\>\>$|\:$ {\it Mstep string}\\
    1.88 +\\
    1.89 +{\it mat\_ppc}::=
    1.90 +\>\>\>{\it ( ( Problem pblID )}$\:|\:${\it ( Method metID ))}\`\\ 
    1.91 +\>\>\>{\it Given  mat\_list}\\ 
    1.92 +\>\>\>{\it Where  mat\_list}\\ 
    1.93 +\>\>\>{\it Find   mat\_list}\\ 
    1.94 +\>\>\>{\it With   mat\_list}\\ 
    1.95 +\>\>\>{\it Relate mat\_list}\\
    1.96 +\\
    1.97 +{\it dialogmode} \>\>\>::= {\it string}\\
    1.98 +{\it domID} \>\>\>::= {\it string}\\
    1.99 +{\it pblID} \>\>\>::= {\it string\_list}\\
   1.100 +{\it metID} \>\>\>::= {\it ( domID , string )}\\
   1.101 +{\it spec}  \>\>\>::= {\it ( domID , pblID , metID )}\\
   1.102 +\\
   1.103 +{\it thm}  \>\>::= {\it ( thmID , MAT )}\>\>\>\>\>\>{\it (* theorem *)}\\
   1.104 +{\it thmID}\>\>::= {\it string}\\
   1.105 +{\it term} \>\>::= {\it MAT}\\
   1.106 +{\it pred} \>\>::= {\it MAT}\>\>\>\>\>\>     {\it (* predicate *)}\`\\
   1.107 +{\it preds}\>\>::= {\it mat\_list}\>\>\>\>\>\>{\it (* predicates *)}\\
   1.108 +{\it rls}  \>\>::= {\it string} \>\>\>\>\>\>{\it (* set of rewrite-rules *)}\\
   1.109 +{\it con}  \>\>::= {\it \&} $\:|\:$ {\it /}
   1.110 +                                  \>\>\>\>\>\>{\it (* }$\land,\lor${\it *)}\\
   1.111 +{\it op}   \>\>::= {\it''plus''} $\:|\:$ {\it''minus''} $\:|\:$ {\it''times''}\`\\
   1.112 +\>\>\hspace*{0.5em}$\:|\:$ {\it''cancel''} $\:|\:$ {\it''pow''} $\:|\:$ {\it''sqrt''}\`\\
   1.113 +
   1.114 +{\it subs} \>\>::= {\it mat\_list}\>\>\>\>\>\>{\it (* substitutions as equalities *)}\\
   1.115 +
   1.116 +\\
   1.117 +{\it int\_list} ::= \>\>\>\>{\it [} $\epsilon \:|\: ($ {\it int} $($
   1.118 +{\it , int} $)^*)$ {\it ]}\\
   1.119 +{\it string\_list} ::= \>\>\>\>{\it [} $\epsilon \:|\: ($ {\it string} $($
   1.120 +{\it , string} $)^*)$ {\it ]}\\
   1.121 +{\it mat\_list} ::= \>\>\>\>{\it [} $\epsilon \:|\: ($ {\it MAT} $($
   1.122 +{\it , MAT} $)^*)$ {\it ]}
   1.123 +\end{tabbing}
   1.124 +
   1.125 +\newpage
   1.126 +\subsection{Interface Kernel --- Frontend}
   1.127 +%------------------------------------------------
   1.128 +\begin{tabbing}
   1.129 +123\={\it pro}\={\it ofID} \=cmd \=123\=123\=123\=12345123451234512345\=\kill {\it KE-FE ::= }\\
   1.130 +\>\>$\:\;${\it( userID , 0 , 0 , [$\,$] , New\_User )}\`(1)\\
   1.131 +\>\>$|\;${\it( userID , proofID , cellID , cellID\_list , dataKF\_list}\`(2)\\
   1.132 +\>{\it dataKF\_list} ::= {\it [ dataKF} $($
   1.133 +{\it , dataKF} $)^*$ {\it ]}\`(3)\\
   1.134 +\\
   1.135 +\>{\it dataKF} ::= {\it New\_Proof} $\:|\:$ {\it End\_Proof}\`(4)\\
   1.136 +\>\>\>$\:|\:$ {\it Request string} $\:|\:$ {\it Message
   1.137 +string} $\:|\:$ {\it Error string}\`(5)\\
   1.138 +\>\>\>$\:|\:$ {\it System string} $\:|\:$ {\it Indicate ind\_list}\`(6)\\
   1.139 +\>\>\>$\:|\:$ {\it Select [ rule} $($ {\it , rule} $)^*$ {\it ]}\`(7)\\
   1.140 +\>\>\>$\:|\:$ {\it Active int} $\:|\:$ {\it Speed int} $\:|\:$ {\it Domain domID}\`(8)\\
   1.141 +\\
   1.142 +\>\>\>$\:|\:$ {\it RuleKF ( edit , rule )}\`(9)\\
   1.143 +\\
   1.144 +\>\>\>$\:|\:$ {\it FormKF ( cellID , edit , indent , nest, MAT )}\`(10)\\
   1.145 +\>\>\>$\:|\:$ {\it PpcKF ( cellID , edit , indent , nest, tag\_ppc )}\`(11)\\
   1.146 +\\
   1.147 +\>\>{\it ind\_list}\>\> ::= {\it [ ind} $($ {\it , ind} $)^*$ {\it ]}\`(12)\\
   1.148 +\>\>\>{\it ind} \> ::= {\it ( ''guide'',} $($ {\it Safe} $\:|\:$ {\it Unsafe} $\:|\:$ {\it Helpless} $)$ {\it)}\`(13)\\
   1.149 +\>\>\>\>$\:|\:$ {\it ( ''proof'',} $($ {\it Incomplete} $\:|\:$ {\it Complete} $\:|\:$ {\it Inconsistent} $)$ {\it)}\`(14)\\ 
   1.150 +\>\>{\it edit}\>\> ::= {\it Write}$\:|\:${\it Protect}\`(15)\\
   1.151 +\>\>{\it indent}\>\> ::= {\it int}\`(16)\\
   1.152 +\>\>{\it nest}\>\> ::= {\it Open}$\:|\:${\it Closed}$\:|\:${\it Nundef}\`(17)\\
   1.153 +\>\>{\it tag\_ppc}\>\> ::= {\it (}\`(18)\\
   1.154 +\>\>\>\>\>( {\it Problem pblID}$\:|\:${\it Method metID} ) {\it,}\`(19)\\ 
   1.155 +\>\>\>\>\>\{ {\it Given  tag\_list ,}\`(20)\\ 
   1.156 +\>\>\>\>\>$\;$ {\it Where  tag\_list ,}\`(21)\\ 
   1.157 +\>\>\>\>\>$\;$ {\it Find   tag\_list ,}\`(22)\\ 
   1.158 +\>\>\>\>\>$\;$ {\it With   tag\_list ,}\`(23)\\ 
   1.159 +\>\>\>\>\>$\;$ {\it Relate tag\_list} \} {\it)}\`(24)\\
   1.160 +\>\>\>{\it tag\_list}\>\> ::= {\it [ tag MAT} $($ {\it , tag MAT} $)^*$ {\it ]}\`(25)\\
   1.161 +\>\>\>\>{\it tag}\>\> ::= {\it Correct}  $\:|\:$ {\it Superfl} $\:|\:$ {\it Incompl}\`(26)\\  
   1.162 +\>\>\>\>\>\>$\:|\:$ {\it False}  $\:|\:$ {\it Syntax}  $\:|\:$ {\it Type}\`(27)
   1.163 +\end{tabbing}
   1.164 +
   1.165 +\end{document}