1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc/tactics.tex Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,24 @@
1.4 +\begin{description}
1.5 +\item{\bf Init\_Proof\_Hid (dialogmode, formalization, specification)} transfers the arguments to the math engine, the latter two in order to solve the example automatically. The tactic is not intended to be used by the student; it generates a proof tree with an empty model.
1.6 +\item{\bf Init\_Proof} generates a proof tree with an empty model.
1.7 +\item{\bf Model\_Problem problem} determines a problemtype (eventually found in the hierarchy) to be used for modeling.
1.8 +\item{\bf Add\_Given, Add\_Find, Add\_Relation formula} inputs a formula to the respective field in a model (necessary as long as there is no facility for the user to input formula directly, and not only select the respective tactic plus formula from a list).
1.9 +\item{\bf Specify\_Theory theory, Specify\_Problem problem, Specify\_Method method} specifies the respective element of the knowledgebase.
1.10 +\item{\bf Refine\_Problem problem} searches for a matching problem in the hierarchy below 'problem'.
1.11 +\item{\bf Apply\_Method method} finishes the model and specification phase and starts the solve phase.
1.12 +\item{\bf Free\_Solve} initiates the solve phase without guidance by a method.
1.13 +\item{\bf Rewrite theorem} applies 'theorem' to the current formula and transforms it accordingly (if possible -- otherwise error).
1.14 +\item{\bf Rewrite\_Asm theorem} is the same tactic as 'Rewrite', but stores an eventual assumption of the theorem (instead of evaluating the assumption, i.e. the condition)
1.15 +\item{\bf Rewrite\_Set ruleset} similar to 'Rewrite', but applies a whole set of theorems ('ruleset').
1.16 +\item{\bf Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, ruleset)} similar to the respective tactics, but substitute a constant (e.g. a bound variable) in 'theorem' before application.
1.17 +\item{\bf Calculate operation} calculates the result of numerals w.r.t. 'operation' (plus, minus, times, cancel, pow, sqrt) within the current formula.
1.18 +\item{\bf Substitute substitution} applies 'substitution' to the current formula and transforms it accordingly.
1.19 +\item{\bf Take formula} starts a new sequence of calculations on 'formula' within an already ongoing calculation.
1.20 +\item{\bf Subproblem (theory, problem)} initiates a subproblem within a calculation.
1.21 +\item{\bf Function formula} calls a function, where 'formula' contains the function name, e.g. 'Function (solve $1+2x+3x^2=0\;\;\;x$)'. In this case the modelling and specification phases are suppressed by default, i.e. the solving phase of this subproblem starts immediately.
1.22 +\item{\bf Split\_And, Conclude\_And, Split\_Or, Conclude\_Or, Begin\_Trans, End\_Trans, Begin\_Sequ, End\_Sequ, Split\_Intersect, End\_Intersect} concern the construction of particular branches of the prooftree; usually suppressed by the dialog guide.
1.23 +\item{\bf Check\_elementwise assumptions} w.r.t. the current formula which comprises elements in a list.
1.24 +\item{\bf Or\_to\_List} transforms a conjunction of equations to a list of equations (a questionable tactic in equation solving).
1.25 +\item{\bf Check\_postcond:} check the current formula w.r.t. the postcondition on finishing the resepctive (sub)problem.
1.26 +\item{\bf End\_Proof} finishes a proof and delivers a result only if 'Check\_postcond' has been successful before.
1.27 +\end{description}
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc/terms.tex Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,109 @@
2.4 +\chapter{List of terms used in the \isac-project}\label{app.terms}
2.5 +
2.6 +\begin{description}
2.7 +\item{\bf }
2.8 +\item{\bf Browser-Window (Browser-Window)}\label{browser-window} is the presentation of data generated by the \see browser, which also handles the http requests generated by the browser window. (The browser-window is that what usually is called a 'browser').
2.9 +\item{\bf Browser (Browser):}\label{browser} There are browsers for \see theories, \see problems, \see methods and \see examples. The browser generates the html-representation of the respective \see browser-window, and handles the respective http-requests.
2.10 +\item{\bf }
2.11 +\item{\bf Calculation (Rechengang)} leads from the \see description of an \see example via the \see modeling phase, the \see specification phase and the \see solving phase to the result.
2.12 +\item{\bf Calculator (Rechner)} is that part of the \see SML-kernel which does single steps of calculation without touching the \see proofstate.
2.13 +\item{\bf }
2.14 +\item{\bf Current formula (aktuelle Formel)} is the unique formula marked on the \see worksheet. If another item on the worksheet is marked, the formula closest (.. to be specified) to the marked item is the current formula.
2.15 +\item{\bf }
2.16 +\item{\bf Course admin (Kurs-Administrator)} is a person administering the use of \isac{} for learning within a group of \see learners.
2.17 +\item{\bf }
2.18 +\item{\bf Course designer (Kurs-Designer)} edits the \see example collection which can be solved by a given \see math knowledge base (edited by a \see mathematics author) and/or edits \see explanations within the \see math knowledge base.
2.19 +\item{\bf }
2.20 +\item{\bf Decorated knowledge (Erweitertes Mathematik-Wissen)} is the \see mathematics knowledge(base) plus \see explanations.
2.21 +\item{\bf Description (Beschreibung)} of an \see example consists of \see formulas, eventually of text and/or a figure. The \see modeling phase transforms the description into a \see model.
2.22 +\item{\bf }
2.23 +\item{\bf Dialog atom (Dialog-Atom)} is a predefined, minimal unit of interaction between the \see learner and \isac. These atoms are symmetrical w.r.t. the two dialog partners.
2.24 +\item{\bf Dialog pattern (Dialog-Muster)} is assembled from \see dialog atoms such that it can adapt to certain situations in a dialog, e.g. if the \see learner produces many errors. Dialog patterns are designed and implementd by a \see dialog author.
2.25 +\item{\bf Dialog mode (Dialog-Modus)} is assembled from \see dialog patterns and supports certain learning strategies, e.g. exploratory learning, written examniation etc. Dialog patterns are designed and implementd by a \see dialog author.
2.26 +\item{\bf Dialog profile (Diaolog-Profil)} defines certain \see dialog modes for examples in the example collection for a certain course. A dialog profile is defined by a \see course designer and set/reset for a specified duration during a course by the \see course admin.
2.27 +\item{\bf Dialog author (Dialog-Autor)} an expert in learning theory who adapts and extends the \see dialog guide.
2.28 +\item{\bf Dialog guide (Dialog-Komponente)} is a component of \isac{} which combines \see dialog atoms to dialog strategies in order to adapt \isac's behaviour to different user models and learning situations.
2.29 +\item{\bf }
2.30 +\item{\bf Example (Beispiel)} is a unit to be calculated and solved separated from others. In general, they are prepared by an author in an \see example collection. Within such a collection the example has a unique identifier.
2.31 +\item{\bf Example browser (Beispiels-Browser)} is an interactive representation of the \see example collection within the \see front-end.
2.32 +\item{\bf Example collection (Beispielsammlung)} contains \see examples, each of them consisting of formulas, of a hidden \see formalization and \see specification, and eventuallly of text and a figure.
2.33 +\item{\bf Example profile (Beispiels-Profil)} describes the structure of an\see example collection; this structure provides data for the \see dialog guide.
2.34 +\item{\bf }
2.35 +\item{\bf Explanation (Erkl\"arung)} is an optional addon (text, formulas, figures, movies, links, \see examples and any combination of these) to elements of the \see math knowledge base.
2.36 +\item{\bf }
2.37 +\item{\bf Formalization (Formalisierung)} contains the formulas in a minimal structure necessary for automated solving the example (together with a \see specification).
2.38 +\item{\bf }
2.39 +\item{\bf Formula (Formel)} consists of variables, constants and functions constants (for logical, algebraic etc. operators); all these parts, however are not yet structured as a (typed) \see term.
2.40 +\item{\bf }
2.41 +\item{\bf Front-end (Frontend)} consists of the \see worksheet, the \see theory browser, the \see problem browser, the \see method browser and the \see example browser.
2.42 +\item{\bf }
2.43 +\item{\bf Interpreter (Interpreter)} comprises the modules \see math engine, the \see calculator and \see dialog guide.
2.44 +\item{\bf }
2.45 +\item{\bf Isabelle} is the name of one of the most successful interactive theorem provers; Isabelle provides the \see theories containing the deductive part of \isac's knowledge base.
2.46 +\item{\bf }
2.47 +\item{\bf Item (Item)} of a \see model, which can be an input item (in the field 'given'), a precondition (in the field 'where'), an ouput item (in the field 'find') or a relation (in the field 'relate'). 'Given', 'find'and 'relate' may be input by the user, where 'where' is supplied by the system. An item consists of the \see item-description and the \see item-data.
2.48 +\item{\bf Item-data (Item-Daten)} are the formulas following the \see item-description.
2.49 +\item{\bf Item-description (Item-Beschreibung)} is an identifier heading each \see item in the fields 'given', 'find' and 'relate'. It indicates the kind of data to be input to the respective item by the users, serves typechecking of the data etc.
2.50 +\item{\bf }
2.51 +\item{\bf KE-base (KE-Basis)} is the \see decorated math-knowledge plus the \see example collection.
2.52 +\item{\bf }
2.53 +\item{\bf Kernel (SML-Kern)} comprises the \see interpreter and the \see knowledge base, all written in SML.
2.54 +\item{\bf }
2.55 +\item{\bf Knowledge base} \see mathematics knowledge base
2.56 +\item{\bf Knowledge browser} is one of the \see theory brosers, \see problem browser, \see method browser.
2.57 +\item{\bf }
2.58 +\item{\bf Learner (Lernender)} a user of \isac, who uses \isac{} for learning and exercising, i.e. who calculates \see examples by use of the \see math knowledge base.
2.59 +\item{\bf }
2.60 +\item{\bf Match (Matchen):} a \see model matches a \see problem, or not. This kind of matching is different from the matching-algorithm of symbolic computation: it checks if all \see items are input, and evaluates the predicates in 'where'.
2.61 +\item{\bf }
2.62 +\item{\bf Math engine (Mathematik-Maschine)} provides for all functions doing \see calculations: for applying \see tactics, for input \see formulas, for calculating resulting formulas, for proposing the next tactic, and for doing calculations automatically; it maintains a \see proofstate for each calculation.
2.63 +\item{\bf Mathematics author (Mathematik-Autor)} an expert in computer mathematics who adapts and extends the \see mathematics knowledge base.
2.64 +\item{\bf Mathematics knowledge base (Mathematische Wissensbasis)} is stored in three SML-datastructures, in an acyclic graph of \see theories, in a hierarchy of \see problems, and in a hierarchy of \see methods. It is extensible by \see math authors and can be both, read by \see learners and interpreted by \isac. See also \see decorated math-knowledge.
2.65 +\item{\bf }
2.66 +\item{\bf Method (Methode)} contains a \see script describing the algorithm for calculating the result, and a guard structured like a \see problem in order to inhibit inappropriate application of the script.
2.67 +\item{\bf Method browser (Methoden-Browser)}
2.68 +\item{\bf }
2.69 +\item{\bf Model (Modell)} consists of \see items. It \see matches a \see problem, or not.
2.70 +\item{\bf Model context (Modell-Kontext)} comprises all the information handled in the \see modeling phase as represented on the worksheet. This is at least one of the folloging items: a \see model (of a problem and/or of a method), a \see problem, a \see theory, a \see problem, a \see method.
2.71 +\item{\bf Modeling phase (Modellierungs-Phase)} is the initial phase in problem solving. In this phase either the system automatically transforms a \see formalization of an example into a \see model or the user inputs the \see items into the model.
2.72 +\item{\bf }
2.73 +\item{\bf Parsing (Parsen)} is the process of transforming an 'plain' formula into a typed term. Parsing requires the specification of a \see theory containing information about infix position of operators etc.
2.74 +\item{\bf }
2.75 +\item{\bf Problem browser (Problem-Browser)}
2.76 +\item{\bf Problem (Problem)} consists of patterns of items which can be \see matched with a \see model during the \see specification phase.
2.77 +\item{\bf }
2.78 +\item{\bf Proofstate (Beweiszustand)} is given by an internal prooftree (partially represented on the \see worksheet) and a \see current formula.
2.79 +\item{\bf }
2.80 +\item{\bf Rewriting (Rewriting)} transforms a formula into a new one by application of a \see theorem. \isac{} provides conditional as well as ordered rewriting.
2.81 +\item{\bf }
2.82 +\item{\bf Script (Skript)} describes the algorithm solving a particular problem; a script contains \see tactics, expressions for guiding the flow of evaluation, and eventually subproblems.
2.83 +\item{\bf }
2.84 +\item{\bf Selection-tool (Auswahls-Tool)} displays the contents of either the \see example collection, or the dependency graph of \see theories, or the hierarchy of \see problems, or the hierarchy of \see methods; and it allows to select a respective item for detailed display.
2.85 +\item{\bf }
2.86 +\item{\bf SML-kernel} \see kernel
2.87 +\item{\bf }
2.88 +\item{\bf Solving phase (L\"osungs-Phase)} is the final phase in problem solving, which generates the solution from the \see model and the \see specification; this phase may comprise all problem solving phases for one or more subproblems.
2.89 +\item{\bf }
2.90 +\item{\bf Specification (Spezifikation)} relates a \see model to the knowledge base while determining a \see theory, \see a problem and a \see method.
2.91 +\item{\bf Specification phase (Spezifikations-Phase} is the second phase in problem solving, which determines the \see theory, \see the problem and the \see method.
2.92 +\item{\bf }
2.93 +\item{\bf Step ((Rechen-) Schritt)} propagates a \see calculation and involves both partners once, i.e. the \see learner and the \see dialog guide. A step is represented by one of the \see dialog atoms.
2.94 +\item{\bf }
2.95 +\item{\bf Tactic (Taktik)} is applicable or not to the current \see formula within the current proofstate, and generates a new formula accordingly.
2.96 +\item{\bf }
2.97 +\item{\bf Term (Term)} is an Isabelle term (simple typed lambda calculus) generated from a \see formula by \see parsing.
2.98 +\item{\bf }
2.99 +\item{\bf Theorem (Theorem)} is a predicate proven true by \see Isabelle w.r.t. certain preconditions. Theorems are applied by \see rewriting.
2.100 +\item{\bf }
2.101 +\item{\bf Theory (Theorie)} is the part of the \see math knowledge base which defines (function) constants and axioms. Within a theory usually the related \see theorems are being proven by \see Isabelle and stored.
2.102 +\item{\bf Theory Browser (Theorie-Browser)}
2.103 +\item{\bf }
2.104 +\item{\bf User (Benutzer)} of \isac{} may be one of the following: \see visitor, \see learner, \see math author, \see dialog author, \see course designer, or \see course admin.
2.105 +\item{\bf }
2.106 +\item{\bf Visitor (Besucher)} a user of \isac, which occasionaly browses an \isac-site, i.e. the \see knowledge base and the \see example collection.
2.107 +\item{\bf }
2.108 +\item{\bf Worksheet (Arbeitsblatt)} contains the \see calculation of an \see example eventually leading to a result.
2.109 +\item{\bf }
2.110 +\item{\bf }
2.111 +\item{\bf }
2.112 +\end{description}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc/urd-content.tex Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,418 @@
3.4 +%nicht vergessen: auch urd.tex (wegen $Revision $) \"andern !
3.5 +\chapter{User Requirements Document}
3.6 +
3.7 +This document describes the user requirements for the \sisac-system.
3.8 +
3.9 +This version of the document captures at least those requirements in detail, which are a prerequisite for the {\em first phase of development, i.e. the development of the kernel of the math knowledgebase, of the indispensible tools for interaction on the knowledge, and of the tools for authoring the example collection.}
3.10 +
3.11 +The design will try to meet these requirements while accepting the structure of the \sisac-math-engine, which is defined by mathematical reasons, and offers new functionality (calculations are done stepwise, the learner can input a formula or a tactic and receive feedback from the engine, the math-engine usually 'knows' the next step).
3.12 +
3.13 +%As new and different the functionality of the envisaged system is, as limited is the functionality w.r.t the expectiations a user can demand from (educational) math software at the state of the art. Thus from the beginning \sisac{} is seen as part of a collection of cooperating modules, and some requirements are stated here with the purpose, to provide for an architecture ready for combining \sisac{} with other components (administration, graphing etc.), and not with the purpose, to implement everything within \sisac{}.
3.14 +
3.15 +The User Requirements Document is structured along the different kinds of users envisaged. The Software Requirements Document, on the other hand, will be structured along the modules implementing the functionality. In order to establish comfortable tracing, the $m:n$ relation between user requirements and software requirements will be accurrately recorded in a double-linked way.
3.16 +
3.17 +Terms marked by \see{} are briefly described in appendix \ref{app.terms}.
3.18 +
3.19 +\section{Kinds of \isac{} users}
3.20 +There are several kinds of \sisac{} users which set the respective requirements:
3.21 +%the following should be consistent with Terms.sml !!!
3.22 +\begin{description}
3.23 +\item{\bf visitor (Besucher):} occasionally drops into an \sisac-site and browses the respective math knowledge base and the example collection. May try to calculate some examples.
3.24 +\item{\bf learner (Lernender):} uses \sisac{} for learning and exercising, i.e. primarliy calculates examples in the example collection by use of the math knowledge base. As a member of courses the learner is called a student.
3.25 +\item{\bf math author (Mathematik-Autor):} is an expert in computer mathematics who adapts and extends the mathematics knowledge base.
3.26 +\item{\bf dialog author (Dialog-Autor):} is an expert in learning theory who adapts and extends the dialog guide.
3.27 +\item{\bf course admin (Kurs-Administrator):} is a person administering the use of \sisac{} for learning within a group of learners.
3.28 +\item{\bf course designer (Kurs-Designer):} adapts and extends the example collection which can be solved by a given math knowledge base, and adds explanations to items in the knowledge base. These tasks do not require special knowledge in computer mathematics.
3.29 +\item{\bf administrator (Administrator):} this r\'ole combines the system administrator installing the software, and the person who implements the overall design of an \sisac-site (introductory pages etc.) on behalf of the site-owner.
3.30 +\end{description}
3.31 +%the above should be consistent with Terms.sml !!!
3.32 +These kinds of users are distinguished by the respective access-rights.
3.33 +
3.34 +\section{General requirements}
3.35 +This section describes the primary decisions for underlying systems, and requirements common to all users.
3.36 +
3.37 +\subparagraph{Decisions for underlying systems} have been done already.
3.38 +As this requirements document shows, \sisac{} is a large system: thus it cannot be done from scratch, rather is has to use as much as components already available. The theorem prover Isabelle provides for both, a comprehensive frontend for interactive deduction (i.e. for definitions, axioms and proving theorems), and a hughe mathematics knowledge base. Both are under rapid development, which \sisac{} shall take advantage of. The kernel of Isabelle, however is relatively stable already, and thus the interfaces to \sisac s math engine (ME) are sufficiently stable.
3.39 +{\bf\UR The deductive part is left to Isabelle. \label{deduct-isa}}
3.40 +{\bf\UR \sisac s math engine closely cooperates with Isabelle \label{me-isa}\\}
3.41 +Thus the math engine is already implemented in the same program language as Isabelle, SML.
3.42 +
3.43 +\subparagraph{\sisac s mathematics engine(ME)} is already given. Thus several requirements, looking like software requirements, are listed here. A calculation (see terms in the \sisac-project \cite{isac:appendices}) undergoes three phases: the modeling phase, the specification phase and the solving phase, where the latter may contain these phases recursively (see the demonstration example in the usecases document \cite{isac:use}).
3.44 +
3.45 +Calculations are created interactively in steps. A step is initiated by the input of a learner: input of a tactic, of a formula or of a 'go-on' command. A tactic is applied to a formula and generates another (the derived) formula. The tactics specified so far are listed in appendix \ref{appendix-tacs}
3.46 +\footnote{Eventually it may turn out, that some special tactics are missing and have to be added.}.
3.47 +An input formula during modeling phase completes a model, and during the solving phase an input formula is considered a derivation of the previous formula.
3.48 +{\bf\UR Calculations are done in steps: formula, tactic, 'go-on'\label{step}}
3.49 +{\bf\UR The the mode of the ME \label{me-mode}} is {\em one} of the following:
3.50 +\begin{tabbing}
3.51 +12345\=12345\=\kill
3.52 +\>step is applicable, result guaranteed\\
3.53 +\>step is applicable, result is not guaranteed\\
3.54 +\>\>(because the learner has input some strange step previously)\\
3.55 +\>the ME is helpless, i.e. it cannot propose a next step\\
3.56 +\>the step is not applicable, plus an error message, why not applicable.
3.57 +\end{tabbing}
3.58 +{\bf\UR A calculation has a tree-like structure \label{calc-tree}}
3.59 +{\bf\UR In the solve-phase each formula is justified by a tactic.\label{tactic}}
3.60 +{\bf\UR Tactics as listed in appendix \ref{appendix-tacs}\label{tacs}}
3.61 +
3.62 +
3.63 +\subparagraph{Requirements for all users:}
3.64 +There are two different way for users to approach \sisac s facilities for learning: (a) the user may browse the knowledge base, and eventually calculate an example (illustrating a definition, a problem, etc.) and (b) the user calculates examples from the example collection, and while asking for justifications enters knowledge browsers. The latter case implements the really innovative didactic approach of \sisac{}, 'learning by doing (calculations)'.
3.65 +{\bf\UR The users access \sisac{} via internet. \label{isac-www}}
3.66 +This raises specific issues, because handling of mathematics formulas on standard browsers is still under construction, and several other relevant standards are under construction.
3.67 +{\bf\UR Access a: from example to knowledge, acces b: from knowledge to example to knowledge --- are both possible. \label{access-ab}}
3.68 +{\bf\UR Consistent ``look \& feel'' for all users. \label{ur:look-feel}}
3.69 +As long as the deductive part is left to Isabelle, the same is with the theory browser. \sisac{} will develop the ``look \& feel'' of its own, and thus violate uniformity w.r.t. the theory browser.
3.70 +{\bf\UR Locking, copying, versioning \label{URlock-copy-version}} is necessary w.r.t. authoring within the multi-user system. TODO !!!
3.71 +%{\bf\UR \label{UR}}
3.72 +
3.73 +\section{Requirements of the visitor}
3.74 +Each user approaching an \sisac-site first time wants to know about the purpose of \sisac{} and about the contents of the site.
3.75 +\subparagraph{Browsers: overview -- detail:}
3.76 +The contents of the knowledgebase and of the example collection are
3.77 +expected to become very large. Thus there need to be facilities to
3.78 +switch from an overview to a detail and vice versa. These facilities
3.79 +should be handled simliarily for all the browsers. Primarliy, there is no direct interaction between the visitor and the ME. Informations for the visitor
3.80 +should be provided in statical HTML-Pages.
3.81 +
3.82 +Visitors should get an overview over {\em all} the knowledge available at an \sisac-site, and {\em all} the explanations, and {\em all} the examples.
3.83 +%The HTML-pages should provide a learning environment for its Visitors. ...WN:nein!
3.84 +Therefore, access to additional information should be gained
3.85 +if available. %This additional information include mathematical details
3.86 +%like methods to solve a problem (which requires to call the ME, however), as well as \sisac\/-internal information like a description of used \emph{items}.
3.87 +
3.88 +{\bf\UR There are 4 kinds of data to be browsed: theories, problems, methods, examples. \label{ur:4-data}}
3.89 +{\bf\UR All 4 kinds of data need a table of contents of variable detail. \label{ur:hierarchy-frame}}
3.90 +{\bf\UR Browse through statical HTML-Pages \label{ur:browse-static}} without e.g. matching a model with a problem.
3.91 +
3.92 +\subparagraph{Do some examples:}
3.93 +Visitors should get an overview over {\em all} the features available at an \sisac-site, and the most exciting feature is stepwise interactive calculating and reasoning guided by the system. This should be demonstrated by some examples, which also the visitor can execute.
3.94 +{\bf\UR Call of a worksheet from a link in the knowledge} for instance demonstrating an example for a definition, a problem, etc.
3.95 +{\bf\UR Execute some selected examples in the example collection. \label{visit-calc}}
3.96 +
3.97 +
3.98 +
3.99 +\section{Requirements of the learner}
3.100 +The typical access of the learner to \sisac{} is via the example collection (see UR\ref{access-ab}). Solving an example typically comprises three phases, modeling, specifying and solving.
3.101 +
3.102 +\subparagraph{Help in the model phase:}
3.103 +In the model phase the learner generally has to input the \see items of a \see model (see the example for reference \ref{model} p.\pageref{model}): input and output items can be 'correct', 'incomplete', 'missing', 'superfluous' or have a 'syntax error'; preconditions can be 'correct' or 'false' --- these properties should be clearly indicated. This help is only possible, if the learner choose an example (with a hidden \see formalization and \see specification) from an \see example collection.%; 'syntax error', of course, is always fed back.
3.104 +
3.105 +If users want to calculate an example {\em unknown} to the system they have two choices:
3.106 +\begin{enumerate}
3.107 +\item specify a problem in order to get help from the system. Again, there are two possibilities:
3.108 + \begin{enumerate}
3.109 + \item first specify the appropriate problem (which contains the \see item-descriptions), and then input the items. The item-descriptions help the user to provide the appropriate item-data.
3.110 +
3.111 + \item first input the items (the item-descriptions are to be looked up in a specific theory), and then specify the problem --- already assisted by the system (see UR\ref{ur-match} and UR\ref{ur-refine}).
3.112 + \end{enumerate}
3.113 +\item do the calculation independently and without relying on assistance by the system (i.e. without specifying a problem, thus the system cannot check for completeness, and cannot assign a \see method). In this case the input of items in the 'given'-field is sufficient; the users can calculate the example by applying tactics (after manual input).
3.114 +\end{enumerate}
3.115 +
3.116 +{\bf\UR Visualization of the feedback on input to a model.\label{model-feedback}}
3.117 +{\bf\UR Do a calculation unknown to the system.\label{unknown-calc}}
3.118 +
3.119 +\subparagraph{Retrieve a matching problem:}
3.120 +Given a model initiating a calculation, or as a subproblem within a
3.121 +calculation, the learner has to determine a problem matching this
3.122 +model. This involves information retrieval from a large
3.123 +problem-hierarchy. There the learner may get lost, and thus he
3.124 +should get help: make the math-engine find a matching problem;
3.125 +visualize the problem found within the hierarchy.
3.126 +
3.127 +In case of an exam, the user is forced to find the correct problem with
3.128 +no or limited help. Therefore it is nessesary to adjust the amount of
3.129 +help given by the browsers (e.g. only ``match'' or ``nomatch'' instead
3.130 +of a detailed listing of all conditions)
3.131 +{\bf\UR Can retrieve and match a problem.\label{ur-match}}
3.132 +{\bf\UR Gets help by automated refinement of a problem.\label{ur-refine}}
3.133 +%{\bf\UR \label{UR }}
3.134 +
3.135 +\subparagraph{Dynamic views into the knowledge base:} UR \ref{ur-match} and UR \ref{ur-refine} is one case, the other is displaying a method with the tactic marked which just has been applied in a calculation (this is well-known from debuggers).
3.136 +{\bf\UR Dynamic views into the knowledge base, \label{ur:dynamic-views}} into the hierarchy of problems and into the hierarchy of methods.
3.137 +
3.138 +
3.139 +\subparagraph{Additional information in a calculation} should be provided any time on request of the learner. This feature comprises a more detailed views onto the proofstate, as well as explanations. A command {\tt 'detail'} will be available on the following items:
3.140 +\begin{center}
3.141 +\begin{tabular}{l l l}
3.142 +{\tt 'detail'} on & element & yields\\
3.143 +\hline\hline
3.144 +whole formula & // & generating tactic\\
3.145 +whole formula & // & associated assumptions\\
3.146 +formula & function-constant & definition in the theory\\
3.147 +formula & floatingpoint-no & precision of this no\\
3.148 +evaluated predicate
3.149 + & // & derivation\\
3.150 +evaluated assumption
3.151 + & // & derivation\\
3.152 +\hline
3.153 +tactic & theorem & theorem instantiated\\
3.154 +theorem instantiated
3.155 + & // & animation of matching\\
3.156 +tactic & ruleset & intermediate steps\\
3.157 +tactic & subproblem & intermediate steps\\
3.158 +\hline
3.159 +error 'not matching'
3.160 + & // & animation of matching\\
3.161 +\hline
3.162 +model & theory & file of the respective theory\\
3.163 +model & problem & model instantiating this problem\\
3.164 +model & problem & inherited assumptions\\
3.165 +model & method & model instantiating the guard\\
3.166 +model & method & script of the respective method\\
3.167 +\footnote{This list may be extended.}
3.168 +\end{tabular}
3.169 +\end{center}
3.170 +%
3.171 +%
3.172 +%wobei
3.173 +%* in idFormulaCurrent und idTacticCurrent auch Subterme (PS) angesprochen werden koennen sollten
3.174 +%* nicht nur OEffnen von untergeordneten Teilen des Beweises wuenschenswert ist, sondern auch verschiedenste andere Rueckgabewerte (void):
3.175 +% - Links auf Definitionen, Erklaerungen, Beweise
3.176 +% - ... (werde Anfang naechster Woche Genaueres liefern) ...
3.177 +%* die Rueckgabewerte somit auch vom aktuellen Status abhaengen
3.178 +%
3.179 +%... also wieder so eine 'unmoegliche Anforderung
3.180 +%
3.181 +{\bf\UR Details of a calculation as given above.\label{detail}}
3.182 +{\bf\UR Explanations to each item in the knowledge base.\label{explanation}\\}
3.183 +The explanations are filtered w.r.t. the current dialog state (explanations given several times are skipped, etc.) and filtered w.r.t. the knowledge profile.
3.184 +
3.185 +\subparagraph{The flow of interaction} shall be adapted to the learner. The learner might be bored because the system offers too little challenge (by using less active dialog atoms -- see UR\ref{dialog-atoms}, or by proceeding in too little steps of calculation) -- or, in contrary, the user might be frustrated by too high challenges (in activity and/or stepwidth).
3.186 +{\bf\UR The 'activity' of the dialog atoms adapts to the learner.\label{}}
3.187 +{\bf\UR The learner can override the dialog atoms chosen by the system. \label{}}
3.188 +{\bf\UR Varying stepwidth with tactics, rule sets and subproblems.\label{stepwidth}}
3.189 +{\bf\UR The stepwidth can be overridden by the learner. \label{}}
3.190 +I.e. the stepwidt mechanically chosen by the dialog guide.
3.191 +
3.192 +\subparagraph{The dialog regards} presettings of the course admin (see Sect.\ref{course-admin} below), when guiding the flow of interaction, and the dialog regards the ongoing interaction with the student.
3.193 +{\bf\UR The system records examples done/not done by a learner \label{expl-done}} regardless which course the learner is logged in.
3.194 +{\bf\UR The dialog regards the performance \label{perform}} in calculations done by the learner in the current session. The performance is measured by response times, errors, difficulty of examples done, requests into the knowledge base, active-passive behaviour.
3.195 +\footnote{The completion of this list is up to a future phase of development, and the evaluation of these data as well.}
3.196 +{\bf\UR The dialog regards the knowledge \label{know}} touched by the learner in the current session.
3.197 +{\bf\UR The dialog regards the history \label{history}} of performance and knowledge touched in previous sessions.
3.198 +
3.199 +
3.200 +\subparagraph{Guarantee of correct results} is given by \sisac s proofstate in the ME. This guarantee can only be given, when each editing on the worksheet is mirrored in the prooftree (eventually cutting certain branches, if an intermediate step is redone). Sometimes the learner might want to edit a calulation (shorten the calculation by cutting intermediate steps, etc.) without affecting the prooftree any more.
3.201 +{\bf\UR \sisac{} guarantees correct results.\label{correct}}
3.202 +In this case the worksheet reflects the proofstate, which shall be indicated on the screen and on the printout; in the latter case this indication should be certificate which cannot be manipulated.
3.203 +{\bf\UR A calculation can be edited arbitrarily.\label{edit}}
3.204 +Once this has been done, the ME cannot resume user guidance. Worksheet and printout don't show the certificate.
3.205 +
3.206 +\subparagraph{The mother language} should be used. The language of math formulas is independent from other languages. Thus the names used in the knowledge base can simply be changed for each language (scriptures with different structure like Japanese will not be considered here). But there are other texts delivered by the system, like error messages, or the fields 'given,...' in a model; these should be implemented multilinqual.
3.207 +{\bf\UR The system ist multilinqual. \label{}}
3.208 +
3.209 +
3.210 +\section{Requirements of the math author}\label{math-author}
3.211 +In the current phase 1 of development (tutoring system only) all the
3.212 +authoring of math knowledge will be done on the SML toplevel,
3.213 +i.e. immediately on the datastructures holding the knowledge. This
3.214 +part of the task is described in the 'interfaces for authors of math
3.215 +knowledge' \cite{develop-experiment}.
3.216 +
3.217 +{\bf\UR Remote access to the sml-kernel \label{}} is required. However, knowledge modfied need not yet imported to the production (i.e. tutoring) system.\\
3.218 +
3.219 +Another result of authoring math knowledge, however, will be tools for the visitor and the learner to view the knowledge generated. This part of the task is described here.
3.220 +
3.221 +%{\bf\UR \label{}}
3.222 +%{\bf\UR \label{}}
3.223 +{\bf\UR Automatic linking-tool \label{URinterlink}} supports setting links to other occurrences of an item: the system suggests links, the author accepts or rejects.
3.224 +%{\bf\UR Automatic links to additional, related informations if available. \label{URinterlink}}
3.225 +%%W.N. kann ich mir nicht vorstellen ...
3.226 +%%A.G.(6.3.) ist nicht so unwahrscheinlich - vor allem mit dem event-modell
3.227 +%% von dinopolis sollte das moeglich sein - eventuell auch mit java-webstart
3.228 +%% (ab 1.4) - ich glaube die moeglichkeit besteht, ueber die implementierung
3.229 +%% hab ich mir noch nicht allzu viele gedanken gemacht - oder gibt es da ein
3.230 +%% problem an das ich nicht gedacht habe ?
3.231 +%%W.N. um das zu beantworten verstehe ich die Details noch zu wenig
3.232 +Automated linking is done between the following items:
3.233 +\begin{center}
3.234 +\begin{tabular}{l l l}
3.235 +item & in \dots & linked to occurrence in\\
3.236 +\hline\hline
3.237 +predicate & theorem & definition in theory\\
3.238 + & pre/postcondition & definition in theory\\
3.239 +theorem & tactic & definition in theory\\
3.240 +\hline
3.241 +TODO
3.242 +\footnote{This list may be completed.}
3.243 +\end{tabular}
3.244 +\end{center}
3.245 +
3.246 +{\bf\UR Exchange data with other \sisac{} sites.\label{x-isac}\\}
3.247 +TODO
3.248 +{\bf\UR Exchange data with other knowledge bases. \label{}\\}
3.249 +TODO
3.250 +
3.251 +\subparagraph{Copyright} may be reserved for the author(s) of a theory, of a part of the problem hierarchy or a method, if is separated from the other parts of the knowledge base.
3.252 +{\bf\UR Copyright on theories, problems and methods.\\}
3.253 +
3.254 +
3.255 +
3.256 +
3.257 +\paragraph{Authoring theories\\}
3.258 +The generation of the theory browser is already implemented by Isabelle. Within phase 1 of development, \sisac{} will take this component without any change.
3.259 +
3.260 +\paragraph{Authoring problems\\}
3.261 +TODO
3.262 +
3.263 +\paragraph{Authoring methods\\}
3.264 +TODO
3.265 +
3.266 +
3.267 +\section{Requirements of the dialog author}\label{dialog-author}
3.268 +We hope that it is possible to develop a language which allows to define dialog patterns (as combinations of dialog atoms already implemented) and dialog modes sequencing dialog patterns. By means of such a language learning strategies could be described, and this description could be interpreted in reaction to a dynamic dialog state and according to an knowledge profile.
3.269 +
3.270 +To do such a 'dialog programming' is considered a comprehensive task, which in general exceeds the knowledge of a course designer or a course admin (both see below) --- thus the statement of respective requirements is separated. A course designer should be able to associate courses with dialog profiles (combining dialog modes), and the course admin should be able to select dialog modes within process of time in a course.
3.271 +
3.272 +The dialog atoms are the following, ordered by descending 'activity' of the learner: All atoms concern a step from the current formula \currf applying a tactic \tac which yields the resulting formula \res(the derivation of \currf), i.e. $f\longrightarrow^{\it tac}\;f^\prime$.
3.273 +\begin{enumerate}
3.274 +\item \label{putres} given \currf, input the next formula \res
3.275 +\item \label{fillres} given a partial \currf (supplied by \sisac), complete \currf such that it is a derivation of \currf
3.276 +\item \label{puttac}given \currf, input a tactic \tac to be applied to \currf
3.277 +\item given \currf, select \tac from a list (supplied by \sisac) to be applied to \currf
3.278 +\item \label{filltac} given \currf and a partial \tac, complete the \tac (i.e. a theorem, a substitution, etc.) such that it can be applied to \currf
3.279 +\item given \currf, \tac, and a partial \res, complete \res such that it is the result of applying \tac to \currf
3.280 +\item given \currf and \res, input \tac such that \res is the result of \currf applying \tac
3.281 +\item given \currf and \res, select \tac from a list (supplied by \sisac) such that \res is the result of \currf applying \tac
3.282 +\item given \currf, \res and a partial \tac, complete \tac such that \res is the result of \currf applying \tac
3.283 +\end{enumerate}
3.284 +{\bf\UR Dialog atoms according to the list above. \label{dialog-atoms}\\}
3.285 +
3.286 +The 'activity' requested from the learner for doing such a dialog atom can be varied by the appropriateness of the lists of tactics supplied by \sisac{} and the structure of the formula to be completed. The appearance of the dialog atoms is very different depending on the phase, modeling or solving.
3.287 +
3.288 +The requirements analysis for a dialog state and a learner model is postponed to a future phase of development; the 'dialog programming' will prepare \sisac{} to meet the user-requirements UR\ref{perform}, UR\ref{know}, UR\ref{history}, and UR\ref{profile}.
3.289 +
3.290 +
3.291 +\section{Requirements of the course admin}\label{course-admin}
3.292 +Authoring in \sisac{} comprises various tasks: authoring mathematics knowledge and authoring the dialog have been described in Sect.\ref{math-author} and Sect.\ref{dialog-author}; these both tasks require more special knowledge than the others. Sect.\ref{course-designer} describes a kind of knowledge ('explanations') which may change from one course to the other, and wich does not require special knowledge on computer mathematics or dialog design.
3.293 +
3.294 +The latter part of authoring is done by the course designer preparing as course in advance (see Sect.\ref{course-designer}). Some of the knowledge prepared in advance underlies time constraints, which are managed by the course admin. The requirements of the course admin are separated in this section (despite the fact that the course designer and the course admin are one and the same person, the lecturer or teacher of the course).
3.295 +
3.296 +\subparagraph{There are groups of learners} in order to support the adminstration of courses. The membership w.r.t. these groups determines the selections of examples in the example collecton (see UR\ref{profile-details}), the selection of explanations in the knowledge (see UR\ref{author-explanation})) and the initial setting of the dialog as captured in UR\ref{detail} and UR\ref{stepwidth}.
3.297 +{\bf\UR There are groups of learners. \label{groups}}
3.298 +{\bf\UR One learner may belong to different groups \label{mem}} but only to {\em one} group within a session.
3.299 +{\bf\UR Administrative information for groups \label{}} is part of any login, and should be available for review at any time during a session.
3.300 +
3.301 +\subparagraph{Time limits for delivering course material} are a general requirement for educational systems, and it applies for example collections as well. This requirement provides the course admin to distribute workload over time and to focus the attention of the learners. Sometimes it may be desirable to have some examples finished within a certain time limit. Also examples (for instance prepared for an examination) may be invisible for learners.
3.302 +%{\bf\UR \label{}}
3.303 +{\bf\UR There are 2 kinds of time limits:\label{UR:time-limits}} (1) given by start and finish, and (2) given by a duration (where start and finish are recorded with the user).
3.304 +{\bf\UR Groups of examples may be locked\label{expl-locked}} for groups of learners for certain time limits. (SR: attention with links from the KB !)
3.305 +{\bf\UR Groups of examples may be invisible\label{invisible}} for all users except the example author for certain time limits. (SR: examples have an author !)
3.306 +{\bf\UR Restricted help for the learners during a exam\label{restrict-know}} %WNnein: depending on the location (classroom) or
3.307 +i.e. particular links into the knowledge base are restricted for a particular group for a limited time.
3.308 +{\bf\UR Access-rights during an exam-session \label{}} are particularily restricted (a user might get unwanted information by opening another session as a member of another group).
3.309 +{\bf\UR Restrictions may be overridden or not\label{other-courses}} depending on the setting by the course-designer. Overriding e.g. allows to look at explanations and examples for other courses.
3.310 +\\.\\
3.311 +TODO: Flowchart for access-rights !
3.312 +
3.313 +\subparagraph{Survey on the progress of the learners} i.e. of the students in a course. Such surveys are indispensable requirements for a course admin. Thus all the surveys below are related to a specific course.
3.314 +%{\bf\UR \label{}}
3.315 +{\bf\UR There is a statistics-tool\label{UR:statistics}} for the learners progress
3.316 +{\bf\UR Statistics are drawn from\label{UR:data-for-statistics}} the following data: TODO
3.317 +
3.318 +Examples for statistics:
3.319 +\begin{itemize}
3.320 +\item Which examples have been done by whom with which performance
3.321 +\item Sorts w.r.t. the examples: frequency of touched, not touched, solved, unsolved (, evaluation of performance, as soon as evaluation functions have been designed) over all students of a course
3.322 +\item Sort w.r.t. the students: likewise over all examples in specified groups
3.323 +\item Which lookups into the knowledge have been done
3.324 +\item Sorts w.r.t. the destination: likewise over students
3.325 +\item Sorts w.r.t. the students: likewise over the knowledge.
3.326 +\end{itemize}
3.327 +
3.328 +Special requirements may be raised by field studies on learning mathematics. \sisac{} shall be open for such special research. I.e. queries over examples, lookups, students {\em and courses}. Anonymous evaluation has to be regarded.
3.329 +{\bf\UR Anonymous evaluation of statistics.\label{}}
3.330 +
3.331 +\subparagraph{Written examinations} can be done due to requirements stated elsewhere: hidden examples UR\ref{invisible}, restricted access to knowledge UR\ref{restrict-know}, adapted dialog UR\ref{dialog-atoms} and evaluation UR\ref{eval-stud-expl} (evaluation of performance as soon as evaluations function have been designed).
3.332 +{\bf\UR Written examinations can be done with \sisac \label{}} following the traditional conventions.
3.333 +
3.334 +
3.335 +\section{Requirements of the course designer}\label{course-designer}
3.336 +
3.337 +A course desinger prepares the learning materials and exercises for a course according to the goals of that course, or according to the learners' level. If \sisac{} is being used for a course, specific explanations may be added to the knowledge
3.338 +\footnote{It is the task of a {\em mathematics author}, however, to edit the {\em contents} of a math knowledgebase~!}
3.339 +and examples will be prepared within the example collection.
3.340 +{\bf\UR Explanations from other \sisac-sites can be imported.\label{}}
3.341 +{\bf\UR Examples from other \sisac-sites can be imported.\label{}}
3.342 +{\bf\UR Copyright for the author of explanations.\label{}}
3.343 +{\bf\UR Copyright for the author of examples.\label{}}
3.344 +
3.345 +
3.346 +\subparagraph{Appearance of example collections:}
3.347 +One application of \sisac{} will be to mechanize tutoring on existing example collections, as found for instance in traditional textbooks. Thus the example collection must copy the structure already given (the enumerations, page breaks, assembly on a page etc.) in order to allow the learner to find a particular example (e.g. given as homework). Traditional textbooks use arbitrary labels for their chapters and sections, the levels are nested arbitrarily deep, and there are arbitrary labels for the examples.
3.348 +
3.349 +For copy-right reasons it also may happen, that the example itself (i.e. text, formulas, figures) is not displayed, only the respective label. In this case the label should be located exactly at the same position on a virtual 'page' on the screen as the original position in the page of the textbook.
3.350 +%{\bf\UR Each example has a unique label. \label{}} Klaus.19.12.02
3.351 +{\bf\UR The labels are defined by the author}\label{UR161a}
3.352 +{\bf\UR The graphical layout is equivalent to textbooks.\label{expl-layout}}
3.353 +%{\bf\UR \label{}}
3.354 +
3.355 +\subparagraph{The structure of example collections} is a hierarchy of groups of examples. A group of examples consists of the part visible to the learner (which may be copied from a textbook) and additional data for \sisac{} to suggest examples of a level appropriate to an individual learner. There are already requirements concerning examples, UR\ref{expl-locked} and UR\ref{invisible}, which apply to groups of examples for convenience.
3.356 +%{\bf\UR \label{}}
3.357 +{\bf\UR There is only one example collection in the system\label{}} in analogy to {\em one} problem-hierarchy and {\em one} method hierarchy. This collection, however, even may comprise several textbooks.
3.358 +{\bf\UR There are groups of examples \label{}} with common properties, see UR\ref{expl-locked} and UR\ref{invisible}.
3.359 +%{\bf\UR The hierarchy of groups of examples can be zoomed in/out.} Klaus.19.12.02 nona
3.360 +{\bf\UR A group and/or an example are weighted\label{}} w.r.t. properties to be defined in a later phase of development (at least the properties 'difficulty' and 'length').
3.361 +{\bf\UR A tool for selecting examples\label{}} w.r.t. the weights (and the user-model etc.) is required. There may be also administrative concerns:
3.362 +\begin{itemize}
3.363 +\item A limit of the number of solved examples may be defined for a group; if the limit is touched, this group has been mastered successfully by a student within a certain course. An evaluation-function for the performance will be advantageous here in the future.
3.364 +\item There might be obligatory examples in a group; i.e. such an example must be solved by a student in order to have the group mastered successfully.
3.365 +\end{itemize}
3.366 +%{\bf\UR \label{}}
3.367 +
3.368 +\subparagraph{Edit examples in the example collection} requires several editors. An example can be described by verbal text, by formulas, and by figures (and eventual by movies). Additionally, each example contains data hidden from the visitor and the learner.
3.369 +{\bf\UR Integrated editing of text, formulas and figures}\label{editors}
3.370 +{\bf\UR A formalizations is a list of formulas.}
3.371 +{\bf\UR A specification is a triple\label{}} of three pointers to a theory, a problem and a method respectively.
3.372 +{\bf\UR Each example is combined with a list of pairs of\label{}} a formalization and a specification respectively.
3.373 +{\bf\UR Formalizations and specifications are hidden\label{}} from the user.
3.374 +{\bf\UR An example may have error schemes\label{}} for particular input items, paired with an explanation (see UR\ref{explanation}\dots UR\ref{explanation-forall} below).
3.375 +
3.376 +
3.377 +\subparagraph{Check of solvability} for each example or for groups of examples is necessary before delivery to the learners. The former can be done by a session opened in parallel to the authoring session.
3.378 +{\bf\UR A tool for batch-processing examples \label{}} is required.
3.379 +{\bf\UR Errors for batch-processing \label{}} are: TODO
3.380 +%{\bf\UR \label{}}
3.381 +\\
3.382 +
3.383 +\subparagraph{Edit explanations in the knowledge base} requires the same range of editors as in UR\ref{editors} plus lookup other sources of knowledge on the web, which could be linked into the knowledge base for use in a particular course. The following requirements are to be covered by a separated tool:
3.384 +{\bf\UR An explanation may consist of\label{explanation}} text, formulas, figures (movies, and links into the KB, into the web, to an example in the resident site.
3.385 +{\bf\UR An explanation is {\em one} combination\label{}} of arbitrary elements from UR\ref{explanation}; i.e. there is {\em one} link which, however, may have nested links.
3.386 +{\bf\UR Explanations are course-specific. \label{author-explanation}}
3.387 +Each course might have different explanations according to the contents of the course, according to the specific example collection, and according to the learners' level.
3.388 +{\bf\UR Each item in a knowledge base can have explanations.\label{explanation-forall}} per course. This should also be possible within formulas, e.g. an explanation to a predicate in a 'where'-field of a model.
3.389 +
3.390 +
3.391 +\subparagraph{A knowledge profile} for each course results from the explanations following the requirements from above, plus from the detail knowledge is used in, from error schemes and from fill-in patterns for theorems.
3.392 +{\bf\UR An example group and/or an example specifies the details\label{profile-details}} as defined in UR\ref{detail}.
3.393 +{\bf\UR There are error schemes,\label{}} eventually several for one theorem in a particular method, or for specific tactics in a particular method. An error scheme is paired with an explanation (UR\ref{explanation}\dots UR\ref{explanation-forall}).
3.394 +{\bf\UR There are fill-in patterns\label{}} for theorems, eventually several for one theorem in a particular method. Such patterns are used for the dialog atoms UR\ref{dialog-atoms}, e.g. \ref{fillres} or \ref{filltac}.
3.395 +
3.396 +
3.397 +\subparagraph{A dialog profile} can be preset according to the students' level. These predefined setting can be overridden by the students in most cases, but not in all cases. The dialog profile will be more elaborated as soon the 'dialog programming' and the user model habe been clarified in a future development phase.
3.398 +{\bf\UR A dialog mode restricts the dialog atoms\label{}} (UR\ref{dialog-atoms}) to be used by the learner within certain time limits (e.g. during the time of a written examination).
3.399 +
3.400 +%\subparagraph{}
3.401 +%{\bf\UR . \label{}\\}
3.402 +%{\bf\UR . \label{}\\}
3.403 +%{\bf\UR . \label{}\\}
3.404 +%{\bf\UR . \label{}\\}
3.405 +
3.406 +
3.407 +\section{Requirements of the administrator}
3.408 +%W.N.: dieser Abschnitt ist f''ur alle
3.409 +The administrator has to set up the system and implement the overall
3.410 +design of an \sisac-site. This includes introductory pages as well as
3.411 +an basic overall design (Corporate Design, links to ``home''...)
3.412 +
3.413 +{\bf\UR Basic parameters to adapt the HTML-outtput to an corporate
3.414 +design (e.g. colors, font, \dots)}
3.415 +%\subparagraph{Customize the appearance}%[UR4.1]
3.416 +%adapt the HTML-output to the coporate design - add advertisements
3.417 +%W.N.???? \dots
3.418 +
3.419 +%{\bf\UR }
3.420 +%\subparagraph{}
3.421 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc/urd.tex Thu Apr 17 18:01:03 2003 +0200
4.3 @@ -0,0 +1,43 @@
4.4 +\documentclass[a4wide]{report}
4.5 +\usepackage{epsfig}
4.6 +\usepackage{latexsym}
4.7 +\bibliographystyle{alpha}
4.8 +
4.9 +\newcommand {\kommentar}[1]{\marginpar{\begin{flushright}\tiny#1\end{flushright}}}
4.10 +\newcommand {\frage}[1]{
4.11 + \marginpar{
4.12 + \begin{tabular}{p{5mm} p{2cm}}
4.13 + \begin{flushleft}
4.14 + {\large?}
4.15 + \end{flushleft}
4.16 + &
4.17 + \begin{flushright}
4.18 + \tiny #1
4.19 + \end{flushright}
4.20 + \\
4.21 + \end{tabular}
4.22 + }
4.23 +
4.24 + }
4.25 +\newcommand {\bigquest}{\marginpar{\huge?}}
4.26 +\newcommand {\cnumber}[1]{\put(8,4){\circle{11}}\put(5,1){#1}\hspace{5mm}}
4.27 +
4.28 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
4.29 +\def\sisac{{\small${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
4.30 +\def\see{$\rightarrow$}
4.31 +
4.32 +\title{\isac\\ User Requirements Document}
4.33 +\author{Andreas Griesmayer, Alan Krempler, Walther Neuper\\
4.34 +{\tt\{agries,akremp,neuper\}@ist.tugraz.at}}
4.35 +\date{$Revision$}
4.36 +%\date{$Revision$}4.2:UR\label{unknown-calc},\label{model-feedback}
4.37 +
4.38 +\includeonly{urd-content}
4.39 +\begin{document}
4.40 +\maketitle
4.41 +\tableofcontents
4.42 +
4.43 +\input{common}
4.44 +\bibliography{bib/didact,bib/math-eng,bib/dia-form,bib/RISC_1,bib/RISC_2,bib/misc,bib/hci,bib/isac}
4.45 +\end{document}
4.46 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc/use-content.tex Thu Apr 17 18:01:03 2003 +0200
5.3 @@ -0,0 +1,945 @@
5.4 +%nicht vergessen: auch use.tex ($Revision $) \"andern !
5.5 +\chapter{Usecases}
5.6 +
5.7 +\noindent This document serves three purposes, it should
5.8 +\begin{enumerate}
5.9 +\item document internal discussions about crucial design questions during the
5.10 +early design phases
5.11 +\item establish data for test cases at the end of the implementation phase
5.12 +\item provide for entry-points to understand \sisac{} for collegues newly joining the \sisac team.
5.13 +\end{enumerate}
5.14 +The use cases - if not stated otherwise - refer to one example presented in \ref{use-expl} on p.\pageref{use-expl}.
5.15 +
5.16 +\section{Enter an \isac{} site}
5.17 +
5.18 +{\bf\UC Somebody visits an \sisac{} site \label{UC:visitor}\\} Anybody dropping into an
5.19 +\sisac-site more or less intentionally first wants to know what is
5.20 +offered at this site. The visitor may never had heard anything about
5.21 +\sisac, and thus should get information on the purpose and the
5.22 +features \sisac. Or somebody may want to know in detail about the
5.23 +contents of the knowledge base and/or the example collection of this
5.24 +particular site.\\ In both cases the owner of the site might have
5.25 +decided to inhibit solving examples from the collection; any user,
5.26 +however, is welcome to browse example collection.
5.27 +
5.28 +\begin{enumerate}
5.29 + \item The Visitor is reaching the entry-page of the \sisac-site. This
5.30 + site containes a welcome-message from the host of the system as well
5.31 + as a brief sumary of its content. The entry-page acts as doorway for
5.32 + \begin{itemize}
5.33 + \item the \sisac-knowledge (i.e. decorated knowledge including explanations) as it contains links to the problems, methods and theories
5.34 + \item the example collection
5.35 + \item input of a new example not known to the system (this feature is locked for visitors, the respective usecases are in \ref{start-calc}).
5.36 + \end{itemize}
5.37 +
5.38 + \item The user might select one of the three main branches of the
5.39 + knowledge base (Fig.\ref{3D-math}. on p.\pageref{3D-math}) and browse
5.40 + them as described in \ref{userbrowse}, or jump directly to an
5.41 + example-collection.
5.42 +
5.43 +\end{enumerate}
5.44 +
5.45 +\begin{figure} [htb]
5.46 +\centerline{\psfig{figure=fig/3D-math-thy.eps,height=7cm}}
5.47 +\caption{The 3 dimensions of \sisac s knowledge base}
5.48 +\label{3D-math}
5.49 +\end{figure}
5.50 +
5.51 +{\bf\UC A subscribed student enters \sisac\label{UC:enter}\\} A student subscribed to
5.52 +a particular course has access to the whole contents of the math
5.53 +knowledge base. The access to parts of the example collection
5.54 +(together with other material) may have been temporarily restricted by
5.55 +the lecturer of that course (eventually in order to introduce new
5.56 +material in wellsized chunks).
5.57 +\begin{enumerate}
5.58 +
5.59 + \item The student enters the entry-page as above.
5.60 +
5.61 + \item The subscribed student starts his access on an login-page
5.62 + provided by \sisac %(there might be a link on the entry-page of the site to reach the login)
5.63 +
5.64 + \item once he authenticated himselve, course-related links and
5.65 + informations are presented (e.g. important example-collections, links
5.66 + to new, just in the course introduced theory, lately calculated
5.67 + examples, \dots). This site is updated by the course-administrator
5.68 + who can synchronize the content with his course.
5.69 +
5.70 + \item The student can choose to browse the presented content
5.71 + (examples or knowledge) similar as described in \ref{userbrowse} -
5.72 + with the restriction, that the range of presented information does
5.73 + not cover the full content of the particular \sisac - site, but is
5.74 + limited to the courses subject.
5.75 +
5.76 +\end{enumerate}
5.77 +
5.78 +{\bf\UC System view: A subscribed student enters \sisac\label{UC:session}\\}
5.79 +There is a userrequirement which insists on the use of standard web-browsers for the front-end as much as possible. The capabilities of web-browsers w.r.t. interactions are very limited, however. In particular, the initalization of a session is an awkward task.
5.80 +
5.81 +\begin{enumerate}
5.82 + \item The user accesses the login-page to start a course session
5.83 +
5.84 + \item The Browser checks the given username and passwort and creates
5.85 + a new Browserdialog which is assigned to the proper UserModel.
5.86 +
5.87 + \item The Browser asks the Browser-dialog for the course-information
5.88 + to present.
5.89 +
5.90 + \item The Browser-dialog gathers the informations from the
5.91 + description-storage and filters it according to the informations
5.92 + from the usermodel.
5.93 +
5.94 + \item The Browser encodes the informations and returns them to the
5.95 + browser-window.
5.96 +\end{enumerate}
5.97 +
5.98 +
5.99 +\begin{figure} [htb]
5.100 +\centerline{\psfig{figure=fig/browser-dialog-startup.eps,width=11cm}}
5.101 +\caption{Setting up a calculation}
5.102 +\label{setup-calc}
5.103 +\end{figure}
5.104 +
5.105 +TODO interaction diagrams of the most crucial points of UC.\ref{UC:session}.
5.106 +
5.107 +%WN.17.4.03: UC System view: calculate an existing example --> 5.3.1
5.108 +%WN.17.4.03: UC System view: start a new calculation --> 5.3.1
5.109 +
5.110 +
5.111 +\section{Use the mathematics knowledge base}
5.112 + \sisac s mathematics knowledge is separated from the knowledge
5.113 + interpreter (the 'mathematics engine'). The knowledge is described
5.114 + such that it can be read by human users {\em and} can be interpreted
5.115 + by the mathematics engine in {\em one and the same} format. Thus the
5.116 + knowledge base is one entry point of interactive learning (besides
5.117 + the example collection).
5.118 +
5.119 + For technical reasons we subsume the example collection here: Handling and representation of knowledge and examples has been unified so far. There are several terms concerning knowledge, see \cite{isac:appendices} 'List of Terms Used in the \sisac{} Project': knowledge, decorated knowledge (i.e. knowledge plus explanations), KE-base (i.e. decorated knowledge plus example collection).
5.120 +
5.121 +\subsection{Browse the knowledge}
5.122 +{\bf\UC User browses through the problem hierarchy\\}
5.123 +\label{userbrowse}
5.124 +A student uses a WEB-Browser to gain an overview of the
5.125 +\sisac s problem hierarchy, see p.\pageref{3D-math}.
5.126 +\begin{enumerate}
5.127 + \item The user decides for 'problems' (and not for theories, methods or examples; this descision may be put on another KE-base browser or on a worksheet).
5.128 +
5.129 + \item The browser-window of the problem-browser shows the root problem
5.130 +
5.131 + \item The browser-window of the problem-browser shows the hierarchy of (sub-)problems (at least the next lower level of subproblems).
5.132 +
5.133 + \item After selecting one of the subproblems this subproblem is displayed; the explanations are compiled w.r.t. the user-model. (These explanations are optional informations which have been added by
5.134 + a course designer, depending on the special course: typical examples, illustrations etc).
5.135 +
5.136 + \item The user may request detailed technical information to the problem (in general useful only for authors).
5.137 +
5.138 + \item Eventually the navigation tool for the hierarchy is updated (nodes can be expanded and collapsed when needed)
5.139 +
5.140 +\end{enumerate}
5.141 +
5.142 +%WN.17.4.03: bitte den folgenden UC auf die entsprechenden Punkte im obigen UC beziehen !
5.143 +{\bf\UC creating the informations to gain an overview of the
5.144 +\emph{mathematics knowledge base} (System-Level UC)\\}
5.145 +The User can gain an overview of the mathematics knowledge base
5.146 +through browsing HTML-Pages as described in \ref{userbrowse}. This HTML-Pages are
5.147 +automatically generated to reflect the content of the knowledge base
5.148 +(with help of the description). It is assumed, that the
5.149 +description-database is synchronized with the
5.150 +knowledge-base. Communications between knowledge base and
5.151 +description-database are not subject of this UC. This UC also does
5.152 +not handle User authentication because this is subject of the
5.153 +dinopolis layer - we assume, that the user has the right to do what is
5.154 +described below.
5.155 +%WN.17.4.03....da steht Einiges, das fuer diesen USEcase (fuer den Benutzer in dieser Situation) nicht interessant ist --- gehoert ins ADD !!!
5.156 +
5.157 +\begin{figure} [htb]
5.158 +\centerline{\psfig{figure=fig/schichten_2.eps,height=7cm}}
5.159 +\caption{browse through static informations}
5.160 +\label{staticbrowse}
5.161 +\end{figure}
5.162 +
5.163 + \begin{enumerate}
5.164 +
5.165 + \item the browser will create a navigation-tree of all
5.166 + problems. The structure of the tree has to be provided by the
5.167 + description-database and is encoded in HTML (or java-scipt...) by
5.168 + the Browser.
5.169 +
5.170 + \item The survey is started by entering the URL of the base-page
5.171 + of the description. This URL contains the node of the information
5.172 + to be shown\footnote{there are several methods to pass the
5.173 + information from browser to server. The destination Page could be
5.174 + an CGI and the parameters could be eincoded with the usual ``?
5.175 + .. \&'', or the parameters could be encoded within the path,
5.176 + decoded by the webserver (f.i. apache) and the servlet-engine and
5.177 + passt to a servlet and so on. There is no need to specify the
5.178 + final method yet} and is passed to the Browsers (\cnumber{2}).
5.179 +
5.180 + \item The browser contacts the
5.181 + description\footnote{access is controlled by the
5.182 + \emph{browser-dialog}} and asks for the respective
5.183 + problem. The problem is held within an object which controls
5.184 + the communication between browser and description-database. It
5.185 + takes care to contain the latest informtions by
5.186 + itself.\footnote{more detailed descriptions of this object and
5.187 + the browsers layers are located inside the ADD}
5.188 +
5.189 +% \item The browser contacts the representation-storage and asks for
5.190 +% a representation of the information of the respective
5.191 +% problem. This access is similar to the access from the description
5.192 +% editor.
5.193 +
5.194 + \item The Browser accesses the representation through its
5.195 + get-methods and builds a HTML-Page\footnote{utilizing the
5.196 + \emph{encoder} - more details in the ADD} with following
5.197 + informations:
5.198 +
5.199 + \begin{itemize}
5.200 + \item the navigation tool showing the hierarchy of problems
5.201 + \item mathematical details which have been extracted from the SML knowledge base by the browser generator.
5.202 + \begin{itemize}
5.203 + \item name of the problem
5.204 + \item
5.205 + \emph{items} (preconditions, input items...).
5.206 + \end{itemize}
5.207 + \item explanations, typical examples, etc added by the course designer via description-editor.
5.208 + \end{itemize}
5.209 +
5.210 + This HTML-Page is delivered to the calling Web-Browser and can be
5.211 + stored for the next access to avoid unneccesary load. If the page
5.212 + is cached, a mechanism has to be implemented to erase the cache
5.213 + when the informtions inside the description-database change.
5.214 +
5.215 + \item when the user clickes on another problem in the navigation tool, the position
5.216 + in the problem hierachy is changed to the selected problem,
5.217 + the related items are presented like in the previous
5.218 + step. Links to these problems are realized by encoding the
5.219 + destination-node within the URL. %as on the first access described
5.220 + in this UC.
5.221 +
5.222 + \end{enumerate}
5.223 +
5.224 + \textit{further navigational help:} If the user has changed the page
5.225 + with the contents of a problem, the survey on the hierarchy might not
5.226 + be up to date. Thus there is button 'where am I~?' showing the
5.227 + position of the current page within the hierarchy.
5.228 +
5.229 +{\bf\UC Browse the example collection\label{UC:expl-coll}\\}
5.230 +TODO
5.231 +
5.232 +
5.233 +
5.234 +\subsection{Access other components of \sisac}
5.235 +\sisac s knowledge base is used to solve examples of applied mathematics --- used by both, the mathematics-engine (interpreting the SML-representation of the knowledge) and the user (going from an example on the worksheet to the knowledge and back). Several such usecases are in \ref{sub-pbl}, others are as follows.
5.236 +
5.237 +{\bf\UC Exercise an example for a problem\label{UC:pbl-expl}\\}
5.238 +%WN.17.4.03 begin:
5.239 +While browsing the hierarchy of problems the student may find one, which seems interesting but unclear. In order to get some idea 'what about', the student wants to solve an example according to this problem. She is lucky, because there is a 'typical examples' in the list of explanations on the browser just below the 'given'\dots'find' of the problem.
5.240 +%WN.17.4.03 end
5.241 +%WN.17.4.03 A Student may want to exercise for a particular problem, thus he can search for a few exercises and practice them. To find them, the user can browse through the problem-tree like described in \ref{userbrowse} and pick a linked exercise.
5.242 +
5.243 +\begin{enumerate}
5.244 +
5.245 +%WN.17.4.03 \item Browse through the problem-tree and pick the wanted problem as described in \ref{userbrowse}.
5.246 +
5.247 + \item Select one of the assigned examples to swich to the
5.248 + example-collection (see UC.\ref{UC:expl-coll}). %WN5.11.02: und kommt er mit <back> am browser wieder zum problem zur''uck ??
5.249 +%WN.17.4.03 The example-collection is organized -- like the problem-tree -- a hierachical structure. One single example is a unit to be calculated and solved separated from others. In general, they are prepared by an author in an example collection. Within such a collection the example has a unique label.%\footnote{see \cite{isac:appendices} for a full description}.
5.250 +
5.251 + \item If the student decides to solve the example, he he hits the
5.252 + (unique) identifier of the example to call the worksheet. %out of the browser.
5.253 +
5.254 + \item The worksheet is provided with the hidden informations about
5.255 + the example and can initialize a new calculation upon
5.256 + them.(see also UC \emph{Start a calculation, \ref{start_calc}})
5.257 +
5.258 +%WN.17.4.03\item The rest of the process of solving the example happens inside the worksheet and is described in an seperate UC. \frage{UC von alan ?}
5.259 +
5.260 +\end{enumerate}
5.261 +
5.262 +
5.263 +{\bf\UC Refine a problem automatically\label{UC:}\\}
5.264 +Let the situation be as in \ref{sub-pbl} on p.\pageref{sub-pbl} and assume additionally, that the user has got lost while browsing the huge hierarchy of problems: The equation contains roots -- is it a 'root-equation'~? It also contains fractions -- is it a 'rational-equation' \dots~? Finally the student decides to let \sisac{} show the type of equation (i.e. the problem) matching the equation at hand.
5.265 +
5.266 +\begin{enumerate}
5.267 +\item The current formula on the worksheet is {\it L = solve\_univariate\_equation} or somewhere in the model (if displayed on the worksheet); the student requests 'refine' (by input of the tactic, or by pushing a botton on the worksheet).
5.268 +\item The data of the model are transferred to the math-engine which searches the (SML-representation of the) problem hierarchy, resulting in a path from the starting-point of the search in the hierarchy down to the matching problem, and the instantation of the matching problem with the model.
5.269 +\item A browser-window for problems comes up.
5.270 +\item The selection-tool on this window high-lights the path from the starting-point to the matching problem.
5.271 +\item And the browser-window shows the problem instantiated with the model.
5.272 +\item On the worksheet the user ackownledges the selection of this problem by putting the tactic 'specify-problem'.
5.273 +\end{enumerate}
5.274 +
5.275 +
5.276 +
5.277 +
5.278 +\section{Do math on the worksheet}
5.279 +
5.280 +
5.281 +
5.282 +% section geht in UC 1.0.4/1.0.5 auf
5.283 +
5.284 +% neu: UC model an example, UC 3.3.1 uebernehmen
5.285 +
5.286 +\subsection{The student starts a calculation}\label{start-calc}
5.287 +
5.288 +--------------below---17.4.03.copy from 5.1.---merge with 5.3.1-----------------------
5.289 +
5.290 +{\bf\UC System view: calculate an existing example \label{start_calc}} This
5.291 +UseCase describes the internal steps when a learner decides to
5.292 +calculate an example. We assume, that the user is already logged in
5.293 +and found the example to do.
5.294 +
5.295 +\begin{enumerate}
5.296 + \item The learner browses to the example to do and selects ``start
5.297 + calculation''. (I.e. the learner has the example collection (graphical layout~!) on the screen, and pushes the label of the example.)
5.298 +
5.299 + \item Starting a calculation is done through accessing a page which
5.300 + embeds an applet or performs a java-webstart (jnlp - file) \cnumber{1}
5.301 +
5.302 + \item This access is intercepted by the Browser to prepare the
5.303 + system for the calculation. \cnumber{1}
5.304 +
5.305 + \item The Browser calls the Browser-Dialog to load the example
5.306 + description and example formalization. \cnumber{2}$\,$\cnumber{3}
5.307 +
5.308 + \item With the formalization %WN+...
5.309 +and the metadata indicating how to handle the exmple (details etc.), %endWN
5.310 +a new worksheet-dialog is created to control the calculation \cnumber{4}.
5.311 +
5.312 + \item %WN.30.12.02 NEU !!!
5.313 + The worksheet-dialog sends the request (4a) to the math-engine which returns the beginning of the calculation. (The beginning of the calculation depends on the kind of metadata from \cnumber{3} which in turn leads to (4a) either 'initiate proof' or 'initiate proof' plus 'finish modeling' or \dots.)
5.314 +
5.315 + \item The initialization of the example is recorded in the dialog-state.
5.316 +
5.317 + \item The example-description, the GID
5.318 +\footnote{Dinopolis global unique identifyer}
5.319 + of the worksheet-dialog %WN+...
5.320 +and the beginning of the calculation %endWN
5.321 +are returned to the browser \cnumber{5}
5.322 +
5.323 + \item Finally, the beginning of the calculation %page ???WN which starts the worksheet
5.324 +is created and returned by the browser \cnumber{6}. This page (HTML with applet or jnlp-file) containes as parameter the GID of the worksheet-dialog and a session-id (GID of the worksheet-dialog)
5.325 +\kommentar{r\"ucksprache mit klaus wie das am sinnvollsten gemacht werden kann}
5.326 + to perform a login to the system without bothering the user to perform a password-request.
5.327 +
5.328 + \item This file forces the WEB-Browser to start the worksheet
5.329 + \cnumber{7}.
5.330 +\end{enumerate}
5.331 +
5.332 +{\bf\UC System view: start a new calculation \label{UC:new_calc}} unknown to the system. A new calculation can be started on the entry-page (UC \ref{UC:visitor}) or by a button on the example browser. The latter case is the same as UC \ref{start_calc} with the only difference that \cnumber{3} is skipped and (4a) requests an 'initiate proof' with empty formalization.
5.333 +%WN.30.12.02 das Folgende ist ein Test des bisherigen Konzeptes; diese wird sich ev. \"andern wenn wir die Module und ihre Schnittstellen (laut Anregung von Klaus) auf abstraktere Weise festlegen
5.334 +\begin{enumerate}
5.335 +\item The user (already logged in) requests 'new calculation' on the entry-page.
5.336 +\item The entry-page, by use of the respective GID associated with the user, contacts the dialog which starts a worksheet-dialog \cnumber{4} with an empty formalization.
5.337 +\item analoguous to UC\ref{start_calc} the worksheet-dialog sends the request (4a) to the math-engine which returns an empty model.
5.338 +\item The initialization of the example is recorded in the dialog-state.
5.339 +\item The GID of the worksheet-dialog and the empty model are returned to the dialog
5.340 +\item The dialog starts (with arguments: the GID of the worksheet-dialog and the empty model) the worksheet.
5.341 +%WN:Andreas, bitte um R\"uckmeldung, inwieweit das so gehen kann !!!
5.342 +\end{enumerate}
5.343 +
5.344 +---------------above---17.4.03.copy from 5.1.---merge with 5.3.1-----------------------
5.345 +
5.346 +{\bf\UC Initialize calculation}
5.347 +
5.348 +Initialize the Worksheet with a starting point (formalization of the
5.349 +problem) for the calculation. choosing from a list of prepared
5.350 +examples or by entering a formula and choosing problem-type and domain
5.351 +from a hierarchy-browser.
5.352 +
5.353 +Result: Complete state of calculation as required by the math-engine
5.354 +(formula,domain, problem-type)
5.355 +
5.356 +Required: List of pre-defined examples or editor for the state of
5.357 +calculation
5.358 +
5.359 +
5.360 +{\bf\UC Connect to the math-engine}
5.361 +
5.362 +Prompt the user for a connection or read the connection from configuration files.
5.363 +Information on available connections could also be stored with a list of examples.
5.364 +
5.365 +Result: Connection to the math-engine
5.366 +
5.367 +Required: Path to the math-engine
5.368 +
5.369 +{\bf\UC Create and display worksheet window}
5.370 +
5.371 +Result: Worksheet-window on-screen, initialized with first step of calculation
5.372 +
5.373 +
5.374 +\subsection{The student does a step in a calculation}
5.375 +
5.376 +Let us assume, the example has been propagated until the following expression (the \emph{current formula}) is on the worksheet (see x.x on page \pageref{UC-step})
5.377 +\[
5.378 +\frac{d}{dx}\left( 4u\sqrt{r^{2}-\left( \frac{v}{2}\right) ^{2}}-4(r^{2}-\left( \frac{v}{2}\right) ^{2}\right) = \]
5.379 +Now, what are the choices for the users (i.e. the students)~?
5.380 +
5.381 +Any of the following actions may be taken at any time during the calculation. The numbering does not imply the order in which the actions are taken.
5.382 +
5.383 +{\bf\UC Choose the formula to continue the calculation with}
5.384 +
5.385 +By default, the calcualtion continues from the last computed formula. If another formula is
5.386 +chosen by clicking on a formula in the worksheet or a new formula is entered, parts of the calculation tree may become
5.387 +invalid and the display has to be updated to notify the user of the effects his action will have on the state of the proof. The user can choose whether to accept
5.388 +the changes.
5.389 +
5.390 +Result: Formula to continue the calculation with, highlighted in the display.
5.391 +
5.392 +Required: State of calculation displayed in a worksheet, containing at least one formula.
5.393 +
5.394 +
5.395 +{\bf\UC Choose the tactic to be applied in the next step of calculation}
5.396 +
5.397 +Possible sources of tactics:
5.398 +
5.399 +Tactics proposed by the system. Optionally, the user can choose whether to accept a proposed tactic.
5.400 +
5.401 +\begin{enumerate}
5.402 +\item Pre-defined examples
5.403 +
5.404 +With pre-defined examples, a standard solution containing the tactics to be applied and their respective order can be stored. The user watches the progress of a calculation defined by the author of the example.
5.405 +
5.406 +\item Tactic chosen by the math-engine
5.407 +
5.408 +Given a problem(type), the math-engine can generate a tactic from the current state of calculation. The user watches a calculation as proposed by the knowledge stored in the system.
5.409 +
5.410 +Optionally, with spaces to be filled in.
5.411 +
5.412 +\end{enumerate}
5.413 +
5.414 +The user can enter a tactic manually, with various levels of support from the system:
5.415 +
5.416 +\begin{enumerate}
5.417 +\setcounter{enumii}{2}
5.418 +
5.419 +\item Tactic chosen from a list of tactics applicable to the curent formula
5.420 +
5.421 +On demand, the math-engine generates a list of tactics applicable to the current state of calculation. The user can choose from the list and pick alternatives according to his own style of solving problems.
5.422 +
5.423 +\item Tactic entered by the user or chosen from a list of all tactics known to the system
5.424 +
5.425 +The user can enter the tactic directly as plain text or by browsing a list of all tactics known to the system. The system gives feedback whether the tactic is applicable to the current situation. The tactic is completely up to the user and his own knowledge.
5.426 +
5.427 +\end{enumerate}
5.428 +
5.429 +Result: Tactic to be applied in the next step of calculation
5.430 +
5.431 +Required: State of calculation
5.432 +
5.433 +{\bf\UC Enter/edit a formula}
5.434 +This proposes the entered formula as a valid derivation of the formula preceding it in the prooftree - an assumption the system will have to verify.
5.435 +If the formula is accepted, an updated state of calculation joining the entered formula to the previous steps is displayed in the worksheet.
5.436 +
5.437 +Optionally, with spaces to be filled in.
5.438 +
5.439 +Result: Indication whether the formula can be accepted as a valid part of calculation. Worksheet display updated.
5.440 +
5.441 +Required: State of calculation and new formula
5.442 +
5.443 +{\bf\UC Optionally adjust the amount of calculation and information wanted}
5.444 + %WN.17.4.03: ?? 'granularity' ?? of calculation
5.445 +Choose the number of steps to be computed and whether to display tactics, conditions,
5.446 +etc.
5.447 +
5.448 +Result: No visible results. The changes will take effect the next time a step in the calculation is started.
5.449 +
5.450 +{\bf\UC Start calculation}
5.451 +
5.452 +Contact the math-engine, display the results. The amount of calculation (number of steps to be taken) is controlled by the options set by action 4.
5.453 +
5.454 +Result: New state of calculation (new formula, applied tactics, new conditions)
5.455 +displayed in the worksheet
5.456 +
5.457 +Required: State as required by the math-engine (formula, problem-type, domain,
5.458 +tactic)
5.459 +
5.460 +
5.461 +\subsection{Subproblem with maximal user-guidance}\label{sub-pbl}
5.462 +
5.463 +%WN{\bf\UC Find the fitting Problem for a given formula\\}
5.464 +Let us assume, the student has finished the {\it model-phase} of a subproblem in the reference example and has the following {\it model} on the screen:
5.465 +{\it
5.466 +\begin{tabbing}
5.467 +123\=123\=123\=given: \=123\=123\=\kill
5.468 +\>x.\>L = solve\_univariate\_equation\\
5.469 +\> \> \>given: \>equality $-\frac{v}{\sqrt{r^2-\left(\frac{v}{2}\right)^2}}
5.470 + +2\sqrt{r^2-\left(\frac{v}{2}\right)^2}-2v=0$,\\
5.471 +\> \> \> \>boundVariable $v$, errorBound $\epsilon=0.001$\\
5.472 +\> \> \>find: \>solutions $L$
5.473 +\end{tabbing}
5.474 +}
5.475 +Now the student has to solve the equation. We further assume, \sisac's knowledgebase contains a {\it method} for solving this particular equation; then it can be found either directly in the list of methods. If the student cannot find it directly, then the {\it problem hierarchy} assists in the search for an appropriate method by {\it refin}ing: the problem {\it [univariate,equation]} will {\it match} the model, apparently; and the problem hierarchy is structured such that the tactic {\it Refine\_Problem [univariate,equation]} will find the appropriate problem (in this case: type of equation) in a search on the children of {\it [univariate,equation]} automatically --- let us assume, the appropriate one is {\it [fraction,root,univariate,equation]}. Eventually the tactic {\it Refine\_Problem} may be disallowed by the dialog guide (for the reason to push students searching the problem hierarchy themselves).
5.476 +
5.477 +{\bf\UC Find the matching problem for a given model\\} The
5.478 +\emph{worksheet} interacts with the user while calculating an
5.479 +example. It might be, that \sisac{} forces the user to find the matching
5.480 +problem by himself. This usecase starts with valid \emph{worksheet-}
5.481 +and \emph{browser-dialogs}. The worksheet-dialog holds all
5.482 +informations regarding the actual calculation while the browser-dialog
5.483 +is responsible for for information representation and browsing. Both
5.484 +dialogs a connected to each other. This connection is established
5.485 +within the login phase. (see also UseCases \emph{A subscribes student
5.486 +enters \sisac} and \emph{Start a calculation} \ref{start_calc}).
5.487 +\begin{figure}
5.488 +\centerline{\resizebox*{11cm}{!}{\includegraphics{fig/select-problem-dialog.eps} } }
5.489 +
5.490 +
5.491 +\caption{Select a Problem for a ProofState}
5.492 +
5.493 +\label{selectproblem}
5.494 +\end{figure}
5.495 +
5.496 +
5.497 +\begin{enumerate}
5.498 + \item On the worksheet the user requests to call the problem browser (without addressing a certain problem) by \dots ???TODO!!!\\
5.499 +Alternative: The user addresses a certain problem (to be matched with the model) by \dots ???TODO!!!.
5.500 +
5.501 + \item The worksheet calls the WEB-Browser with the URL of the
5.502 + Problem-Browser and the GID of the browser dialog to use
5.503 + \cnumber{1}, \cnumber{2}.
5.504 +
5.505 + \item The browser calls the \emph{browser-dialog} to get informations
5.506 + about the active Problem-Description \cnumber{4} (i.e. root of the
5.507 + Problemtree). The Problem is also passed to the
5.508 + \emph{worksheet-dialog} to check if the selected problem matches the
5.509 + model \cnumber{5}.
5.510 +
5.511 + \item The \emph{worksheet-dialog} performs the match with help of the
5.512 + \emph{mathematic-engine}. The result of the match-operation answers
5.513 + how far the problem matches the model
5.514 + \begin{itemize}
5.515 + \item are all preconditions met
5.516 + \item are all neccesary informations \emph{given} present
5.517 + \item does the model-formular match the problem-pattern
5.518 + \end{itemize}
5.519 + this informations are passed back to the browser-dialog \cnumber{6}.
5.520 +
5.521 + \item The Dialog returns the gathered informations to the
5.522 + \emph{Browser} \cnumber{7} which has to create a HTML-Page which
5.523 + presents the informations out of the \emph{description-storage} analogous
5.524 + to UC\ref{userbrowse} and the result of the matching:
5.525 +% \end{enumerate}
5.526 + \begin{itemize}
5.527 + \item Matches the \emph{Problem} to the \emph{Proofstate} ?
5.528 + \begin{itemize}
5.529 + \item Are all informations present and correct?
5.530 + \item Are the preconditions fulfilled ?
5.531 + \item Is the formular of the correct form ?
5.532 + \end{itemize}
5.533 + \end{itemize}
5.534 +
5.535 + The Browser has to mark this informations in an clear way to ease
5.536 + their interpretation. For example: if the formular does not match
5.537 + the problem (there is no integral-formular in an integral-problem),
5.538 + the problem simply does not match. On the other hand, it might be,
5.539 + that the selected problem matches the problem, but a information is
5.540 + missing (the variable to integrate is not given). This details have
5.541 + to be returned to the Browser-Window \cnumber{7} to let the learner
5.542 + judge if he wants to take the selected problem.
5.543 +
5.544 + \item The user can browse through the problems using the hierachy or
5.545 + select the actual problem.
5.546 +
5.547 +%\begin{enumerate}
5.548 + \item If the learner decides to select a problem, he can hit the
5.549 + ``select-item'' button. If the browser receives this call, the
5.550 + ``pushes'' the problem to the worksheet-dialog. \cnumber{8} which
5.551 + can call its \emph{worksheet} \cnumber{9} to rebuild its presentation of
5.552 + the calculation.
5.553 +
5.554 +%\footnote{ This signal is realized through a listener
5.555 +% structure --- so, more than one \emph{WorkSheet} can listen to
5.556 +% changes within a calculation }.
5.557 +
5.558 +\end{enumerate}
5.559 +
5.560 +\section{Authoring}\label{use:authoring}
5.561 +\subsection{Author the knowledge base}
5.562 +
5.563 +{\bf\UC Build the structure of the knowledge base description\\}
5.564 +All informations about the structure of the knowledge base are stored
5.565 +inside the SML-part of the system. This structure has to be known by
5.566 +the Broswers to enable the user to browse the systen. To reduce the
5.567 +load of the math-engine and to enhance the informations available for a
5.568 +problem, the informations of the mathengine are copied to the
5.569 +description-database. Here, the problem-descriptions can be enriched
5.570 +with additional informations using the \emph{description editor}. The
5.571 +structure for the browsers is created through querying the
5.572 +Browsergenerators. This UC concernes about creating the structure
5.573 +inside the description-database and add additional informations.
5.574 +
5.575 +\begin{figure} [htb]
5.576 +\centerline{\psfig{figure=fig/schichten_1.eps,height=7cm}} %gen_structure.eps,width=11cm}}
5.577 +\caption{Structure generation}
5.578 +\label{genstructure}
5.579 +\end{figure}
5.580 +
5.581 + \begin{description}
5.582 +
5.583 + \item [\cnumber{1}] The structure-transfer is started by the
5.584 + description-administrator\footnote{Access has to be controlled by
5.585 + the description-editor which is responsible for the
5.586 + user-authentication - only identifyed users may access}.
5.587 + \kommentar{authenticationmodule einfuehren - wo werden die
5.588 + userinfos gespeichert, kann man auch rechte auf einzelne knoten
5.589 + geben, wie werde diese rechte gespeichert...}
5.590 + \begin{itemize}
5.591 + \item The user starts the description-editor
5.592 +
5.593 + \item The description-editor starts the
5.594 + authentication-process which authentificates the user and
5.595 + results in an permission object which identifies the
5.596 + user\footnote{The authentication process utilizes the
5.597 + Dinopolis framework - a detailed description can not be
5.598 + given yet}.
5.599 +
5.600 + \item The \emph{description-editor} Calls the
5.601 + \emph{description-storage} to initiate the structure
5.602 + transfer.
5.603 +
5.604 + \item The \emph{description-storage} starts the transfer if
5.605 + the permissions suffice.
5.606 +
5.607 + \end{itemize}
5.608 +
5.609 + \item [\cnumber{2}] \emph{browser-generators} are queried for the
5.610 + structure of the knowledge base. A XML Description of each node
5.611 + is created and stored within the XML-Description database.
5.612 + \begin{itemize}
5.613 +
5.614 + \item the \emph{browser-generator} is asked by the
5.615 + \emph{description-storage} for the root-node of the problem
5.616 + hierachy\footnote{This query is transferred through the
5.617 + wrapper which translates java-objects into a character stream
5.618 + which is used to communicate with the Math-Engine and vice
5.619 + versa - the syntax of the communication with the wrapper has
5.620 + to be defined within the ADD}.
5.621 +
5.622 + \item Afterwards, the \emph {browser-generator} is asked for
5.623 + the mathematical informations of this problem. Mathematical
5.624 + informations contain:
5.625 + \begin{itemize}
5.626 + \item subproblems
5.627 + \item items of the problem
5.628 + %WN//\item preconditions ... siehe Terms.tex
5.629 + %WN//\item postconditions
5.630 + \end{itemize}
5.631 +
5.632 + \item A XML - Description is built for this informations. All
5.633 + informations are stored in dedicated fields which identify
5.634 + their type. Subproblems are stored as list of references to
5.635 + their XML-Description which are built resursively in the same
5.636 + way. A reference to the parent problem has to be added too.
5.637 +
5.638 + \item The XML-Descriptions are put into the storage. A
5.639 + reference to the root problem is set.
5.640 +
5.641 + \end{itemize}
5.642 +
5.643 + \item [\cnumber{3}] After creating the structure, the
5.644 + \emph{description editor} can browse through the XML-Files and
5.645 + add additional information.
5.646 + \begin{itemize}
5.647 +
5.648 + \item The description editor asks the description-storage
5.649 + about the root problem
5.650 +
5.651 + \item The description-storage returns a so called
5.652 + \emph{description-object}, which containes all necessary
5.653 + informations, to the editor. \footnote{see ADD and SDD for
5.654 + more details}
5.655 +
5.656 + \item The description containes fields which might be changed
5.657 + by the description editor through set-methods. Again, access
5.658 + to this methods is only given after checking the
5.659 + permission-object. A change of mathematical informations out
5.660 + of the math-engine is not allowed. Only additional
5.661 + informations like text, images and references to further
5.662 + informations (URLs, examples) are allowed. Changes have to be
5.663 + propagated to the description-storage and other users of the
5.664 + same informations (e.g. another description-editor or a
5.665 + browser).
5.666 +
5.667 + \item As the representation containes information about the
5.668 + subproblems, the editor also can navigate through the hierachy
5.669 + to edit other than the root-problem by loading their
5.670 + representation.
5.671 +
5.672 + \end{itemize}
5.673 +
5.674 + \end{description}
5.675 +
5.676 +\subsection{Author the example collection}
5.677 +{\bf\UC An author adds some examples\\}
5.678 +Let us assume that some of the examples from a traditional mathematics textbook
5.679 +have been implemented in an \sisac{} example collection. Now an author wants
5.680 +to add some more examples from another section. Then he has to accomplish the
5.681 +following tasks.
5.682 +\begin{enumerate}
5.683 +\item {\bf He opens the example browser} and zooms into the table of contents in order to locate the position where to insert the new section.
5.684 +\item {\bf He inserts the new section} by first selecting the section preceeding the new one. Then he selects the level of the new section (which may be the same as the preceeding one, or one level deeper) and inputs the headline of the new section. \kommentar{AG: vielleicht sollten wir das eigentliche example und den ``verzeichnisbaum'' (level/headline) voneinander trennen, damit man ein examle in verschiedenen beispielsammlungen verwenden kann}.\\
5.685 +Alternatives:
5.686 +
5.687 + \begin{enumerate}
5.688 + \item {\bf The required headers are all present} already, and the author starts immediately with (3) editing an example. In this case the location of the examples label and text (or figures) is determined immediately.
5.689 + \item {\bf The new section is several levels deeper} in the hierarchy than the last preceeding section already input. In this case at least a label (and eventually a headline) for each level down to the level of the new section is input one after the other.
5.690 + \end{enumerate}
5.691 +
5.692 +\item {\bf He edits the first example} by declaring its label according to the textbook. Then he edits the examples text, the formulas inserted in the text, and eventually a figure --- copying the layout presented in the textbook.
5.693 +\item {\bf He adds the 'hot spot' for calculation} of the example; now the description of the example as visible to the student is finished.
5.694 +\item {\bf He adds the formalization} of the example together with its specification necessary for automatically solving the example (which is the prerequisite for user guidance in tutoring).
5.695 +\end{enumerate}
5.696 +
5.697 +
5.698 +{\bf\UC An author checks the example(s)}%WN FIXXXME5.11. vom vorigen abgetrennt -- ``uberarbeiten !!!
5.699 +\begin{enumerate}
5.700 +\item {\bf He checks the executability} of the examle by activating the 'hot spot' and thus calling the math engine, which first checks the syntax of the formalization, and then starts the calculation in a worksheet which pops up. (The calculagion usually will be done in an automated way chosen by the author.)
5.701 +\item {\bf He adds another example} after the first one has been finished by editing the examples label analogously to (3).
5.702 +\item {\bf The final check over all examples} newly input so far makes the author sure that the examples are ready to use for tutoring. The sequence of examples is determined by marking the first and the last one, and then it will take some time until all these examples have been calculated automatically. This 'batch mode' of calculation creates some protocol the author can inspect for the results: a list of the examples computed correctly, those not finished correctly, and those not terminating.\\
5.703 +Alternatives:
5.704 + \begin{enumerate}
5.705 + \item {\bf The calculation of an example does not succeed,} which can be seen on the worksheet presenting the calculation. In this case the example author needs expertise for authoring math knowledge (given by himself or by some other person) and requires to start the authoring tools for the math knowledge base.
5.706 + \end{enumerate}
5.707 +\end{enumerate}
5.708 +
5.709 +After adaption of the math knowledge base the respective formalization or even
5.710 +the text and figure of the example may be up to change. I.e. editing all elements of an example (including deletion) must be possible.
5.711 +
5.712 +
5.713 +\section{The example for reference}\label{use-expl}
5.714 +\sisac{} features a new kind of calculations in applied mathematics, and it is an issue to make the novel functionality of this software as clear as possible. In order to meet this issue, an example is given to be referenced by the use-cases within this document. The example is taken from a calculus course at highschools; thus it should not pose problems ot understand the underlying mathematics. Nevertheless the example covers all major features offered by \sisac.
5.715 +
5.716 +\subsection{Description, formalization and modeling phase}
5.717 +The {\bf description} of an {\bf example}\footnote{These terms are defined in appendix \ref{app.terms} of \cite{isac:appendices} 'List of Terms used in the \sisac-project'} may consist of text, formulas and figures:
5.718 +\begin{center}\begin{minipage}{4.2in}\it
5.719 +Given a circle with radius $r=7$, inscribe a rectangle with
5.720 +length~u and width~v. Determine u and v such that the rectangles area~A is a maximum.
5.721 +\end{minipage}\end{center}
5.722 +\begin{figure} [htb]
5.723 +\centerline{\psfig{figure=fig/coil-kernel-uv.eps,width=5.0cm}}
5.724 +\caption{Figure for the maximum example}
5.725 +\label{fig.coil-kernel-uv}
5.726 +\end{figure}
5.727 +The inital step in solving such an example is, to construct a {\bf model} from the description. The respective model looks like this, if all items are input:\label{model}
5.728 +\begin{tabbing}
5.729 +1234,\=relate \=: \= \=\kill
5.730 +%\>Problem [maximum, calculus, optimization] \\
5.731 +\>given\>: $[$ Constants $\;$ \framebox{$r=7$} $]$\\
5.732 +\>where \>: $\,0\leq 7$ \\
5.733 +\>find X \>: $[$ Maximum $\;$\framebox{$A$},\\
5.734 +\> \>\>AdditionalValues $\;$\framebox{$[u,v]$} $]$\\
5.735 +\>with \>:{\tiny $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$} \\
5.736 +\>\>\>{\tiny $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land
5.737 +(\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2 $\\
5.738 +\`$\Longrightarrow A^\prime \leq A$} \\
5.739 +\>relate\>: $[$ \framebox{$A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2$} $]$
5.740 +\end{tabbing}
5.741 +The boxes mark the items meant for input by the user, whereas the surrounding information is provided by the system and serves user guidance. If the model is perfect, \sisac{} can solve the example autonomously.
5.742 +
5.743 +In order to provide userguidance already in the model phase, each example is accompanied by a {\bf formalization} prepared by an author and normally hidden from the user:
5.744 +{\it
5.745 +\begin{tabbing}
5.746 +1234,\=$F_{III}$\=$\equiv\;\;(\;$\=\kill
5.747 +\>$F_I$\>$\equiv\;\;(\;$\>$\{r=7\},\;\; \{ A,[u,v]\},\;\;$\\
5.748 +\>\>\>$\{0\leq\frac{u}{2}\leq r,\;\;
5.749 + \{A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\}\;)$\\
5.750 +\\
5.751 +\>$F_{II}$\>$\equiv\;\;(\;\{r=7\},\;\; \{ A,[u,v]\},\;\;$\\
5.752 +\>\>\>$\{0\leq\frac{v}{2}\leq r,\;\;
5.753 + \{A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\}\;)$\\
5.754 +\\
5.755 +\>$F_{III}$
5.756 +\>$\equiv\;\;(\;\{r=7\},\;\; \{ A,[u,v]\},\;\;$\\
5.757 +\>\>\>$\{0\leq\alpha\leq\frac{\pi}{2},\;
5.758 + \{A=2uv-u^2,\frac{u}{2}=r\sin\alpha,\frac{v}{2}=r\cos\alpha\})$
5.759 +\end{tabbing}}
5.760 +In this case the formalization comprises three variants, $F_I, F_{II}, F_{III}$, which presumerably cover all possibilities students would consider in a particular course.
5.761 +
5.762 +Given such a formalization and a specification (see below) , \sisac{} can solve an example autonomously {\em and} in stepwise interaction down to the result.
5.763 +\\
5.764 +
5.765 +If \sisac{} is being used to solve an example unknown to the system (i.e. without a hidden specification and formalization prepared by an author) \sisac{} cannot provide user guidance at the beginning of this phase (see UC.\ref{UC:new_calc}). In particular, the items {\it Constants}, {\it Maximum} and {\it AdditionalValues} have to be found in the theory {\it Descript.thy}.
5.766 +
5.767 +
5.768 +
5.769 +\subsection{Knowledgebase and specification phase}
5.770 +The knowledge base comprises three parts, theories, problems and methods.
5.771 +
5.772 +\paragraph{Theories} contain the knowledge deduced from axioms and definitions by formal proof (done by the interactive theorem prover Isabelle). For the example at hand knowledge is prepared like the following:
5.773 +\begin{verbatim}
5.774 +
5.775 + theory 'calculus'
5.776 +
5.777 + consts
5.778 + d_d :: "[real, real]=> real"
5.779 +
5.780 + rules
5.781 + diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
5.782 + diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
5.783 + diff_quot "Not (v = 0) ==> (d_d bdv (u / v) =
5.784 + (d_d bdv u * v - u * d_d bdv v) / v ^ 2)"
5.785 + ...
5.786 +\end{verbatim}
5.787 +
5.788 +\paragraph{Problems} capture the aspect of application of knowledge.
5.789 +{\it\begin{tabbing}
5.790 +123\=4512345\=\=4512345\kill
5.791 +\>\> $|$\\
5.792 +\>\> \nod e\=quation \\
5.793 +\>\> $|$\>\nod u\=nivariate\\
5.794 +\>\> $|$\>$|$ \>\nod linear \\
5.795 +\>\> $|$\>$|$ \>\nod p\=olynomial \\
5.796 +\>\> $|$\>$|$ \>\nod rational\\
5.797 +\>\> $|$\>$|$ \>\nod \dots\\
5.798 +\>\> \nod function \\
5.799 +\>\> $|$\>\nod make \\
5.800 +\>\> $|$\> \>\nod by\_elimination \\
5.801 +\>\> $|$\> \>\nod by\_new\_variable \\
5.802 +\>\> $|$\>\nod differentiate \\
5.803 +\>\> $|$\>$|$ \>\nod for\_maximum \\
5.804 +\>\> $|$\>$|$ \>$|$ \>\nod on\_interval\\
5.805 +\>\> $|$\>$|$ \>\nod \dots \\
5.806 +\>\> $|$\>\nod integrate \\
5.807 +\>\> $|$\> \>\nod \dots \\
5.808 +\>\> \nod optimization \\
5.809 +\>\> $|$\>\nod linear \\
5.810 +\>\> $|$\>$|$ \>\nod \dots \\
5.811 +\>\> $|$\>\nod calculus \\
5.812 +\end{tabbing}}
5.813 +The example at hand shall be described by the {\it problem [calculus, optimization]} (note the reverse order w.r.t. the hierarchy above, which seems more usual in many cases, e.g. {\it [linear, univariate, equation]}), and will be broken down into the subproblems {\it [make, function]}, {\it [on\_interval, for\_maximum, differentiate, function]} and {\it [tool, find\_values]}. The root-problem of the example looks like
5.814 +{\it
5.815 +\begin{tabbing}
5.816 +1234,\=relate \=: $\equiv$\= ${\it let}\:$ \=$\exists m\_$\kill
5.817 +\>Solve\_problem [maximum, calculus, optimization] \\
5.818 +\>given\>: $[$ Constants fix\_ $]$\\
5.819 +\>where \>: ${\it map}\;(\$\,0\leq\,\$)\; {\it fix\_}$ \\
5.820 +\>find \>: $[$ Maximum m\_\\
5.821 +\> \>\>AdditionalValues vs\_ $]$\\
5.822 +\>with \>: ${\it let}\:x_1 = \{{\it m\_}\}\cup\{{\it vs\_}\}\cup({\it Vars}\:{\it rs\_});$\\
5.823 +\>\>\>\>$x_2 = {\it map}\:{\it primed}\:x_1;$\\
5.824 +\>\>\>$\:{\it in}\;\,{\it map}\:({\it op}\land)\:{\it rs\_}\:\$\: \land\:\$$ \\
5.825 +\>\>\>\>$\forall\,\$\,x_2\,\$.\,(\,\lambda\,\$\,x_1\,\$\,.\,\$\,{\it map}\,({\it op}\land)\,{\it rs\_}\,\$\,)\,\$\,x_2\,\$\, $ \\
5.826 +\>relate\>: rs\_
5.827 +\end{tabbing}}
5.828 +This problem is {\bf matched} with the formalization and yields the model shown above.
5.829 +
5.830 +\paragraph{Methods} describe the algorithms solving the problems. The method solving the example calls the subproblems mentioned:
5.831 +{\it\begin{tabbing}
5.832 +123\=123\=123\=123\=123\=123\=\kill
5.833 +\> {\tt Script} Maximum\_value (fix\_::bool list) (m\_::real) (rs\_::bool list) \\
5.834 +\>\>\>\>\> (v\_::real) (itv\_::real set) (err\_::bool) = \\
5.835 +\>\> ({\tt let}\\
5.836 +\>\>\> e\_ = (hd o (filter (Testvar m\_))) rs\_; \\
5.837 +\>\>\> t\_ = ({\tt if} \#1 $<$ Length rs\_ \\
5.838 +\>\>\>\> {\tt then} (Subproblem (Reals,[make, funtion],no\_met) [m\_, v\_, rs\_]) \\
5.839 +\>\>\>\> {\tt else} (hd rs\_)); \\
5.840 +\>\>\> mx\_ = Subproblem (Reals,[on\_interval, for\_maximum, differentiate, \\
5.841 +\>\>\>\>\> function], maximum\_on\_interval) [ t\_, v\_, itv\_ ] \\
5.842 +\>\> {\tt in} (Subproblem (Reals,[tool,find\_values],find\_values) \\
5.843 +\>\>\>\>\> [ mx\_, (Rhs t\_), v\_, m\_, (dropWhile (ident e\_), rs\_])))\\
5.844 +\end{tabbing}}
5.845 +
5.846 +An example is given a {\bf specification} ('it is specified'), if a pointer into each of the three parts of the knowledge base is fixed, i.e. a pointer to a theory, a problem and a method. For the example this is {\it (differentiate, [calculus, optimization], Maximum\_value)}.
5.847 +
5.848 +\subsection{Interaction on the worksheet and the browsers}
5.849 +Within a calculation the centre of interaction with the user is a so-called {\bf worksheet}. At certain points the user may want to view the knowledge base in a so-called {\bf browser-window} and/or select some knowledge, or the dialog presents such a window.
5.850 +
5.851 +\paragraph{In the modeling phase} the user inputs formulas on the worksheet, and on the worksheet they get most of the feedback. After a while the worksheet could look like this:
5.852 +{\it
5.853 +\begin{tabbing}
5.854 +123\=123\=123\=relate...\=123\=\kill
5.855 +\>Solve\_problem [maximum, calculus, optimization] \\
5.856 +\>\>Model\\
5.857 +\>\>\>given: \>$[$ Constants $r=7\;]$\\
5.858 +\>\>\>where: \>$\,0\leq r$\\
5.859 +\>\>\>find: \>$[$ Maximum, AdditionalValues $[u,v]\;]$\\
5.860 +\>\>\>relate:\>$[A=2uv,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\;\frac{u}{2}=r\sin{\alpha}\;]$
5.861 +\end{tabbing}}
5.862 +where {\it Solve\_problem [maximum, calculus, optimization]}, {\it Constants}, {\it Maximum}, {\it AdditionalValues}, and $0\leq r$ have been supplied by the system, and several items are marked: {\it Maximum} with 'missing', $A=2uv$ with 'incorrect', and $\frac{u}{2}=r\sin{\alpha}$ with 'superfluous'. Regarding this kind of feedback\label{model-feedback} users may successfully complete modeling; if they are not capable to do it, they just hit a 'go-on' button and \sisac{} gets the correct model from the hidden formalization and specification. For the following let us assume, that the model is completed correctly:
5.863 +{\it
5.864 +\begin{tabbing}
5.865 +123\=123\=123\=relate...\=123\=\kill
5.866 +\>Solve\_problem [maximum, calculus, optimization] \\
5.867 +\>\>Model\\
5.868 +\>\>\>given: \>$[$ Constants $r=7]$\\
5.869 +\>\>\>where: \>$\,0\leq r$\\
5.870 +\>\>\>find: \>$[$ Maximum , AdditionalValues $[u,v]\;]$\\
5.871 +\>\>\>relate:\>$[A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\frac{u}{2}=r\sin{\alpha}]$\\
5.872 +\>\>Theory: \>\>%Reals
5.873 +\\
5.874 +\>\>Problem:\>\>%[maximum, calculus, optimization]
5.875 +\\
5.876 +\>\>Method: \>\>%[make\_fun, by\_elimination]
5.877 +\end{tabbing}}
5.878 +The superfluous item $\frac{u}{2}=r\sin{\alpha}$ does not matter, below there are the {\bf specification-fields} to be determined (i.e. input by the user) within the specification phase.
5.879 +
5.880 +\paragraph{The specification phase} requires data from the knowledge base in general. In the case of the examples model above the decision is required, which kind of problem the given model can be matched with: {\it[linear, optimization]}, or {\it[calculus, optimization]}, or some other problem. The information necessary for this decision can be found in the hierarchy of problems.
5.881 +
5.882 +Learners can {\bf browse} the hierarchy of problems (theories, methods) and they can {\bf apply} the problem (theory, method); the latter transfers the problem (theory, method) to the respective field below the model on the worksheet.
5.883 +
5.884 +For instance, applying the problem {\it[linear, optimization]} would cause this display on the worksheet:
5.885 +{\it
5.886 +\begin{tabbing}
5.887 +123\=123\=123\=relate...\=123\=\kill
5.888 +\>Solve\_problem [maximum, calculus, optimization] \\
5.889 +\>\>Model\\
5.890 +\>\>\>given: \>$[$\underline{Constants $r=7$}$]$\\
5.891 +\>\>\>where: \>$\,0\leq r$\\
5.892 +\>\>\>find: \>$[$Maximum , \underline{AdditionalValues $[u,v]$}$]$\\
5.893 +\>\>\>relate:\>$[\underline{A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\frac{u}{2}=r\sin{\alpha}}]$\\
5.894 +\>\>Theory:\\
5.895 +\>\>Problem:\>\> [linear, optimization]\\
5.896 +\>\>Method:
5.897 +\end{tabbing}}
5.898 +\noindent where some items in the model would be marked with some\underline{ error-feedback}. For instance, applying a theory even might cause the feedback 'syntax-error' when the model contains function constants not defined in the theory or in one of the theories parents.
5.899 +
5.900 +Browsing problems (when started from a model on the worksheet) matches the problem selected with the model on the worksheet, i.e. on the browser-window the same feedbacks are given as for the model on the worksheet described on p.\pageref{model-feedback}.
5.901 +
5.902 +\subsection{The solving phase and subproblems}
5.903 +Before we describe \sisac s features for the solving phase, we fix one correct model and one specification (out of several possible ones) as follows:
5.904 +{\it
5.905 +\begin{tabbing}
5.906 +123\=123\=123\=relate...\=123\=\kill
5.907 +\>Solve\_problem [maximum, calculus, optimization] \\
5.908 +\>\>Model\\
5.909 +\>\>\>given: \>$[$Constants $r=7]$\\
5.910 +\>\>\>where: \>$\,0\leq r$\\
5.911 +\>\>\>find: \>$[$Maximum $A$, AdditionalValues $[u,v]]$\\
5.912 +\>\>\>relate:\>$[A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\frac{u}{2}=r\sin{\alpha}]$\\
5.913 +\>\>Theory: \>\>Reals\\
5.914 +\>\>Problem:\>\>[maximum, calculus, optimization]\\
5.915 +\>\>Method: \>\>[make\_fun, by\_elimination]
5.916 +\end{tabbing}}
5.917 +
5.918 +...
5.919 +
5.920 +%\[
5.921 +%\frac{d}{dx}\left( 4u\sqrt{r^{2}-\left( \frac{v}{2}\right) ^{2}}-4(r^{2}-\left( \frac{v}{2}\right) ^{2}\right) \]\label{UC-step}
5.922 +%$$
5.923 +%\frac{d}{dv}\left( 4v\sqrt{r^{2}-\left( \frac{v}{2}\right)^2}-4\left(r^2-\left( \frac{v}{2}\right)^2\right)\right) =
5.924 +%$$
5.925 +%$$
5.926 +%= 4\sqrt{r^2-\left( \frac{v}{2}\right)^2} - \frac{v^2}{\sqrt{r^2-\left( \frac{v}{2}\right) ^2}} + 4v\left(r^2-\left( \frac{v}{2}\right)^2\right)\\
5.927 +%$$
5.928 +
5.929 +Simplification within the maximum-example:
5.930 +$$
5.931 +\frac{d}{du}\left(2u\sqrt{r^2-\left(\frac{u}{2}\right)^2} - u^2\right) = \dots
5.932 +$$
5.933 +$$
5.934 += 2\sqrt{r^2-\left(\frac{u}{2}\right)^2} - \frac{u^2}{2\sqrt{r^2-\left(\frac{u}{2}\right)^2}} - 2u
5.935 +$$
5.936 +
5.937 +Equation within the maximum-example:
5.938 +$$
5.939 +2\sqrt{r^2-\left(\frac{u}{2}\right)^2} - \frac{u^2}{2\sqrt{r^2-\left(\frac{u}{2}\right)^2}} - 2u = 0
5.940 +$$
5.941 +
5.942 +.\\.\\.\\.\\.\\.\\.\\.\\.\\.\\.\\.\\
5.943 +
5.944 +{\it }{\it }{\it }
5.945 +
5.946 +%\sqrt{r^2-\left(\frac{u}{2}\right)^2}
5.947 +%\sqrt{r^2-\left(\frac{v}{2}\right)^2}
5.948 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc/use.tex Thu Apr 17 18:01:03 2003 +0200
6.3 @@ -0,0 +1,41 @@
6.4 +\documentclass[a4wide]{report}
6.5 +\usepackage{epsfig}
6.6 +\usepackage{latexsym}
6.7 +\bibliographystyle{alpha}
6.8 +
6.9 +\newcommand {\kommentar}[1]{\marginpar{\begin{flushright}\tiny#1\end{flushright}}}
6.10 +\newcommand {\frage}[1]{
6.11 + \marginpar{
6.12 + \begin{tabular}{p{5mm} p{2cm}}
6.13 + \begin{flushleft}
6.14 + {\large?}
6.15 + \end{flushleft}
6.16 + &
6.17 + \begin{flushright}
6.18 + \tiny #1
6.19 + \end{flushright}
6.20 + \\
6.21 + \end{tabular}
6.22 + }
6.23 +
6.24 + }
6.25 +\newcommand {\bigquest}{\marginpar{\huge?}}
6.26 +\newcommand {\cnumber}[1]{\put(8,4){\circle{11}}\put(5,1){#1}\hspace{5mm}}
6.27 +
6.28 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
6.29 +\def\sisac{{\small${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
6.30 +
6.31 +\title{\isac\\ Usecases}
6.32 +\author{Andreas Griesmayer, Alan Krempler, Walther Neuper\\
6.33 +{\tt\{agries,akremp,neuper\}@ist.tugraz.at}}
6.34 +\date{$Revision$}
6.35 +%\date{$Revision$}wn
6.36 +
6.37 +\includeonly{use-content}
6.38 +\begin{document}
6.39 +\maketitle
6.40 +\tableofcontents
6.41 +
6.42 +\input{common}
6.43 +\bibliography{bib/didact,bib/math-eng,bib/dia-form,bib/RISC_1,bib/RISC_2,bib/misc,bib/hci,bib/isac}
6.44 +\end{document}
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/sml/CLEANUP Thu Apr 17 18:01:03 2003 +0200
7.3 @@ -0,0 +1,31 @@
7.4 +rm *~
7.5 +cd Scripts
7.6 + rm *~
7.7 + rm #*
7.8 + rm .#*
7.9 + cd ..
7.10 +cd ME
7.11 + rm *~
7.12 + rm #*
7.13 + rm .#*
7.14 + cd ..
7.15 +cd DG
7.16 + rm *~
7.17 + rm #*
7.18 + rm .#*
7.19 + cd ..
7.20 +cd IsacKnowledge
7.21 + rm *~
7.22 + rm #*
7.23 + rm .#*
7.24 + cd ..
7.25 +cd kbtest
7.26 + rm *~
7.27 + rm #*
7.28 + rm .#*
7.29 + cd ..
7.30 +cd systest
7.31 + rm *~
7.32 + rm #*
7.33 + rm .#*
7.34 + cd ..
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/sml/DG-ME-states.sml Thu Apr 17 18:01:03 2003 +0200
8.3 @@ -0,0 +1,706 @@
8.4 +(* use"DG-ME-states.sml";
8.5 + W.N.24.11.99
8.6 + *)
8.7 +
8.8 +val seed = ref 2;
8.9 +fun rand1_1() = (seed:= !seed +1; (!seed mod 2) * ~2 + 1);
8.10 +(*> rand1_1();rand1_1();rand1_1();rand1_1();rand1_1();rand1_1();
8.11 +val it = ~1 : int
8.12 +val it = 1 : int
8.13 +val it = ~1 : int
8.14 +val it = 1 : int TODO !!!*)
8.15 +
8.16 +type userID = int;
8.17 +type proofID = int;
8.18 +
8.19 +
8.20 +
8.21 +
8.22 +(*** imperative proof states ***)
8.23 +
8.24 +type proofs = (userID * (proofID * ptree) list) list;
8.25 +val proofs = ref ([]:proofs);
8.26 +(*
8.27 +proofs:= [(3,[(31, EmptyPtree), (32, EmptyPtree)]),
8.28 + (4,[(41, EmptyPtree), (42, EmptyPtree)])];
8.29 +*)
8.30 +exception PROOFS of string;
8.31 +
8.32 +
8.33 +(** create new instances of users and ptrees
8.34 + new keys are the lowest possible in the association list **)
8.35 +
8.36 +(* add users *)
8.37 +fun new_key u n = case assoc (u, n) of
8.38 + None => n
8.39 +| Some _ => new_key u (n+1);
8.40 +fun get_userID (u: proofs) = (new_key u 1):userID;
8.41 +(*
8.42 +> val new_userID = get_userID (!proofs);
8.43 +val it = 1 : int
8.44 +> proofs:= (!proofs) @ [(new_userID, [])];
8.45 +> !proofs;
8.46 +val it = [(3,[(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[])]
8.47 +*)
8.48 +
8.49 +(* add proofs to a users active proofs *)
8.50 +fun get_proofID (uI:userID) (p: proofs) =
8.51 + case assoc (p, uI) of
8.52 + None => raise PROOFS ("get_proofID: no userID " ^
8.53 + (string_of_int uI))
8.54 + | Some ps => (new_key ps 1):proofID;
8.55 +(*
8.56 +> get_proofID 1 (!proofs);
8.57 +val it = 1 : proofID
8.58 +*)
8.59 +fun add_pID (uI:userID) (p: proofs) =
8.60 + let val new_ID = get_proofID uI p;
8.61 + val new_pts = (the (assoc (p, uI))) @ [(new_ID,EmptyPtree)];
8.62 + in (new_ID, (overwrite (p,(uI,new_pts))):proofs) end;
8.63 +(*
8.64 +> val (new_proofID, new_proofs) = add_pID 1 (!proofs);
8.65 +> proofs:= new_proofs;
8.66 +> !proofs;
8.67 +val it = [(3,[(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : proofs
8.68 +> val (new_proofID, new_proofs) = add_pID 3 (!proofs);
8.69 +> proofs:= new_proofs;
8.70 +> !proofs;
8.71 +al it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : proofs
8.72 +> assoc2 (!proofs, (3, 1));
8.73 +val it = Some EmptyPtree : ptree option
8.74 +> assoc2 (!proofs, (3, 2));
8.75 +val it = None : ptree option
8.76 +*)
8.77 +
8.78 +
8.79 +(** retrieve, update, delete a ptree by userID, proofID **)
8.80 +
8.81 +fun get_prf (uI:userID) (pI:proofID) (p:proofs) =
8.82 + (the (assoc2 (p,(uI, pI))))
8.83 + handle _ => raise PROOFS ("get_proof " ^ (string_of_int uI) ^
8.84 + " " ^ (string_of_int pI) ^ " not existent");
8.85 +(*
8.86 +> get_prf 3 1 (!proofs);
8.87 +val it = EmptyPtree : ptree
8.88 +*)
8.89 +fun get_proof (uI:userID) (pI:proofID) = get_prf uI pI (!proofs);
8.90 +
8.91 +
8.92 +
8.93 +fun del_assoc ([],_) = []
8.94 + | del_assoc a =
8.95 + let fun del ([], key) ps = ps
8.96 + | del ((keyi, xi) :: pairs, key) ps =
8.97 + if key = keyi then ps @ pairs
8.98 + else del (pairs, key) (ps @ [(keyi, xi)])
8.99 + in del a [] end;
8.100 +(*
8.101 +> val ps = [(1,"1"),(2,"2"),(3,"3"),(4,"4")];
8.102 +> del_assoc (ps,3);
8.103 +val it = [(1,"1"),(2,"2"),(4,"4")] : (int * string) list
8.104 +*)
8.105 +
8.106 +(* delete doesn't report non existing elements *)
8.107 +fun del_assoc2 (uI:userID) (pI:proofID) ps =
8.108 + let val new_ps = del_assoc (the (assoc (ps, uI)), pI)
8.109 + in overwrite (ps, (uI, new_ps)) end;
8.110 +(*
8.111 +> proofs:= del_assoc2 4 41 (!proofs);
8.112 +> !proofs;
8.113 +val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#)]),(1,[(#,#)])] : proofs
8.114 +> proofs:= del_assoc2 4 41 (!proofs);
8.115 +> !proofs;
8.116 +val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#)]),(1,[(#,#)])] : proofs
8.117 +
8.118 +> proofs:= del_user 3 (!proofs);
8.119 +> !proofs;
8.120 +val it = [(4,[(#,#)]),(1,[(#,#)])] : proofs
8.121 +*)
8.122 +
8.123 +fun overwrite2 (ps, (((uI:userID), (pI:proofID)), p)) =
8.124 + let val new_ps = overwrite (the (assoc (ps, uI)), (pI, p))
8.125 + in (overwrite (ps, (uI, new_ps)))
8.126 + handle _ => raise PROOFS ("overwrite2 " ^ (string_of_int uI) ^
8.127 + " " ^ (string_of_int pI) ^ " not existent")
8.128 + end;
8.129 +(*
8.130 +> val (pt,pos) = (EmptyPtree,[]);
8.131 +> val (pt,_,_) = cappend_problem pt pos "loc" (empty_spec ,[]:cterm' list) [];
8.132 +> proofs:= upd_ptree 4 42 pt (!proofs);
8.133 +> get_ptree 4 42 (!proofs);
8.134 +Nd (PblObj {branch=#,cell=#,env=#,formal=#,...) : ptree
8.135 +> get_ptree 1 1 (!proofs);
8.136 +val it = EmptyPtree : ptree
8.137 +*)
8.138 +fun upd_proof (uI:userID) (pI:proofID) p =
8.139 + proofs:= overwrite2 ((!proofs), ((uI, pI), p));
8.140 +
8.141 +
8.142 +
8.143 +(*** imperative dialog states
8.144 + they use userID, proofID; + assoc
8.145 + exactly the same way as proofs do
8.146 + wrt. userID, proofID; + assoc (dps, cellID) ***)
8.147 +
8.148 +datatype dtm =
8.149 +(* in comment the dhpases ..v *)
8.150 +(*<------------------------ 1 --------------------->*)
8.151 + PutRes
8.152 + | FillRes
8.153 +(*<--- 2ai ---><--- 2aii --->< ------- 2b --------->*)
8.154 + | PutFun
8.155 + | SelFun
8.156 + | PutArg
8.157 + | FillArg
8.158 + | SelArg
8.159 +(*<---------- 2a ---------- >< ------- 2b --------->*)
8.160 + | PutRule
8.161 + | FillRule
8.162 + | SelRule
8.163 + | PutRuleRes
8.164 + | FillRuleRes
8.165 + | DtmUndef;
8.166 +
8.167 +val rule_dtms = [(*PutArg,FillArg,SelArg,*)
8.168 + PutRule(*,FillRule*),SelRule];
8.169 +val form_dtms = [PutRuleRes(*,FillRuleRes*)];
8.170 +
8.171 +(* dpstate: for each user, each proof *)
8.172 +datatype act =
8.173 + Tt (*Tutor, giving control to St*)
8.174 + | TskipS (*continues recursion in do_dmts*)
8.175 + | St (*student gets the control*)
8.176 + | ACundef;
8.177 +
8.178 +datatype dast =
8.179 + Broken (*St: breaks datom*)
8.180 + | AccepT (*datom finished by agreement*)
8.181 + | ErroR (*ME reported error in this datom*)
8.182 + | NoDtm (*after resume no continue_pattern, no do_dtm*)
8.183 + | FixDtm (*after resume no continue_pattern, but dtm fixed in resume*)
8.184 + | DAundf;
8.185 +
8.186 +type dct = int; (*dstep counter:
8.187 + set into dph in resume_ via init_dct from dstate,
8.188 + decr. in dph in any datom when DPform left;
8.189 + dct in dstate in/decr by SpeedPlus/Minus
8.190 + *)
8.191 +val default_dct = (1*2-1):dct;
8.192 +(*(max dphases from St: to St:) * (max dphs per dphase) - (1st dtm)*)
8.193 +
8.194 +
8.195 +datatype dph =
8.196 + DPdoneR of (* this datom is already done, finishing DPrule*)
8.197 + mstep_ * (* current rule for DPrule -> DPform*)
8.198 + (* or next_step for DPform -> DPform | DPrule*)
8.199 + mout * (* DPrule -> DPform: form generated by mstep_-check *)
8.200 + (* DPform -> DPform: empty*)
8.201 + dct (* dstep counter: decr at DPform in any datom*)
8.202 + | DPdoneF of (* this datom is already done, finishing DPform*)
8.203 + mstep_ * (* current rule for DPrule -> DPform*)
8.204 + (* or next_step for DPform -> DPform | DPrule*)
8.205 + mout * (* DPrule -> DPform: form generated by mstep_-check *)
8.206 + (* DPform -> DPform: empty*)
8.207 + dct (*dstep counter: decr at DPform in any datom*)
8.208 + | DPruleId of (* 2ai 10.00: NOTYET IMPL.*)
8.209 + mstep_ * mstID *(* <- ME, thus applicable *)
8.210 + dct (*dstep counter*)
8.211 + | DPrule of (* 2aii | 2a *)
8.212 + mstep_ * (* <- ME, thus applicable *)
8.213 + mstep_ * (* <- user, <>empty <=> <>(<- ME) *)
8.214 + dct (*dstep counter: decr at DPform in any datom*)
8.215 + | DPform of (* 2b | 1 *)
8.216 + mstep_ * (* <- ME or user, applicable *)
8.217 + mout * (* <- ME, calculated by mstep_ *)
8.218 + foppFK * (* <- user, <>empty <=> <>mout(<- ME)*)
8.219 + dct; (*dstep counter: decr at DPform in any datom*)
8.220 +fun dph2str (DPrule (m1,m2,i)) =
8.221 + "DPrule ("^(mstep_2str m1)^
8.222 + ","^(mstep_2str m2)^
8.223 + ","^(string_of_int i)^")"
8.224 + | dph2str (DPform (m,mo,f,i)) =
8.225 + "DPform ("^(mstep_2str m)^
8.226 + ","^(mout2str mo)^
8.227 + ","^(foppFK2str f)^
8.228 + ","^(string_of_int i)^")"
8.229 + | dph2str (DPdoneR (m,mo,i)) =
8.230 + "DPdoneR ("^(mstep_2str m)^
8.231 + ","^(mout2str mo)^
8.232 + ","^(string_of_int i)^")"
8.233 + | dph2str (DPdoneF (m,mo,i)) =
8.234 + "DPdoneF ("^(mstep_2str m)^
8.235 + ","^(mout2str mo)^
8.236 + ","^(string_of_int i)^")";
8.237 +fun dct_of (DPrule (_,_,dc)) = dc
8.238 + | dct_of (DPform (_,_,_,dc)) = dc
8.239 + | dct_of (DPdoneR (_,_,dc)) = dc
8.240 + | dct_of (DPdoneF (_,_,dc)) = dc;
8.241 +
8.242 +
8.243 +type acti = int;
8.244 +(* 6 St PutRes ..more active
8.245 + 5 St FillRes
8.246 + 4 St SelRule .. St FillRuleRes | Tt PutRuleRes if speed > 0
8.247 + 3 St FillRule .. St FillRuleRes | Tt PutRuleRes if speed > 0
8.248 + 2 St SelRule .. Tt PutRuleRes | Tt PutRuleRes if speed > 0
8.249 + 1 St FillRule .. Tt PutRuleRes | Tt PutRuleRes if speed > 0
8.250 + 0 Tt PutRule .. Tt PutRuleRes ..less active*)
8.251 +val default_acti = 4:acti;
8.252 +type speed = int;
8.253 +(* 1 TskipS if dct > 0
8.254 + 0 St | Tt unchanged*)
8.255 +val default_speed = 1:speed;
8.256 +
8.257 +(* dstate: for each user *)
8.258 +type hide = {rules : mstID list, pbls : pblID list,
8.259 + rlss : rls' list, thms : thmID list};
8.260 +
8.261 +datatype dstate =
8.262 + EmptyDstate
8.263 + | Dstate of
8.264 + hide * (*msteps, thms, rls to do tacitly *)
8.265 + acti * (* = 0: Tt active, < 0: St active in sel_dtm *)
8.266 + speed * (*decides on 'skip datoms' in sel_dtm *)
8.267 + cellID * (*last cell generated by KE: for newcell*)
8.268 + dct; (*dstep counter as set by init_dct in resume_dpst:
8.269 + dct = dct + (if speed >2 then speed-2 else 0);
8.270 + in/decr in resume_ by SpeedPlus/Minus*)
8.271 +(*18.4.01: speed = dct+1 ...sh fun incr_/decr_speed
8.272 + ... "uberlegen: isac.010418b-dctBEHALTEN
8.273 + + Auto -> speed=3 -- remains in dstate .. ugly, but hard to change*)
8.274 +
8.275 +
8.276 +val default_hide =
8.277 + {rules = ["Take" ,"Group",
8.278 + "Split_And" ,"Conclude_And",
8.279 + "Split_Or" ,"Conclude_Or",
8.280 + "Begin_Trans" ,"End_Trans",
8.281 + "Begin_Sequ",
8.282 + "Split_Intersect" ,"End_Intersect",
8.283 + "Check_elementwise","Collect_Trues",
8.284 + "End_Proof'"],
8.285 + pbls = [["reals","differentiate"]],
8.286 + rlss = ["rearrange_assoc"],
8.287 + thms = ["add_commute","add_left_commute","add_assoc",
8.288 + "mult_commute","mult_left_commute","mult_assoc"]}:hide;
8.289 +val test_hide = (*maintaining test_FE-KE.sml*)
8.290 + {rules = ["Take" ,"Group",
8.291 + "Split_And" ,"Conclude_And",
8.292 + "Split_Or" ,"Conclude_Or",
8.293 + "Begin_Trans" ,"End_Trans",
8.294 + "Begin_Sequ",
8.295 + "Split_Intersect" ,"End_Intersect",
8.296 + "Check_elementwise","Collect_Trues"],
8.297 + pbls = [["reals","differentiate"]],
8.298 + rlss = [],
8.299 + thms = []}:hide;
8.300 +val spec_hide = (*hide specification*)
8.301 + {rules = specsteps @ ["Apply_Method"],
8.302 + pbls = [], rlss = [], thms = []}:hide;
8.303 +
8.304 +(*######################################################################*)
8.305 +(*for demo0*) val default_hide = spec_hide; (*for demo0*)
8.306 +(*######################################################################*)
8.307 +
8.308 +val default_dstate =
8.309 + Dstate (default_hide,
8.310 + 0, (*Tt active*)
8.311 + 2, (*PutRuleRes,Tt..PutRule,TskipS..PutRuleRes,Tt..*)
8.312 + 0, (*lowest cellID written by KE*)
8.313 + default_dct);(*maximum dphase count*)
8.314 +fun d2str EmptyDstate = "EmptyDstate"
8.315 + | d2str (Dstate (_, a, s, c, d)) =
8.316 + "Dstate (hide..,"^(string_of_int a)^","^
8.317 + (string_of_int s)^","^(string_of_int c)^","^(string_of_int d)^")";
8.318 +
8.319 +fun get_acti EmptyDstate = default_acti
8.320 + | get_acti (Dstate (h,a,s,c,d)) = a;
8.321 +fun set_acti n EmptyDstate = Dstate (default_hide,n,default_speed,0,default_dct)
8.322 + | set_acti n (Dstate (h,_,s,c,d)) = Dstate (h, n,s,c,d);
8.323 +
8.324 +fun get_speed EmptyDstate = default_speed
8.325 + | get_speed (Dstate (h,a,s,c,d)) = s:speed;
8.326 +fun set_speed n EmptyDstate = Dstate (default_hide,default_acti,n,0,default_dct)
8.327 + | set_speed n (Dstate (h,a,_,c,d)) = Dstate (h,a, n,c,d);
8.328 +fun incr_speed EmptyDstate =
8.329 + Dstate (default_hide,default_acti,default_speed,0,default_dct)
8.330 + | incr_speed (Dstate (h,a,s,c,d)) =
8.331 + Dstate (h,a,s+1,c,if s+1>2 then s-1 else 1);
8.332 +fun decr_speed EmptyDstate =
8.333 + Dstate (default_hide,default_acti,0,0,default_dct)
8.334 + | decr_speed (Dstate (h,a,s,c,d)) =
8.335 + Dstate (h,a,if s>0 then s-1 else 0,c,if s-1>2 then s-2 else 1);
8.336 +
8.337 +fun get_dct EmptyDstate = default_dct
8.338 + | get_dct (Dstate (h,a,s,c,d)) = d;
8.339 +fun get_dct' EmptyDstate = default_dct
8.340 + | get_dct' (Dstate (_,_,s,_,c)) = if s>2 then s else c;
8.341 +fun set_dct n EmptyDstate = Dstate (default_hide,default_acti,default_speed,0,n)
8.342 + | set_dct n (Dstate (h,a,s,c,_)) = Dstate (h,a,s,c,n);
8.343 +
8.344 +fun getdecr_cellID EmptyDstate =
8.345 + (Dstate (default_hide,default_acti,default_speed,0,default_dct),~1)
8.346 + | getdecr_cellID (Dstate (h,a,s,c,d)) = (Dstate (h,a,s,c-1,d),c-1);
8.347 +
8.348 +(*init dct in resume_dpst, see in/decr_speed !*)
8.349 +fun init_dct (Dstate (_,_,s,_,c)) (DPdoneR (r,sf,_)) = DPdoneR (r,sf,if s>2 then s else c)
8.350 + | init_dct (Dstate (_,_,s,_,c)) (DPdoneF (r,sf,_)) = DPdoneF (r,sf,if s>2 then s else c)
8.351 + | init_dct (Dstate (_,_,s,_,c)) (DPform (r,sf,uf,_))= DPform(r,sf,uf,if s>2 then s else c)
8.352 + | init_dct (Dstate (_,_,s,_,c)) (DPrule (sr,ur,_)) = DPrule (sr,ur,if s>2 then s else c)
8.353 + | init_dct (Dstate (_,_,s,_,c)) dph = raise error ("dct_of called for "^(dph2str dph));
8.354 +
8.355 +
8.356 +
8.357 +type dpstate =
8.358 + dtm * (* PutRule,FillRule,... *)
8.359 + act * (* Tt, St,.. *)
8.360 + dast * (* Broken, AccepT, ErroR,...*)
8.361 + (user_cmd option) * (* if this is Some, dast is Broken*)
8.362 + dph * (* contains mstep m, dct*)
8.363 + pos'; (* pointing into ptree, where
8.364 + mstep is applied to | form has been written to*)
8.365 +val e_dpst = (DtmUndef,Tt,DAundf,None,
8.366 + DPdoneR (e_mstep_,EmptyMout,0),e_pos'):dpstate;
8.367 +
8.368 +
8.369 +(* the dialog-proof-history;
8.370 + one cellID can address several dpstates,
8.371 + the first dpstate found (beginnin from the heade of dps)
8.372 + is taken to the head of dps: this is the _current_ dpstate
8.373 + *)
8.374 +type dps = (cellID * dpstate) list;
8.375 +
8.376 +(*for test-writeln*)
8.377 +fun last_dct (((_,(_,_,_,_,dph,_))::_):dps) = dct_of dph
8.378 + | last_dct _ = ~9999;
8.379 +
8.380 +
8.381 +fun act2str Tt ="Tt"
8.382 +| act2str TskipS ="TskipS"
8.383 +| act2str St ="St"
8.384 +| act2str ACundef ="ACundef";
8.385 +fun dast2str Broken ="Broken"
8.386 +| dast2str AccepT ="AccepT"
8.387 +| dast2str ErroR ="ErroR"
8.388 +| dast2str NoDtm = "NoDtm"
8.389 +| dast2str FixDtm = "FixDtm"
8.390 +| dast2str DAundf ="DAundf";
8.391 +fun dtm2str PutRes ="PutRes"
8.392 +| dtm2str FillRes ="FillRes"
8.393 +| dtm2str PutFun ="PutFun"
8.394 +| dtm2str SelFun ="SelFun"
8.395 +| dtm2str PutArg ="PutArg"
8.396 +| dtm2str FillArg ="FillArg"
8.397 +| dtm2str SelArg ="SelArg"
8.398 +| dtm2str PutRule ="PutRule"
8.399 +| dtm2str FillRule ="FillRule"
8.400 +| dtm2str SelRule ="SelRule"
8.401 +| dtm2str PutRuleRes ="PutRuleRes"
8.402 +| dtm2str FillRuleRes="FillRuleRes"
8.403 +| dtm2str DtmUndef ="DtmUndef";
8.404 +fun cmd2str None = "None"
8.405 + | cmd2str (Some c) = "Some "^(user_cmd2str c);
8.406 +fun dpst2str ((dtm,act,(*dod,*)dast,cmd,dph,pos):dpstate) =
8.407 + " ("^(dtm2str dtm)^","^(act2str act)^","^
8.408 + (*(dod2str dod)^","^*)(dast2str dast)^","^(cmd2str cmd)^","^
8.409 + (dph2str dph)^","^(pos'2str pos)^")";
8.410 +fun appnl s = s^"\n";
8.411 +fun dp2str (cellID,dpst) = pair2str(string_of_int cellID,
8.412 + dpst2str dpst);
8.413 +fun dps2str (dps:dps) = (strs2str' o (map (appnl o dp2str))) (take(11,dps));
8.414 +(*
8.415 +> val dps = [(1,e_dpst),(2,e_dpst)]:dps;
8.416 +> writeln(dps2str dps);
8.417 +*)
8.418 +
8.419 +
8.420 +
8.421 +(* use"DG-ME-states.sml";
8.422 + *)
8.423 +
8.424 +
8.425 +type delcells = cellID list;
8.426 +
8.427 +
8.428 +
8.429 +(* use"DG-ME-states.sml";
8.430 + *)
8.431 +
8.432 +
8.433 +(*select the subsequent datom,
8.434 + acti = 0..6,
8.435 + speed 0..Infinite, speed > 2: skip-count d set by SpeedPlus*)
8.436 +fun sel_dtm dph (acti:acti) (speed:speed) =
8.437 + case dph of
8.438 + DPdoneF (r,f,d) =>
8.439 + (case (acti, speed) of
8.440 + (0,0) => (DPrule (r, e_mstep_, d) , PutRule , Tt )
8.441 + | (0,1) => (DPrule (r, e_mstep_, d) , PutRule , Tt )
8.442 + | (0,2) => (DPrule (r, e_mstep_, d-1) , PutRule , TskipS)(*form halts*)
8.443 + | (0,_) => if d<=0
8.444 + then (DPform (r, f,EmptyFoppFK,d ), PutRes , Tt )
8.445 + else (DPform (r, f,EmptyFoppFK,d-1), PutRes , TskipS)(*18.4.01*)
8.446 + | (1,_) => (DPrule (r, e_mstep_, d) , FillRule, St )
8.447 + | (2,_) => (DPrule (r, e_mstep_, d) , SelRule , St )
8.448 + | (3,_) => (DPrule (r, e_mstep_, d) , FillRule, St )
8.449 + | (4,_) => (DPrule (r, e_mstep_, d) , SelRule , St )
8.450 + | (5,_) => (DPform (r, f, EmptyFoppFK, d), FillRes , St )
8.451 + | (_,_) => (DPform (r, f, EmptyFoppFK, d), PutRes , St )
8.452 + )
8.453 + | DPdoneR (r,f,d) =>
8.454 + (case (acti, speed) of
8.455 + (0,0) => (DPform (r, f, EmptyFoppFK, d) , PutRuleRes , Tt )
8.456 + | (0,1) => (DPform (r, f, EmptyFoppFK, d-1), PutRuleRes , TskipS)
8.457 + | (0,2) => (DPform (r, f, EmptyFoppFK, d) , PutRuleRes , Tt )
8.458 + | (0,_) => if d<=0
8.459 + then (DPform (r, f, EmptyFoppFK, d) , PutRuleRes , Tt )
8.460 + else (DPform (r, f, EmptyFoppFK, d-1), PutRuleRes , TskipS)
8.461 + | (1,0) => (DPform (r, f, EmptyFoppFK, d) , PutRuleRes , Tt )
8.462 + | (1,_) => (DPform (r, f, EmptyFoppFK, d-1), PutRuleRes , TskipS)
8.463 + | (2,0) => (DPform (r, f, EmptyFoppFK, d) , PutRuleRes , Tt )
8.464 + | (2,_) => (DPform (r, f, EmptyFoppFK, d-1), PutRuleRes , TskipS)
8.465 + | (3,0) => (DPform (r, f, EmptyFoppFK, d) , FillRuleRes, St )
8.466 + | (3,_) => (DPform (r, f, EmptyFoppFK, d-1), PutRuleRes , TskipS)
8.467 + | (4,0) => (DPform (r, f, EmptyFoppFK, d) , FillRuleRes, St )
8.468 + | (4,_) => (DPform (r, f, EmptyFoppFK, d-1), PutRuleRes , TskipS)
8.469 + | (5,_) => (DPform (r, f, EmptyFoppFK, d) , FillRuleRes, St )
8.470 + | (_,_) => (DPform (r, f, EmptyFoppFK, d) , PutRuleRes , St )
8.471 + )
8.472 + (*broken*)
8.473 + | DPform (r,sf,uf,d) =>
8.474 + (case (acti, speed) of
8.475 + (0,0) => (DPform (r, sf, uf, d ), PutRuleRes , Tt )
8.476 + | (0,1) => (DPform (r, sf, uf, d-1), PutRuleRes , TskipS)(*18.4.01*)
8.477 + | (0,2) => (DPform (r, sf, uf, d ), PutRuleRes , Tt )
8.478 + | (0,_) => if d<=0
8.479 + then (DPform (r, sf, uf, d ), PutRuleRes , Tt )
8.480 + else (DPform (r, sf, uf, d-1), PutRuleRes , TskipS)(*18.4.01*)
8.481 + | (1,0) => (DPform (r, sf, uf, d ), PutRuleRes , Tt )
8.482 + | (1,_) => (DPform (r, sf, uf, d-1), PutRuleRes , TskipS)(*18.4.01*)
8.483 + | (2,0) => (DPform (r, sf, uf, d ), PutRuleRes , Tt )
8.484 + | (2,_) => (DPform (r, sf, uf, d-1), PutRuleRes , TskipS)(*18.4.01*)
8.485 + | (3,0) => (DPform (r, sf, uf, d ), FillRuleRes, St )
8.486 + | (3,_) => (DPform (r, sf, uf, d-1), PutRuleRes , TskipS)(*18.4.01*)
8.487 + | (4,0) => (DPform (r, sf, uf, d ), FillRuleRes, St )
8.488 + | (4,_) => (DPform (r, sf, uf, d-1), PutRuleRes , TskipS)(*18.4.01*)
8.489 + | (5,0) => (DPform (r, sf, uf, d ), FillRuleRes, St )
8.490 + | (_,_) => (DPform (r, sf, uf, d ), PutRuleRes , St )
8.491 + )
8.492 + | DPrule (sm,um,d) =>
8.493 + (case (acti, speed) of
8.494 + (0,0) => (DPrule (sm, um, d) , PutRule , Tt )
8.495 + | (0,1) => (DPrule (sm, um, d) , PutRule , Tt )
8.496 + | (0,2) => (DPrule (sm, um, d-1) , PutRule , TskipS)
8.497 + | (0,_) => if d<=0
8.498 + then (DPrule (sm, um, d) , PutRule , Tt )
8.499 + else (DPrule (sm, um, d-1) , PutRule , TskipS)
8.500 + | (1,_) => (DPrule (sm, um, d) , FillRule , St )
8.501 + | (2,_) => (DPrule (sm, um, d) , SelRule , St )
8.502 + | (3,_) => (DPrule (sm, um, d) , FillRule , St )
8.503 + | (4,_) => (DPrule (sm, um, d) , SelRule , St )
8.504 + | (5,_) => (DPrule (sm, um, d-1) , PutRule , TskipS)
8.505 + | (_,_) => (DPrule (sm, um, d-1) , PutRule , TskipS)
8.506 + )
8.507 +
8.508 +
8.509 +
8.510 +
8.511 +
8.512 +(* imperative dialog state: association lists only *)
8.513 +type dials =
8.514 + (userID * dstate) list * (*personal dst (user-model) *)
8.515 + (userID * (proofID * cellID list) list) list * (*0..~1..~2..///5.00 *)
8.516 + (userID * (proofID * (cellID * dpstate) list) list) list;
8.517 + (*dpstate: info to each cell in a proof*)
8.518 +
8.519 +val dials = ref (([],[],[]):dials);
8.520 +exception DIALS of string;
8.521 +(*
8.522 +> dials:= ([(3, EmptyDstate), (4, EmptyDstate)],
8.523 + [(3, [(31, [~3101,~3102]), (32, [~3201,~3202])]),
8.524 + (4, [(31, [~3101,~3102]), (32, [~3201,~3202])])],
8.525 + [(3, [(31, [(3101,e_dpst)]), (32, [])]),
8.526 + (4, [(41, []), (42, [])])]);
8.527 +get_dpst 3 31 3101;
8.528 +get_dph 3 31 3101;
8.529 +*)
8.530 +
8.531 +fun get_dstate (uI:userID) =
8.532 + (the (assoc (fst3 (!dials), uI)))
8.533 + handle _ => raise DIALS ("get_dstate " ^ (string_of_int uI) ^
8.534 + " not existent");
8.535 +
8.536 +(*for maintainance of test-FE-KE.sml: sets hide only*)
8.537 +fun set_dstate (uI:userID) h acti speed =
8.538 + let val (ds,xx,dps) = !dials;
8.539 + val Dstate (_,_,_,cell,dct) = (the (assoc (fst3 (!dials), uI)))
8.540 + handle _ => raise DIALS ("get_dstate " ^ (string_of_int uI) ^
8.541 + " not existent");
8.542 + in dials:= (overwrite (ds, (uI, Dstate (h,acti,speed,cell,dct))),
8.543 + xx, dps) end;
8.544 +
8.545 +(*unused after 5.00; keep for other usage*)
8.546 +fun get_newcells (uI:userID) (pI:proofID) =
8.547 + (the (assoc2 (snd3 (!dials), (uI,pI))))
8.548 + handle _ => raise DIALS ("get_newcells " ^ (string_of_int uI) ^
8.549 + " not existent");
8.550 +
8.551 +fun get_dps (uI:userID) (pI:proofID) =
8.552 + (the (assoc2 (thd3 (!dials), (uI,pI))))
8.553 + handle _ => raise DIALS ("get_dps " ^ (string_of_int uI) ^
8.554 + " not existent");
8.555 +
8.556 +(*for testing*)
8.557 +fun get_dpst uI pI cI = the (assoc ((get_dps uI pI), cI));
8.558 +
8.559 +fun g_dph ((_,_,(*_,*)_,_,dph,_):dpstate) = dph;
8.560 +fun get_dph uI pI cI = g_dph (get_dpst uI pI cI);
8.561 +
8.562 +fun g_mstp (DPform ((_,m),_,_,_)) = [m]
8.563 + | g_mstp (DPrule ((_,m),_,_)) = [m]
8.564 + | g_mstp _ = [];
8.565 +fun get_msteps uI pI cI = g_mstp (get_dph uI pI cI);
8.566 +
8.567 +fun g_frm (DPform ((_,_),Form' (FormKF (_,_,_,_,f)),_,_)) = [f]
8.568 + | g_frm _ = [];
8.569 +fun get_forms uI pI cI = g_frm (get_dph uI pI cI);
8.570 +
8.571 +fun g_ppc (DPform ((_,_),Form' (PpcKF (_,_,_,_,(_,f))),_,_)) = [f]
8.572 + | g_ppc _ = [];
8.573 +fun get_ppcs uI pI cI = g_ppc (get_dph uI pI cI);
8.574 +
8.575 +fun g_cll (DPform ((_,_),Form' (FormKF (c,_,_,_,_)),_,_)) = [c]
8.576 + | g_cll (DPform ((_,_),Form' (PpcKF (c,_,_,_,_)),_,_)) = [c]
8.577 + | g_cll _ = [];
8.578 +fun get_cells uI pI cI = g_cll (get_dph uI pI cI);
8.579 +
8.580 +
8.581 +fun g_hist ((dtm,act,dast,cmd,_,pos):dpstate) =
8.582 + "("^(dtm2str dtm)^", "^(act2str act)^(*", "^(dod2str dod)^*)
8.583 + ", "^(dast2str dast)^", "^(cmd2str cmd)^", "^(pos'2str pos)^")";
8.584 +fun g_pair (c,dpst) = "("^(string_of_int c)^", "^(g_hist dpst)^")\n";
8.585 +fun get_history uI pI = (strs2str' o (map g_pair)) (get_dps uI pI);
8.586 +(*for testing*)
8.587 +
8.588 +
8.589 +fun init_dps (uI:userID) (pI:proofID) (nc:cellID list) (dps:dps) =
8.590 + let val (d,_,_) = !dials;
8.591 + in dials:= (d,
8.592 + overwrite2 (snd3 (!dials), ((uI, pI), nc)),
8.593 + overwrite2 (thd3 (!dials), ((uI, pI), dps))) end;
8.594 +
8.595 +(*update imperative dialog-state*)
8.596 +fun upd_dial (uI:userID) (pI:proofID)
8.597 + (d:dstate) (nc:cellID list) (dps:dps) =
8.598 + dials:= (overwrite (fst3 (!dials), (uI, d)),
8.599 + overwrite2 (snd3 (!dials), ((uI, pI), nc)),
8.600 + overwrite2 (thd3 (!dials), ((uI, pI), dps)));
8.601 +(*
8.602 +dials:= ([(3, EmptyDstate), (4, EmptyDstate)],
8.603 + [(3, [(31, [~3101,~3102]), (32, [~3201,~3202])]),
8.604 + (4, [(31, [~3101,~3102]), (32, [~3201,~3202])])],
8.605 + [(3, [(31, [(3101,[e_dpst,e_dpst])]), (32, [])]),
8.606 + (4, [(41, []), (42, []:dps)])]);
8.607 +> upd_dial 3 33 default_dstate [~1,~2,~3] [(1,[e_dpst])];
8.608 +> !dials;
8.609 + ([(3,Dstate #),(4,EmptyDstate)],[(3,[#,#,#]),(4,[#,#])],
8.610 + [(3,[#,#,#]),(4,[#,#])]) : dials
8.611 +
8.612 +thd3 (!dials);
8.613 +
8.614 +*)
8.615 +
8.616 +
8.617 +(** add and delete proofs **)
8.618 +
8.619 +fun add_proof (uI:userID) =
8.620 + let val (new_proofID, new_proofs) = add_pID uI (!proofs)
8.621 + in proofs:= new_proofs;
8.622 + init_dps uI new_proofID [] []; (*30.10.00*)
8.623 + new_proofID end;
8.624 +fun del_proof (uI:userID) (pI:proofID) =
8.625 + (proofs:= del_assoc2 uI pI (!proofs);
8.626 + dials:= (del_assoc (fst3 (!dials), pI),
8.627 + del_assoc2 uI pI (snd3 (!dials)),
8.628 + del_assoc2 uI pI (thd3 (!dials)));
8.629 + pI);
8.630 +
8.631 +
8.632 +(** add and delete users **)
8.633 +
8.634 +fun add_user () =
8.635 + let val new_uI = get_userID (!proofs)
8.636 + in proofs:= (!proofs) @ [(new_uI, [])];
8.637 + dials := ((fst3 (!dials)) @ [(new_uI, default_dstate)],
8.638 + (snd3 (!dials)) @ [(new_uI, [])],
8.639 + (thd3 (!dials)) @ [(new_uI, [])]);
8.640 + new_uI end;
8.641 +(*
8.642 +> add_user (); add_user (); !proofs; !dials;
8.643 +*)
8.644 +(* delete doesn't report non existing elements *)
8.645 +fun del_user (uI:userID) =
8.646 + (proofs:= del_assoc (!proofs, uI);
8.647 + dials:= (del_assoc (fst3 (!dials), uI),
8.648 + del_assoc (snd3 (!dials), uI),
8.649 + del_assoc (thd3 (!dials), uI));
8.650 + uI:userID);
8.651 +
8.652 +
8.653 +(* -------------- test all exported funs --------------
8.654 +
8.655 +> proofs:=[]; dials:=([],[],[]);
8.656 +> add_user (); add_user (); !proofs; !dials;
8.657 +val it = 1 : userID
8.658 +val it = 2 : userID
8.659 +val it = [(1,[]),(2,[])] : proofs
8.660 +val it = ([(1,EmptyDstate),(2,EmptyDstate)],
8.661 + [(1,[]),(2,[])],
8.662 + [(1,[]),(2,[])])
8.663 +> add_proof 1; add_proof 1; !proofs; !dials;
8.664 +val it = 1 : proofID
8.665 +val it = 2 : proofID
8.666 +val it = [(1,[(#,#),(#,#)]),(2,[])] : proofs
8.667 +val it = ([(1,EmptyDstate),(2,EmptyDstate)],
8.668 + [(1,[#,#]),(2,[])],
8.669 + [(1,[#,#]),(2,[])])
8.670 +> val (pt,pos) = (EmptyPtree,[]);
8.671 +> val (pt,_,_) = cappend_problem pt pos [] (empty_ppc_ct',empty_spec) [];
8.672 +
8.673 +> upd_proof 1 2 (EmptyScr,pt,[]);
8.674 +> get_proof 1 1; get_proof 1 2;
8.675 +val it = (EmptyScr,EmptyPtree,[]) : ptree
8.676 +val it = (EmptyScr,Nd (PblObj #,[]),[]) : pstate
8.677 +
8.678 +> upd_dial 1 2 default_dstate [~1,~2] [(1200,[e_dpst])];
8.679 +> get_dstate 1;
8.680 +val it = Dstate
8.681 + {pbls=[[#,#]],rlss=["rearrange_assoc"],
8.682 + rules=["Take","Group","Split_And","Conclude_And","Split_Or","Conclude_Or",
8.683 + "Begin_Trans","End_Trans",...],
8.684 + thms=["add_commute","add_left_commute","add_assoc","mult_commute",
8.685 + "mult_left_commute","mult_assoc"]} : dstate
8.686 +
8.687 +> get_dps 1 1; get_dps 1 2;
8.688 +val it = [] : (cellID * dpstate list) list
8.689 +val it = [(1200,[e_dpst])] : (cellID * dpstate list) list
8.690 +> get_newcells 1 1; get_newcells 1 2;
8.691 +val it = [] : (cellID * cellID) list
8.692 +val it = [(~1,1),(~2,2)] : (cellID * cellID) list
8.693 +
8.694 +> del_proof 2 1; !proofs; !dials;
8.695 +val it = [(1,[(#,#),(#,#)]),(2,[])] : proofs
8.696 +val it = ([(2,EmptyDstate)],[(1,[#,#]),(2,[])],[(1,[#,#]),(2,[])])
8.697 +
8.698 +> del_user 1; !proofs; !dials;
8.699 +val it = [(2,[])] : proofs
8.700 +val it = ([(2,EmptyDstate)],[(2,[])],[(2,[])]) : dials
8.701 +
8.702 +> add_user (); add_user (); !proofs; !dials;
8.703 +val it = 1 : userID
8.704 +val it = 3 : userID
8.705 +val it = [(2,[]),(1,[]),(3,[])] : proofs
8.706 +val it = ([(2,EmptyDstate),(1,EmptyDstate),(3,EmptyDstate)],
8.707 + [(2,[]),(1,[]),(3,[])],
8.708 + [(2,[]),(1,[]),(3,[])]) : dials
8.709 +*)
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/sml/DG/dialog.sml Thu Apr 17 18:01:03 2003 +0200
9.3 @@ -0,0 +1,927 @@
9.4 +(* use"DG/dialog.sml";
9.5 + use"dialog.sml";
9.6 + *)
9.7 +
9.8 +
9.9 +
9.10 +fun set_newcell (c:cellID) (FormKF (_,_,indent,nest,ct')) =
9.11 + FormKF (c, Protect, indent, nest, ct')
9.12 + | set_newcell c (PpcKF (_,_,indent,nest,ppc)) =
9.13 + PpcKF (c, Protect, indent, nest, ppc)
9.14 + | set_newcell _ New_user = New_user; (*for tests*)
9.15 +(*val dpst = (DmtUndef,T,SkipNil,DAundf,
9.16 + DPundef,[],999,ACnew);
9.17 +> val f = FormKF (0,0,empty_cterm');
9.18 +> set_newcell dpst f;
9.19 +val it = FormKF (999,0,"empty_cterm'") : inout
9.20 +*)
9.21 +
9.22 +
9.23 +
9.24 +
9.25 +(*** change dps ***)
9.26 +
9.27 +fun set_dph_dct' c (DPform (r,sf,uf,_)) = DPform (r,sf,uf,c)
9.28 + | set_dph_dct' c (DPrule (sr,ur,_) ) = DPrule (sr,ur,c)
9.29 + | set_dph_dct' c (DPdoneF (m,f,_) ) = DPdoneF (m,f,c)
9.30 + | set_dph_dct' c (DPdoneR (m,f,_) ) = DPdoneR (m,f,c);
9.31 +
9.32 +fun set_dph_dct dct (((c,(dtm,act,dast,cmd,dph,pos))::dps):dps) =
9.33 + ((c,(dtm,act,dast,cmd,set_dph_dct' dct dph,pos))::dps):dps;
9.34 +
9.35 +fun set_done' (DPform (r,sf,uf,c)) =
9.36 + DPdoneF (r, if uf = EmptyFoppFK then sf else Form' (FoPpcFK uf), c)
9.37 + | set_done' (DPrule (sr,ur,c)) =
9.38 + DPdoneR (if ur = e_mstep_ then sr else ur, EmptyMout, c)
9.39 + | set_done' dph = dph;
9.40 +
9.41 +(* 10.1.01
9.42 +fun set_next' (DPform (r,sf,uf,c)) = DPrule (r,e_mstep_,c)
9.43 + | set_next' (DPdoneF (r,f,c)) = DPrule (r,e_mstep_,c)
9.44 + | set_next' (DPrule (sr,ur,c)) = DPform (sr,EmptyMout,EmptyFoppFK,c)
9.45 + | set_next' (DPdoneR (r,f,c)) = DPform (r,f,EmptyFoppFK,c);
9.46 +*)
9.47 +
9.48 +
9.49 +fun set_dast (((c,(dtm,act,_,cmd,dph,pos))::dps):dps) dast =
9.50 + ((c,(dtm,act,dast,cmd,set_done' dph,pos))::dps):dps;
9.51 +
9.52 +fun set_error ((dp as (c,(dtm,act,_,cmd,dph,pos))::dps):dps) =
9.53 + ((c,(dtm,act,ErroR,cmd,dph,pos))::dps):dps;
9.54 + (*~~~ used in continue_pattern*)
9.55 +
9.56 +fun set_done dph pos dast (((c,(dtm,act,_,cmd,_,_))::dps):dps) =
9.57 + ((c,(dtm,act,dast,cmd,dph,pos))::dps):dps;
9.58 +
9.59 +fun set_broken (((c,(dtm,act,_,cmd,dph,pos))::dps):dps) =
9.60 + ((c,(dtm,act,Broken,cmd,dph,pos))::dps):dps;
9.61 + (*~~~ DPform, DPrule used in sel_dtm*)
9.62 +
9.63 +fun set_cmd cmd (((c,(dtm,act,dast,_,dph,pos))::dps):dps) =
9.64 + ((c,(dtm,act,dast,Some cmd,dph,pos))::dps):dps;
9.65 +
9.66 +fun set_broken_cmd cmd (((c,(dtm,act,_,_,dph,pos))::dps):dps) =
9.67 + ((c,(dtm,act,Broken,Some cmd,dph,pos))::dps):dps;
9.68 +
9.69 +(*add to dps due to immediate input of St in resume_*, without adding dat*)
9.70 +fun add_dps (xxx:dpstate) (((c,(dtm,act,dast,cmd,dph,pos))::dps):dps) =
9.71 + ((c,xxx)::(c,(dtm,act,dast,cmd,set_done' dph,pos))::dps):dps;
9.72 +
9.73 +(*add empty head to dps, for recording user_cmd only*)
9.74 +fun add_dps_cmd cmd' (((dp as (c,(dtm,act,dast,cmd,dph,pos)))::dps):dps) =
9.75 +((c,(DtmUndef,ACundef,DAundf,Some cmd',dph,pos))::
9.76 + (c,(dtm,act,dast,cmd,set_done' dph,pos))::dps):dps;
9.77 +
9.78 +(*resume from cmd, no dtm done in do_dtms because of 'NoDtm'*)
9.79 +fun repeat_dtm_cmd cmd' (((c,(dtm,act,_,cmd,dph,pos))::dps):dps) =
9.80 + ((c,(dtm,act,NoDtm,cmd,dph,pos))::
9.81 + (c,(DtmUndef,ACundef,DAundf,Some cmd',dph,pos))::dps):dps;
9.82 +
9.83 +(*add a dtm for do_dtms, without continue_pattern*)
9.84 +fun add_fix dtm act (( (dp as (c,(_,_,_,_,dph,pos)))::dps):dps) =
9.85 + ((c,(dtm,act,FixDtm,None,dph,pos))::dp::dps):dps;
9.86 +
9.87 +
9.88 +
9.89 +
9.90 +
9.91 +(*create a new cellID for the formula to be output*)
9.92 +fun app_dat d ((dp as (c,xxx)::dps):dps) f =
9.93 + let val (d,c) = getdecr_cellID d;
9.94 + in (d, ((c,xxx)::dps):dps, [set_newcell c f]) end;
9.95 +
9.96 +
9.97 +
9.98 +
9.99 +(* 16.4. ------
9.100 +fun nxt_leave (((c,(dtm,act,dast,cmd,dph,pos))::dps):dps) =
9.101 + ((c,(dtm,act,dast,cmd,dph,pos))::dps):dps; *)
9.102 +
9.103 +
9.104 +
9.105 +
9.106 +(** decide if an mstep_ / mstep belongs to a hide_.. list **)
9.107 +
9.108 +fun hide (mI,m) ((pos,_):pos') (p:ptree)
9.109 + (Dstate ({rules = hm, pbls = hp, rlss = hr, thms = ht},_,_,_,_)) =
9.110 + let val _= 1(*writeln("#### hide: mI = "^mI);
9.111 + val _= writeln("#### hide: hm = "^(strs2str hm));
9.112 + val _= writeln("#### hide: mI mem hm = "^(bool2str (mI mem hm)));*)
9.113 + in
9.114 + if mI mem hm orelse
9.115 + (mI mem specsteps
9.116 + andalso (snd3 (get_obj g_spec p pos)) mem hp) then true
9.117 + else case m of
9.118 + Rewrite_Inst (_, (ID,_)) => ID mem ht
9.119 + | Rewrite (ID,_) => ID mem ht
9.120 + | Rewrite_Set_Inst (_, ID) => ID mem hr
9.121 + | Rewrite_Set ID => ID mem hr
9.122 + | _ => false
9.123 + end;
9.124 +(*> val m = ("Add_Given",
9.125 + Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"):mstep_;
9.126 +> val p = ([],Pbl):pos';
9.127 +> proofs:= []; dials:=([],[],[]);
9.128 +> StdinSML 0 0 0 0 New_User;
9.129 +> val ([(1,d)],_,_) = !dials;
9.130 +> StdinSML 1 0 0 0 New_Proof;
9.131 +> val fmz = [];
9.132 +> val (dI',pI',mI') =
9.133 + ("Script.thy",["Script.thy","squareroot","univariate","equation"],
9.134 + ("Script.thy","sqrt-equ-test"));
9.135 +"--- s1 ---";
9.136 +> val (_,1,1,1,[],[PpcKF (_,_,_,_,ppc),req],_) =
9.137 + StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
9.138 +> val [(1,[(1,pt)])] = !proofs; (*hier kommen nicht die aktuellen werte ?!?*)
9.139 +> hide m p pt d;
9.140 +*)
9.141 +
9.142 +
9.143 +
9.144 +
9.145 +fun separable_arg ((ID,m):mstep_) = not (mstep2str m = "");
9.146 +(*> separable_arg (mk_mstep_ (Rewrite ("add_commute","b::rat + a = a + b")));
9.147 +val it = true : bool
9.148 +> separable_arg (mk_mstep_ End_Ruleset);
9.149 +val it = false : bool *)
9.150 +
9.151 +exception DIALOG of string;
9.152 +
9.153 +
9.154 +
9.155 +(*repeat calling ME until nextstep not in hide*)
9.156 +fun me_repeat_hide (m as (mI,mm)) (pos:pos') (c:cid)
9.157 + (p:ptree) (d as Dstate (hid,_,_,_,_)) =
9.158 + let (*val _= writeln("### vor me: m = "^(mstep_2str m));
9.159 + val _= writeln("### vor me: pos= "^(pos'2str pos));
9.160 + val _= writeln("### vor me: ist= "^(istate2str(get_istate p pos)));
9.161 + val _= writeln("### vor me: = "^());*)
9.162 + val (pos,c',f,m' as (mI',mm'),s,p) = me m pos c p;
9.163 + (*val _= writeln("### nach me: pos= "^(pos'2str pos));
9.164 + val _= writeln("### nach me: f = "^(mout2str f));
9.165 + val _= writeln("### nach me: = "^());*)
9.166 + in case f of
9.167 + Error' _ => raise DIALOG ("me_repeat_hide: "^mI
9.168 + ^" resulted in Error'")
9.169 +(* Error' e => (pos,c@c',f,m':mstep_,s,p) 2.5.01*)
9.170 + | _ =>
9.171 + if mm' = Empty_Mstep
9.172 + then (pos,c@c',f,m':mstep_,s,p)
9.173 + else
9.174 + if hide m' pos p d
9.175 + then me_repeat_hide (m':mstep_) pos ((c @ c'):cid) p d
9.176 + else (pos,c@c',f,m':mstep_,s,p)
9.177 + end;
9.178 +
9.179 +
9.180 +
9.181 +(** determine the next datom **)
9.182 +
9.183 +
9.184 +(*for testphase*)
9.185 +fun restrict_dtms SelRule = SelRule (*rule_dtm*)
9.186 + | restrict_dtms dtm =
9.187 + if dtm mem form_dtms then PutRuleRes (*the only form_dtm*)
9.188 + else PutRule; (*rule_dtm*)
9.189 +
9.190 +val form_dtms = [PutRes,FillRes,PutRuleRes,FillRuleRes];
9.191 +
9.192 +fun restrict_dtms dtm act =
9.193 + if dtm mem form_dtms then
9.194 + let val dtm = case dtm of
9.195 + FillRes => PutRes
9.196 + | FillRuleRes => PutRuleRes
9.197 + | x => x;
9.198 + val act = if act = St then Tt else act;
9.199 + in (dtm, act) end
9.200 + else (*rule_dtms*)
9.201 + (case (dtm, act) of
9.202 + (PutRule, St) => (SelRule, St)
9.203 + | (FillRule, St) => (SelRule, St)
9.204 + | xx => xx);
9.205 +
9.206 +
9.207 +fun continue_pattern (((dp as (c, (_, _, _, _, DPdoneR((str,End_Proof'),_,dc),
9.208 + pos)))::dps):dps) _ = (*=========*)
9.209 + ((c,(PutRule,Tt,DAundf,None,DPrule((str,End_Proof'),e_mstep_,dc)
9.210 + ,pos))::dp::dps):dps
9.211 +
9.212 + | continue_pattern ((c, (dtm, act, ErroR, cmd, dph, pos))::dps) d =
9.213 + (c, (dtm, act, DAundf,cmd, dph, pos))::
9.214 + (c, (dtm, act, ErroR, cmd, set_done' dph, pos))::dps
9.215 +
9.216 + | continue_pattern ((dp as (c, (dtm, act, _, _, dph, pos)))::dps) d =
9.217 + let
9.218 + (*val _= writeln("#### continue_pattern, before sel_dtm, dph-dct="^
9.219 + (string_of_int(dct_of dph)));*)
9.220 + val (dph,dtm,act) =
9.221 + sel_dtm dph (get_acti d) (get_speed d);
9.222 + (*val _= writeln("#### continue_pattern, after sel_dtm, dtm+act="^
9.223 + (dtm2str dtm)^"+"^(act2str act));*)
9.224 + val (dtm,act) = restrict_dtms dtm act; (*TODO !!!*)
9.225 + (*val (d,c) = if dtm mem form_dtms then getdecr_cellID d else (d,c);
9.226 + not here !.. in do_dtm may be an ErroR*)
9.227 + (*val _= writeln("#### continue_pattern, after restrict, dtm+act="^
9.228 + (dtm2str dtm)^"+"^(act2str act));(**)
9.229 + (**)val _= writeln("#### continue_pattern, after sel_dtm, dph-dct="^
9.230 + (string_of_int(dct_of dph)));*)
9.231 + in (c,(dtm,act,DAundf,None,dph,pos))::dp::dps end;
9.232 +
9.233 +(* use"DG/dialog.sml";
9.234 + use"dialog.sml";
9.235 + *)
9.236 +
9.237 +
9.238 +
9.239 +(** dialog atoms **)
9.240 +
9.241 + (*PutRule,TskipS -------------- *)
9.242 +fun do_dtm (p:ptree) (d:dstate)
9.243 + ((dp as (c,(PutRule,TskipS,dast,cmd,
9.244 + dph as DPrule (am,um,dc),pos))::dps):dps) =
9.245 + let
9.246 + val ef = get_form am pos p;
9.247 + val (dp,dats) = case ef of
9.248 + Error' e =>
9.249 + (set_error dp,
9.250 + [System("PutRule TskipS failed for \n"^
9.251 + (mstep2str (snd am))^"\n with "^(inout2str e))])
9.252 + | Form' f =>
9.253 + ((*writeln("###% do_dtm PutRule,TskipS");*)
9.254 + (set_done (DPdoneR (am,Form' f,dc)) pos AccepT dp,
9.255 + [RuleKF (EdUndef, snd am)]))
9.256 + | x => raise error ("do_dtm PutRule,TskipS: get_form->"^(mout2str x))
9.257 + in ([]:cellID list, p, dp, d, dats) end
9.258 +
9.259 + (*PutRule,Tt ------------------- *)
9.260 + | do_dtm p d
9.261 + (dp as (c,(PutRule,Tt,dast,cmd,
9.262 + dph as DPrule (am,um,dc),pos))::dps) =
9.263 + ([], p, dp, d, [RuleKF (EdUndef, snd am), Request "Accept ?"])
9.264 +
9.265 + (*PutRule,St ------------------- *)
9.266 + | do_dtm p d
9.267 + (dp as (c,(PutRule,St,dast,cmd,
9.268 + dph as DPrule (am,um,dc),pos))::dps) =
9.269 + ([], p, dp, d, [Request "apply a rule !"])
9.270 +
9.271 + (*SelRule,St ------------------- *)
9.272 + | do_dtm (pst as pt:ptree) d
9.273 + (dp as (c,(SelRule,St,dast,cmd,
9.274 + dph as DPrule (am,um,dc),pos))::dps) =
9.275 + let val sel = sel_rules pt pos;
9.276 + (*val _= writeln("#### SelRule,St: after sel");*)
9.277 + in([], pst, dp, d, [Select sel, Request "select a rule !"]) end
9.278 +
9.279 +
9.280 + (*PutRuleRes,TskipS ------------- *)
9.281 + | do_dtm p d
9.282 + (dp as (_,(PutRuleRes,TskipS,_,_,DPform (sr,_,_,dc), pos))::dps) =
9.283 + let
9.284 + val (pos',cs,ef,m,s,p) = me_repeat_hide sr pos [] p d;
9.285 + (*val _= writeln"### PutRuleRes,TskipS --------------\n";
9.286 + val _= writeln (pr_ptree pr_short (snd3 p));*)
9.287 + val (d, dp, dat) = case ef of
9.288 + Error' e =>
9.289 + let val dp = set_error dp;
9.290 + in (d, dp, [System ("PutRuleRes TskipS failed for \n"^
9.291 + (mstep_2str sr)^"\n with "^(inout2str e))]) end
9.292 + | Form' f =>
9.293 + let
9.294 + val dp = set_done (DPdoneF(m,EmptyMout,dc)) pos' AccepT dp;
9.295 + val (d, dp, dat) = app_dat d dp f;
9.296 + in (d, dp, dat) end;
9.297 + in (cs, p, dp, d, dat) end
9.298 +
9.299 + (*PutRuleRes,Tt ------------- *)
9.300 + | do_dtm p d
9.301 + (dp as (_,(PutRuleRes,Tt,_,_,DPform (sr,Form' f',f,dc), pos))::dps) =
9.302 + let val (d,dp,dat) = app_dat d dp f';
9.303 + in ([], p, dp, d, dat @ [Request "Accept ?"]) end
9.304 +
9.305 + (*PutRes,TskipS ------------- *)
9.306 + | do_dtm p d
9.307 + ((dp as (_,(PutRes,TskipS,_,_,DPform (sr,f',f,dc), pos))::dps):dps) =
9.308 + let
9.309 + val (pos',cs,ef,m,s,p) = me_repeat_hide sr pos [] p d;
9.310 + val (d, dp, dat) = case ef of
9.311 + Error' e =>
9.312 + let val dp = set_error dp;
9.313 + in (d, dp, [System ("PutRuleRes TskipS failed for \n"^
9.314 + (mstep_2str sr)^"\n with "^(inout2str e))]) end
9.315 + | Form' f =>
9.316 + let
9.317 + val dp = set_done (DPdoneF(m,EmptyMout,dc)) pos' AccepT dp;
9.318 + val (d, dp, dat) = app_dat d dp f;
9.319 + in (d, dp, dat) end;
9.320 + in (cs, p, dp, d, dat) end
9.321 +
9.322 + (*PutRes,Tt ------------- *)
9.323 + | do_dtm p d
9.324 + (dp as (_,(PutRes,Tt,_,_,DPform (sr,f',f,dc), pos))::dps) =
9.325 + let val Form' f''' = (case f' of
9.326 + EmptyMout => get_form sr pos p (*a not applicable occurred before*)
9.327 + | f'' => f'');
9.328 + val (d,dp,dat) = app_dat d dp f''';
9.329 + in ([], p, dp, d, dat @ [Request "Accept ?"]) end
9.330 +
9.331 + | do_dtm p d dps =
9.332 + ((*p___:=p; d___:=d; dps___:=dps;*)
9.333 + raise error ("do_dtm not implemented: "^(dps2str dps))
9.334 + );
9.335 +
9.336 +
9.337 +fun mstep_of (DPdoneR ((_, r),_,_)) = r
9.338 + | mstep_of (DPdoneF ((_, r),_,_)) = r
9.339 + | mstep_of (DPrule ((_,sr),(_,ur),_)) = if ur = Empty_Mstep then sr else ur
9.340 + | mstep_of (DPform ((_, r),_,_,_)) = r;
9.341 +
9.342 +fun last_mstep ((dp as ((_,(_,_,_,_,dph,_))::_)):dps) = mstep_of dph;
9.343 +
9.344 +(* val dp=dp';val d=d';
9.345 + (*for recursions: ...*)
9.346 + val cs=cs @ cs';val dats=dats @ dats';
9.347 + *)
9.348 +fun do_dtms cs p (dp as ((_,(_,_,NoDtm,_,_,_)))::_) dats d =
9.349 + (cs, p, dp, d, dats)
9.350 + | do_dtms cs p (dp as ((_,(_,_,FixDtm,_,_,_)))::_) dats d =
9.351 + do_dtm p d dp
9.352 +
9.353 + | do_dtms cs p dp dats d =
9.354 + if last_mstep dp = End_Proof'
9.355 + then (cs, p, dp, d, dats @ [Request "start another example", End_Proof])
9.356 + else
9.357 + let
9.358 + (*val _= writeln("### do_dtms, bef.continue_pattern, d-dct="^
9.359 + ((string_of_int o get_dct) d));(**)
9.360 + (**)val _= writeln("### do_dtms, bef.continue_pattern, dps-dct="^
9.361 + ((string_of_int o last_dct) dp));*)
9.362 + val dp = continue_pattern dp d;
9.363 + (*val _= writeln("### do_dtms, after continue_pat,dp =\n"^(dps2str dp));*)
9.364 + val (cs',p,dp,d,dats') = do_dtm p d dp;
9.365 + (*val _= writeln("### do_dtms,after do_dtm, d-dct="^
9.366 + ((string_of_int o get_dct) d));(**)
9.367 + (**)val _= writeln("### do_dtms,after do_dtm, dps-dct="^
9.368 + ((string_of_int o last_dct) dp));*)
9.369 + (*val _= writeln("### do_dtms, after do_dtm, dp =\n"^(dps2str dp));*)
9.370 + in case hd dp of
9.371 + (_,(_,_,ErroR,_,_,_)) => (cs @ cs', p, dp:dps, d, dats @ dats')
9.372 + | (_,(_,TskipS,_,_,DPdoneR ((_,Empty_Mstep),_,_),_)) =>
9.373 + (cs @ cs', p, dp:dps, d, dats @ dats' (*@
9.374 + [Message "no next step can be proposed"]*))
9.375 + | (_,(_,TskipS,_,_,DPdoneF ((_,Empty_Mstep),_,_),_)) =>
9.376 + (cs @ cs', p, dp:dps, d, dats @ dats' (*@
9.377 + [Message "no next step can be proposed"]*))
9.378 + | (_,(_,TskipS,_,_,_,_)) => do_dtms (cs @ cs') p dp (dats @ dats') d
9.379 + | _ => (cs @ cs', p, dp:dps, d, dats @ dats') end;
9.380 +
9.381 +
9.382 +
9.383 +
9.384 +(*=========St*)
9.385 +(*------------DPrule*)
9.386 +fun resume_St_DPrule_Command (p:ptree) (dp:dps)
9.387 + (d:dstate) (sr:mstep_, ur:mstep_, dc:dct) (cmd':user_cmd) =
9.388 + case cmd' of
9.389 + YourTurn =>
9.390 + ([]:cid, p, set_broken dp, set_acti ~1 d, [])
9.391 + | Rules =>
9.392 + let val ((_,(_,_,_,_,_,pos))::_) = dp;
9.393 + val pt = p;
9.394 + in ([], p, repeat_dtm_cmd Rules dp, d, [Select (sel_rules pt pos)]) end
9.395 + | Auto =>
9.396 + ([], p, ((set_dph_dct 9999) o (add_dps_cmd Auto)) dp,
9.397 + ((set_acti 0) o (set_speed 3(*sel_dtm: formulae + rules*))) d, [])
9.398 + | SpeedPlus =>
9.399 + let val d = incr_speed d;
9.400 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.401 + | SpeedMinus =>
9.402 + let val d = decr_speed d;
9.403 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.404 + | ActivePlus =>
9.405 + let val s = get_acti d;
9.406 + val s = if s > 6 then s else s + 1;
9.407 + in ([], p, repeat_dtm_cmd ActivePlus dp, set_acti s d, [Active s]) end
9.408 + | ActiveMinus =>
9.409 + let val s = get_acti d;
9.410 + val s = if s > 0 then s - 1 else s;
9.411 + in ([], p, repeat_dtm_cmd ActiveMinus dp, set_acti s d, [Active s]) end
9.412 + | _ =>
9.413 + ([], p, dp, d, [System((cmd2str (Some cmd'))^
9.414 + " not impl. in resume_St_DPrule_Command")]);
9.415 +(*St:data ... cmd not expected*)
9.416 +(*example,howcomes,whatfor: dpst ganz neu
9.417 + forward,back,undo ???
9.418 + yourturn,myturn,dontknow, notaccept: continue variiert
9.419 + accept: einfach wiederholen
9.420 + notaccept=dontknow:
9.421 + rules: liefert vorbereitende Infor f"ur curr.dtm
9.422 + *)
9.423 +
9.424 +fun resume_St_DPrule_FoPpcFK (p:ptree) (dp:dps) (d:dstate)
9.425 + (sr:mstep_,ur:mstep_,dc:dct) (f:foppFK) =
9.426 + (*wechsle dph auf 1,
9.427 + applicable -> 2b, not -> 2a*)
9.428 + ([]:cid, p, dp, d, [System"resume_St_DPrule_FoPpcFK not impl."]);
9.429 +
9.430 +fun resume_St_DPrule_RuleFK (p:ptree)
9.431 + ((dp as (c, (dtm,act,dast,cmd,dph,pos))::dps):dps)
9.432 + (d:dstate) (sr:mstep_, ur:mstep_ , dc:dct) (r:mstep) =
9.433 + let
9.434 + (*val _= writeln("####### resume_St_DPrule_RuleFK, begin");*)
9.435 + val m = mk_mstep_ r;
9.436 + val ef = get_form m pos p;
9.437 + val (dp',dats) = case ef of
9.438 + Error' e =>
9.439 + let val dp = set_error dp;
9.440 + in (dp, [Error_ (inout2str e)]) end
9.441 + | Form' f =>
9.442 + let val dp = set_done (DPdoneR(m,Form' f,dc)) pos AccepT dp;
9.443 + in (dp, []) end;
9.444 + in ([], p, dp', d, dats) end;
9.445 +
9.446 +
9.447 +(*------------DPform*)
9.448 +fun resume_St_DPform_Command p
9.449 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.450 + d (au,sf,uf,dc) cmd' =
9.451 + (*S:data ... cmd not expected*)
9.452 + (*example,howcomes,whatfor: sinnvoll !
9.453 + forward,back,undo ???
9.454 + yourturn: dhpase bleibt, act -> Tt
9.455 + myturn: ??
9.456 + dontknow, notaccept:
9.457 + accept: gleiche dph wiederholen
9.458 + notaccept: ??
9.459 + rules: zur"uck auf DPrule, sinnvoll
9.460 + *)
9.461 + ([]:cid, p, dp:dps , d,[System"resume_St_DPform_Command not impl."]);
9.462 +
9.463 +fun resume_St_DPform_FoPpcFK p
9.464 + ((dp as (c, (dtm, act, (*skip,*) dast, cmd, dph, pos))::dps):dps)
9.465 + d (au,sf,uf,dc) f =
9.466 + (*normalfall: wenn f =(parsed)= DPform (_,f),
9.467 + dann
9.468 + val ( , ,f, , ) = me_repeat_hide ... (18.12.99)
9.469 +
9.470 +
9.471 + let val (pos, cs, ef, m, s, p) =
9.472 + me_repeat_hide (mk_mstep_ f) pos [c] p d;
9.473 + in case ef of
9.474 + Error' e =>
9.475 + | Form' mo => raise DIALOG "test"
9.476 + *)
9.477 + ([]:cid, p, dp:dps, d, [System"resume_St_DPform_FoPpcFK not impl."]);
9.478 +
9.479 +fun resume_St_DPform_RuleFK p
9.480 + ((dp as (c, (dtm, act, (*skip,*) dast, dmc, dph, pos))::dps):dps)
9.481 + d (au,sf,uf,dc) r =
9.482 + (*geht im selben dstep zur"uck auf 2a | 2ai*)
9.483 + ([]:cid, p, dp:dps , d, [System"resume_St_DPform_RuleFK not impl."]);
9.484 +
9.485 +
9.486 +(*=========Tt*)
9.487 +(*------------DPrule*)
9.488 +fun resume_Tt_DPrule_Command p
9.489 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.490 + d (sr,ur,dc:dct) cmd' =
9.491 + (*St:ackonwledge ... cmd expected*)
9.492 + (*example,howcomes,whatfor,dontknow:
9.493 + forward,back,undo ???
9.494 + notaccept: sinnvoll -- pattern "T: explains 'howcomes'
9.495 + rules: die andgeforderte r droht ur zu "uberschreiben
9.496 + im n"achsten Schritt (nicht hier in diesem
9.497 + *)
9.498 + case cmd' of
9.499 + Accept =>
9.500 + let val ef = get_form sr pos p;
9.501 + val (dp',dats) = case ef of
9.502 + Error' e =>
9.503 + let val dp = set_error dp;
9.504 + in (dp, [System (*Tt !!!*) (inout2str e)]) end
9.505 + | Form' f =>
9.506 + let val dp = set_done (DPdoneR (sr, Form' f, dc))
9.507 + pos AccepT dp;
9.508 + in (dp, []) end;
9.509 + in ([], p, dp', d, dats) end
9.510 + | Rules => (*Broken @@@*)
9.511 + let val dp' = ((add_fix SelRule St) o (set_broken_cmd Rules)) dp;
9.512 + in ([], p, dp', d, []) end
9.513 + | YourTurn => (*implicit Accept*)
9.514 + let val ef = get_form sr pos p;
9.515 + val (dp',dats) = case ef of
9.516 + Error' e =>
9.517 + let val dp = set_error dp;
9.518 + in (dp, [System (*Tt !!!*) (inout2str e)]) end
9.519 + | Form' f =>
9.520 + let val dp = set_cmd YourTurn dp;
9.521 + val dp = set_done (DPdoneR (sr, Form' f, dc))
9.522 + pos AccepT dp;
9.523 + in (dp, []) end;
9.524 + in ([], p, dp', d, dats) end
9.525 + | Auto =>
9.526 + ([], p, ((set_dph_dct 9999) o (add_dps_cmd Auto)) dp,
9.527 + ((set_speed 3) o (set_acti 0)) d, [])
9.528 + | SpeedPlus => (*implicit Accept ??? NOT CLEAR !!!31.10.00*)
9.529 + let val d = incr_speed d;
9.530 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.531 + | SpeedMinus =>
9.532 + let val d = decr_speed d;
9.533 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.534 + | ActivePlus => (*previous dtm once more*)
9.535 + let val s = get_acti d;
9.536 + val s = if s > 6 then s else s + 1;
9.537 + in ([], p, repeat_dtm_cmd ActivePlus dp, set_acti s d, [Active s]) end
9.538 + | ActiveMinus =>
9.539 + let val s = get_acti d;
9.540 + val s = if s > 0 then s - 1 else s;
9.541 + in ([], p, repeat_dtm_cmd ActiveMinus dp, set_acti s d, [Active s]) end
9.542 + | cc =>
9.543 + ([]:cid, p, dp:dps, d,
9.544 + [System ("resume_Tt_DPrule_Command: not impl. for "^
9.545 + (cmd2str (Some cc)))]);
9.546 +
9.547 +fun resume_Tt_DPrule_FoPpcFK p
9.548 + ((dp as (c, (dtm, act, (*skip,*) dast, cmd, dph, pos))::dps):dps)
9.549 + d (sr,ur,dc:dct) f =
9.550 + (*implicit S:Accept f"ur sr?ur, check new f*)
9.551 + ([]:cid, p, dp:dps, d, [System"resume_Tt_DPrule_FoPpcFK not impl."]);
9.552 +
9.553 +
9.554 +fun resume_Tt_DPrule_RuleFK p
9.555 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.556 + d (sr,ur,dc:dct) r =
9.557 + (*r "uberschreibt ur *)
9.558 + let
9.559 + val m = mk_mstep_ r;
9.560 + val ef = get_form m pos p;
9.561 + val (dp',dats) = case ef of
9.562 + Error' e =>
9.563 + (set_error dp, [Error_ (inout2str e)])
9.564 + | Form' f =>
9.565 + (if m = sr
9.566 + then (set_done (DPdoneR(m,Form' f,dc)) pos AccepT dp, [])
9.567 + else (((add_dps (PutRule,St,AccepT,Some MyTurn,
9.568 + DPdoneR (m,Form' f,dc),pos)) o set_broken) dp,
9.569 + []));
9.570 + in ([], p, dp', d, dats) end;
9.571 +
9.572 +
9.573 +(*Tt presented a formula, St answered with command*)
9.574 +fun resume_Tt_DPform_Command p
9.575 + ((dp as (c, (dtm, act, dast, cmd, _, pos))::dps):dps)
9.576 + d (au,sf,uf,_) cmd' =
9.577 + (*example,howcomes,whatfor,dontknow:
9.578 + forward,back,undo ???
9.579 + yourturn,myturn: impl.S:accept ! *)
9.580 + (*notaccept: sinnvoll -- pattern "Tt: explains 'howcomes'
9.581 + rules: impl.S:accept !
9.582 + *)
9.583 + case cmd' of
9.584 + Accept => (* sf proposed by ME, gen.by au, thus error-check superfluous *)
9.585 + let (*val _= writeln("#### resume_Tt_DPform_Command");*)
9.586 + val (pos,cs,ef,m,s,p) = me_repeat_hide au pos [] p d;
9.587 + val (dp,dats) = case ef of
9.588 + Error' e =>
9.589 + let val dp = set_error dp;
9.590 + in (dp, [Error_ (inout2str e)]) end
9.591 + | Form' f =>
9.592 + let val dp = set_done(DPdoneF(m, EmptyMout, get_dct d)) pos AccepT dp
9.593 + in (dp, []) end
9.594 + in ([], p, dp, d, dats) end
9.595 + | Rules => (*implicit Accept*)
9.596 + let val (pos,cs,ef,m,s,p) = me_repeat_hide au pos [] p d;
9.597 + val (dp,dats) = case ef of
9.598 + Error' e =>
9.599 + let val dp = set_error dp;
9.600 + in (dp, [Error_ (inout2str e)]) end
9.601 + | Form' f =>
9.602 + let val dp =
9.603 + ((add_dps (SelRule,St,FixDtm,None,DPrule(m,e_mstep_,0),pos)) o
9.604 + (set_cmd Rules) o
9.605 + (set_done (DPdoneF (m, EmptyMout, get_dct d)) pos AccepT))dp;
9.606 + in (dp, []) end
9.607 + in ([], p, dp, d, dats) end
9.608 + | YourTurn => (*implicit Accept*)
9.609 + let val (pos,cs,ef,m,s,p) = me_repeat_hide au pos [] p d;
9.610 + val (dp,dats) = case ef of
9.611 + Error' e =>
9.612 + let val dp = set_error dp;
9.613 + in (dp, [Error_ (inout2str e)]) end
9.614 + | Form' f =>
9.615 + let val dp = set_done(DPdoneF(m, EmptyMout, get_dct d)) pos AccepT dp
9.616 + in (dp, []) end
9.617 + in ([], p, dp, d, dats) end
9.618 + | Auto =>
9.619 + ([], p, ((set_dph_dct 9999) o (add_dps_cmd Auto)) dp,
9.620 + ((set_speed 3) o (set_acti 0)) d, [])
9.621 + | SpeedPlus => (*implicit Accept ??? NOT CLEAR !!!31.10.00*)
9.622 + let val d = incr_speed d;
9.623 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.624 + | SpeedMinus =>
9.625 + let val d = decr_speed d;
9.626 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.627 + | ActivePlus => (*previous dtm once more*)
9.628 + let val s = get_acti d;
9.629 + val s = if s > 6 then s else s + 1;
9.630 + in ([], p, repeat_dtm_cmd ActivePlus dp, set_acti s d, [Active s]) end
9.631 + | ActiveMinus =>
9.632 + let val s = get_acti d;
9.633 + val s = if s > 0 then s - 1 else s;
9.634 + in ([], p, repeat_dtm_cmd ActiveMinus dp, set_acti s d, [Active s]) end
9.635 + | _ =>
9.636 + ([], p, dp, d, [System((cmd2str (Some cmd'))^
9.637 + " not impl. in resume_St_DPrule_Command")]);
9.638 +
9.639 +
9.640 +
9.641 +
9.642 +
9.643 +
9.644 +(* use"DG/dialog.sml";
9.645 + use"dialog.sml";
9.646 + *)
9.647 +
9.648 +
9.649 +
9.650 +fun resume_Tt_DPform_FoPpcFK p
9.651 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.652 + d (au,sf,uf,dc) f =
9.653 + (*implic.St:accept der sf, abschliessen, check f*)
9.654 + ([]:cid, p, dp:dps, d, [System"resume_Tt_DPform_FoPpcFK not impl."]);
9.655 +
9.656 +
9.657 +(* val (dp as (c, (dtm, act, dast, cmd, dph, pos))::dps)=dp;
9.658 + resume_Tt_DPform_RuleFK p
9.659 + (((c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.660 + d (au,sf,uf,dc) r;
9.661 + *)
9.662 +(*Tt presented a formula sf, asking 'Accept ?' | 'Select a rule !' ...,
9.663 + St answers with Rule r, supposed to be applied to sf (implicit accept)*)
9.664 +fun resume_Tt_DPform_RuleFK p
9.665 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.666 + d (au,sf,uf,dc) r =
9.667 + let
9.668 + (*val _= writeln("###% resume_dpst T DPform RuleFK, dc = "^
9.669 + (string_of_int dc));*)
9.670 + val dp = set_dast dp AccepT; (*implicit accept !*)
9.671 + val (pos,cs,ef,m,s,p) = me_repeat_hide au pos [] p d;(*14.10.00 repeat?!?*)
9.672 + in case ef of
9.673 + Error' e =>
9.674 + ([]:cid, p, set_error dp, d,
9.675 + [System ("resume_Tt_DPform_RuleFK failed for \n"^
9.676 + (mstep_2str au)^"\n with "^(inout2str e))])
9.677 + | Form' f =>
9.678 + (* val Form' f=ef;
9.679 + *)
9.680 + let val m = mk_mstep_ r;
9.681 + in case get_form m pos p of
9.682 + Error' e =>
9.683 + ([], p, add_dps (PutRule,St,ErroR,Some MyTurn,
9.684 + (*DPdoneR (m,EmptyMout,dc),pos) dp 2.Feb.01*)
9.685 + DPrule (au, m, dc), pos) dp,
9.686 + d, [Error_ (inout2str e)])
9.687 + | Form' f =>
9.688 + ((*writeln("###% resume_dpst T DPform RuleFK, dc = "^
9.689 + (string_of_int dc));*)
9.690 + ([],p, add_dps (PutRule,St,AccepT,Some MyTurn,
9.691 + DPdoneR (m,Form' f,dc),pos) dp, d, []))
9.692 + end
9.693 + end;
9.694 +
9.695 +(*=========TskipS, 2.5.01*)
9.696 +(*------------Command*)
9.697 +(*2.5.01: weiter nach Auto -> helpless: voriges result schon in pt*)
9.698 +fun resume_TskipS_DPdoneF_Command p
9.699 + ((dp as (c, (dtm, act, dast, cmd, _, pos))::dps):dps) d cmd' =
9.700 + case cmd' of
9.701 + Accept => ([], p, repeat_dtm_cmd Accept dp, d, [])
9.702 + | Rules => ([], p, ((add_fix SelRule St) o (set_broken_cmd Rules)) dp, d, [])
9.703 + | YourTurn => ([], p, repeat_dtm_cmd YourTurn dp, d,
9.704 + [Message "no next step can be proposed"])
9.705 + | Auto => ([], p, repeat_dtm_cmd YourTurn dp, d,
9.706 + [Error_ "no next step can be proposed"])
9.707 + | SpeedPlus =>
9.708 + let val d = incr_speed d;
9.709 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.710 + | SpeedMinus =>
9.711 + let val d = decr_speed d;
9.712 + in ([], p, repeat_dtm_cmd SpeedPlus dp, d, [Speed (get_speed d)]) end
9.713 + | ActivePlus => (*previous dtm once more*)
9.714 + let val s = get_acti d;
9.715 + val s = if s > 6 then s else s + 1;
9.716 + in ([], p, repeat_dtm_cmd ActivePlus dp, set_acti s d, [Active s]) end
9.717 + | ActiveMinus =>
9.718 + let val s = get_acti d;
9.719 + val s = if s > 0 then s - 1 else s;
9.720 + in ([], p, repeat_dtm_cmd ActiveMinus dp, set_acti s d, [Active s]) end
9.721 + | cc =>
9.722 + ([]:cid, p, dp:dps, d,
9.723 + [System ("resume_Tt_DPrule_Command: not impl. for "^
9.724 + (cmd2str (Some cc)))]);
9.725 +
9.726 +
9.727 +
9.728 +(*2.5.01: weiter nach Auto -> helpless: voriges result schon in pt*)
9.729 +fun resume_TskipS_DPdoneF_RuleFK p
9.730 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps) d r =
9.731 + let val m = mk_mstep_ r;
9.732 + val dc = get_dct' d;
9.733 + in case get_form m pos p of
9.734 + Error' e =>
9.735 + ([], p, add_dps (PutRule,St,ErroR,None,
9.736 + DPrule (e_mstep_, m, dc), pos) dp,
9.737 + d, [Error_ (inout2str e)])
9.738 + | Form' f =>
9.739 + ((*writeln("###% resume_dpst T DPform RuleFK, dc = "^
9.740 + (string_of_int dc));*)
9.741 + ([],p, add_dps (PutRule,St,AccepT,Some MyTurn,
9.742 + DPdoneR (m,Form' f,dc),pos) dp, d, []))
9.743 + end;
9.744 +
9.745 +
9.746 +(* val (dp as (c, (dtm, act, dast, cmd, dph, pos))::dps)=dp;
9.747 + resume_dpst (p:ptree)(((c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.748 + (d:dstate) (dat:inout);
9.749 + *)
9.750 +(*resume from St-input*)
9.751 +fun resume_dpst (p:ptree)
9.752 + ((dp as (c, (dtm, act, dast, cmd, dph, pos))::dps):dps)
9.753 + (d:dstate) (dat:inout) =
9.754 + let val dph' = init_dct d dph;
9.755 + (*val _= writeln("### resume_dpst begin,dct= "^(string_of_int(dct_of dph')));*)
9.756 + in case act of
9.757 + St => (*input from St:data *)
9.758 + (case dph' of (*dph is as left before prompt St:*)
9.759 + DPrule (sr,ur,dc) =>
9.760 + (case dat of
9.761 + Command cmd' => (*St:data ... cmd' not expected*)
9.762 + resume_St_DPrule_Command p dp d (sr,ur,dc) cmd'
9.763 + | FoPpcFK f =>
9.764 + resume_St_DPrule_FoPpcFK p dp d (sr,ur,dc) f
9.765 + | RuleFK r => (* usecase 2/4 *)
9.766 + resume_St_DPrule_RuleFK p dp d (sr,ur,dc) r)
9.767 + | DPform (au,sf,uf,dc) =>
9.768 + (case dat of
9.769 + Command cmd' => (*S:data ... cmd' not expected*)
9.770 + resume_St_DPform_Command p dp d (au,sf,uf,dc) cmd'
9.771 + | FoPpcFK f =>
9.772 + resume_St_DPform_FoPpcFK p dp d (au,sf,uf,dc) f
9.773 + | RuleFK r =>
9.774 + resume_St_DPform_RuleFK p dp d (au,sf,uf,dc) r)
9.775 + | _ => raise DIALOG "TODO dhpase 2ai")
9.776 + | Tt => (*input from S:ackowledge*)
9.777 + (case dph' of (*dph is as left before prompt St:*)
9.778 + DPrule (sr,ur,dc) =>
9.779 + (case dat of
9.780 + Command cmd' => (*St:ackonwledge ... cmd' expected*)
9.781 + resume_Tt_DPrule_Command p dp d (sr,ur,dc) cmd'
9.782 + | FoPpcFK f =>
9.783 + resume_Tt_DPrule_FoPpcFK p dp d (sr,ur,dc) f
9.784 + | RuleFK r =>
9.785 + resume_Tt_DPrule_RuleFK p dp d (sr,ur,dc) r)
9.786 + | DPform (au,sf,uf,dc) =>
9.787 + (case dat of
9.788 + Command cmd' => (*St:ackonwledge ... cmd' expected*)
9.789 + resume_Tt_DPform_Command p dp d (au,sf,uf,dc) cmd'
9.790 + | FoPpcFK f =>
9.791 + resume_Tt_DPform_FoPpcFK p dp d (au,sf,uf,dc) f
9.792 + | RuleFK r =>
9.793 + (*val DPform (au,sf,uf,dc)=dph';
9.794 + val RuleFK r=dat;
9.795 + *)
9.796 + resume_Tt_DPform_RuleFK p dp d (au,sf,uf,dc) r)
9.797 + | _ => raise error "TODO dhpase 2ai")
9.798 + | TskipS => (*if do_dtms left due Empty_Mstep,2.5.01*)
9.799 + (case dph' of (*dph is as left before prompt St:*)
9.800 + DPrule (sr,ur,dc) =>
9.801 + (case dat of
9.802 + Command cmd' => (*St:ackonwledge ... cmd' expected*)
9.803 + resume_Tt_DPrule_Command p dp d (sr,ur,dc) cmd'
9.804 + | FoPpcFK f =>
9.805 + resume_Tt_DPrule_FoPpcFK p dp d (sr,ur,dc) f
9.806 + | RuleFK r =>
9.807 + resume_Tt_DPrule_RuleFK p dp d (sr,ur,dc) r)
9.808 + | DPform (au,sf,uf,dc) =>
9.809 + (case dat of
9.810 + Command cmd' => (*St:ackonwledge ... cmd' expected*)
9.811 + resume_Tt_DPform_Command p dp d (au,sf,uf,dc) cmd'
9.812 + | FoPpcFK f =>
9.813 + resume_Tt_DPform_FoPpcFK p dp d (au,sf,uf,dc) f
9.814 + | RuleFK r =>
9.815 + (*val DPform (au,sf,uf,dc)=dph';
9.816 + val RuleFK r=dat;
9.817 + *)
9.818 + resume_Tt_DPform_RuleFK p dp d (au,sf,uf,dc) r)
9.819 + | DPdoneF _ =>
9.820 + (case dat of
9.821 + Command cmd' => resume_TskipS_DPdoneF_Command p dp d cmd'
9.822 + | FoPpcFK f => raise error "TODO resume_TskipS_DPdoneF_FoPpcFK"
9.823 + | RuleFK r => resume_TskipS_DPdoneF_RuleFK p dp d r
9.824 + )
9.825 + | _ => raise error "TskipS => TODO dhpase 2ai")
9.826 + | _ => ([]:cid, p, dp, d,
9.827 + [System ("failed to resume "^
9.828 + ((pair2str o (apfst string_of_int) o
9.829 + (apsnd dpst2str)) (hd dp)))]) end;
9.830 +
9.831 +
9.832 +
9.833 +
9.834 +
9.835 +fun init_dpst (c:cellID) (Init_Proof e) (d:dstate as Dstate (_,acti,speed,_,_)) =
9.836 + let
9.837 + val m = mk_mstep_(Init_Proof e);
9.838 + (*val d = default_dstate; 30.10.00 -> New_User*)
9.839 + (*val ef = get_form m e_pos' empty_pstate;*)
9.840 + val (pos,cs,ef,m,s,p) = me_repeat_hide m e_pos' [] EmptyPtree d;
9.841 + val (dp',dats) = case ef of
9.842 + Error' err =>
9.843 + ([(c,(PutRule, TskipS, ErroR, None,
9.844 + DPdoneR(mk_mstep_ (Init_Proof e),EmptyMout,0),([],Pbl)))],
9.845 + [Error_ "example not accept"])
9.846 + | Form' f =>
9.847 + ([(c,(PutRule, TskipS, AccepT, None,
9.848 + DPdoneR(mk_mstep_ (Init_Proof e),Form' f,(get_dct d)-1),(*TskipS*)
9.849 + ([],Pbl)))],
9.850 + []);
9.851 + in ([]:cellID list, p, dp', d, dats @ [Active acti, Speed speed]) end;
9.852 +
9.853 +
9.854 +
9.855 +
9.856 +
9.857 +
9.858 +(*in dps one cellID may address several dpst;
9.859 + the dpsts are _PRE_pended during history of dialog,
9.860 + thus the latest worked on is in front of the others;
9.861 +
9.862 + in case an elder cellID has been touched on the FE
9.863 + the dpst found is made the head of the dps*)
9.864 +fun dpst_athead (dps:dps,c) =
9.865 + let
9.866 + fun ass done ([],c) =
9.867 + raise error ("call_DG_ME: acellID "^(string_of_int c)^" is unknown")
9.868 + | ass done ((ci, xi) :: pairs, c:cellID) =
9.869 + if c = ci
9.870 + then ((ci, xi) :: (done @ pairs)):dps
9.871 + else ass (done @ [(ci, xi)]) (pairs, c);
9.872 + in ass [] (dps,c) end;
9.873 +(* val dps = [(3,e_dpst),(2,e_dpst),(1,e_dpst)]:dps;
9.874 +> dpst_athead (dps,2);
9.875 +val it =
9.876 + [(2,(Prompt,Tt,SkipUdf,DAundf,None,DPdone,(#,#))),
9.877 + (3,(Prompt,Tt,SkipUdf,DAundf,None,DPdone,(#,#))),
9.878 + (1,(Prompt,Tt,SkipUdf,DAundf,None,DPdone,(#,#)))] : dps *)
9.879 +
9.880 +
9.881 +(*11.10.00:call_DG_ME
9.882 +args:
9.883 + p :
9.884 + dp :
9.885 + d :
9.886 + ac : cellID (known in dps) above the current cellID
9.887 + c : current cellID (generated by FE)
9.888 + dat:
9.889 +values:
9.890 + cs :
9.891 + dats:
9.892 + ns : ////after 23.5.00
9.893 + p :
9.894 + dp :
9.895 + d :
9.896 +*)
9.897 +(* val p=get_proof uI pI;val dp=get_dps uI pI;val d=get_dstate uI;
9.898 + val (ac,c)=(acI,cI);
9.899 +*)
9.900 +fun call_DG_ME (p:ptree) (dp:dps) (d:dstate)
9.901 + (ac:cellID, c:cellID) (dat:inout) =
9.902 + case dat of
9.903 + (RuleFK (Init_Proof e)) =>
9.904 + let val (cs,p,dp',d',dats) = init_dpst c (Init_Proof e) d;
9.905 + (*val _ = writeln("## call_DG_ME,nach init_dpst, d-dct="^
9.906 + ((string_of_int o get_dct) d'));(**)
9.907 + (**)val _ = writeln("## call_DG_ME,nach init_dpst, dps-dct="^
9.908 + ((string_of_int o last_dct) dp'));*)
9.909 + (*val _= writeln("###% call_DG_ME: after init_dpst | resume_dpst, dp'=\n"^
9.910 + (dps2str dp'));*)
9.911 + (*val _= writeln("###% call_DG_ME: after init_dpst | resume_dpst, d'= "^
9.912 + (d2str d'));*)
9.913 + in do_dtms cs p dp' dats d' end
9.914 + | _ =>
9.915 + let val dp as ((_,(_,_,_,_,_,pos))::_) = dpst_athead (dp,ac);
9.916 + in if pos = ([],Res)
9.917 + then ([], p, dp, d, [Message "end of example"])
9.918 + else let val (cs,p,dp',d',dats) = resume_dpst p dp d dat;
9.919 + (*val _ = writeln("## call_DG_ME,nach resume_dpst, d-dct="^
9.920 + ((string_of_int o get_dct) d'));
9.921 + (**)val _ = writeln("## call_DG_ME,nach resume_dpst, dps-dct="^
9.922 + ((string_of_int o last_dct) dp'));*)
9.923 + (*val _= writeln("###% call_DG_ME end, dp' =\n"^(dps2str dp'));*)
9.924 + (* val d = update_dstate ... TODO*)
9.925 + in do_dtms cs p dp' dats d' end
9.926 + end;
9.927 +
9.928 +
9.929 +(* use"DG/dialog.sml";
9.930 + *)
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/sml/IsacKnowledge/Atools.ML Thu Apr 17 18:01:03 2003 +0200
10.3 @@ -0,0 +1,441 @@
10.4 +(* tools for arithmetic
10.5 + WN.8.3.01
10.6 + use"../knowledge/Atools.ML";
10.7 + use"knowledge/Atools.ML";
10.8 + use"Atools.ML";
10.9 + *)
10.10 +
10.11 +(*
10.12 +copy from doc/math-eng.tex WN.28.3.03
10.13 +
10.14 +\section{Coding standards}
10.15 +\subsection{Rule sets}
10.16 +The actual version of the coding standards for rulesets is in {\tt /Isa02/Tools.ML} where it can be viewed using the knowledge browsers.
10.17 +
10.18 +There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below.
10.19 +\begin{description}
10.20 +
10.21 +\item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents).
10.22 +
10.23 +\item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents) such, that the rewrites can be presented to the student.
10.24 +
10.25 +\item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with numerical constants only (i.e. all terms which can be expressed by the definitions of the respective theory and the respective parent theories). In particular, this ruleset includes evaluating in/equalities with numerical constants only.
10.26 +
10.27 +\end{description}
10.28 +The following rulesets are used for internal purposes and usually invisible to the (naive) user:
10.29 +\begin{description}
10.30 +
10.31 +\item [*\_erls]
10.32 +\item [*\_prls]
10.33 +\item [*\_srls]
10.34 +
10.35 +\end{description}
10.36 +{\tt append_rls, merge_rls, remove_rls}
10.37 +*)
10.38 +
10.39 +"******* Atools.ML begin *******";
10.40 +theory' := overwritel (!theory', [("Atools.thy",Atools.thy)]);
10.41 +
10.42 +(** evaluation of numerals and special predicates on the meta-level **)
10.43 +(*-------------------------functions---------------------*)
10.44 +local (* rlang 09.02 *)
10.45 + (*.a 'c is coefficient of v' if v does occur in c.*)
10.46 + fun coeff_in v c = v mem (vars c);
10.47 +in
10.48 + fun occurs_in v t = coeff_in v t;
10.49 +end;
10.50 +
10.51 +(*("occurs_in", ("Atools.occurs'_in", eval_occurs'_in ""))*)
10.52 +fun eval_occurs_in _ _
10.53 + (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
10.54 + ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
10.55 + writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
10.56 + if occurs_in v t
10.57 + then Some ((term2str p) ^ " = True",
10.58 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
10.59 + else Some ((term2str p) ^ " = True",
10.60 + Trueprop $ (mk_equality (p, HOLogic.false_const))))
10.61 + | eval_occurs_in _ _ _ _ = None;
10.62 +
10.63 +(*evaluate 'is_atom'*)
10.64 +(*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
10.65 +fun eval_is_atom (thmid:string) _ (t as (Const(op0,_) $ arg)) thy =
10.66 + (case arg of
10.67 + Free (n,_) => Some (mk_thmid thmid op0 n "",
10.68 + Trueprop $ (mk_equality (t, true_as_term)))
10.69 + | _ => Some (mk_thmid thmid op0 "" "",
10.70 + Trueprop $ (mk_equality (t, false_as_term))))
10.71 + | eval_is_atom _ _ _ _ = None;
10.72 +
10.73 +(*evaluate 'is_even'*)
10.74 +fun even i = (i div 2) * 2 = i;
10.75 +(*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
10.76 +fun eval_is_even (thmid:string) _ (t as (Const(op0,_) $ arg)) thy =
10.77 + (case arg of
10.78 + Free (n,_) =>
10.79 + (case int_of_str n of
10.80 + Some i =>
10.81 + if even i then Some (mk_thmid thmid op0 n "",
10.82 + Trueprop $ (mk_equality (t, true_as_term)))
10.83 + else Some (mk_thmid thmid op0 "" "",
10.84 + Trueprop $ (mk_equality (t, false_as_term)))
10.85 + | _ => None)
10.86 + | _ => None)
10.87 + | eval_is_even _ _ _ _ = None;
10.88 +
10.89 +(*evaluate 'is_const'*)
10.90 +(*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
10.91 +fun eval_const (thmid:string) _ (t as (Const(op0,t0) $ arg)) (thy:theory) =
10.92 + (case arg of
10.93 + Const (n1,_) =>
10.94 + Some (mk_thmid thmid op0 n1 "",
10.95 + Trueprop $ (mk_equality (t, false_as_term)))
10.96 + | Free (n1,_) =>
10.97 + if is_numeral n1
10.98 + then Some (mk_thmid thmid op0 n1 "",
10.99 + Trueprop $ (mk_equality (t, true_as_term)))
10.100 + else Some (mk_thmid thmid op0 n1 "",
10.101 + Trueprop $ (mk_equality (t, false_as_term)))
10.102 + | _ => None)
10.103 + | eval_const _ _ _ _ = None;
10.104 +
10.105 +(*. evaluate binary, associative, commutative operators: *,+,^ .*)
10.106 +(*("plus" ,("op +" ,eval_binop "#add_")),
10.107 + ("times" ,("op *" ,eval_binop "#mult_")),
10.108 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))*)
10.109 +
10.110 +(* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
10.111 + ("xxxxxx",op_,t,thy);
10.112 + *)
10.113 +fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
10.114 + thmid ^ "Float ((" ^
10.115 + (string_of_int v11)^","^(string_of_int v12)^"), ("^
10.116 + (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
10.117 + (string_of_int v21)^","^(string_of_int v22)^"), ("^
10.118 + (string_of_int p21)^","^(string_of_int p22)^"))";
10.119 +
10.120 +fun eval_binop (thmid:string) (op_:string)
10.121 + (t as ( Const(op0,t0) $
10.122 + (Const(op0',t0') $ v $ t1) $ t2))
10.123 + thy = (*binary . (v.n1).n2*)
10.124 + if op0 = op0' then
10.125 + case (numeral t1, numeral t2) of
10.126 + (Some n1, Some n2) =>
10.127 + let val (T1,T2,Trange) = dest_binop_typ t0
10.128 + val res = calc op0 n1 n2
10.129 + val rhs = var_op_float v op_ t0 T1 res
10.130 + val prop = Trueprop $ (mk_equality (t, rhs))
10.131 + in Some (mk_thmid_f thmid n1 n2, prop) end
10.132 + | _ => None
10.133 + else None
10.134 + | eval_binop (thmid:string) (op_:string)
10.135 + (t as
10.136 + (Const (op0, t0) $ t1 $
10.137 + (Const (op0', t0') $ t2 $ v)))
10.138 + thy = (*binary . n1.(n2.v)*)
10.139 + if op0 = op0' then
10.140 + case (numeral t1, numeral t2) of
10.141 + (Some n1, Some n2) =>
10.142 + let val (T1,T2,Trange) = dest_binop_typ t0
10.143 + val res = calc op0 n1 n2
10.144 + val rhs = float_op_var v op_ t0 T1 res
10.145 + val prop = Trueprop $ (mk_equality (t, rhs))
10.146 + in Some (mk_thmid_f thmid n1 n2, prop) end
10.147 + | _ => None
10.148 + else None
10.149 +
10.150 + | eval_binop (thmid:string) (op_:string)
10.151 + (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
10.152 + (case (numeral t1, numeral t2) of
10.153 + (Some n1, Some n2) =>
10.154 + let val (T1,T2,Trange) = dest_binop_typ t0;
10.155 + val res = calc op0 n1 n2;
10.156 + val rhs = term_of_float Trange res;
10.157 + val prop = Trueprop $ (mk_equality (t, rhs));
10.158 + in Some (mk_thmid_f thmid n1 n2, prop) end
10.159 + | _ => None)
10.160 + | eval_binop _ _ _ _ = None;
10.161 +(*
10.162 +> val Some (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
10.163 +> term2str t;
10.164 +val it = "-1 + 2 = 1"
10.165 +> val t = str2term "-1 * (-1 * a)";
10.166 +> val Some (thmid, t) = eval_binop "#mult_" "op *" t thy;
10.167 +> term2str t;
10.168 +val it = "-1 * (-1 * a) = 1 * a"*)
10.169 +
10.170 +
10.171 +
10.172 +(*.evaluate < and <= for numerals.*)
10.173 +(*("le" ,("op <" ,eval_equ "#less_")),
10.174 + ("leq" ,("op <=" ,eval_equ "#less_equal_"))*)
10.175 +fun eval_equ (thmid:string) (op_:string) (t as
10.176 + (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
10.177 + (case (int_of_str n1, int_of_str n2) of
10.178 + (Some n1', Some n2') =>
10.179 + if calc_equ (strip_thy op0) (n1', n2')
10.180 + then Some (mk_thmid thmid op0 n1 n2,
10.181 + Trueprop $ (mk_equality (t, true_as_term)))
10.182 + else Some (mk_thmid thmid op0 n1 n2,
10.183 + Trueprop $ (mk_equality (t, false_as_term)))
10.184 + | _ => None)
10.185 +
10.186 + | eval_equ _ _ _ _ = None;
10.187 +
10.188 +
10.189 +(*evaluate identity
10.190 +> reflI;
10.191 +val it = "(?t = ?t) = True"
10.192 +> val t = str2term "x = 0";
10.193 +> val None = rewrite_ thy dummy_ord e_rls false reflI t;
10.194 +
10.195 +> val t = str2term "1 = 0";
10.196 +> val None = rewrite_ thy dummy_ord e_rls false reflI t;
10.197 +----------- thus needs Calc !
10.198 +> val t = str2term "0 = 0";
10.199 +> val Some (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
10.200 +> term2str t';
10.201 +val it = "True"
10.202 +
10.203 +val t = str2term "Not (x = 0)";
10.204 +atomt t; term2str t;
10.205 +*** -------------
10.206 +*** Const ( Not)
10.207 +*** . Const ( op =)
10.208 +*** . . Free ( x, )
10.209 +*** . . Free ( 0, )
10.210 +val it = "x ~= 0" : string*)
10.211 +
10.212 +(*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
10.213 + the arguments: thus this Calculation MUST be at the head of an rls*)
10.214 +(*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
10.215 +fun eval_ident (thmid:string) (op_:string) (t as
10.216 + (Const (op0,t0) $ t1 $ t2 )) thy =
10.217 + if t1 = t2
10.218 + then Some (mk_thmid thmid op0
10.219 + ("("^(Sign.string_of_term (sign_of thy) t1)^")")
10.220 + ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
10.221 + Trueprop $ (mk_equality (t, true_as_term)))
10.222 + else Some (mk_thmid thmid op0
10.223 + ("("^(Sign.string_of_term (sign_of thy) t1)^")")
10.224 + ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
10.225 + Trueprop $ (mk_equality (t, false_as_term)))
10.226 + | eval_ident _ _ _ _ = None;
10.227 +(* TODO
10.228 +> val t = str2term "x =!= 0";
10.229 +> val Some (str, t') = eval_ident "ident_" "b" t thy;
10.230 +> term2str t';
10.231 +val str = "ident_(x)_(0)" : string
10.232 +val it = "(x =!= 0) = False" : string
10.233 +> val t = str2term "1 =!= 0";
10.234 +> val Some (str, t') = eval_ident "ident_" "b" t thy;
10.235 +> term2str t';
10.236 +val str = "ident_(1)_(0)" : string
10.237 +val it = "(1 =!= 0) = False" : string
10.238 +> val t = str2term "0 =!= 0";
10.239 +> val Some (str, t') = eval_ident "ident_" "b" t thy;
10.240 +> term2str t';
10.241 +val str = "ident_(0)_(0)" : string
10.242 +val it = "(0 =!= 0) = True" : string
10.243 +*)
10.244 +
10.245 +(*.evaluate identity of terns, which stay ready for evaluation in turn;
10.246 + thus returns False only for numerals.*)
10.247 +(*("equal" ,("op =",eval_equal "#equal_")):calc*)
10.248 +fun eval_equal (thmid:string) (op_:string) (t as
10.249 + (Const (op0,t0) $ t1 $ t2 )) thy =
10.250 + if t1 = t2
10.251 + then Some (mk_thmid thmid op0
10.252 + ("("^(Sign.string_of_term (sign_of thy) t1)^")")
10.253 + ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
10.254 + Trueprop $ (mk_equality (t, true_as_term)))
10.255 + else (case (is_num t1, is_num t2) of
10.256 + (true, true) =>
10.257 + if free2int t1 = free2int t2
10.258 + then Some (mk_thmid thmid op0
10.259 + ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
10.260 + Trueprop $ (mk_equality (t, true_as_term)))
10.261 + else Some (mk_thmid thmid op0
10.262 + ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
10.263 + Trueprop $ (mk_equality (t, false_as_term)))
10.264 + | _ => None)
10.265 + | eval_equal _ _ _ _ = None;
10.266 +(*
10.267 +> val t = str2term "(x + 1) = (x + 1)";
10.268 +> val Some (str, t') = eval_equal "equal_" "b" t thy;
10.269 +> term2str t';
10.270 +val str = "equal_(x + 1)_(x + 1)" : string
10.271 +val it = "(x + 1 = x + 1) = True" : string
10.272 +> val t = str2term "x = 0";
10.273 +> val None = eval_equal "equal_" "b" t thy;
10.274 +
10.275 +> val t = str2term "1 = 0";
10.276 +> val Some (str, t') = eval_equal "equal_" "b" t thy;
10.277 +> term2str t';
10.278 +val str = "equal_(1)_(0)" : string
10.279 +val it = "(1 = 0) = False" : string
10.280 +> val t = str2term "0 = 0";
10.281 +> val Some (str, t') = eval_equal "equal_" "b" t thy;
10.282 +> term2str t';
10.283 +val str = "equal_(0)_(0)" : string
10.284 +val it = "(0 = 0) = True" : string
10.285 +*)
10.286 +
10.287 +
10.288 +(** evaluation on the metalevel **)
10.289 +
10.290 +(*. evaluate HOL.divide .*)
10.291 +(*("divide_" ,("HOL.divide" ,eval_cancel "#divide_"))*)
10.292 +fun eval_cancel (thmid:string) _ (t as
10.293 + (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
10.294 + (case (int_of_str n1, int_of_str n2) of
10.295 + (Some n1', Some n2') =>
10.296 + let
10.297 + (*val _= writeln"@@@ eval_cancel Some";*)
10.298 + val sg = sign2 n1' n2';
10.299 + val (T1,T2,Trange) = dest_binop_typ t0;
10.300 + val gcd' = gcd (abs n1') (abs n2');
10.301 + in if gcd' = abs n2'
10.302 + then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
10.303 + val prop = Trueprop $ (mk_equality (t, rhs))
10.304 + in Some (mk_thmid thmid op0 n1 n2, prop) end
10.305 + else if 0 < n2' andalso gcd' = 1 then None
10.306 + else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
10.307 + ((abs n2') div gcd')
10.308 + val prop = Trueprop $ (mk_equality (t, rhs))
10.309 + in Some (mk_thmid thmid op0 n1 n2, prop) end
10.310 + end
10.311 + | _ => ((*writeln"@@@ eval_cancel None";*)None))
10.312 +
10.313 + | eval_cancel _ _ _ _ = None;
10.314 +
10.315 +
10.316 +local
10.317 +
10.318 +open Term;
10.319 +
10.320 +in
10.321 +fun termlessI (_:subst) uv = termless uv;
10.322 +fun term_ordI (_:subst) uv = term_ord uv;
10.323 +end;
10.324 +
10.325 +
10.326 +(** rule set, for evaluating list-expressions in scripts 8.01.02
10.327 +
10.328 +val simprls =
10.329 + Rls{preconds = [], rew_ord = ("tless_true",tless_true),
10.330 + rules = [Calc ("Atools.ident",eval_ident "#ident_"),
10.331 + Calc ("Atools.Var",eval_var "#Var_"),
10.332 + Calc ("Atools.Length",eval_Length "#Length_"),
10.333 + Calc ("Atools.Nth",eval_Nth "#Nth_"),
10.334 + Calc ("op <",eval_equ "#less_"),
10.335 + Calc ("op <=",eval_equ "#less_equal_"),
10.336 + Calc ("Atools.ident",eval_ident "#ident_"),
10.337 +
10.338 + Thm ("if_True",num_str if_True),
10.339 + Thm ("if_False",num_str if_False)
10.340 + ],
10.341 + scr = Script ((term_of o the o (parse thy))
10.342 + "empty_script")
10.343 + }:rls; *)
10.344 +
10.345 +(** rule set for evaluating listexpr in scripts FIXXXME -> ListG.ML**)
10.346 +val list_rls =
10.347 + Rls{id="list_rls",preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
10.348 + erls = e_rls, srls = Erls, calc = [], asm_thm=[],
10.349 + rules = (*8.01: copied from*)
10.350 + [Thm ("length_Nil_",num_str length_Nil_),
10.351 + Thm ("length_Cons_",num_str length_Cons_),
10.352 +(* Thm ("",),
10.353 + Thm ("",),
10.354 + Thm ("",),
10.355 + Thm ("",),
10.356 +*)
10.357 + Calc ("op *",eval_binop "#mult_"),
10.358 + Calc ("op +", eval_binop "#add_"),
10.359 +
10.360 + Calc ("Atools.ident",eval_ident "#ident_"),
10.361 + Calc ("Atools.Var",eval_var "#Var_"),
10.362 + Calc ("Atools.Length",eval_Length "#Length_"),(*8.01 Thm length_Nil_ !*)
10.363 + Calc ("Atools.Nth",eval_Nth "#Nth_"), (*8.01 Thm nth_Cons_ !!*)
10.364 + Calc ("op <",eval_equ "#less_"),
10.365 + Calc ("op <=",eval_equ "#less_equal_"),
10.366 + Calc ("Atools.ident",eval_ident "#ident_"),
10.367 +
10.368 + Thm ("if_True",num_str if_True),
10.369 + Thm ("if_False",num_str if_False)
10.370 + ], scr = EmptyScr}:rls;
10.371 +
10.372 +ruleset' := overwritel (!ruleset',
10.373 + [("list_rls",list_rls)
10.374 + ]);
10.375 +
10.376 +val tless_true = dummy_ord;
10.377 +rew_ord' := overwritel (!rew_ord',
10.378 + [("tless_true", tless_true)]);
10.379 +
10.380 +val calculate_Atools =
10.381 + append_rls "calculate_Atools" e_rls
10.382 + [Calc ("op <",eval_equ "#less_"),
10.383 + Calc ("op <=",eval_equ "#less_equal_"),
10.384 + Calc ("op =",eval_equal "#equal_"),
10.385 +
10.386 + Thm ("real_unari_minus",num_str real_unari_minus),
10.387 + Calc ("op +",eval_binop "#add_"),
10.388 + Calc ("op -",eval_binop "#subtract_"),
10.389 + Calc ("op *",eval_binop "#mult_")
10.390 + ];
10.391 +
10.392 +val Atools_erls =
10.393 + append_rls "Atools_erls" e_rls
10.394 + [Thm ("not_true",num_str not_true),
10.395 + Thm ("not_false",num_str not_false),
10.396 + Thm ("and_true",and_true),
10.397 + Thm ("and_false",and_false),
10.398 + Thm ("or_true",or_true),
10.399 + Thm ("or_false",or_false)
10.400 + ];
10.401 +
10.402 +(*val atools_erls = waere zu testen ...
10.403 + merge_rls calculate_Atools
10.404 + (append_rls Atools_erls (*i.A. zu viele rules*)
10.405 + [Calc ("Atools.ident",eval_ident "#ident_"),
10.406 + Calc ("Atools.is'_const",eval_const "#is_const_"),
10.407 + Calc ("Atools.occurs'_in",
10.408 + eval_occurs_in "#occurs_in"),
10.409 + Calc ("Tools.matches",eval_matches "#matches")
10.410 + ] (*i.A. zu viele rules*)
10.411 + );*)
10.412 +val atools_erls =
10.413 + Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
10.414 + erls = e_rls, srls = Erls, calc = [], asm_thm = [],
10.415 + rules = [Thm ("refl",num_str refl),
10.416 + Thm ("le_refl",num_str le_refl),
10.417 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
10.418 + Thm ("not_true",num_str not_true),
10.419 + Thm ("not_false",num_str not_false),
10.420 + Thm ("and_true",and_true),
10.421 + Thm ("and_false",and_false),
10.422 + Thm ("or_true",or_true),
10.423 + Thm ("or_false",or_false),
10.424 + Thm ("and_commute",num_str and_commute),
10.425 + Thm ("or_commute",num_str or_commute),
10.426 +
10.427 + Calc ("op <",eval_equ "#less_"),
10.428 + Calc ("op <=",eval_equ "#less_equal_"),
10.429 +
10.430 + Calc ("Atools.ident",eval_ident "#ident_"),
10.431 + Calc ("Atools.is'_const",eval_const "#is_const_"),
10.432 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
10.433 + Calc ("Tools.matches",eval_matches "")
10.434 + ],
10.435 + scr = Script ((term_of o the o (parse thy))
10.436 + "empty_script")
10.437 + }:rls;
10.438 +ruleset' := overwritel
10.439 + (!ruleset',
10.440 + [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
10.441 + ]);
10.442 +"******* Atools.ML end *******";
10.443 +
10.444 +
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/sml/IsacKnowledge/Atools.thy Thu Apr 17 18:01:03 2003 +0200
11.3 @@ -0,0 +1,58 @@
11.4 +(* tools for arithmetic
11.5 + WN.8.3.01
11.6 +
11.7 + remove_thy"Atools";
11.8 + use_thy_only"knowledge/Atools";
11.9 + use_thy"knowledge/Atools";
11.10 + use_thy"knowledge/Isac";
11.11 +
11.12 +
11.13 + use"ROOT.ML";
11.14 + cd"knowledge";
11.15 +*)
11.16 +
11.17 +
11.18 +Atools = Complex + Descript +
11.19 +
11.20 +(*-------------------- consts------------------------------------------------*)
11.21 +consts
11.22 +
11.23 + Arbfix, Undef :: real
11.24 + dummy :: real
11.25 +
11.26 + occurs'_in :: "[real, real] => bool" ("_ occurs'_in _")
11.27 +
11.28 + "pow" :: [real, real] => real (infixr "^^^" 80)
11.29 +(* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
11.30 + ~~~~ ~~~~ ~~~~ ~~~*)
11.31 + "abs" :: real => real ("(|| _ ||)")
11.32 +(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
11.33 + "absset":: real set => real ("(||| _ |||)")
11.34 + (*is numeral constant ?*)
11.35 + "is'_const" :: real => bool ("_ is'_const" 10)
11.36 + "is'_atom" :: real => bool ("_ is'_atom" 10)
11.37 + "is'_even" :: real => bool ("_ is'_even" 10)
11.38 +
11.39 + (* identity on term level*)
11.40 + "ident" :: ['a, 'a] => bool ("(_ =!=/ _)" [51, 51] 50)
11.41 +
11.42 +
11.43 +
11.44 +(*-------------------- rules------------------------------------------------*)
11.45 +rules (*for evaluating the assumptions of conditional rules*)
11.46 +
11.47 + real_unari_minus "- a = (-1) * a"
11.48 +
11.49 + rle_refl "(n::real) <= n"
11.50 +(*reflI "(t = t) = True"*)
11.51 + radd_left_cancel_le "((k::real) + m <= k + n) = (m <= n)"
11.52 + not_true "(~ True) = False"
11.53 + not_false "(~ False) = True"
11.54 + and_true "(a & True) = a"
11.55 + and_false "(a & False) = False"
11.56 + or_true "(a | True) = True"
11.57 + or_false "(a | False) = a"
11.58 + and_commute "(a & b) = (b & a)"
11.59 + or_commute "(a | b) = (b | a)"
11.60 +
11.61 +end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/sml/ROOT.ML Thu Apr 17 18:01:03 2003 +0200
12.3 @@ -0,0 +1,144 @@
12.4 +(* Compilation of isac, wn.7.3.01
12.5 +
12.6 + ======================= system setup from scratch, wn.7.3.01 ==========
12.7 + source modified: Isa99.WN/src/Pure/thm.ML
12.8 + Isa99.WN/src/HOL/Tools/numeral_syntax.ML
12.9 +
12.10 + === HOL + "Anderungen --- " ---: INSTALL, dann aufruf mit ...
12.11 + /usr/local/sw/sml/Isabelle99/bin/isabelle
12.12 +
12.13 + === HOL-Real *.html:
12.14 + cd /usr/local/sw/sml/Isabelle99/src/HOL/
12.15 + /usr/local/sw/sml/Isabelle99/bin/isatool usedir -i true HOL Real/
12.16 + (*5 min! erg"anzt HOL/index.html mit Session*)
12.17 +
12.18 + === HOL-Real binaries:
12.19 + /usr/local/sw/sml/Isabelle99/bin/isatool make HOL-Real
12.20 + (*Building Pure(0:02:28) HOL (0:08:44) HOL-Real (0:05:32 elapsed time)*)
12.21 + =======================================================================
12.22 +
12.23 +startup
12.24 + cd ~/isabelle/heaps/smlnj-110_x86-linux/
12.25 + sml @SMLload=02-HOL-Real-isac
12.26 +
12.27 + cd"~/develop/sml/";
12.28 + use"ROOT.ML";
12.29 +
12.30 +=====================
12.31 +
12.32 +thy.html:
12.33 + cd ~/ME99/
12.34 + /usr/local/sw/sml/Isabelle99/bin/isatool usedir -i true HOL-Real isac/
12.35 + (*contents.html: FullCollectionHead -> None*)
12.36 +
12.37 +save image:
12.38 + cd"~/isabelle/heaps/smlnj-110_x86-linux/";
12.39 + SMLofNJ.exportML"HOL-Real-isac020702-richard";
12.40 + chmod u+x HOL-Real-isac020702-richard-linux
12.41 +*)
12.42 +
12.43 +
12.44 +Compiler.Control.Print.printDepth:=6; (*4 default*)
12.45 +Compiler.Control.Print.printDepth:=5; (*4 default*)
12.46 +Compiler.Control.Print.printDepth:=4; (*4 default*)
12.47 +Compiler.Control.Print.printLength:=999; (*8 default*)
12.48 +Compiler.Control.Print.stringDepth:=250; (*250 default*)
12.49 +
12.50 +(*this function from Isabelle2002/src/Pure/library.ML
12.51 + is covered by fn : term list -> term -> term list -> term list
12.52 + reestablish it again here*)
12.53 +(* cd"~/develop/isac/";
12.54 + *)
12.55 +fun find_first _ [] = None
12.56 + | find_first pred (x :: xs) =
12.57 + if pred x then Some x else find_first pred xs;
12.58 +
12.59 +use"library.sml";
12.60 +use"definitions.sml";
12.61 +cd "Scripts";
12.62 + use"term_G.sml";
12.63 + use"calculate.sml";
12.64 + use"rewrite.sml";
12.65 + use"reverse-rew.sml";
12.66 + use_thy"Script"; (*+ ListG,Tools*)
12.67 +(* cd"Isa02";
12.68 + remove_thy"ListG";
12.69 + *)
12.70 + use"scrtools.sml";
12.71 + cd "..";
12.72 +use"globals.sml";
12.73 +cd "ME";
12.74 + use"mstools.sml";
12.75 + use"sequent.sml";
12.76 + use"ptyps.sml";
12.77 + use"modspec.sml";
12.78 + use"generate.sml";
12.79 + use"appl.sml";
12.80 + use"script.sml";
12.81 + use"solve.sml";
12.82 + cd "..";
12.83 +"******* build ME complete *******";
12.84 +use"DG-ME-states.sml";
12.85 +cd "DG";
12.86 + use"dialog.sml";
12.87 + cd "..";
12.88 +use"print_exn_G.sml";
12.89 +use"stdin-out.sml";
12.90 +"******* build ME & DG complete *******";
12.91 +
12.92 +cd "IsacKnowledge";
12.93 + use_thy"Isac";
12.94 +(* remove_thy"Typefix";
12.95 + use_thy"knowledge/Isac";
12.96 + *)
12.97 + cd "../";
12.98 +"******* build ME & DG complete, knowledge added *******";
12.99 +
12.100 +cd"kbtest";
12.101 + use"complex.sml";
12.102 + use"diff.sml";
12.103 + use"diffapp.sml";
12.104 + use"float.sml";
12.105 + (*use"inssort.sml"; problems with recdef in Isabelle2002*)
12.106 + use"logexp.sml";
12.107 + use"poly.sml";
12.108 + (*use"polyeq.sml"; WN.7.3.03 nach 'nested' rewrite_set*)
12.109 + (*use"rateq.sml"; WN.7.3.03 nach 'nested' rewrite_set*)
12.110 + use"ratrooteq.sml";
12.111 + use"rational.sml";
12.112 + use"root.sml";
12.113 + use"rooteq.sml";
12.114 + (*use"rlang.sml"; -------------------intermediate---- *)
12.115 + use"termorder.sml";
12.116 + use"trig.sml";
12.117 + use"vect.sml";
12.118 + "******* kbtests complete *******";
12.119 + cd "../";
12.120 +
12.121 +cd "systest";
12.122 + use"calculate.sml";
12.123 + use"details.sml";
12.124 + use"list_rls.sml";
12.125 + use"refine.sml";
12.126 + use"root-equ.sml";
12.127 + use"script.sml";
12.128 + (* use"script_if.sml"; missing: is_rootequation_in*)
12.129 + use"scriptnew.sml";
12.130 + use"subp-rooteq.sml";
12.131 + use"FE-KE.sml";
12.132 + (**)
12.133 + use"testdaten.sml";
12.134 + proofs:= []; dials:=([],[],[]);
12.135 + "******* systests complete *******";
12.136 + cd "../";
12.137 +
12.138 +Compiler.Control.Print.printDepth:=9; (*4 default*)
12.139 +Compiler.Control.Print.printDepth:=4; (*4 default*)
12.140 +Compiler.Control.Print.printLength:=8; (*8 default*)
12.141 +Compiler.Control.Print.printLength:=9999; (*8 default*)
12.142 +Compiler.Control.Print.stringDepth:=9999; (*250 default*)
12.143 +
12.144 +(*
12.145 +val ttt = (term_of o the o (parse thy))
12.146 + "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2";
12.147 +*)
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/sml/definitions.sml Thu Apr 17 18:01:03 2003 +0200
13.3 @@ -0,0 +1,312 @@
13.4 +(* data-definitions, which should not occur in code-files to be re-evaluated
13.5 + use"definitions.sml";
13.6 + *)
13.7 +
13.8 +type cterm' = string;
13.9 +val empty_cterm' = "empty_cterm'";
13.10 +type thmID = string;
13.11 +type thm' = thmID * cterm';
13.12 +type rls' = string;
13.13 +
13.14 +(*.fun calculate_ fetches the evaluation-function via this list.*)
13.15 +(*ie. there is NO rewriting involved in contrary to eval_rls*)
13.16 +type calc =
13.17 + (string * (*op in calculate_ from scripts*)
13.18 + (string * (*op in isa-term 'Const(op,_)' *)
13.19 + (string -> term -> theory -> (string * term) option))); (*eval_fun*)
13.20 +fun e_evalfn (_:'a) (_:term) (_:theory) = None:(string * term) option;
13.21 +
13.22 +type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
13.23 +type subst = (term * term) list; (*here for ets2str*)
13.24 +fun subst2str (s:subst) =
13.25 + (strs2str o
13.26 + (map (pair2str o
13.27 + (apsnd (Sign.string_of_term (sign_of thy))) o
13.28 + (apfst (Sign.string_of_term (sign_of thy)))))) s;
13.29 +
13.30 +
13.31 +
13.32 +datatype rule =
13.33 + Thm of (string * thm)
13.34 +| Calc of string * (*check for equality*)
13.35 + (string -> term -> theory -> (string * term) option)
13.36 +| Rls_ of rls (*.ie. rule sets may be nested.*)
13.37 +and scr =
13.38 + EmptyScr
13.39 + | Script of term (*for meth'*)
13.40 + | Rfuns of {init_state : term ->
13.41 + (term * (*the current formula:
13.42 + goes locate_gen -> next_tac via istate*)
13.43 + term * (*the final formula*)
13.44 + rule list (*of reverse rewrite set (#1#)*)
13.45 + list * (*may be serveral, eg. in norm_rational*)
13.46 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
13.47 + (term * (*... rewrite with ...*)
13.48 + term list)) (*... assumptions*)
13.49 + list), (*derivation from given term to normalform
13.50 + in reverse order with sym_thm;
13.51 + (#1#) could be extracted from here #1*)
13.52 +
13.53 + normal_form: term -> (term * term list) option,
13.54 + locate_rule: rule list list -> term -> rule
13.55 + -> (rule * (term * term list)) list,
13.56 + next_rule : rule list list -> term -> rule option,
13.57 + attach_form: rule list list -> term -> term
13.58 + -> (rule * (term * term list)) list}
13.59 +and rls =
13.60 + Erls (*for init e_rls*)
13.61 + | Rls of {id : string, (*for trace_rewrite:=true*)
13.62 + preconds : term list, (*unused 20.8.02*)
13.63 + rew_ord : string * (subst -> (term * term) -> bool),(*for rules*)
13.64 + erls : rls, (*for the conditions in rules*)
13.65 + (* '^ because of rewrite in applicable_in;
13.66 + compare type meth'; FIXXME take name as string into Rls !*)
13.67 + srls : rls, (*for evaluation of list_fns in script*)
13.68 + calc : calc list, (*for Calculate in scr*)
13.69 + asm_thm : thm' list, (*FIXXME remove with put_asm*)
13.70 + rules : rule list,
13.71 + scr : scr} (*Script term (how to restrict type ???)*)
13.72 + | Seq of {id : string, (*for trace_rewrite:=true*)
13.73 + preconds : term list, (*unused 20.8.02*)
13.74 + rew_ord : string * (subst -> (term * term) -> bool),(*for rules*)
13.75 + erls : rls, (*for the conditions in rules*)
13.76 + (* '^ because of rewrite in applicable_in;
13.77 + compare type meth'; FIXXME take name as string into Rls !*)
13.78 + srls : rls, (*for evaluation of list_fns in script*)
13.79 + calc : calc list, (*for Calculate in scr*)
13.80 + asm_thm : thm' list, (*FIXXME remove with put_asm*)
13.81 + rules : rule list,
13.82 + scr : scr} (*Script term (how to restrict type ???)*)
13.83 + | Rrls of {id : string, (*for trace_rewrite:=true*)
13.84 + prepat : (term list *
13.85 + (*preconds, eval with subst from pattern*)
13.86 + term ) (*pattern matched in subterms*)
13.87 + list, (*meta-conjunction is or*)
13.88 + rew_ord : string * (subst -> (term * term) -> bool),(*for rules*)
13.89 + erls : rls, (*for the conditions in rules and pat*)
13.90 + (* '^ because of rewrite in applicable_in
13.91 + compare type meth'*)
13.92 + calc : calc list, (*for Calculate in scr*)
13.93 + asm_thm : thm' list, (*FIXXME remove with put_asm*)
13.94 + scr : scr}; (*Rfuns {...} (how to restrict type ???)*)
13.95 +(*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
13.96 + from rls, and then contain both Script _AND_ Rfuns !!!*)
13.97 +
13.98 +
13.99 +
13.100 +val e_rule = Thm ("refl",refl) : rule;
13.101 +fun id_of_thm (Thm (id, _)) = id
13.102 + | id_of_thm _ = raise error "id_of_thm";
13.103 +fun thm_of_thm (Thm (_, thm)) = thm
13.104 + | thm_of_thm _ = raise error "thm_of_thm";
13.105 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
13.106 +fun rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thm thm)^")"
13.107 + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
13.108 + | rule2str (Rls_ _) = "Rls_ rls";(*FIXXME*)
13.109 +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
13.110 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
13.111 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
13.112 + | eqrule _ = false;
13.113 +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
13.114 + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
13.115 + | memrls r _ = raise error ("memrls: incomplete impl. r= "^(rule2str r));
13.116 +
13.117 +
13.118 +type rrlsstate = (*state for reverse rewriting*)
13.119 + (term * (*the current formula:
13.120 + goes locate_gen -> next_tac via istate*)
13.121 + term * (*the final formula*)
13.122 + rule list (*of reverse rewrite set (#1#)*)
13.123 + list * (*may be serveral, eg. in norm_rational*)
13.124 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
13.125 + (term * (*... rewrite with ...*)
13.126 + term list)) (*... assumptions*)
13.127 + list); (*derivation from given term to normalform
13.128 + in reverse order with sym_thm;
13.129 + (#1#) could be extracted from here #1*)
13.130 +val e_type = Type("empty",[]);
13.131 +val a_type = TFree("'a",[]);
13.132 +val e_term = Const("empty",e_type);
13.133 +val a_term = Free("empty",a_type);
13.134 +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
13.135 +
13.136 +
13.137 +
13.138 +
13.139 +(*22.2.02: ging auf Linux nicht (Stefan)
13.140 +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
13.141 +val e_term = Const("empty", Type("'a", []));
13.142 +val e_scr = Script e_term;
13.143 +
13.144 +
13.145 +(*ad thm':
13.146 + there are two kinds of theorems ...
13.147 + (1) known by isabelle
13.148 + (2) not known, eg. calc_thm, instantiated rls
13.149 + the latter have a thmid "#..."
13.150 + and thus outside isa we ALWAYS transport both(thmid,string_of_thm)
13.151 + and have a special assoc_thm / assoc_rls in this interface *)
13.152 +type theory' = string; (* = domID ^".thy" *)
13.153 +fun string_of_thy thy =
13.154 +((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory';
13.155 +val theory2domID = string_of_thy;
13.156 +val theory2theory' = string_of_thy;
13.157 +
13.158 +type rew_ord' = string;
13.159 +
13.160 +val theory' = ref ([]:(theory' * theory) list);
13.161 +val rew_ord' = ref ([]:(rew_ord' * (subst -> (term * term) -> bool)) list);
13.162 +val ruleset' = ref ([]:(string * rls) list);
13.163 +val theorem' = ref ([]:(string * thm) list);
13.164 +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
13.165 +local
13.166 + fun ii (_:term) = e_rrlsstate;
13.167 + fun no (_:term) = Some (e_term,[e_term]);
13.168 + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
13.169 + fun ne (_:rule list list) (_:term) = Some e_rule;
13.170 + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
13.171 +in
13.172 +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
13.173 + next_rule=ne,attach_form=fo};
13.174 +end;
13.175 +
13.176 +
13.177 +
13.178 +fun dummy_ord (_:subst) (_:term,_:term) = true;
13.179 +val e_rls =
13.180 + Rls{id = "e_rls",
13.181 + preconds = [],
13.182 + rew_ord = ("dummy_ord", dummy_ord),
13.183 + erls = Erls,srls = Erls,
13.184 + calc = [],
13.185 + asm_thm = [],
13.186 + rules = [], scr = EmptyScr}:rls;
13.187 +val e_rrls = Rrls {id = "e_rrls",
13.188 + prepat = [],
13.189 + rew_ord = ("dummy_ord", dummy_ord),
13.190 + erls = Erls,
13.191 + calc = [],
13.192 + asm_thm=[],
13.193 + scr=e_rfuns}:rls;
13.194 +ruleset' := overwritel (!ruleset', [("e_rls",e_rls),
13.195 + ("e_rrls",e_rrls)
13.196 + ]);
13.197 +
13.198 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,asm_thm,rules,scr}) =
13.199 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
13.200 + asm_thm=asm_thm,rules=rules,scr=scr}
13.201 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,asm_thm,rules,scr}) =
13.202 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
13.203 + asm_thm=asm_thm,rules=rules,scr=scr}
13.204 + | rep_rls (Rls {id,...}) =
13.205 + raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)
13.206 + | rep_rls (Seq {id,...}) =
13.207 + raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
13.208 +fun rep_rrls
13.209 + (Rrls {id,asm_thm, calc, erls, prepat, rew_ord,
13.210 + scr=Rfuns
13.211 + {attach_form,init_state,locate_rule,
13.212 + next_rule,normal_form}}) =
13.213 + {id=id,asm_thm=asm_thm, calc=calc, erls=erls, prepat=prepat,
13.214 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
13.215 + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
13.216 + | rep_rrls (Rls {id,...}) =
13.217 + raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
13.218 + | rep_rrls (Seq {id,...}) =
13.219 + raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
13.220 +(*.id requested for all, Rls,Seq,Rrls.*)
13.221 +fun id_rls (Rls {id,...}) = id
13.222 + | id_rls (Seq {id,...}) = id
13.223 + | id_rls (Rrls {id,...}) = id;
13.224 +
13.225 +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.226 + asm_thm=at,rules =rs,scr=sc}) r =
13.227 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.228 + asm_thm=at,rules = rs @ r,scr=sc}:rls)
13.229 + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.230 + asm_thm=at,rules =rs,scr=sc}) r =
13.231 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.232 + asm_thm=at,rules = rs @ r,scr=sc}:rls)
13.233 + | append_rls id (Rrls _) _ = raise error
13.234 + ("append_rls: not for reverse-rewrite-rule-set "^id);
13.235 +
13.236 +fun eq_rule (Thm thm1, Thm thm2) = thm1 = thm2
13.237 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
13.238 + | eq_rule _ = false;
13.239 +
13.240 +fun merge_rls _ Erls rls = rls
13.241 + | merge_rls _ rls Erls = rls
13.242 + | merge_rls id
13.243 + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
13.244 + asm_thm=at1,rules =rs1,scr=sc1})
13.245 + r2 =
13.246 + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
13.247 + rew_ord=ro1,erls=(*merge_rls er1 er2*)er1,
13.248 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
13.249 + ((#srls o rep_rls) r2),
13.250 + calc=ca1 @ ((#calc o rep_rls) r2),
13.251 + asm_thm=at1 @ ((#asm_thm o rep_rls) r2),
13.252 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
13.253 + scr=sc1}:rls)
13.254 + | merge_rls id
13.255 + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
13.256 + asm_thm=at1,rules =rs1,scr=sc1})
13.257 + r2 =
13.258 + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
13.259 + rew_ord=ro1,erls=(*merge_rls er1 er2*)er1,
13.260 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
13.261 + ((#srls o rep_rls) r2),
13.262 + calc=ca1 @ ((#calc o rep_rls) r2),
13.263 + asm_thm=at1 @ ((#asm_thm o rep_rls) r2),
13.264 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
13.265 + scr=sc1}:rls)
13.266 + | merge_rls _ _ _ = raise error
13.267 + "merge_rls: not for reverse-rewrite-rule-sets";
13.268 +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.269 + asm_thm=at,rules =rs,scr=sc}) r =
13.270 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.271 + asm_thm=at,rules = gen_rems eq_rule (rs, r),
13.272 + scr=sc}:rls)
13.273 + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.274 + asm_thm=at,rules =rs,scr=sc}) r =
13.275 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
13.276 + asm_thm=at,rules = gen_rems eq_rule (rs, r),
13.277 + scr=sc}:rls)
13.278 + | remove_rls id (Rrls _) _ = raise error
13.279 + ("remove_rls: not for reverse-rewrite-rule-set "^id);
13.280 +
13.281 + gen_rems (op=) ([1,2,3], [3,4,5]);
13.282 +
13.283 +
13.284 +
13.285 +fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known")
13.286 + | assoc' ((keyi, xi) :: pairs, key) =
13.287 + if key = keyi then Some xi else assoc' (pairs, key);
13.288 +
13.289 +fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
13.290 + handle _ => raise error ("ME_Isa: '"^thy^"' not in system");
13.291 +fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
13.292 + handle _ => raise error ("ME_Isa: '"^rls^"' not in system");
13.293 +
13.294 +fun termopt2str (Some t) =
13.295 + "Some " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
13.296 + | termopt2str None = "None";
13.297 +fun term2str t = Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t;
13.298 +(*for tests only*)
13.299 +fun terms2str ts= (strs2str o (map (Sign.string_of_term
13.300 + (sign_of (assoc_thy "Isac.thy"))))) ts;
13.301 +
13.302 +(*recursive defs:*)
13.303 +fun scr2str (Script s) = "Script "^(term2str s)
13.304 + | scr2str (Rfuns _) = "Rfuns";
13.305 +
13.306 +
13.307 +type domID = string; (* domID ^"thy" = theory' ??check 3.00!!*)
13.308 +val e_domID = "e_domID":domID;
13.309 +type pblID = string list; (* domID::...*)
13.310 +val e_pblID = ["e_pblID"]:pblID;
13.311 +type metID = (domID * string);
13.312 +val e_metID = (e_domID,"e_metID"):metID;
13.313 +
13.314 +fun metID2str ((domID,mI):metID) = pair2str (domID,mI);
13.315 +
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/sml/globals.sml Thu Apr 17 18:01:03 2003 +0200
14.3 @@ -0,0 +1,111 @@
14.4 +(* global variables needed in ME, DG, and updated in knowledge
14.5 + WN.8.01 from modspec.sml
14.6 +*)
14.7 +
14.8 +(* data for methods stored in 'methods'-database *)
14.9 +type meth' =
14.10 + (*defaults for Rewrite' (rls, rrls have their own data):*)
14.11 + {rew_ord' : rew_ord', (*for rules in Detail*)
14.12 + erls : rls, (*the eval_rls for cond. in rules*)
14.13 + (* '^ because of rewrite in applicable_in
14.14 + compare type scr and rls*)
14.15 + srls : rls, (*for evaluating list expressions in scr*)
14.16 + prls : rls, (*for evaluating predicates in ppc*)
14.17 + calc : calc list, (*for Calculate in scr*)
14.18 + asm_thm : thm' list, (*put asm into environment*)
14.19 + asm_rls : rls' list, (*27.8.02: ??? unused (from default hard_gen ?)*)
14.20 + (* compare type pbt:*)
14.21 + ppc: ((string * (*field*)
14.22 + (term * (*description*)
14.23 + term)) (*id | struct-var*)
14.24 + list),
14.25 + pre: term list, (*preconditions*)
14.26 + (*script*)
14.27 + scr: scr
14.28 + };
14.29 +val e_meth' = {rew_ord' = "e_rew_ord'": rew_ord',
14.30 + erls = e_rls, srls = e_rls, prls = e_rls,
14.31 + calc = [],
14.32 + asm_thm = []: thm' list,
14.33 + asm_rls = []: rls' list,
14.34 + ppc = []: (string * (term * term)) list,
14.35 + pre = []: term list,
14.36 + scr = EmptyScr: scr}:meth';
14.37 +
14.38 +
14.39 +(** problem-types stored in format for usage in specify **)
14.40 +(*25.8.01 ----
14.41 +val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
14.42 + (term * (* description *)
14.43 + term)) (* id | struct-var *)
14.44 + list)
14.45 + ) list);*)
14.46 +type pbt =
14.47 + {thy : theory, (* which allows to compile that pbt
14.48 + TODO: search generalized for subthy (ref.p.69*)
14.49 + cas : term option,(*'CAS-command'*)
14.50 + prls : rls, (* for preds in where_*)
14.51 + where_: term list, (* where - predicates*)
14.52 + ppc : ((string * (* field "#Given",..*)
14.53 + (term * (* description *)
14.54 + term)) (* id | struct-var *)
14.55 + list),
14.56 + met : metID list}; (* methods solving the pbt*)
14.57 +val e_pbt = {thy=ProtoPure.thy,cas=None,prls=Erls,
14.58 + where_=[],ppc=[],met=[]}:pbt;
14.59 +
14.60 +datatype ptyp =
14.61 + Ptyp of string * (*key within pblID*)
14.62 + pbt list * (*several pbts with different domIDs
14.63 + TODO: select by subthy (ref.p.69
14.64 + presently only _one_ elem*)
14.65 + ptyp list;
14.66 +val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]);
14.67 +
14.68 +type ptyps = ptyp list;
14.69 +val ptyps = ref ([e_Ptyp]:ptyps);
14.70 +
14.71 +(**+ breadth-first search on hierarchy of problem-types +**)
14.72 +
14.73 +type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)
14.74 +
14.75 +fun get_py thy d _ [] =
14.76 + raise error ("get_pbt not found: "^(strs2str d))
14.77 + | get_py thy d (k::[]) ((Ptyp (k',[py],_))::pys) =
14.78 + if k=k' then py
14.79 + else get_py thy d ([k]:pblRD) pys
14.80 + | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') =
14.81 + if k=k' then get_py thy d ks pys
14.82 + else get_py thy d (k::ks) pys';
14.83 +(*> ptyps:=
14.84 +[Ptyp ("1",[("ptyp 1",([],[]))],
14.85 + [Ptyp ("11",[("ptyp 11",([],[]))],
14.86 + [])
14.87 + ]),
14.88 + Ptyp ("2",[("ptyp 2",([],[]))],
14.89 + [Ptyp ("21",[("ptyp 21",([],[]))],
14.90 + [])
14.91 + ])
14.92 + ];
14.93 +> get_py SqRoot.thy ["1"] ["1"] (!ptyps);
14.94 +> get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);
14.95 + _REVERSE_ .......... !!!!!!!!!!*)
14.96 +
14.97 +(*TODO: search generalized for subthy*)
14.98 +fun get_pbt (*thy:theory TODO:subthy*) (pblID:pblID) =
14.99 + let val pblRD = rev pblID;
14.100 + in get_py ProtoPure.thy pblID pblRD (!ptyps) end;
14.101 +(* get_pbt thy ["1"];
14.102 + get_pbt thy ["21","2"];
14.103 + *)
14.104 +
14.105 +
14.106 +
14.107 +
14.108 +val methods =
14.109 + ref ([]:(metID * meth') list);
14.110 +
14.111 +
14.112 +fun get_met metID = (the (assoc (!methods, metID)))
14.113 + handle _ => error ("unknown method: "^(metID2str metID));
14.114 +
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/sml/library.sml Thu Apr 17 18:01:03 2003 +0200
15.3 @@ -0,0 +1,143 @@
15.4 +(* use"library.sml";
15.5 + WN.22.10.99
15.6 + for both, math-engine and isa-98-1-HOL-plus
15.7 + however, functions closely related to original isabelle-98-1 functions
15.8 + are in isa-98-1-HOL-plus/rewrite-parse/library_G
15.9 +*)
15.10 +
15.11 +(*.id2int.
15.12 +fun id2int*)
15.13 +
15.14 +fun gen_insI eq pr (x, xs) =
15.15 + if gen_mem eq (x, xs)
15.16 + then (writeln ("### occurs twice: "^(pr x)); xs)
15.17 + else x :: xs;
15.18 +fun gen_union eq pr (xs, []) = xs
15.19 + | gen_union eq pr ([], ys) = ys
15.20 + | gen_union eq pr (x :: xs, ys) = gen_union eq pr (xs, gen_ins eq (x, ys));
15.21 +
15.22 +fun cons2 (f,g) x = (f x, g x); (*PL softwareparadigmen*)
15.23 +
15.24 +fun nth _ [] = raise error "nth _ []"
15.25 + | nth 1 (x::xs) = x
15.26 + | nth n (x::xs) = nth (n-1) xs;
15.27 +
15.28 +fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *)
15.29 +fun or_ (b1,b2) = b1 orelse b2;
15.30 +fun takerest (i, ls) = (rev o take) (length ls - i, rev ls);
15.31 +fun pair2tri ((a,b),c) = (a,b,c);
15.32 +fun fst3 (a,_,_) = a;
15.33 +fun snd3 (_,b,_) = b;
15.34 +fun thd3 (_,_,c) = c;
15.35 +
15.36 +fun skip_blanks strl =
15.37 + let
15.38 + fun skip strl [] = strl
15.39 + | skip strl (" "::ss) = skip strl ss
15.40 + | skip strl ( s ::ss) = skip (strl @ [s]) ss
15.41 + in skip [] strl end;
15.42 +
15.43 +
15.44 +
15.45 +fun de_quote str =
15.46 + let fun scan ss' [] = ss'
15.47 + | scan ss' ("\""::ss) = scan ss' ss
15.48 + | scan ss' (s::ss) = scan (ss' @ [s]) ss;
15.49 + in (implode o (scan []) o explode) str end;
15.50 +(*> de_esc "\"d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v\"";
15.51 +val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : string*)
15.52 +
15.53 +
15.54 +
15.55 +(* conversions to (quoted) strings
15.56 + FIXME: rename *2str --> *2strq (quoted elems)
15.57 + now *2str' (elems NOT quoted) instead of *2str *)
15.58 +
15.59 +val commas = space_implode ",";
15.60 +
15.61 +fun strs2str strl = "[" ^ (commas (map quote strl)) ^ "]";
15.62 +(*> val str = strs2str ["123","asd"]; writeln str;
15.63 +val it = "[\"123\", \"asd\"]" : string
15.64 +"123", "asd"] *)
15.65 +fun strs2str' strl = "[" ^ (commas strl) ^ "]";
15.66 +fun list2str strl = "[" ^ (commas strl) ^ "]";
15.67 +(*> val str = list2str ["123","asd"]; writeln str;
15.68 +val str = "[123, asd]" : string
15.69 +[123, asd] *)
15.70 +fun spair2str (s1,s2) = "(" ^ (quote s1) ^ ", " ^ (quote s2) ^ ")";
15.71 +fun pair2str (s1,s2) = "(" ^ s1 ^ ", " ^ s2 ^ ")";
15.72 +(*16.11.00
15.73 +fun subs2str (subs:(string * string) list) =
15.74 + (list2str o (map pair2str)) subs;*)
15.75 +fun subs2str (subs: string list) = list2str subs;
15.76 +(*> val sss = ["(bdv,x)","(err,#0)"];
15.77 +> subs2str sss;
15.78 +val it = "[(bdv,x),(err,#0)]" : string*)
15.79 +fun subs2str' (subs:(string * string) list) = (*12.12.99???*)
15.80 + (list2str o (map pair2str)) subs;
15.81 +(*> val subs = subs2str [("bdv","x")]; writeln subs;
15.82 +val subs = "[(\"bdv\", \"x\")]" : string
15.83 +[("bdv", "x")] *)
15.84 +fun con2str land_lor = quote " &| ";
15.85 +fun ints2str ints = (strs2str o (map string_of_int)) ints;
15.86 +fun ints2str' ints = (strs2str' o (map string_of_int)) ints;
15.87 +
15.88 +
15.89 +(* use"library.sml";
15.90 + *)
15.91 +
15.92 +
15.93 +(*needed in Isa + ME*)
15.94 +fun get_thy str =
15.95 + let fun get strl [] = strl
15.96 + | get strl ("."::ss) = strl
15.97 + | get strl ( s ::ss) = get (strl @ [s]) ss
15.98 + in implode( get [] (explode str)) end;
15.99 +
15.100 +fun strip_thy str = (* ~/Design.98/ModelSpec.sml/declare.sml *)
15.101 + let fun strip bdVar [] = implode (rev bdVar)
15.102 + | strip bdVar ("."::_ ) = implode (rev bdVar)
15.103 + | strip bdVar (c ::cs) = strip (bdVar @[c]) cs
15.104 + in strip [] (rev(explode str)) end;
15.105 +
15.106 +fun ids_of t =
15.107 + let fun con ss (Const (s,_)) = s::ss
15.108 + | con ss (Free (s,_)) = s::ss
15.109 + | con ss (Abs (s,_,b)) = s::(con ss b)
15.110 + | con ss (t1 $ t2) = (con ss t1) @ (con ss t2)
15.111 + | con ss _ = ss
15.112 + in map strip_thy ((distinct o (con [])) t) end;
15.113 +(*
15.114 +> val t = (term_of o the o (parse thy))
15.115 + "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
15.116 +> ids_of t;
15.117 +["solve'_univar","Pair","R","Cons","univar","equation","Nil",...]*)
15.118 +
15.119 +
15.120 +fun overwritel (al, []) = al
15.121 + | overwritel (al, b::bl) = overwritel (overwrite (al, b), bl);
15.122 +(*> val aaa = [(1,11),(2,22),(3,33)];
15.123 +> overwritel (aaa, [(2,2222),(4,4444)]);
15.124 +val it = [(1,11),(2,2222),(3,33),(4,4444)] : (int * int) list*)
15.125 +
15.126 +local
15.127 +fun intsto1 0 = []
15.128 + | intsto1 n = (intsto1 (n-1)) @ [n]
15.129 +in
15.130 +fun intsto n = if n < 0 then (raise error "intsto < 0") else intsto1 n
15.131 +end;
15.132 +
15.133 +
15.134 +type 'a stack = 'a list;
15.135 +fun top ((x::xs):'a stack) = x
15.136 + | top _ = raise error "top called for empty list";
15.137 +fun pop ((x::xs):'a stack) = xs:'a stack
15.138 + | pop _ = raise error "pop called for empty list";
15.139 +fun push x (xs:'a stack) = x::xs:'a stack;
15.140 +
15.141 +
15.142 +fun drop_last l = ((rev o tl o rev) l);
15.143 +
15.144 +fun bool2str true = "true"
15.145 + | bool2str false = "false";
15.146 +
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/sml/print_exn_G.sml Thu Apr 17 18:01:03 2003 +0200
16.3 @@ -0,0 +1,20 @@
16.4 +(* use"print_exn_G.sml";
16.5 + W.N.11.99
16.6 +*)
16.7 +
16.8 +
16.9 +fun print_exn_unit e =
16.10 + case e of
16.11 + PTREE str =>
16.12 + (writeln ("Exception PTREE " ^ str))
16.13 + | PROOFS str =>
16.14 + (writeln ("Exception PROOFS " ^ str))
16.15 + | DIALS str =>
16.16 + (writeln ("Exception DIALS " ^ str))
16.17 +(* | TERM (msg,ts) =>
16.18 + (writeln ("Exception TERM raised:\n" ^ msg);
16.19 + seq (writeln o Sign.string_of_term sign) ts) *)
16.20 + | e => raise e;
16.21 +
16.22 +(*raises the exception in order to have a polymorphic type!*)
16.23 +fun print_exn_G e = (print_exn_unit e; raise e);
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/sml/stdin-out.sml Thu Apr 17 18:01:03 2003 +0200
17.3 @@ -0,0 +1,99 @@
17.4 +(* conversions for SMLs stdIn, stdOut via pipelining
17.5 + use"stdin-out.sml";
17.6 + W.N.19.11.99
17.7 +
17.8 +
17.9 +*)
17.10 +
17.11 +
17.12 +fun xxx () = (1 handle _ => 2);
17.13 +
17.14 +
17.15 +(*exception DG_ME_STATES of string;*)
17.16 +
17.17 +fun StdinSML (0:userID) (0:proofID)
17.18 + (0:cellID) (0:cellID) New_User =
17.19 + (("@@@@@begin@@@@@",add_user(), 0, 0:cellID, []:delcells, [New_User],
17.20 + "@@@@@end@@@@@")
17.21 + handle _ =>
17.22 + ("@@@@@begin@@@@@", 0, 0, 0, [],
17.23 + [System "error ke101, please quit frontend"],
17.24 + "@@@@@end@@@@@"))
17.25 + | StdinSML userID 0 0 0 End_User =
17.26 + (("@@@@@begin@@@@@",del_user userID, 0, 0, [], [End_User],
17.27 + "@@@@@end@@@@@")
17.28 + handle _ =>
17.29 + ("@@@@@begin@@@@@", 0, 0, 0, [],
17.30 + [System "error ke102, please quit frontend"],
17.31 + "@@@@@end@@@@@"))
17.32 + | StdinSML userID proofID 0 0 New_Proof =
17.33 + (("@@@@@begin@@@@@",userID, add_proof userID, 0, [], [New_Proof],
17.34 + "@@@@@end@@@@@")
17.35 + handle _ =>
17.36 + ("@@@@@begin@@@@@", 0, 0, 0, [],
17.37 + [System "error ke103, please quit frontend"],
17.38 + "@@@@@end@@@@@"))
17.39 + | StdinSML userID proofID 0 0 End_Proof =
17.40 + (("@@@@@begin@@@@@",userID, del_proof userID proofID, 0, [], [End_Proof],
17.41 + "@@@@@end@@@@@")
17.42 + handle _ =>
17.43 + ("@@@@@begin@@@@@", 0, 0, 0, [],
17.44 + [System "error ke104, please quit frontend"],
17.45 + "@@@@@end@@@@@"))
17.46 +
17.47 +(*| StdinSML uI pI acI cI (Command Example) =
17.48 + ... kann neue proofID nicht in call_Dg_ME erzeugen *)
17.49 +
17.50 +(* 11.10.00:
17.51 +args:
17.52 + uI : userID
17.53 + pI : proofID
17.54 + acI : cellID above the current cellID
17.55 + cI : current cellID
17.56 + cI<0 <=> cell generated by KE
17.57 + 0<cI <=> cell generated by user (form-cells + rule-cells !)
17.58 + acI=cI <=> user_cmd (and no cell generated by user) input only
17.59 + dat :
17.60 +values:
17.61 + uI : userID
17.62 + pI : proofID
17.63 + cI : the cellID under which ev. output has to be placed
17.64 + cs : cellIDs to be deleted
17.65 + dats:
17.66 +*)
17.67 + | StdinSML uI pI acI cI dat =
17.68 + let
17.69 + (*val _ = writeln("# StdinSML, d-dct="^
17.70 + ((string_of_int o get_dct o get_dstate) uI));(**)
17.71 + (**)val _ = writeln("# StdinSML, d-speed="^
17.72 + ((string_of_int o get_speed o get_dstate) uI));(**)
17.73 + (**)val _ = writeln("# StdinSML, dps-dct="^
17.74 + ((string_of_int o last_dct) (get_dps uI pI)));*)
17.75 + val (cs, p, dp, d, dats) =
17.76 + call_DG_ME (get_proof uI pI) (get_dps uI pI)
17.77 + (get_dstate uI) (acI,cI) dat;
17.78 + val _ = upd_proof uI pI p;
17.79 + val _ = upd_dial uI pI d [] dp;
17.80 + (*val _ = writeln("# StdinSML, d-dct="^
17.81 + ((string_of_int o get_dct) d));(**)
17.82 + (**)val _ = writeln("# StdinSML, d-speed="^
17.83 + ((string_of_int o get_speed) d));(**)
17.84 + (**)val _ = writeln("# StdinSML, dps-dct="^
17.85 + ((string_of_int o last_dct) dp));*)
17.86 + (*val _= writeln("### StdinSML, after call_DG_ME: dp=\n"^
17.87 + (dps2str dp));*)
17.88 + in ("@@@@@begin@@@@@",uI:userID, pI:proofID, cI:cellID,
17.89 + cs:cellID list, dats:inout list,"@@@@@end@@@@@") end
17.90 +(**) handle _ =>
17.91 + ("@@@@@begin@@@@@", uI, pI, cI, [],
17.92 + [System "error ke105, start another example"],
17.93 + "@@@@@end@@@@@")
17.94 +(**);
17.95 +
17.96 +
17.97 +(*
17.98 + use"DG-ME-states.sml";
17.99 + use"DG/dialog.sml";
17.100 + use"stdin-out.sml";
17.101 + *)
17.102 +