(* $Header: /users/lal/black/hol/Disser/RCS/wellfrmTactics.sml,v 1.26 1997/07/10 22:48:19 black Exp $ *)
(* *created  "Mon Dec 23 09:21:17 1996" *by "Paul E. Black" *)
(* *modified "Thu Jul 10 16:46:32 1997" *by "Paul E. Black" *)

(*-----------------------------------------------------------------------
	Tactics, conversions, etc. for Well Formed conditions and
	other constructs.
			after Peter Homeier
 -----------------------------------------------------------------------*)

new_parent "wellformed";

add_theorems_to_sml "c_ast";
add_definitions_to_sml "wellformed";
add_theorems_to_sml "wellformed";

load_library {lib = Sys_lib.string_lib , theory = "-"};

(* it is bothersome to fully declare these every time *)
val CONS_Term = (--`CONS:Cvar->Cvar list->Cvar list`--);
val nullCvarList = (--`[]:Cvar list`--);

use "cast2hol.sml";

(* function to test conversions *)
fun test_conv cnv trm boolean =
    test_result (concl (cnv trm)) (--`^trm = ^boolean`--);

(*-----------------------------------------------------------------------
	Some utility functions for IS_SUBSET and DL.
 -----------------------------------------------------------------------*)

(* prove a theorem about truth or falsity of (Var ...) = (Var ...) terms.
   The simple way is
	prove((--`^cvarTerm = F`--),
	      REWRITE_TAC [Var_one_one] THEN
	      CONV_TAC (DEPTH_CONV (FIRST_CONV
				[string_EQ_CONV,Num_lib.num_EQ_CONV])) THEN
	      REWRITE_TAC [CTypes_all_distinct])
   but since CTypes_all_distinct is SO big, it slows down ALL comparisons
   for the False case.  If the name or variant differs, it only takes about
   10 mS per proof.  If the type is the only difference (which happens 
   rarely in C), it takes the full 50 mS per proof.  So this should be about
   5 times faster. *)
fun Cvar_EQ_CONV cvarTerm =
let val {lhs=l,rhs=r} = dest_eq cvarTerm in
    if l = r then
	EQT_INTRO (REFL l)
    else
    let val {lhs=lvar,rhs=rvar} = dest_eq cvarTerm
	val [lnm,lvari,_] = strip_op (--`Var`--) lvar
	val [rnm,rvari,_] = strip_op (--`Var`--) rvar
	val tac =
	    if lvari <> rvari then
		PURE_ONCE_REWRITE_TAC [Var_one_one] THEN
		CONV_TAC (DEPTH_CONV Num_lib.num_EQ_CONV)
	    else if lnm <> rnm then
		PURE_ONCE_REWRITE_TAC [Var_one_one] THEN
		CONV_TAC (DEPTH_CONV string_EQ_CONV)
	    else
		(* this is the SLOWEST tactic by a factor of 5 *)
		REWRITE_TAC [Var_one_one, CTypes_all_distinct,
			     CConsts_all_distinct] THEN
		CONV_TAC (DEPTH_CONV 
			(FIRST_CONV [Num_lib.num_EQ_CONV,string_EQ_CONV]))
    in
	prove ((--`^cvarTerm = F`--), tac THEN REWRITE_TAC [])
    end
end;

(* tests

test_conv Cvar_EQ_CONV (--`(Var "a" 0 (Ptr Char)) = (Var "a" 0 (Ptr Char))`--)
								(--`T`--);
test_conv Cvar_EQ_CONV (--`(Var "a" 0 Char) = (Var "b" 0 Char)`--) (--`F`--);
test_conv Cvar_EQ_CONV (--`(Var "a" 0 Char) = (Var "a" 1 Char)`--) (--`F`--);
test_conv Cvar_EQ_CONV (--`(Var "a" 0 Char) = (Var "a" 0 Int)`--) (--`F`--);
test_conv Cvar_EQ_CONV (--`(Var "a" 0 (Ptr Char)) = (Var "a" 0 (Ptr Int))`--)
								(--`F`--);
test_conv Cvar_EQ_CONV (--`(Var "a" 0 Char) = (Var "b" 2 Void)`--) (--`F`--);
val _ = "should work under type conformance, but doesn't now";
test_conv Cvar_EQ_CONV
    (--`(Var "a" 0 (Ptr Char)) = (Var "a" 0 (Array Char (CCint 5)))`--)
								(--`T`--);

*)

