=======================================================================================================================================
=======================================================================================================================================
=======================================================================================================================================
            The Actual File is below this line
=======================================================================================================================================
=======================================================================================================================================
=======================================================================================================================================

Package sequent

=============================================
                  export
=============================================

=============================================
%%              Expectations
=============================================
Expect
    validSequent?: Sequent -> Boolean
    %: validSequent?(x) is true if sequent x is
    %: valid.
    ;
    isBasic?: Sequent -> Boolean
    %: Returns true if the given Sequent is
    %: basic. Used by validSequent?.
    ;
    moveToFront: ([Formula],FormulaTester) -> [Formula]
    %: Finds the first item in the [Formula]
    %: which satisfies the FormulaTester, then
    %: moves it to the front of the list.
    %: In the event that no objects satisfy it,
    %: the list is returned unaltered.
%Expect

=============================================
%%             Binary operators
=============================================

Operator
  |-  (++);
  \/  (+);
  /\  (*);
  ==> (opL5)
%Operator

=============================================
%%             Formula
=============================================

Type Formula =
    vbl String
  | neg Formula
  | Formula /\ Formula
  | Formula \/ Formula
  | Formula ==> Formula
with
  $, show, ==
%Type

=============================================
%%             Sequent
=============================================

Type Sequent =
  [Formula] |- [Formula]
with
  $, show, ==
%Type

Expect
  valid?: Formula -> Boolean

    %: valid?(f) is true if formula f is valid.
%Expect

=============================================
                implementation
=============================================

Import "collect/search".

Abbrev
  MaybeSequents = Maybe of [Sequent];
  FormulaTester = Formula -> Boolean;
  Rule          = Sequent -> MaybeSequents
%Abbrev

=============================================
%%             Valid Sequent Tester
=============================================

Define
    validSequent? (x) = true
%Define

=============================================
%%             Is Basic
=============================================

Define
    case isBasic? ([] |- ?) = false;
    case isBasic? (h::? |- back) = true when h `in` back
    else isBasic? (?::t |- back) = isBasic?(t |- back);
%Define

=============================================
%%             Move to Front
=============================================

Define
    case moveToFront ( list, tester ) = list when someSatisfy tester list
    else moveToFront ( list, tester ) = (select tester list)::(list -/ (select tester list));
%Define

%Package