(* ----------------------------------------------------------------------------
* $Id: MLDEMO.mi,v 1.5 1995/11/04 18:00:25 pesch Exp $
* ----------------------------------------------------------------------------
* Copyright (c) 1993 Universitaet Passau
* ----------------------------------------------------------------------------
* This file is part of MAS.
* ----------------------------------------------------------------------------
* $Log: MLDEMO.mi,v $
* Revision 1.5 1995/11/04 18:00:25 pesch
* Changed comments violating documentation rules. Should be rewritten.
*
* Revision 1.4 1994/11/28 21:04:11 dolzmann
* New revision of the MASLOG system: New functions and bug fixes of old one.
*
* Revision 1.3 1993/12/17 17:15:37 dolzmann
* Additional input procedures are added.
*
* Revision 1.2 1993/10/03 18:28:04 dolzmann
* New version of procedure FORMKVD
*
* Revision 1.1 1993/07/13 14:44:08 dolzmann
* The maslog-system and a simple example.
*
* ----------------------------------------------------------------------------
*)
IMPLEMENTATION MODULE MLDEMO;
(* Maslog Demonstration Implementation Module. *)
(******************************************************************************
* M A S L O G D E M O N S T R A T I O N *
*-----------------------------------------------------------------------------*
* Author: Andreas Dolzmann *
* Language: Modula II (mtc or mocka are possible) *
* System: Program for the computer algebra system MAS by Heinz Kredel. *
* Project: MASLOG
* Remark: This module requires the MASLOG-System. *
* Abstract: This module implements a primitive application for the MASLOG- *
* System. *
******************************************************************************)
FROM MASELEM IMPORT GAMMAINT;
FROM MASSTOR IMPORT ADV, COMP, FIRST, INV, LIST, LIST1, LISTVAR, RED,
SIL;
FROM MASERR IMPORT ERROR, confusion, fatal, harmless, severe, spotless;
FROM MASLISPU IMPORT Declare, PROCF1, PROCP1;
FROM MASBIOS IMPORT BKSP, BLINES, CREAD, CREADB, DIBUFF, DIGIT, LETTER,
LISTS, SWRITE;
FROM MASSYM IMPORT ATOM, UWRIT1, UWRITE;
FROM MASSYM2 IMPORT ACOMP, ASSOCQ, ENTER, SYMBOL, SYWRIT;
FROM SACLIST IMPORT ADV2, AREAD, AWRITE, CCONC, CINV, CLOUT, CONC,
LIST10, LIST2, LIST3, LIST4, LIST5;
FROM MLOGBASE IMPORT ANY, BOOL, EQUIV, ET, EXIST, FALSUM, FORALL,
FORGARGS, FORGLVAR, FORGOP, FORISBOOLVAR, FORISLVAR,
FORISVAR, FORMKBINOP, FORMKCNST, FORMKFOR, FORMKLVAR,
FORMKQUANT, FORMKUNOP, FORMKVAR, FORPARGS, FORPBINOP,
FORPBINOPA, FORPFOR, FORPLVAR, FORPQUANT, FORPQUANTA,
FORPUNOP, FORPUNOPA, FORPVAR, FORPVARA, FORTST, IMP,
NON, REP, TVAR, VEL, VERUM, XOR;
FROM MASLOG IMPORT FORAPPLYAT, FORCONTBDVAR, FORCONTVAR, FORMKCNF,
FORMKDNF, FORMKPOS, FORMKPRENEX, FORMKVD, FORPREPQE,
FORSMPL, FORSUBSTVAR;
FROM MLOGIO IMPORT FORIREAD, FORPPRT, FORPPVAR, FORPREAD, FORRDVAR,
FORTEXW, KEYREAD;
CONST rcsidi = "$Id: MLDEMO.mi,v 1.5 1995/11/04 18:00:25 pesch Exp $";
CONST copyrighti = "Copyright (c) 1993 Universitaet Passau";
VAR BbfParserSyms: LIST;
(******************************************************************************
* I M P L E M E N T A T I O N O F T H E A T O M I C F O R M U L A S *
******************************************************************************)
PROCEDURE MLDMKATOM(rel,left,right:LIST):LIST;
(* maslog demonstration make atomic formula. rel is the relation symbol
(either EQU or NEQ), left and right are beta integers or variables. The
formula (left rel right) is returned. *)
BEGIN
RETURN LIST3(rel,left,right);
END MLDMKATOM;
(******************************************************************************
* L O W L E V E L P R O C E D U R E S *
******************************************************************************)
PROCEDURE mldbbtst(l: LIST): BOOLEAN;
(* maslog demonstration black-box test. l is a list; mldbbtst returns true if
and only if l represents a bb-objekt. bb-objekts are lists of the form
(REL,a,b), where REL is an element of the set {EQU,NEQ} and a, b are either a
variable (represented as in MASLOG) or an atom. For program tests mldbbtst
accepts additionally all lists of the form (KEY,...), where KEY is an
arbitrary keyword but is not of the EQU or NEQ. These lists have not any
interpretation. *)
VAR op, arg1, arg2, red: LIST;
BEGIN
IF l = SIL THEN RETURN FALSE; END;
IF SYMBOL(l) OR ATOM(l) THEN RETURN FALSE; END;
ADV(l,op,red);
IF NOT SYMBOL(op) THEN RETURN FALSE; END;
IF (ACOMP(op,EQU)=0) OR (ACOMP(op,NEQ)=0)
THEN
IF (red = SIL) OR (RED(red) = SIL) THEN RETURN FALSE; END;
ADV2(red,arg1,arg2,red);
IF red <> SIL THEN RETURN FALSE; END;
IF (NOT ATOM(arg1) AND NOT FORISVAR(arg1)) OR
NOT ATOM(arg2) AND NOT FORISVAR(arg2)
THEN
RETURN FALSE;
ELSE
RETURN TRUE;
END;
ELSE
RETURN TRUE; (* change to FALSE, if you will avoid the
acception of (KEY,...) as a bb-formula. *)
END;
END mldbbtst;
PROCEDURE mldbbpprt(phi: LIST);
(* maslog demonstration black-box pretty print. phi is a bb-formula; writes
phi formated in the output stream. *)
VAR op, red, arg1, arg2, dummy: LIST;
BEGIN
ADV(phi,op,red);
IF (op=EQU) OR (op=NEQ)
THEN
ADV2(red,arg1,arg2,dummy);
SWRITE("[");
IF FORISVAR(arg1) THEN
FORPPVAR(arg1);
ELSE
UWRIT1(arg1);
END;
bbpprtop(op);
IF FORISVAR(arg2) THEN
FORPPVAR(arg2);
ELSE
UWRIT1(arg2);
END;
SWRITE("]");
ELSE
SWRITE("[");
UWRIT1(phi);
SWRITE("]");
END;
END mldbbpprt;
PROCEDURE bbpprtop(op: LIST);
(* black box pretty print operator. op is a symbol of the set {EQU, NEQ};
writes op in the output stream. *)
BEGIN
IF (op=EQU) THEN SWRITE("="); RETURN; END;
IF (op=NEQ) THEN SWRITE("<>"); RETURN; END;
END bbpprtop;
PROCEDURE mldbbtexw(phi: LIST);
(* maslog demonstration black-box tex write. phi is bb-formula; writes phi in
tex style in the output stream. *)
VAR op, red, arg1, arg2, dummy: LIST;
BEGIN
ADV(phi,op,red);
IF (op=EQU) OR (op=NEQ)
THEN
BLINES(0);
ADV2(red,arg1,arg2,dummy);
SWRITE("(");
SWRITE("\mbox{\tt ");
UWRIT1(arg1);
SWRITE("}");
bbtexwop(op);
SWRITE("\mbox{\tt ");
UWRIT1(arg2);
SWRITE("}");
SWRITE(")");
ELSE
BLINES(0);
SWRITE("\mbox{\tt ");
UWRIT1(phi);
SWRITE("}");
END;
END mldbbtexw;
PROCEDURE bbtexwop(op: LIST);
(* black-box tex write operator. op is a element of the set {EQU,NEQ}; writes
op in tex stye in the output stream. *)
BEGIN
IF (op=EQU) THEN SWRITE("="); RETURN; END;
IF (op=NEQ) THEN SWRITE("\neq"); RETURN; END;
END bbtexwop;
PROCEDURE mldbbmkneg(phi: LIST): LIST;
(* maslog demonstration black-box make negation. phi is a bb-formula; the
negation of phi is returned. Remark: You can always move the negation inside
an atomic formular. *)
VAR op, res:LIST;
BEGIN
ADV(phi,op,res);
IF op=EQU THEN RETURN CCONC(LIST1(NEQ),res);
ELSIF op=NEQ THEN RETURN CCONC(LIST1(EQU),res);
ELSE RETURN FORMKUNOP(NON,phi);
END;
END mldbbmkneg;
PROCEDURE mldbbsmpl(phi: LIST): LIST;
(* maslog demonstration black-box simplify. phi is a bb-formula; returns a
simplification of phi. *)
VAR op,res, a, b, dummy: LIST;
BEGIN
IF phi=SIL THEN RETURN SIL; END;
ADV(phi,op,res);
IF (op=NEQ) OR (op=EQU)
THEN
ADV2(res,a,b,dummy);
IF ATOM(a) AND ATOM(b)
THEN
IF (op=EQU) AND (a=b)
THEN
RETURN FORMKCNST(VERUM);
ELSIF (op=EQU) AND (a<>b)
THEN
RETURN FORMKCNST(FALSUM);
ELSIF (op=NEQ) AND (a<>b)
THEN
RETURN FORMKCNST(VERUM);
ELSE (* (op=NEQ) AND (a=b) *)
RETURN FORMKCNST(FALSUM)
END;
ELSE
RETURN phi;
END;
ELSE
RETURN phi;
END;
END mldbbsmpl;
PROCEDURE mldbbsubstvar(phi, old, new:LIST):LIST;
(* maslog demonstration black-box substitute variable. phi is a bb-formula,
old and new are variables. mldsubstvar returns a formula in which all
occurences of old are substituted with new. *)
VAR op, res, a, b, dummy, aname, asort, bname, bsort,
oname, osort: LIST;
BEGIN
ADV(phi,op,res);
IF (op=EQU) OR (op=NEQ)
THEN
ADV2(res,a,b,dummy);
FORPVAR(old,oname,osort);
IF NOT ATOM(a)
THEN
FORPVAR(a,aname,asort);
IF (aname=oname) AND (asort=osort)
THEN
a:=new;
END;
END;
IF NOT ATOM(b)
THEN
FORPVAR(b,bname,bsort);
IF (bname=oname) AND (bsort=osort)
THEN
b:=new;
END;
END;
RETURN LIST3(op,a,b);
ELSE
RETURN phi;
END;
END mldbbsubstvar;
PROCEDURE mldbbcontvar(phi,var:LIST):BOOLEAN;
(* maslog demonstration black-box contains variable. phi is a bb-formula, var
is a variable; mldbbcontvar returns true if and only if phi contains var. *)
VAR op, res, a, b, dummy: LIST;
BEGIN
ADV(phi,op,res);
IF (op=EQU) OR (op=NEQ)
THEN
ADV2(res,a,b,dummy);
IF (a=var) OR (b=var) THEN RETURN TRUE; ELSE RETURN FALSE; END;
ELSE
RETURN FALSE;
END;
END mldbbcontvar;
PROCEDURE mldbblsvars(phi:LIST):LIST;
(* maslog demonstration black-box list variables. phi is a bb-formula;
a list of all variables in phi is returned. *)
VAR op, lhs, rhs, red, dummy,result: LIST;
BEGIN
result:=SIL;
ADV(phi,op,red);
IF (op=EQU) OR (op=NEQ) THEN
ADV2(red,lhs,rhs,dummy);
IF FORISVAR(lhs) THEN
result:=COMP(lhs,result);
END;
IF FORISVAR(rhs) THEN
result:=COMP(rhs,result);
END;
RETURN result;
ELSE
RETURN SIL;
END;
END mldbblsvars;
PROCEDURE mldbbread():LIST;
(* maslog demonstration black-box read. a bb-formula is read from the
inputstream. *)
VAR c:GAMMAINT;
VAR result:LIST;
VAR lhs,rhs,rel,sym:LIST;
BEGIN
lhs:=readarg();
(* SWRITE("lhs");UWRIT1(lhs);BLINES(0); *)
rel:=KEYREAD();
(* SWRITE("rel");CLOUT(rel);BLINES(0); *)
sym:=ASSOCQ(rel,BbfParserSyms);
IF sym=SIL THEN
DIBUFF();
ERROR(severe,"unknown relation");
RETURN SIL;
ELSE
sym:=FIRST(sym);
END;
rhs:=readarg();
(* SWRITE("rhs");UWRIT1(rhs);BLINES(0); *)
RETURN MLDMKATOM(sym,lhs,rhs);
END mldbbread;
PROCEDURE readarg():LIST;
(* read argument. A argument of a relation is read from the inputstream. *)
VAR c: GAMMAINT;
VAR result:LIST;
BEGIN
c:=CREADB();
IF LETTER(c) THEN
BKSP();
result:=FORRDVAR();
RETURN result;
ELSIF DIGIT(c) THEN
BKSP;
result:=AREAD();
RETURN result;
ELSE
DIBUFF();
ERROR(severe,"ATOM or SYMBOL expected");
RETURN SIL;
END;
END readarg;
PROCEDURE InitBbfParser();
(* Initialize black-box formula parser. *)
BEGIN
BbfParserSyms:=SIL;
LISTVAR(BbfParserSyms);
BbfParserSyms:=LIST4(LISTS("<>"),NEQ,LISTS("="),EQU);
RETURN;
END InitBbfParser;
PROCEDURE apply(phi:LIST):LIST;
(* apply. phi is a list; phi is returned and written in the outputstream. *)
BEGIN
UWRITE(phi);
RETURN phi;
END apply;
(******************************************************************************
* H I G H L E V E L P R O C E D U R E S *
******************************************************************************)
PROCEDURE MLDTST(l: LIST):LIST;
(* maslog demonstration test 1. l is a list; MLDTST returns 1 if l represents
a formula otherwise 0. *)
BEGIN
IF FORTST(l,mldbbtst)
THEN
RETURN LIST(1);
ELSE
RETURN LIST(0);
END;
END MLDTST;
PROCEDURE MLDMKPOS(phi: LIST): LIST;
(* maslog demonstration make positive. phi is a formula; a formula equivalent
to phi, which is relative positive, is returned. Relative positive means that
negations are only in front of atomic formulas. *)
BEGIN
RETURN FORMKPOS(phi,NON,mldbbmkneg);
END MLDMKPOS;
PROCEDURE MLDMKPOS1(phi, pref: LIST): LIST;
(* maslog demonstration make positive 1. phi is a formula; pref is a symbol
of the set \{ET, VEL, NON\}; a formula equivalent to phi, which is relative
positive, is returned. Relative positive means that negations are only in
front of atomic formulas. pref is a switch that controls the substitution of
the operators IMP, REP, EQUIV, XOR.*)
BEGIN
RETURN FORMKPOS(phi,pref,mldbbmkneg);
END MLDMKPOS1;
PROCEDURE MLDMKDNF(phi: LIST): LIST;
(* maslog demonstration make disjunctive normal form. phi is a formula;
MLMKDNF returns a formula in strict disjunctive normal form which is
equivalent to phi. *)
BEGIN
RETURN FORMKDNF(phi,mldbbmkneg);
END MLDMKDNF;
PROCEDURE MLDMKCNF(phi: LIST): LIST;
(* maslog demonstration make disjunctive normal form. phi is a formula;
MLDMKCNF returns a formula in strict conjunctive normal form which is
equivalent to phi. *)
BEGIN
RETURN FORMKCNF(phi,mldbbmkneg);
END MLDMKCNF;
PROCEDURE MLDMKPRENEX(phi, pref: LIST): LIST;
(* maslog demonstration make prenex. phi is a formula; pref is an element of
\{EXIST, FORALL\}; a formula psi in prenex normal form is returned. phi must
be a relative positive formula without additional operation symbols like IMP,
REP, etc. All bound variables in phi must have different specifications
(i.e. different names or different types). The only transformation which is
used to calculate psi is the interchange of a junctor with a quantifier. The
formula psi has the minimal number of blocks of quantifiers under all prenex
formulas which are built using only the interchange of a junctor with an
quantifier. The argument pref is only respected, if there are two equivalent
formulas with the same optimal number of blocks of quantifiers. In this case
the formula is returned which has a "`pref"'-quantifier as the outermost
operation symbol.*)
BEGIN
RETURN FORMKPRENEX(phi,pref);
END MLDMKPRENEX;
PROCEDURE MLDSUBSTVAR(phi,old,new:LIST):LIST;
(* maslog demonstration substitute variables. phi is a formula; old and new
are variables; a formula in which the variable old is substituted by the
variable new is returned. *)
BEGIN
RETURN FORSUBSTVAR(phi,old,new,mldbbsubstvar);
END MLDSUBSTVAR;
PROCEDURE MLDMKVD(phi: LIST):LIST;
(* maslog demonstration make variables disjoint. formula is a formula, this
procedure returns a formula in which all bound variables of the same sort
have different names. Only the minimal number of renamings are done to make
the names different.*)
BEGIN
RETURN FORMKVD(phi,mldbbsubstvar,mldbblsvars);
END MLDMKVD;
PROCEDURE MLDSMPL(phi: LIST): LIST;
(* maslog demonstration simplify. phi is a formula; a formula phi1 equivalent
to phi is returned. The formula phi1 is simplified, that means the constants
VERUM and FALSUM are eliminated, and nested operators are eliminated. (In this
case the procedure takes advantage of associativity of ET and VEL, and the
idempotenz of NON. *)
BEGIN
RETURN FORSMPL(phi,mldbbsmpl,mldbbmkneg);
END MLDSMPL;
PROCEDURE MLDPREPQE(phi: LIST):LIST;
(* maslog demonstration prepare quantifier elimination. phi is a prenex
formu\-la; a formula psi equivalent to phi is returned. psi is built according
to the following rules: If the innermost block of quantifiers is an
exist-quantifier, then matrix(phi) is transformed in CNF and the innermost
block of quantifiers is moved inside the conjunction. If the innermost
quantifier is a forall-quantifier, then matrix(phi) is transformed in DNF and
the innermost block of quantifiers is moved inside the disjunction.*)
BEGIN
RETURN FORPREPQE(phi,mldbbmkneg);
END MLDPREPQE;
PROCEDURE MLDAPPLYAT(phi:LIST):LIST;
(* maslog demonstration apply to atomic formulas. phi is a formula; the
formula phi is returned and all atomic formulas are written in the outout
stream. *)
BEGIN
RETURN FORAPPLYAT(phi,apply);
END MLDAPPLYAT;
PROCEDURE MLDPPRT(phi: LIST);
(* maslog demonstration pretty print. phi is a formula; this procedure writes
the formula phi formated in the output stream. *)
BEGIN
FORPPRT(phi, mldbbpprt);
RETURN;
END MLDPPRT;
PROCEDURE MLDTEXW(phi: LIST);
(* maslog demonstration tex write. phi is a formula; this procedure writes phi
in tex style in the output stream. *)
BEGIN
FORTEXW(phi, mldbbtexw);
RETURN
END MLDTEXW;
PROCEDURE MLDCONTVAR(phi,var:LIST):LIST;
(* maslog demonstration contain variable. phi is a formula, var is a variable;
1 is returned, if phi contains var as an unbound variable, otherwise 0 is
returned. *)
BEGIN
IF FORCONTVAR(phi,var,mldbbcontvar)
THEN
RETURN 1;
ELSE
RETURN 0;
END;
END MLDCONTVAR;
PROCEDURE MLDCONTBDVAR(phi,var:LIST):LIST;
(* maslog demonstration contains bound variable. phi is a formula, var is a
variable; 1 is returned, if phi contains var as bound variable, otherwise 0
is returned. *)
BEGIN
IF FORCONTBDVAR(phi,var)
THEN
RETURN LIST(1);
ELSE
RETURN LIST(0);
END;
END MLDCONTBDVAR;
PROCEDURE MLDPREAD():LIST;
BEGIN
RETURN FORPREAD(mldbbread);
END MLDPREAD;
PROCEDURE MLDIREAD():LIST;
BEGIN
RETURN FORIREAD(mldbbread);
END MLDIREAD;
BEGIN (* OF INITIALIZATION *)
Declare(EQU,"EQU");
Declare(NEQ,"NEQ");
InitBbfParser();
END MLDEMO.
(* -EOF- *)