fun eqsTorF thm = 
let val rhs = (#rhs o dest_eq o concl) thm in
    rhs = (--`T`--) orelse rhs = (--`F`--)
end;

(* return true if the term has a particular operator in it *)
fun hasOpr (opr:string) thm =
if is_comb thm then
    let val {Rator=rat,Rand=rnd} = dest_comb thm in
	if is_const rat andalso (#Name o dest_const) rat = opr then
	    true
	else
	    hasOpr opr rat orelse hasOpr opr rnd
    end
else if is_abs thm then
    hasOpr opr (#Body (dest_abs thm))
else
    false;

(* test

hasOpr "IS_EL" (--`IS_EL 6 [4;5;6]`--) = true;

hasOpr "IS_EL" (--`!x.4 + 5 < 17 + x`--) = false;

hasOpr "IS_EL" (--`?x.IS_EL x [a;T;F]`--) = true;

*)

(* reduce a predicate which is recursively defined using IS_EL *)
fun piecewise_reduce defnThm iseqconv predThm =
let
    (* rewrite one step of PRED.  The resulting theorem is something like
		|- PRED a b = IS_EL (hd a) b /\ PRED (tl a) b
       or
		|- PRED a b = T
     *)
    val spredThm = PURE_ONCE_REWRITE_RULE
	    [GEN_REWRITE_CONV (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
			     [defnThm] (concl predThm)] predThm
in
if eqsTorF spredThm then
    spredThm
else
let
    (* reduce the IS_EL and the boolean result.  The result is something like
		|- PRED a b = PRED (tl a) b
       or
		|- PRED a b = F
     *)
    val rpredThm = ONCE_REWRITE_RULE [] (CONV_RULE (ONCE_DEPTH_CONV
					(IS_EL_CONV iseqconv)) spredThm)
in
if eqsTorF rpredThm then
    rpredThm
else if hasOpr "IS_EL" (concl rpredThm) then
    (print_thm rpredThm; print "\n";
     raise HOL_ERR {origin_structure = "wellfrmTactics",
		    origin_function  = "piecewise_reduce",
		    message = "cannot reduce term"})
else
    piecewise_reduce defnThm iseqconv rpredThm
end end;

(*-----------------------------------------------------------------------
	Prove whether or not the first set (list) is a subset of the
	second set (list).
 -----------------------------------------------------------------------*)

fun IS_SUBSET_CONV iseqconv issTm =
    (* fail quickly when term doesn't start with IS_SUBSET *)
    if (#Name o dest_const o fst o strip_comb) issTm <> "IS_SUBSET" then
	raise HOL_ERR {origin_structure = "wellfrmTactics",
		       origin_function  = "IS_SUBSET",
		       message = "term doesn't begin with IS_SUBSET"}
    else
	piecewise_reduce IS_SUBSET iseqconv (REFL issTm);

(* tests

test_conv (IS_SUBSET_CONV Cvar_EQ_CONV)
	(--`IS_SUBSET [(Var "b" 1 Char)]
		[(Var "a" 0 Int);(Var "b" 1 Char);(Var "c" 0 Int)]`--) T;
test_conv (IS_SUBSET_CONV Cvar_EQ_CONV)
	(--`IS_SUBSET [(Var "b" 1 Char);(Var "a" 0 Int)]
		[(Var "a" 0 Int);(Var "b" 1 Char);(Var "c" 0 Int)]`--) T;
test_conv (IS_SUBSET_CONV Cvar_EQ_CONV)
	(--`IS_SUBSET [(Var "c" 0 Char);(Var "a" 1 Int)]
		[(Var "a" 0 Int);(Var "b" 1 Char);(Var "c" 0 Int)]`--) F;

val _ = "should fail since IS_EL q (APPEND ...) can't be decided by this";
IS_SUBSET_CONV Cvar_EQ_CONV
	(--`IS_SUBSET [(Var "c" 0 Char);(Var "a" 0 Int)]
		(APPEND [Var "a" 0 Int] [(Var "b" 1 Char);(Var "c" 0 Int)])`--)
handle e=>Raise e;

val _ = "should fail since term doesn't begin with IS_SUBSET";
IS_SUBSET_CONV Cvar_EQ_CONV (--`T`--) handle e=>Raise e;

*)

(*-----------------------------------------------------------------------
	Prove that the list has no duplicates.
 -----------------------------------------------------------------------*)

fun DL_CONV iseqconv issTm =
    (* fail quickly when term doesn't start with DL *)
    if (#Name o dest_const o fst o strip_comb) issTm <> "DL" then
	raise HOL_ERR {origin_structure = "wellfrmTactics",
		       origin_function  = "DL",
		       message = "term doesn't begin with DL"}
    else
	piecewise_reduce DL iseqconv (REFL issTm);

(* tests

test_conv (DL_CONV Cvar_EQ_CONV)
	(--`DL [(Var "a" 0 Int);(Var "b" 1 Char);(Var "a" 0 Char)]`--) T;

test_conv (DL_CONV Cvar_EQ_CONV)
	(--`DL [(Var "b" 1 Char);(Var "a" 0 Int);(Var "b" 1 Char);
						(Var "c" 0 Int)]`--) F;
test_conv (DL_CONV Cvar_EQ_CONV)
	(--`DL [(Var "a" 0 Char);(Var "b" 1 Char);(Var "b" 1 Char)]`--) F;

"should fail since term doesn't begin with DL";
DL_CONV Cvar_EQ_CONV (--`T`--) handle e=>Raise e;

*)

fun prove_DL vlst =
	ONCE_REWRITE_RULE [] (DL_CONV Cvar_EQ_CONV (--`DL ^vlst`--));

(*-----------------------------------------------------------------------
	Prove whether or not the first set (list) is a subset of the
	second set (list) given type conformance.
 -----------------------------------------------------------------------*)

fun IS_SUBSET_TYCONF_CONV issTm =

let

(* prove a theorem about truth or falsity of Ctypes_conform ty1 ty2. *)
fun Ctypes_conform_CONV ctm =
let val [_,_] = strip_op (--`Ctypes_conform`--) ctm (* check for predicate *)
    fun prove_ctypes ctmeq =
    prove(ctmeq,
	  REWRITE_TAC [Ctypes_conform,is_Ptr,is_Array,is_Struct,is_Funty,
		       CTy_subty,Struct_subty,Funty_frmty,Funty_toty,
		       CTypes_all_distinct] THEN
	  CONV_TAC (DEPTH_CONV string_EQ_CONV) THEN REWRITE_TAC [])
in
    prove_ctypes (--`^ctm = F`--)
	handle _ =>
	    prove_ctypes (--`^ctm = T`--)
end;

(* these are only for testing *)
val T = (--`T`--);
val F = (--`F`--);

(* tests

test_conv Ctypes_conform_CONV
	(--`Ctypes_conform (Ptr Char) (Array Char (CCid "UNK"))`--) T;
test_conv Ctypes_conform_CONV
	(--`Ctypes_conform (Ptr Int) (Array Char (CCid "UNK"))`--) F;
test_conv Ctypes_conform_CONV
	(--`Ctypes_conform (Struct "fred") (Struct "fred")`--) T;
test_conv Ctypes_conform_CONV
	(--`Ctypes_conform (Struct "fred") (Struct "gary")`--) F;

val _ = "this should fail because it isn't a complete Ctypes_conform";
test_conv Ctypes_conform_CONV (--`Ctypes_conform Int`--) F;

*)

(* determine the truth or falsity of TYPE_CONF v1 v2, that is,
   the variables are equal given type conformance *)
fun Cvar_Conf_CONV tctm =
let val [_,_] = strip_op (--`TYPE_CONF`--) tctm (* check for predicate *)
    fun prove_cvars_conf tctmeq =
    prove(tctmeq,
	    REWRITE_TAC [TYPE_CONF_DEF] THEN
	    CONV_TAC (DEPTH_CONV (FIRST_CONV
				[string_EQ_CONV,Num_lib.num_EQ_CONV])) THEN
	    (* quickly finish cases where name or disambiguator differ *)
	    REWRITE_TAC [] THEN
	    CONV_TAC (DEPTH_CONV Ctypes_conform_CONV) THEN
	    REWRITE_TAC [])
in
    prove_cvars_conf (--`^tctm = F`--)
	handle _ =>
	    prove_cvars_conf (--`^tctm = T`--)
end;

(* tests

test_conv Cvar_Conf_CONV
	(--`TYPE_CONF (Var "a" 0 (Ptr Char)) (Var "a" 0 (Ptr Char))`--) T;
test_conv Cvar_Conf_CONV
	(--`TYPE_CONF (Var "a" 0 Char) (Var "b" 0 Char)`--) F;
test_conv Cvar_Conf_CONV
	(--`TYPE_CONF (Var "a" 0 Char) (Var "a" 1 Char)`--) F;
test_conv Cvar_Conf_CONV
	(--`TYPE_CONF (Var "a" 0 Char) (Var "a" 0 Int)`--) F;
test_conv Cvar_Conf_CONV
	(--`TYPE_CONF (Var "a" 0 (Ptr Char)) (Var "a" 0 (Ptr Int))`--) F;
test_conv Cvar_Conf_CONV
	(--`TYPE_CONF (Var "a" 0 Char) (Var "b" 2 Void)`--) F;
test_conv Cvar_Conf_CONV
 (--`TYPE_CONF (Var "a" 0 (Ptr Char)) (Var "a" 0 (Array Char (CCint 5)))`--) T;

test_conv (SOME_EL_CONV Cvar_Conf_CONV)
	(--`SOME_EL (TYPE_CONF (Var "b" 1 Char))
		[(Var "a" 0 Int);(Var "b" 1 Char);(Var "c" 0 Int)]`--) T;
test_conv (SOME_EL_CONV Cvar_Conf_CONV)
	(--`SOME_EL (TYPE_CONF (Var "c" 0 (Array Int (CCid "UNK"))))
		[(Var "a" 0 Int);(Var "b" 1 Char);(Var "c" 0 (Ptr Int))]`--) T;

*)

(* reduce a predicate which is recursively defined *)
fun piecewise_reduce_ty defnThm predThm =
let
    (* rewrite one step of PRED.  The resulting theorem is something like
		|- PRED a b = SOME_EL (hd a) b /\ PRED (tl a) b
       or
		|- PRED a b = T
     *)
    val spredThm = PURE_ONCE_REWRITE_RULE
	    [GEN_REWRITE_CONV (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
			     [defnThm] (concl predThm)] predThm
in
if eqsTorF spredThm then
    spredThm
else
let
    (* reduce the element check.  The result is something like
		|- PRED a b = PRED (tl a) b
       or
		|- PRED a b = F
     *)
    val rpredThm = ONCE_REWRITE_RULE [] (CONV_RULE (ONCE_DEPTH_CONV
				(SOME_EL_CONV Cvar_Conf_CONV)) spredThm)
in
if eqsTorF rpredThm then
    rpredThm
else if hasOpr "SOME_EL" (concl rpredThm) then
    (print_thm rpredThm; print "\n";
     raise HOL_ERR {origin_structure = "wellfrmTactics",
		    origin_function  = "piecewise_reduce_ty",
		    message = "cannot reduce term"})
else
    piecewise_reduce_ty defnThm rpredThm
end end;

(* fail quickly if term isn't IS_SUBSET_TYCONF s1 s2 *)
val [_,_] = strip_op (--`IS_SUBSET_TYCONF`--) issTm

in
	piecewise_reduce_ty IS_SUBSET_TYCONF (REFL issTm)
end; (* IS_SUBSET_TYCONF_CONV *)

(* tests

test_conv IS_SUBSET_TYCONF_CONV
	(--`IS_SUBSET_TYCONF [(Var "b" 1 Char)]
		[(Var "a" 1 Char);(Var "b" 0 Char);(Var "a" 1 Int)]`--) F;
test_conv IS_SUBSET_TYCONF_CONV
	(--`IS_SUBSET_TYCONF [(Var "b" 1 (Ptr Char));(Var "a" 0 Int)]
		[(Var "a" 0 Int);(Var "b" 1 (Array Char (CCid "UNK")));
							(Var "c" 0 Int)]`--) T;

val _ = "should fail since SOME_EL q (APPEND ...) can't be decided by this";
test_conv IS_SUBSET_TYCONF_CONV
	(--`IS_SUBSET_TYCONF [(Var "c" 0 Char);(Var "a" 0 Int)]
	    (APPEND [Var "a" 0 Int] [(Var "b" 1 Char);(Var "c" 0 Int)])`--) F
handle e=>Raise e;

val _ = "should fail since term isn't a complete IS_SUBSET_TYCONF";
test_conv IS_SUBSET_TYCONF_CONV
	(--`IS_SUBSET_TYCONF []`--) F handle e=>Raise e;

*)

(*-----------------------------------------------------------------------
	Prove that a list of variables is well-formed.
	SKIMP: WF_xs x is currently vacuously true, so this doesn't
	really "prove" anything.
 -----------------------------------------------------------------------*)

fun prove_WF_xs vlst = ONCE_REWRITE_RULE [] (SPEC vlst WF_xs);

(*-----------------------------------------------------------------------
	Generate unique variants of a set of variables with respect to
	a base set.  (Homeier Section 10.1, pp 231-234)
 -----------------------------------------------------------------------*)

local
fun
    variant x s =
	let val [nm,vnum,ty] = strip_op (--`Var`--) x in
	if s = (--`[]:Cvar list`--) then
	    (--`Var ^nm ^vnum ^ty`--)
	else
	let val [shd,stl] = strip_op CONS_Term s
	    val [snm,snum,sty] = strip_op (--`Var`--) shd
	    val uniquevar =
		if nm = snm andalso ty = sty then
		let val xnumber = dest_num vnum and
			snumber = dest_num snum
		    val newindex = mk_num (max xnumber (snumber+1)) in
			(* same name & type; make variant number higher *)
			(--`Var ^nm ^newindex ^ty`--)
		end
		else
		    (* different; index okay *)
		    x
	in
	    variant uniquevar stl
	end end and
    variants vl s =
	if vl = (--`[]:Cvar list`--) then
	    (--`[]:Cvar list`--)
	else
	let val [x,xs] = strip_op CONS_Term vl
	    val x' = variant x s
	    val news = (--`CONS ^x' ^s`--) in
	    (--`CONS ^x' ^(variants xs news)`--)
	end
in
fun variants_CONV (trm:term) =
let val [cvarList,baseSet] = strip_op (--`variants`--) trm in
    mk_thm([], (--`^trm = ^(variants cvarList baseSet)`--))
end end;

(* test ...

val varis1 =
    (--`variants [Var "a" 0 Int;Var "b" 2 Int;Var "a" 0 Int;Var "c" 3 Int]
		 [Var "a" 3 Int;Var "d" 0 Int;Var "a" 1 Int;Var "c" 2 Int]`--);

test_result (concl (variants_CONV varis1))
(--`^varis1 = [Var "a" 4 Int;Var "b" 2 Int;Var "a" 5 Int;Var "c" 3 Int]`--);

*)

(*-----------------------------------------------------------------------
	Define logical versions of program variables.  Logical variables
	are only used in assertions, and therefore represent the same
	value during execution.  They are used as "initial" values.
 -----------------------------------------------------------------------*)

local
fun prependHat nm =
	(mk_str o logicalVersion o dest_str) nm and
    logicalForm v =
	let val [nm,vnum,ty] = strip_op (--`Var`--) v in
	    (--`Var ^(prependHat nm) ^vnum ^ty`--)
	end and
    logicals vl =
	if vl = (--`[]:Cvar list`--) then
	    (--`[]:Cvar list`--)
	else
	let val [v,vrest] = strip_op CONS_Term vl in
	    (--`CONS ^(logicalForm v) ^(logicals vrest)`--)
	end
in
fun logicals_CONV (trm:term) =
let val [cvarList] = strip_op (--`logicals`--) trm in
    mk_thm([], (--`^trm = ^(logicals cvarList)`--))
end end;

(* test ...

val logs1 =
    (--`logicals [Var "a" 0 Int;Var "b" 2 Int;Var "a" 0 Int]`--);

val loga = mk_str "^a" and
    logb = mk_str "^b" and
    logc = mk_str "^c";

test_result (concl (logicals_CONV logs1))
	(--`^logs1 = [Var ^loga 0 Int;Var ^logb 2 Int;Var ^loga 0 Int]`--);

*)

fun prove_logicals a = GSYM (logicals_CONV (--`logicals ^a`--));

(*-----------------------------------------------------------------------
	Create AND's of pairwise equivalency of two lists of Cvars.
	For instance, given (--`pairwiseEqual [a;b] [c;d]`--), return
		|- pairwiseEqual [a;b] [c;d] = (a=c) /\ (b=d)
	where a, b, c, and d are Var's.
 -----------------------------------------------------------------------*)

local
fun pairwiseEqual cvl1 cvl2 =
	if cvl1 = (--`[]:Cvar list`--) then
	    if cvl2 <> (--`[]:Cvar list`--) then
		raise Fail "pairwiseEqual: lists not same length"
	    else
		(--`T`--)
	else
	let val [v1,v1rest] = strip_op CONS_Term cvl1 and
		[v2,v2rest] = strip_op CONS_Term cvl2
	    val rest = pairwiseEqual v1rest v2rest 
	    val hv1 = cexpr2hol v1
	    val hv2 = cexpr2hol v2
	in
	    if rest = (--`T`--) then (* empty list *)
		(--`(^hv1 = ^hv2)`--)
	    else
		(--`(^hv1 = ^hv2) /\ ^rest`--)
	end
in
fun pairwiseEqual_CONV (trm:term) =
let val [cvl1,cvl2] = strip_op (--`pairwiseEqual`--) trm in
    mk_thm([], (--`^trm = ^(pairwiseEqual cvl1 cvl2)`--))
end end;

(* test ...

val pweq1 = (--`pairwiseEqual [Var "a" 0 Int;Var "b" 0 (Ptr Char)]
			      [Var "c" 0 Int;Var "d" 0 (Ptr Char)]`--);

test_result (concl (pairwiseEqual_CONV pweq1))
(--`^pweq1 =
     (a:num = c) /\ (b:string = d)`--);

*)

fun prove_pairwiseEqual a b =
	GSYM (pairwiseEqual_CONV (--`pairwiseEqual ^a ^b`--));

(*-----------------------------------------------------------------------
	Some utilities for GV_c_CONV and FV_c_CONV
 -----------------------------------------------------------------------*)

(* convert a HOL list into an SML list *)
fun lsthol2sml tm =
    if is_const tm then
	[]
    else
    let val (_,[lhd,ltl]) = strip_comb tm in
	lhd :: (lsthol2sml ltl)
    end;

(* convert an SML list into a HOL list *)
fun lstsml2hol [] = (--`[]:Cvar list`--)
 |  lstsml2hol (x::xs) = (--`CONS ^x ^(lstsml2hol xs)`--);

(*-----------------------------------------------------------------------
	Prove a theorem about what the global variables used by 
	functions called in a C AST statement are.
 -----------------------------------------------------------------------*)

(* extract the variable name from a Var:
	(--`Var "var" 0 Int`--) -> "var"
*)
fun dest_cvar cvar =
let val [var,_,_] = strip_op (--`Var`--) cvar in
	dest_str var
end;


local (* for GV_c_CONV *)

(* return the globals for the function fnameVar in the
   environment (list of WF_fnp theorems) *)
fun globalsFor [] fnameVar =
    let val warnmsg = "No WF_fnp theorem for " ^ (dest_cvar fnameVar) in
    (print (warnmsg ^ "\n");
     raise HOL_ERR {origin_structure = "wellfrmTactics",
		    origin_function  = "GV_c_CONV",
		    message = warnmsg})
    end
 |  globalsFor (fhd::ftl) fnameVar =
    let val [thmName,_,globls,_] = (strip_op (--`Func`--) o el 2 o
					strip_op (--`WF_fnp`--) o concl) fhd in
	if fnameVar = thmName then
	    lsthol2sml globls
	else
	    globalsFor ftl fnameVar
    end;

fun globalCvarsP env plst =
    foldrpl (fn plhd=>(fn rest=>union (globalCvarsE env plhd) rest)) plst []
and globalCvarsL env lval =
    let val (rator,rands) = strip_comb lval in
	if rator = (--`Vref`--) then
	    []
	else if rator = (--`Aryref`--) then
	    globalCvarsE env (el 2 rands)
	else if rator = (--`Deref`--) then
	    globalCvarsE env (el 1 rands)
	else if rator = (--`Field`--) then
	    globalCvarsL env (el 1 rands)
	else
	    (print "globalCvarsL: can't handle the following term:\n";
	     print_term lval; print "\n";
	     raise HOL_ERR {origin_structure = "wellfrmTactics",
			    origin_function  = "GV_c_CONV",
			    message = "unknown Lvalue"})
    end
and globalCvarsE env expr =
    let val (rator,rands) = strip_comb expr in
	if rator = (--`Lval`--) then
	    globalCvarsL env (el 1 rands)
	else if rator = (--`Assign`--) then
	    union (globalCvarsL env (el 1 rands))
					(globalCvarsE env (el 2 rands))
	else if rator = (--`Binary`--) then
	    union (globalCvarsE env (el 1 rands))
					(globalCvarsE env (el 3 rands))
	else if rator = (--`LUnary`--) then
	    globalCvarsL env (el 2 rands)
	else if rator = (--`Unary`--) then
	    globalCvarsE env (el 2 rands)
	else if rator = (--`Call`--) then
	    union (globalsFor env (el 1 rands))
		  (globalCvarsP env (el 2 rands))
	else if rator = (--`Const`--) then
	    []
	else
	    (print "GV_c_CONV: can't handle:\n";
	     print_term expr; print "\n";
	     raise HOL_ERR {origin_structure = "wellfrmTactics",
			    origin_function  = "GV_c_CONV",
			    message = "unknown Lvalue"})
    end;

fun globalCvars env stmt =
if is_const stmt then
    []
else
let val (rator,rands) = strip_comb stmt in
    if rator = (--`Simple`--) orelse rator = (--`Ret`--) then
	globalCvarsE env (el 1 rands)
    else if rator = (--`If`--) orelse rator = (--`CWhile`--) then
	union (globalCvarsE env (el 1 rands)) (globalCvars env (el 2 rands))
    else if rator = (--`IfElse`--) then
	union (globalCvarsE env (el 1 rands))
	(union (globalCvars env (el 2 rands)) (globalCvars env (el 3 rands)))
    else if rator = (--`Seq`--) then
	union (globalCvars env (el 1 rands)) (globalCvars env (el 2 rands))
    else if rator = (--`Block`--) then
	globalCvars env (el 2 rands)
    else
       (print "GV_c_CONV: don't know how to handle:\n";
	print_term stmt; print "\n";
	raise HOL_ERR {origin_structure = "wellfrmTactics",
		       origin_function  = "GV_c_CONV",
		       message = "unknown CStmt"})
end;

in

fun GV_c_CONV environ fvcstm = 
    let val [stmt] = strip_op (--`GV_c`--) fvcstm in
	mk_thm([], (--`^fvcstm = ^(lstsml2hol (globalCvars environ stmt))`--))
    end;

end;

(*-----------------------------------------------------------------------
	Prove a theorem about what the free variables of a C AST
	statement are.
 -----------------------------------------------------------------------*)

local (* for FV_c_CONV *)

(* if the variable is a member of the bound vars, return an empty
   list.  Otherwise return the variable in a list *)
fun ifnotmem bvars v =
    if mem v bvars then
	[]
    else
	[v];

fun freeCvarsP bvars plst =
    foldrpl (fn plhd=>(fn rest=>union (freeCvarsE bvars plhd) rest)) plst []
and freeCvarsL bvars lval =
    let val (rator,rands) = strip_comb lval in
	if rator = (--`Vref`--) then
	    ifnotmem bvars (el 1 rands)
	else if rator = (--`Aryref`--) then
	    union (ifnotmem bvars (el 1 rands)) (freeCvarsE bvars (el 2 rands))
	else if rator = (--`Deref`--) then
	    freeCvarsE bvars (el 1 rands)
	else if rator = (--`Field`--) then
	    freeCvarsL bvars (el 1 rands)
	else
	    (print "freeCvarsL: can't handle:\n";
	     print_term lval; print "\n";
	     raise HOL_ERR {origin_structure = "wellfrmTactics",
			    origin_function  = "FV_c_CONV",
			    message = "unknown Lvalue"})
    end
and freeCvarsE bvars expr =
    let val (rator,rands) = strip_comb expr in
	if rator = (--`Lval`--) then
	    freeCvarsL bvars (el 1 rands)
	else if rator = (--`Assign`--) then
	    union (freeCvarsL bvars (el 1 rands))
					(freeCvarsE bvars (el 2 rands))
	else if rator = (--`Binary`--) then
	    union (freeCvarsE bvars (el 1 rands))
					(freeCvarsE bvars (el 3 rands))
	else if rator = (--`LUnary`--) then
	    freeCvarsL bvars (el 2 rands)
	else if rator = (--`Unary`--) then
	    freeCvarsE bvars (el 2 rands)
	else if rator = (--`Call`--) then
	    freeCvarsP bvars (el 2 rands)
	else
	    []
    end;

fun freeCvars bvars stmt =
if is_const stmt then
    []
else
let val (rator,rands) = strip_comb stmt in
    if rator = (--`Simple`--) orelse rator = (--`Ret`--) then
	freeCvarsE bvars (el 1 rands)
    else if rator = (--`If`--) orelse rator = (--`CWhile`--) then
	union (freeCvarsE bvars (el 1 rands)) (freeCvars bvars (el 2 rands))
    else if rator = (--`IfElse`--) then
	union (freeCvarsE bvars (el 1 rands))
	(union (freeCvars bvars (el 2 rands)) (freeCvars bvars (el 3 rands)))
    else if rator = (--`Seq`--) then
	union (freeCvars bvars (el 1 rands)) (freeCvars bvars (el 2 rands))
    else if rator = (--`Block`--) then
	freeCvars (lsthol2sml (el 1 rands) @ bvars) (el 2 rands)
    else
       (print "FV_c_CONV: don't know how to handle:\n";
	print_term stmt; print "\n";
	raise HOL_ERR {origin_structure = "wellfrmTactics",
		       origin_function  = "FV_c_CONV",
		       message = "unknown CStmt"})
end;

in

fun FV_c_CONV fvcstm = 
    let val [stmt] = strip_op (--`FV_c`--) fvcstm in
	mk_thm([], (--`^fvcstm = ^(lstsml2hol (freeCvars [] stmt))`--))
    end;

end;

(*-----------------------------------------------------------------------
	Prove a theorem about what the free variables of a hol 
	expression are.
 -----------------------------------------------------------------------*)

local

fun typeisfun v = "fun" = (#Tyop o dest_type o type_of) v handle _ => false;

fun listOfFreevars smlLst =
    if null smlLst then
	nullCvarList
    else if typeisfun (hd smlLst) then
	listOfFreevars (tl smlLst)
    else
	(--`CONS ^(holvar2c (hd smlLst)) ^(listOfFreevars (tl smlLst))`--)
in
fun FV_a_CONV fvterm = 
    let val [holterm] = strip_op (--`FV_a`--) fvterm in
	mk_thm([], (--`^fvterm = ^(listOfFreevars (free_vars holterm))`--))
    end
end;

(*-----------------------------------------------------------------------
	Prove the well-formedness of a command, if possible.  Raise an
	exception if it can't be proven.
 -----------------------------------------------------------------------*)

fun prove_WF_c command = ONCE_REWRITE_RULE [] (SPEC command WF_c);

(*-----------------------------------------------------------------------
	Prove the syntactic well-formedness of a function with its pre-
	and postconditions, if possible.
 -----------------------------------------------------------------------*)

(* auxiliary function to extract the left result of a conversion.
   For instance, given
	|- 3 = 1 + 2
   this returns the 3.  Used often as
	val thethm = GSYM (ADD_CONV (--`1 + 2`--))
	val theres = lresult thethm
 *)
val lresult = #lhs o dest_eq o concl;

fun prove_append a b = GSYM (APPEND_CONV (--`APPEND ^a ^b`--));

(* return the difference of two sets *)
fun difference [] b = []
 |  difference (h::l) b =
    let val diffTail = difference l b in
	if mem h b then
	    diffTail
	else
	    h :: diffTail
    end;

(* Try to prove a predicate by applying general conversions (convs) and
   finally a conversion yielding bool (bconv).  If it proves false, warn
   the user and printed reduced values. *)
fun prove_with_convs_or_warn convs bconv tm tmascii =
(* this takes a while, so let the user know what is happening *)
(print ("(trying to prove " ^ tmascii ^ " ...)\n");
let val thm = (REDEPTH_CONV (FIRST_CONV (bconv::convs)) tm) in
if (#rhs o dest_eq o concl) thm <> (--`T`--) then
    (* term was not true - warn user and print reduction *)
    (let val reduced = (REDEPTH_CONV(FIRST_CONV convs) tm)
	 val [seta,setb] = (#2 o strip_comb o #rhs o dest_eq o concl) reduced
     in
	 print ("Could not prove " ^ tmascii ^ "\n");
	 print ">>> Here is the most reduced version\n";
	 print_thm reduced;
	 print "\n";
	 print ">>> These are missing or don't have exactly the same type\n";
	 print_term (lstsml2hol (difference (lsthol2sml seta)
					    (lsthol2sml setb)))
     end;
     raise HOL_ERR {origin_structure = "wellfrmTactics",
		    origin_function  = "prove with conversions",
		    message = "cannot prove term true"})
else
    (* get rid of =T *)
    EQT_ELIM thm
end);

fun WF_fn_syn_TAC env (asl, goal) =
let val [pre,func,post] = strip_op (--`WF_fn_syntax`--) goal
    val [fname,formls,globls,somebody] = strip_op (--`Func`--) func
    val [body] = strip_op (--`SOMEBody`--) somebody
    val xEqthm = prove_append formls globls
    val x = lresult xEqthm
    val x0Eqthm = prove_logicals x
    val x0 = lresult x0Eqthm
    val WFxsthm = prove_WF_xs x
    val DLxthm = prove_DL x
    val WFcthm = prove_WF_c body
    val ISSglob = prove_with_convs_or_warn [(GV_c_CONV env),APPEND_CONV]
			(IS_SUBSET_CONV Cvar_EQ_CONV)
				(--`IS_SUBSET (GV_c ^body) ^globls`--)
				    "IS_SUBSET (GV_c body) globls"
    val ISSbodx = prove_with_convs_or_warn [FV_c_CONV,APPEND_CONV]
			(IS_SUBSET_CONV Cvar_EQ_CONV)
				(--`IS_SUBSET (FV_c ^body) ^x`--)
				    "IS_SUBSET (FV_c body) x"
    val ISSprex = prove_with_convs_or_warn [FV_a_CONV,APPEND_CONV]
			(IS_SUBSET_TYCONF_CONV)
				(--`IS_SUBSET_TYCONF (FV_a ^pre) ^x`--)
				    "IS_SUBSET_TYCONF (FV_a pre) x"
    val ISSpostx= prove_with_convs_or_warn [FV_a_CONV,APPEND_CONV]
			(IS_SUBSET_TYCONF_CONV)
			(--`IS_SUBSET_TYCONF (FV_a ^post) (APPEND ^x ^x0)`--)
			     "IS_SUBSET_TYCONF (FV_a post) (APPEND x x0)"
    val penultThm = List.foldr (uncurry ADD_ASSUM)
			(SPEC fname
			    (MATCH_MP WF_fn_syn
			 	(LIST_CONJ [xEqthm, x0Eqthm, WFxsthm, DLxthm,
					    WFcthm, ISSglob, ISSbodx, ISSprex,
					    ISSpostx])))
			asl
in
(*  print_thm penultThm; *)
    (ACCEPT_TAC penultThm) (asl, goal)
end;

(*-----------------------------------------------------------------------
	Prove the well-formedness of a procedure by converting to 
	simplier subgoals: proving syntactic correctness and partial
	correctness.
 -----------------------------------------------------------------------*)

fun WF_fnp_TAC (asl, goal) =
let val [pre,func,post] = strip_op (--`WF_fnp`--) goal
    val [fname,formls,globls,somebody] = strip_op (--`Func`--) func
    val [body] = strip_op (--`SOMEBody`--) somebody
    val xEqthm = prove_append formls globls
    val x = lresult xEqthm
    val x0Eqthm = prove_logicals x
    val x0 = lresult x0Eqthm
    val wffnsynGoal = (--`WF_fn_syntax ^pre ^func ^post`--)
    val pwEqthm = prove_pairwiseEqual x x0
    val partlGoal=(--`(Partial(^(lresult pwEqthm)/\^pre) ^body ^post):bool`--)
in
    ([(asl,wffnsynGoal),(asl,partlGoal)],
     fn [th1,th2] => 
     let val pwEqverbose = PURE_REWRITE_RULE [pwEqthm] th2 in
(*
  (print_term(concl (CONJ xEqthm (CONJ x0Eqthm(CONJ wffnsynthm pwEqverbose))));
   print "\n");
 *)
	 (MATCH_MP WF_fnpc
		(LIST_CONJ [xEqthm, x0Eqthm, th1, pwEqverbose]))
     end)
end;

(* end of $Source: /users/lal/black/hol/Disser/RCS/wellfrmTactics.sml,v $ *)