use "utils.sml";

(* This file implements a fragment of the intuitionistic sequent calculus
   LJ in SML, with a very simple set of non-logical symbols. *)

(* Algebraic datatypes of terms and formulas: *)

datatype term = const of int | var of string | f1 of term | g2 of term*term;

(* We'll keep the formulas propositional for now *)

infixr &&;	(* declares && to be an infix operator associating to the rihgt *)
infixr ||;
infixr -:;  (* it's important that implication associates to the right, not left *)

datatype form = top | bot | && of form*form | || of form*form | -: of form*form 
	        | ! of form | p1 of term | q2 of term*term | r0 | s0 | p0;

(* Sample terms and forms: *)

const 1;
f1(var "x");
g2(const 1, f1(var "y"));
r0-:bot;  (* read as r0 implies bottom *)
p1(const 1)&&p1(var "x");

(* remember the non-logical symobls are f1,g2,p1,q2,r0,s0,p0 - reserve these! *)

(* LJ Sequents: *)

infixr |-;
datatype sequent = |- of (form list)*form;

(* sample sequent *)
[r0,bot,p1(f1(const 1))] |- r0&&s0;


(* There are many different ways to represent the rules of the calculus.
   They are represented here as transformations from CONCLUSION
   to PREMISE.  bot is used to represent the empty sequence as well. *)

fun Id (x as (G|-a)) = if (member a G) then [] else [x];

fun andR (G|-(a&&b)) = [G|-a, G|-b]
  | andR x = [x];    (* if the rule doesn't apply, leave it alone! *)

fun andL 1 ((a&&b)::G |- c) = [a::G |- c] 
  | andL 2 ((a&&b)::G |- c) = [b::G |- c]
  | andL n  x = [x];

fun orL ((a||b)::G |- c) = [a::G |- c, b::G |- c]
  | orL x = [x];

fun orR 1 (G|-(a||b)) = [G|-a]
  | orR 2 (G|-(a||b)) = [G|-b]
  | orR n x = [x];

fun impR (G|-(a-:b)) = [(a::G)|-b]
  | impR x = [x];

fun impL (((a-:b)::G)|-c) = [G|-a, b::G|-c]
  | impL x = [x];

fun negR (G|-(!a)) = [a::G |- bot]
  | negR x = [x];

fun negL ((!a)::G |- bot) = [G|-a]
  | negL x = [x];

(* a structural rule *)

fun weakR (G|-a) = if not (a = bot) then [G|-bot] else [G|-a];

(* Ex exchanges the first element with the nth element of the rest of 
   the list: e.g, (EX 1) exchanges the first two elements *)
fun EX n ((a::b::G)|-c) = 
  let val h = (nth n (b::G)) 
	in [(h::(replace a n (b::G))) |- c] end
  | EX n x = [x];

(* interactive version of exchange-left: *)
fun exL S = ( print "which formula should I move to the front? ";
	      let val n = getint() in (EX n S) end);


(*  A simple interactive theorem prover  *)

(* converts a string from getstring to a rule.  Be aware that getstring always
   gives you string ending in "\n" *)
fun toRule "Id\n" = Id
  | toRule "andR\n" = andR
  | toRule "orR 1\n" = (orR 1)
  | toRule "orR 2\n" = (orR 2)
  | toRule "impR\n" = impR
  | toRule "negR\n" = negR
  | toRule "impL\n" = impL
  | toRule "andL 1\n" = (andL 1)
  | toRule "andL 2\n" = (andL 2)
  | toRule "orL\n" = orL
  | toRule "negL\n" = negL
  | toRule x = (fn y => [y]);

fun termtoString (const n) = Int.toString(n)
  | termtoString (var s) = s
  | termtoString (f1 t) = "f1("^(termtoString t)^")"
  | termtoString (g2(t1,t2)) = "g2("^(termtoString t1)^","^(termtoString t2)^")";

fun formtoString top = "top"
  | formtoString bot = "bot"
  | formtoString r0 = "r0"
  | formtoString s0 = "s0"
  | formtoString p0 = "p0"
  | formtoString (p1 t) = "p1("^(termtoString t)^")"
  | formtoString (q2(t1,t2)) = "q2("^(termtoString t1)^","^(termtoString t2)^")"
  | formtoString (a&&b) = "("^(formtoString a)^"&&"^(formtoString b)^")"
  | formtoString (a||b) = "("^(formtoString a)^"||"^(formtoString b)^")"
  | formtoString (a-:b) = "("^(formtoString a)^"->"^(formtoString b)^")"
  | formtoString (!a) = "(!"^(formtoString a)^")";

fun printseq ([]|-c) = print(" |- "^(formtoString c)^".\n")
  | printseq ([a]|-c) = ( print(formtoString a); printseq ([]|-c) )
  | printseq ((a::b::G)|-c) = ( print((formtoString a)^", ");
			        printseq ((b::G)|-c) );

(* subproof automatically tries the Id rule first: *)
fun subproof [] = print "subproof complete.\n"
  | subproof (h::t) = if (nil = (Id h)) then (subproof t) else
       ( printseq h;
         print "------------------------- what do I do now?! ";
         subproof ( (toRule (getstring())) h );
         subproof t
       );

fun prove S = ( subproof [S]; print "\nProof Complete!\n" );

val S1 = ([r0&&s0,p1(const 5)] |- s0);
val S2 = ([p0&&(r0&&s0)]|-(p0&&r0)&&s0);