(* ----------------------------------------------------------------------------
 * $Id: MLOGBASE.md,v 1.2 1994/11/28 21:04:12 dolzmann Exp $
 * ----------------------------------------------------------------------------
 * Copyright (c) 1993 Universitaet Passau
 * ----------------------------------------------------------------------------
 * This file is part of MAS.
 * ----------------------------------------------------------------------------
 * $Log: MLOGBASE.md,v $
 * Revision 1.2  1994/11/28  21:04:12  dolzmann
 * New revision of the MASLOG system: New functions and bug fixes of old one.
 *
 * Revision 1.1  1993/12/17  17:12:12  dolzmann
 * MASLOG is divided into three parts. (MLOGBASE, MLOGIO, MASLOG)
 * Additional input procedures are added.
 *
 * ----------------------------------------------------------------------------
 *)

DEFINITION MODULE MLOGBASE;
(* Maslog Base Definition Module. *)

(******************************************************************************
*			       M L O G B A S E				      *
*-----------------------------------------------------------------------------*
* Author:   Andreas Dolzmann                                                  *
* Language: MODULA II (mocka or mtc are possible.)                            *
* System:   Program for the computer algebra system MAS by Heinz Kredel.      *
* Project:  MASLOG
* Remark:   Libraries maskern, maslisp are used.                              *
* Abstract: A package for the MAS computer algebra system by Heinz Kredel.    *
*           This package implements basic routins on formulas of the first    *
*           order predicate calculus.                                         *
******************************************************************************)

FROM MASSTOR IMPORT LIST;

(******************************************************************************
*                       T Y P E   D E F I N I T I O N S                       *
******************************************************************************)

TYPE PROCFB1=PROCEDURE(LIST):BOOLEAN;
TYPE PROCFB2=PROCEDURE(LIST, LIST):BOOLEAN;

(******************************************************************************
*                              C O N S T A N T S                              *
******************************************************************************)

CONST rcsid = "$Id: MLOGBASE.md,v 1.2 1994/11/28 21:04:12 dolzmann Exp $";
CONST copyright = "Copyright (c) 1993 Universitaet Passau";

(******************************************************************************
*                       G L O B A L   V A R I A B L E S                       *
******************************************************************************)


VAR ET, VEL, NON, VERUM, FALSUM, EXIST, FORALL, 	(* symbols for	*)
	TVAR, REP, IMP, EQUIV, ANTIV, XOR, LVAR: LIST;	(* keywords.	*)

VAR ANY, BOOL: LIST;	(* Special identifier in VARTAB *)

(******************************************************************************
*			 B A S I C   R O U T I N E S                          *
******************************************************************************)

PROCEDURE FORGOP(phi: LIST): LIST;
(* formula get operation. phi is a formula; the operation keyword of the
formula phi is returned.*)

PROCEDURE FORGARGS(phi: LIST): LIST;
(* formula get arguments. phi is a formula; the arguments of the top level
operation of the formula phi are returned. You must not apply FORGARGS to
formulas without arguments! *)

PROCEDURE FORGLVAR(lvar: LIST): LIST;
(* formula get list of variables. lvar is an object that describes a list of
variables; FORGLVAR returns a list of all variables in lvar.  *)

PROCEDURE FORPFOR(phi: LIST; VAR op: LIST; VAR args: LIST);
(* formula parse formula. phi is a formula; FORPFOR returns in op the top
level operation symbol of phi and in args the arguments of the operation op.
*)

PROCEDURE FORPARGS(phi: LIST; VAR first, red: LIST);
(* formula parse arguments. phi is an object that describes a list of
arguments of an operation; FORPARGS returns in first the 1st argument of the
list and in red the list of all following arguments. *)

PROCEDURE FORPUNOP(phi: LIST; VAR op, arg: LIST);
(* formula parse unary operation. phi is a unary operation. The operator
symbol op and the argument arg are returned. *)

PROCEDURE FORPBINOP(phi: LIST; VAR op, first, second: LIST);
(* formula parse binary operation. phi is a binary operation. The operator
symbol op and the arguments first and second are returned. *)

PROCEDURE FORPUNOPA(arglist: LIST; VAR arg: LIST);
(* formula parse unary operation argument. arglist is a list containing the
argument of a unary operator; FORPUNOPA returns in arg the arguments *)

PROCEDURE FORPBINOPA(red: LIST; VAR first, second: LIST);
(* formula parse binary operation argument. red is a list of the arguments of
a binary operator; FORPBINOPA returns in first the 1st and in second the 2nd
argument.  *)

PROCEDURE FORPQUANT(phi: LIST; VAR quant, vars, formula: LIST);
(* formula parse quantifier. phi is a quantified formula; FORPQUANT returns in
quant the quantifier of the formula phi, in vars the list of the bound
variables (as an lvar object) and in formula the formula phi without
quantifier. *)

