(*
 * $Id: aswchecker.sml$ (C) 2007 DJ Greaves. CBG Squanderer.
 * http://www.cl.cam.ac.uk/users/djg/pubs/aswchecker.txt
 *
 * A toy implementation of the ATP set out in:
 *   author = "Andersen and Stirling and Winskel",
 *   title = "A Compositional Proof System for the Modal mu-Calculus",
 *   booktitle = "{LICS}: {IEEE} Symposium on Logic in Computer Science",
 *   year = "1994",
 *   url = "citeseer.ist.psu.edu/andersen94compositional.html" }
 *)

load "Int";

(*
 * Atomic action type
 *)
datatype act_t =
	Idle   (* denoted as asterisk in the paper *)
      | Act of string 
      | Apair of act_t * act_t
      | Act_any
;

fun
   Acs (Apair(a,b)) = "(" ^ Acs a ^ "," ^ Acs b ^ ")"
|  Acs (Act s) = s
|  Acs _ = "?"
;

fun
  Actsl [] = ""
| Actsl [item] = Acs item
| Actsl (h::t) = Acs h ^ "," ^ Actsl t
;

fun
  sfold f [] = ""
| sfold f [item] = f item
| sfold f (h::t) = f h ^ "," ^ sfold f t
;


(*
 * This is the process calc set out in table 1 of the paper.
 *)
datatype L_t =   
   Nil
 | Prefix of act_t * L_t
 | Sum of L_t * L_t
 | Product of L_t * L_t
 | Relabel of L_t * ((act_t * act_t) list)
 | Restrict of L_t * act_t list
 | Lvar of string
 | Rec of L_t * L_t
 | Lbind of (L_t * L_t) list * L_t
;


fun
  Ts Nil = "Nil"
| Ts (Prefix(a, p)) = Acs a ^ "." ^ Ts p
| Ts (Sum(a, b)) = Ts a ^ "+" ^ Ts b
| Ts (Product(a, b)) = Ts a ^ " x " ^ Ts b
| Ts (Restrict(a, b)) = Ts a ^ "{" ^ "}"
| Ts (Rec(a, b)) = "Rec(" ^ Ts a ^ ", " ^ Ts b ^ ")"
| Ts (Lvar s) = s
| Ts (Lbind(_, s)) = "Lbind(" ^ Ts s ^ ")"
| Ts _ = "?Ts"
;


exception operate_error of string;
exception prove_error of string;

(*
 * This is the operation semantics of the process calc set out in table 2 of the paper.
 *)
fun
  Operate e Idle x = SOME x

| Operate e a (Prefix(k, t)) = if a=Act_any orelse a=k then SOME t else NONE

| Operate e a (Sum(l, r)) = 
  let val r0 = Operate e a l
  in if r0<>NONE then r0
     else Operate e a r
  end

| Operate e (Apair(la, ra)) (Product(l, r)) = 
  let val rl = Operate e la l
      val rr = Operate e ra r
  in if rl <> NONE andalso rr <> NONE then SOME(Product(valOf rl, valOf rr))
     else NONE
  end

