home *** CD-ROM | disk | FTP | other *** search
- -------------------------------------------------------------------------------
- -- --
- -- Library Unit: Prover -- Prove or process user requests --
- -- --
- -- Author: Bradley L. Richards --
- -- --
- -- Version Date Notes . . . --
- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - --
- -- 1.0 - - - - - Never existed. First version implemented after --
- -- Parser et al reached version 2.0 --
- -- 2.0 20 Jun 86 Initial Version --
- -- 2.05 13 Jul 86 Split into separate spec and package files --
- -- 2.1 21 Jul 86 Demonstration Version --
- -- 2.3 19 Aug 86 Maintain rule base in an AVL tree for efficiency --
- -- Implement functors, asserta, assertz, retract, --
- -- parse, log, ln. --
- -- 3.0 10 Oct 86 Final thesis product --
- -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - --
- -- --
- -- Library units used: AVL -- AVL tree package --
- -- Data_def -- common data definitions --
- -- Listing -- error and warning message routines --
- -- Math -- Verdix math package (for LN, LOG, etc.) --
- -- Parser -- Fuzzy Prolog parser --
- -- Text_io -- Standard i/o packages
- -- Unchecked_deallocation -- Used to release bindings (private) --
- -- --
- -- Description: This package contains only one visible routine: Prove. --
- -- This procedure processes one request, which must take the form of --
- -- an expression. --
- -- Note that the rule_base may be modified by asserts/retracts --
- -- when processing a request. These side effects are not undone by --
- -- backtracking (the same as Prolog--but important nonetheless). --
- -- --
- -------------------------------------------------------------------------------
- -- --
- -- Package Specification --
- -- --
- -------------------------------------------------------------------------------
-
- with avl, data_def, listing, math, parser, text_io, unchecked_deallocation;
- use data_def, listing, math, parser, text_io;
- package prover is
-
- procedure prove( goal : in AST_ptr );
-
- prover_error : exception; -- raised when bizarre errors occur
-
- private
-
- package fp_io is new float_io(float); use fp_io;
- package int_io is new integer_io(integer); use int_io;
- package arg_io is new enumeration_io(argument_type); use arg_io;
- package token_io is new enumeration_io(token_type); use token_io;
- package node_io is new enumeration_io(AST_node_type); use node_io;
-
- --
- -- Set up the generic AVL tree package used to maintain the optimized
- -- rule base.
- --
- function clause_equal( a, b : AST_ptr ) return boolean;
- function clause_less_than( a, b : AST_ptr ) return boolean;
- package AVLs is new avl(AST, AST_ptr, clause_equal, clause_less_than);
- use AVLs;
-
- procedure free_binding is new unchecked_deallocation(binding, binding_list);
-
- end prover;
-