PROCEDURE FORPQUANTA(red: LIST; VAR lvar, formula: LIST);
(* formula parse quantifier arguments. red is the reductum of a quantified
formula (e.g returned from FORPFOR); FORPQUANTA returns in lvar a list of all
quantified variables as an lvar object and in formula the formula without
quantifier.  *)

PROCEDURE FORPLVAR(lvar: LIST; VAR varlist: LIST);
(* formula parse list of variables. lvar is an object that describes a list of
variables; the list of all variables in lvar is returned in varlist. *)

PROCEDURE FORPVAR(var: LIST; VAR name, sort: LIST);
(* formula parse variable. phi is a variable; FORPVAR returns in name the name
and in sort the sort of var. *)

PROCEDURE FORPVARA(red: LIST; VAR name, sort:LIST);
(* formula parse variable arguments. red is the reductum of a variable (e.g.
returned from FORPFOR); FORPVARA returns in name the name and in sort the sort
of the variable. *)

PROCEDURE FORMKFOR(op,args:LIST):LIST;
(* formula make formula. op is a operation symbol; args a list of arguments;
the formula op(arg1,arg2,...) is returned, if args=(arg1,arg2,...).  You can
generate constants with this function, too. *)

PROCEDURE FORMKCNST(cnst: LIST):LIST;
(* formula make constant, i.e. a function with 0 arguments. cnst is a
constant; the formula 'cnst()' is returned *)

PROCEDURE FORMKUNOP(op,arg:LIST):LIST;
(* formula make unary operation. op is a operation symbol, arg is a argument;
the formula op(arg) is returned. *)

PROCEDURE FORMKBINOP(op,arg1,arg2:LIST): LIST;
(* formula make binary operation. op is the operation symbol, arg1, arg2 are
the arguments; the formula op(arg1,arg2) is returned. *)

PROCEDURE FORMKVAR(name,sort:LIST):LIST;
(* formula make variable. name is the name, sort the sort of the variable; an
object that describes the variable is returned. *)

PROCEDURE FORMKLVAR(vars:LIST):LIST;
(* formula make list of variables. vars is a list of the form (var1,
var2,...); an lvar object that represents the list of variables in vars is
returned. *)

PROCEDURE FORMKQUANT(quant,vars,formula:LIST):LIST;
(* formula make quantifier. quant is the quantifier symbol, vars is a list of
variables, and formula the bound formula; the formula 'quant vars: formula'
is returned. *)

PROCEDURE FORTST(L: LIST; bbtst:PROCFB1):BOOLEAN;
(* formula test. L is a list, bbtst a bb-procedure to test whether a list
represents a bb-formula or not; FORTST returns TRUE, if and only if L
represents a formula. *)

PROCEDURE FORISVAR(L: LIST):BOOLEAN;
(* formula is variable. L is a list; FORISVAR returns TRUE if and only if L
represents a variable. (The type of the variable is not checked.)  *)

PROCEDURE FORISBOOLVAR(L: LIST):BOOLEAN;
(* formula is boolean variable. L is a list; FORISBOOLVAR returns true if and
only if L represents a boolean variable *)

PROCEDURE FORISLVAR(L: LIST): BOOLEAN;
(* formula is variable list. L is a list; FORISLVAR returns TRUE if and only
if L represents an lvar-object. *)

(******************************************************************************
*                      I S   A T O M I C   F O R M U L A                      *
******************************************************************************)

PROCEDURE FORISATOM(phi: LIST): BOOLEAN;
(* formula is atomic formula. phi is a formula, FORISATOM returns true, if and
only if phi is an atomic formula. An atomic formula is either VERUM or FALSUM
or a bb-formula or a variable of type bool. *)

PROCEDURE FORISBBFOR(phi: LIST):BOOLEAN;
(* formula is black-box formula. phi is a formula. TRUE is returned iff
phi is a black-box formula. *)

(******************************************************************************
*                                 V A R T A B                                 *
******************************************************************************)

PROCEDURE FORVTSTORE():LIST;
(* formula variable table store. The actual VARTAB is returned. *)

PROCEDURE FORVTRESTORE(vt: LIST):LIST;
(* formula variable table restore. Vt is a variable table. 
The actual VARTAB is set to the value of vt. The old value of VARTAB is 
returned. *)

PROCEDURE FORVTENTER(sym: LIST):LIST;
(* formula variable table enter. Sym is a CLIST. 
The symbol with print name sym is entered in 
the actual variable table, if no symbol with name sym exists. 
The unique identifier is returned. 
*)

PROCEDURE FORVTGET(id: LIST): LIST;
(* formula variable table get. The clist of the 
name of the symbol with identifier id is 
returned. If no symbol with identifier id exists, then 
SIL is returned. *)

END MLOGBASE.

(* -EOF- *)