| Operate e a (Restrict(p, Lambda)) = 
  if not(List.exists (fn x=>a=x) Lambda) 
	then NONE
  else
  let val p' = Operate e a p
  in if p'=NONE then NONE
     else SOME(Restrict(valOf p', Lambda))
  end

| Operate e a (Relabel(p, Xi)) = 
  let val beta = (List.find (fn (x,y)=>a=x) Xi) 
  in if beta=NONE then NONE else
     let val p' = Operate e (#2(valOf beta)) p
     in if p' = NONE then NONE 
	else SOME(Relabel(valOf p', Xi))
     end
  end

| Operate e a (R as Rec(Lvar x, t)) = 
  let val e' = (x, R)::e
  in Operate e' a t
  end

| Operate e a (V as Lvar varname) =
  let val r = (List.find (fn (x,y)=>varname=x) e) 
  in if r=NONE then raise operate_error("unbound var: " ^ varname)
     else SOME(#2(valOf r))
  end
;


(*
 * Assertion language
 *)
datatype A_t =   
   Not of A_t
 | Implies of A_t * A_t
 | Biimp of A_t * A_t
 | Conj of A_t * A_t
 | Disj of A_t * A_t
 | Diamond of act_t list * A_t
 | Box of act_t list * A_t
 | Avar of string
 | Mu of A_t * string list * A_t
 | Nu of A_t * string list * A_t
 | Atrue | Afalse

(* Extensions to the asertion language, used for internal processing: *)
 | Abind of (A_t * A_t) list * A_t
 | Arelab of (act_t * act_t) list * A_t
 | Arestrict of act_t list * A_t
 | Aquot of A_t * L_t
;

fun
  As (Avar s) = s
| As (Box(acts, a)) = "[" ^ Actsl acts ^  "]" ^ As a
| As (Diamond(acts, a)) = "<" ^ Actsl acts ^ ">" ^ As a
| As (Mu(x, tags, y)) = "Mu " ^ As x ^ "." ^ As y
| As (Nu(x, tags, y)) = "Nu " ^ As x ^ "." ^ As y
| As (Aquot(n, d)) =  As n ^ "/(" ^ Ts d ^ ")"
| As (Abind(_, n)) =  "Abind(_, " ^ As n ^ ")"
| As _ = "?"
;

fun goal2str (t, e:('a list * 'b list), name, A) = "." ^ name ^ "( " ^ (Int.toString(length(#1 e))) ^  "," ^(Int.toString(length(#2 e))) ^  "):   " ^ Ts t ^ " |- " ^ As A
;

fun goal2str (t, (et, ea), name, A) = "." ^ name ^ "( " ^ sfold (fn(a,b)=>Ts a) et ^  "," ^(Int.toString(length ea)) ^  "):   " ^ Ts t ^ " |- " ^ As A
;


(*
 * Use DeMorgan-like identities to convert to NNF (negative normal form).
 *)
fun
  nnf true  Atrue  = Afalse
| nnf true  Afalse = Atrue
| nnf false Atrue  = Atrue
| nnf false Afalse = Afalse

| nnf k     (Biimp(a, b))    = nnf k (Conj(Implies(a, b), Implies(b, a)))
| nnf k     (Implies(a, b))  = nnf k (Disj(Not a, b))
| nnf false (V as Avar _)    = V
| nnf true  (V as Avar _)    = Not V

| nnf false (Conj(a, b)) = Conj(nnf false a, nnf false b)
| nnf true  (Conj(a, b)) = Disj(nnf true a, nnf true b)

| nnf false (Not a) = nnf true a
| nnf true  (Not a) = nnf false a

| nnf false (Disj(a, b)) = Disj(nnf false a, nnf false b)
| nnf true  (Disj(a, b)) = Conj(nnf true a, nnf true b)

| nnf false (Box(a, b))  = Box(a, nnf false b) 
| nnf true  (Box(a, b)) =  Diamond(a, nnf true b)

| nnf false (Diamond(a, b))  = Diamond(a, nnf false b)
| nnf true  (Diamond(a, b)) =  Box(a, nnf true b)

| nnf false (Nu(a, l, b))   = Nu(a, l, nnf false b) 
| nnf true  (Nu(a, l, b))   = Mu(a, l, Abind([(a, nnf true a)], nnf true b)) 

| nnf false (Mu(a, l, b))   = Mu(a, l, nnf false b)
| nnf true  (Mu(a, l, b))   = Nu(a, l, Abind([(a, nnf true a)], nnf true b)) 
;


fun subst(A, s) = Abind(s, A)
;


fun 
  vOf f (SOME a, m, l) = a
| vOf f (NONE, v, l) = raise prove_error("unbound var " ^ f v ^ " in " ^ (foldr (fn ((a,b), c)=>f a ^ "," ^ c) "" l))
;

fun taghash e x =
    let fun tg stack e (Rec(v,body)) =  (tg stack e v) ^ "REC" ^  (tg stack e body)
	  | tg stack e (Prefix(p,q)) = (Acs p) ^ "." ^  (tg stack e q)
	  | tg stack (el, ea) (Lvar s) = 
	    if List.exists (fn x=>x=s) stack then s
	    else s ^ "[" ^  (tg (s::stack) (el, ea) (#2(vOf Ts (List.find (fn(x,y)=>x=Lvar s) el, Lvar s, el)))) ^ "/" ^ s ^ "]"
	  | tg stack e (Sum(p,q)) = (tg stack e p) ^ "SUM" ^  (tg stack e q)
	  | tg stack e (Product(p,q)) = (tg stack e p) ^ "PROD" ^  (tg stack e q)
	  | tg stack e (other) = raise prove_error("taghash of " ^ Ts other)
    in tg [] e x
    end
;


(* Partition action set into those that do and do not pair with Idle *)
fun idlediv(l) = 
    let
	fun k ([], cc, cd) = (rev cc, rev cd)
	  | k ((a as Apair(Idle, alpha))::t, cc, cd) = k(t, alpha::cc, cd)
	  | k ((a as Apair(beta, alpha))::t, cc, cd) = k(t, cc, a::cd)
	  | k (_, cc, cd) = raise prove_error "Idlediv: Action was not a pair"
    in k (l, [], [])
    end
;

(* Take quotient of action set, discarding those that do not divide. *)
fun actiondiv(l, denominator) =
    let
	fun k (Apair(beta, alpha), c) = if beta=denominator then alpha::c else c
	  | k (_, c) = raise prove_error "Divide: Action was not a pair"
    in foldr k [] l
    end

;

fun reassoc_x A = A (* for now *)
;

fun relabel_x A = A (* for now *)
;

fun restrict_x A = A (* for now *)
;


(*
 * Rule one step reason function.  Note that Idle must be kept at the head of action lists where present.
 *
 * Note that nil denotes false and the list containing nil denotes true.
 *)
val rule_invalid = nil;
val rule_taut = [ nil ];

fun R e rulename [] = []
  | R e rulename [item] = [ map (fn (t,A) => (t, e, rulename, A)) item ]
  | R e rulename [X,Y] = [ map (fn (t,A) => (t, e, rulename^"0", A)) X,
			   map (fn (t,A) => (t, e, rulename^"1", A)) Y ]
;


fun
  rules e (t, Atrue) = R e "Atrue" rule_taut
| rules e (t, Afalse) = R e "Afalse" rule_invalid

| rules e (t, V as Avar _) = rules e (t, #2(vOf As (List.find (fn (x,y)=>x=V) (#2 e), V, #2 e)))


(*
 * Rules E from table 2 : Boolean connectives
 *)
| rules e (t, Conj(l, r)) = R e "/\\" [[(t, l), (t, r)]]
| rules e (t, Disj(l, r)) = R e "\\/" [[(t, l)], [(t, r)]]

(*
 * Rules E from table 2 : Idling modalities
 *)
| rules e (t, Box(Idle::l, A)) = R e "[*]" [[(t, A), (t, Box(l, A))]]
| rules e (t, Diamond(Idle::l, A)) = R e "<*>" [[(t, A)], [(t, Diamond(l, A))]]

(*
 * Rules E from table 2 : Fixed points
 *)
| rules e (t, Mu(X, U, A)) =
  if List.exists (fn x=>x=taghash e t) U
  then R e "MuI" rule_invalid
  else R e "Mu" [[(t, subst(A, [(X, Mu(X, (taghash e t)::U, A))]))]]

| rules e (t, Nu(X, U, A)) =
  if List.exists (fn x=>x=taghash e t) U
  then R e "Nu0" rule_taut
  else R e "Nu1" [[(t, subst(A, [(X, Nu(X, (taghash e t)::U, A))]))]]

(*
 * Rules E from table 3 : Dynamic process operators.
 *)
| rules e (Nil, Box(kappa, A)) = R e "0[]" rule_taut (* should be invalid ??? *)

| rules e (Prefix(a, t), Box(kappa, A)) =
  R e ".[]" (if List.exists (fn x=>x=a orelse x=Act_any) kappa
  then [[(t, A)]]
  else rule_taut (* should be invalid ???*))

| rules e (Prefix(a, t), Diamond(kappa, A)) =
  R e ".<>" (if List.exists (fn x=>x=a) kappa
  then [[(t, A)]]
  else rule_invalid)

| rules e (Sum(l, r), B as Box(kappa, A)) = R e "+[]" [[ (l, B), (r, B) ]]
| rules e (Sum(l, r), B as Diamond(kappa, A)) = R e "+<>" [[ (l, B), (r, B) ]]


| rules e (E as Rec(x, t), B as Box(kappa, A))     = R e "rec[]" [[ (Lbind([(x, E)], t), B) ]]
| rules e (E as Rec(x, t), B as Diamond(kappa, A)) = R e "Rec<>" [[ (Lbind([(x, E)], t), B) ]]

(*
 * Table 4: Relabel rules
 *)
| rules e (Relabel(t, Xi), B as Box(kappa, A)) =
  let fun p a = if a=Idle then Idle else #1(valOf(List.find (fn (x,y)=>y=a) Xi)) 
      val preimage = map p kappa
  in R e "{}[]" [[ (t, Box(preimage, Arelab(Xi, A))) ]] 
  end

| rules e (Relabel(t, Xi), B as Diamond(kappa, A)) =
  let fun p a = if a=Idle then Idle else #1(valOf(List.find (fn (x,y)=>y=a) Xi)) 
      val preimage = map p kappa
  in R e "{}<>" [[ (t, Diamond(preimage, Arelab(Xi, A))) ]] 
  end

(* 
 * Table 4: Restrict rules
 *)
| rules e (Restrict(t, Lambda), B as Box(kappa, A)) =
  let fun p a = List.exists (fn x=>x=a) Lambda 
      val kappa' = List.filter p kappa
  in R e "R[]" [[ (t, Box(kappa', Arestrict(Lambda, A))) ]] 
  end

| rules e (Restrict(t, Lambda), B as Diamond(kappa, A)) =
  let fun p a = List.exists (fn x=>x=a) Lambda 
      val kappa' = List.filter p kappa
  in R e "R<>" [[ (t, Diamond(kappa', Arestrict(Lambda, A))) ]] 
  end

(* 
 * Table 4: Shift rules
 *)
| rules e (t, Arelab(Xi, A)) = R e "Xi" [[ (Relabel(t, Xi), A) ]]
| rules e (t, Arestrict(Lambda, A)) = R e "R" [[ (Restrict(t, Lambda), A) ]]
| rules e (t, Aquot(A, t1)) = R e "/" [[ (Product(t, t1), A) ]]

(*
 * Table 5: Product rules.
 *)
| rules e (P as Product(l, r), B as Box(kappa, A)) =
  let val (i, ni) = idlediv(kappa)
      fun lbind (el, ea) nb = (nb::el, ea)
      fun pbox e (Product(l, Nil), Box(kappa, A)) = R e "x0[]" rule_taut


	| pbox e (Product(t, Prefix(a, p)), Box(kappa, A)) =
	  let val i = actiondiv(kappa, a)
	  in R e "x.[]"  [[ (t, Box(i, Aquot(A, p))) ]]
	  end
	      
	| pbox e (Product(t, Sum(l, r)), Box(kappa, A)) =
	  R e "x+[]" [[ (Product(t, l), Box(kappa, A)), (Product(t, r), Box(kappa, A)) ]]
	  
	  
	| pbox e (Product(t, E as Rec(x, t')), B as Box(kappa, A)) =
	  R (lbind e (x, E)) "xrec[]" [[ (Product(t, t'), B) ]]

	| pbox e (Product(l, V as Lvar _), A) = 
	  pbox e (Product(l, #2(valOf(List.find (fn(x,y)=>x=V) (#1 e)))), A) 


	| pbox e (t, A) = raise prove_error("No pbox for " ^ Ts t ^ " |- " ^ As A ^ "\n")
			      
  in if null i then pbox e (P, B)
     else if null ni then
	 R e "x2[*]" [[ (l, Box(i, Aquot(A, r))) ]]
     else R e "x3[*]" [[ (l, Box(i, Aquot(A, r))), (P, Box(ni, A)) ]]
  end

| rules e (P as Product(l, r), D as Diamond(kappa, A)) =
  let val (i, ni) = idlediv(kappa)
      fun lbind (el, ea) nb = (nb::el, ea)
      fun pdia e (Product(t, Prefix(a, p)), Diamond(kappa, A)) =
	  let val i = actiondiv(kappa, a)
	  in R e "x.<>" [[ (t, Diamond(i, Aquot(A, p))) ]]
	  end
	      
	| pdia e (Product(t, Sum(l, r)), Diamond(kappa, A)) =
	  R e "x+<>" [[ (Product(t, l), Diamond(kappa, A))], [(Product(t, r), Diamond(kappa, A)) ]]
	  
	| pdia e (Product(t, E as Rec(x, t')), B as Diamond(kappa, A)) =
	  R (lbind e (x, E)) "xre<>" [[ (Product(t, t'), B) ]]
	  
	| pdia e (Product(l, V as Lvar _), A) = 
	  pdia e (Product(l, #2(valOf(List.find (fn(x,y)=>x=V) (#1 e)))), A) 

	| pdia e (t, A) = raise prove_error("No pdia for " ^ Ts t ^ " |- " ^ As A ^ "\n")
			      
  in if null i then pdia e (P, D)
     else if null ni then
	 R e "x2<*>" [[ (l, Diamond(i, Aquot(A, r))) ]]
     else R e "x3<*>" [[ (l, Diamond(i, Aquot(A, r)))], [(P, Diamond(ni, A)) ]]
  end


(*
 * Table 6: Reassociation for product rules
 *)
| rules e (Product(t, Product(l, r)), A) =
  R e "xx" [[ (Product(Product(t, l), r), reassoc_x A) ]]

| rules e (Product(t, Relabel(l, Xi)), A) = 
  let val Xi' = map (fn (x, y) => (Apair(Act_any, x), y)) Xi (*perhaps relabel range instead *)
  in R e "x{}" [[ (Relabel(Product(t, l), Xi'), relabel_x A) ]]
  end

| rules e (Product(t, Restrict(l, Lambda)), A) = 
  let val Lambda' = map (fn x => Apair(Act_any, x)) Lambda
  in R e "xR" [[ (Restrict(Product(t, l), Lambda), restrict_x A) ]]
  end

(*
 * Bind and lookup operations
 *)
| rules (el, ea) (Lbind(l, t), A) = rules (l@el, ea) (t, A)
| rules (el, ea) (t, Abind(l, A)) = rules (el, l@ea) (t, A)
| rules e (V as Lvar _, A) = rules e (#2(valOf(List.find (fn(x,y)=>x=V) (#1 e))), A)

| rules e (t, A) = raise prove_error("No rule for " ^ Ts t ^ " |- " ^ As A ^ "\n")
;



(*
 *
 *)
fun tablaux_prove (a as (t, e, name, A)) =
    let val _ = print(goal2str a ^ "\n")
	val tablaux = rules e (t, A)
	fun z (a as (t, e, name, A)) (b as (t', e', name', A')) = (print("cf: " ^ goal2str a ^ " with " ^ goal2str b ^ ":" ^ (if A=A' then "T" else "") ^  "\n"); a=b)
	(* = app (fn l=>(if List.exists (z a) l then raise prove_error "looping rule" else ())) tablaux *)
	val _ = app (fn l=>(if List.exists (fn x=>x=a) l then raise prove_error "looping rule" else ())) tablaux
	fun k nil = true
	  | k (h::t) = tablaux_prove h andalso k t
    in if length tablaux = 0 then false
       else List.exists null tablaux
	    orelse List.exists k tablaux
    end
;

fun tablaux_toplevel m expected (t, A) =
    let val _ = print (m ^ ": " ^ (if expected then "Proving" else "Refuting") ^ "...")
	val A' = nnf false A
	val e0 = (nil, nil)
	val ans = tablaux_prove (t, e0, "Start", A')
	val _ = if ans then print "Proved\n" else print "Invalid\n"
	val _ = if ans <> expected then raise prove_error "Wrong answer" else ()
    in ()
    end


fun test () =
    let val va = Avar "a"
	val vb = Avar "b"
	val a1 = Act "a1"
	val a2 = Act "a2"
	val a3 = Act "a3"
	val pa12 = Apair(a1, a2)
	val pa21 = Apair(a2, a1)
	val goal = Act "goal"
	val seq1 = Prefix(a1, Prefix(a2, Prefix(goal, Nil)))
    val _ = 
    (
     tablaux_toplevel "true1" true (seq1, Atrue);
     tablaux_toplevel "true2" true (seq1, Not Afalse);


(*     tablaux_toplevel "diamond-distribute" true (seq1, Diamond([a1], Avar "a")); *)
     tablaux_toplevel "diamond1t" true (seq1, Diamond([a1, a2], Box([goal], Atrue)));
     tablaux_toplevel "diamond1f" false (seq1, Diamond([a2], Box([goal], Atrue)));

      (* requires negation rules: tablaux_toplevel "dijs"  true (Nil, Disj(va, Not va));  *)
     ())
     
    (* Now check safety of a parallel comp *)
    val p1 = Rec(Lvar "p1", Prefix(a1, Prefix(a2, Lvar "p1")))
    val p2 = Rec(Lvar "p2", Prefix(a2, Prefix(a1, Lvar "p2")))

    val safe_product = (Product(p1, p2), Nu(va, [], Diamond([pa12, pa21], va))) 
    val _ = tablaux_toplevel "safe_product" true safe_product;

     in ()

     end
;
val _ = test();


(* eof ... under construction TODO: shift aux's, Idle to head, convert from CCS.  *)