(* $Header: /users/lal/black/hol/Disser/RCS/cast2hol.sml,v 1.21 1997/06/04 20:12:13 black Exp $ *)
(* *created  "Wed Aug  9 12:31:36 1995" *by "Paul E. Black" *)
(* *modified "Wed Jun  4 14:09:58 1997" *by "Paul E. Black" *)

(*----------------------------------------------------------------------------
	Routines to convert between C and HOL expressions.
 ----------------------------------------------------------------------------*)

new_parent "c_ast";

use "utilities.sml";

(* return a "logical" (assertion language only) version of a variable name *)
fun logicalVersion str = "^" ^ str;

(* make ptr a new unary type constructor *)
new_type {Arity=1, Name="ptr"};

(* make void a new base type (0-ary type constructor) *)
new_type {Arity=0, Name="void"};

val unknownArraySize = (--`CCid  ^(mk_str "UNK")`--);


add_theory_to_sml "string";

(* convert a :string into a :ascii list *)
val EXPLODE = new_recursive_definition {
    name = "EXPLODE",
    def = (--`(EXPLODE "" = []) /\
	      (EXPLODE (STRING a s) = CONS a (EXPLODE s))`--),
    rec_axiom = string_Axiom,
    fixity = Prefix
};

val IMPLODE = new_list_rec_definition("IMPLODE",
    (--`(IMPLODE [] = "") /\
	(!h l. IMPLODE (CONS h l) = STRING h (IMPLODE l))`--));

(* this is interesting even if it is not used *)
prove((--`!a.IMPLODE (EXPLODE a) = a`--),
    (INDUCT_THEN string_Induct) ASSUME_TAC THEN
    (* STRIP_TAC by itself fails on the subgoal IMPLODE (EXPLODE "") = "" *)
    TRY STRIP_TAC THEN
    ASM_REWRITE_TAC [STRING_11, IMPLODE, EXPLODE]
);

(* character constants are represented by strings since ASCII's 
   are so ugly.  CHAR converts a string into an ASCII *)
val CHAR = new_definition("CHAR", (--`!a.CHAR a = HD (EXPLODE a)`--));

(*-----------------------------------------------------------------------
		Some semantics of address-of and dereference
 -----------------------------------------------------------------------*)

new_constant{Name = "deref", Ty = ==`:'a ptr ->'a`==};

new_constant{Name = "adrof", Ty = ==`:'a -> 'a ptr`==};

val deref_adrof_I =
    mk_thm([], (--`!(x:'a) . deref (adrof x) = x`--));

(*---------------------------------------------------------------------------
		Definitions and theorems for arrays
 ---------------------------------------------------------------------------*)

(* C arrays are functions from numbers (indices) to values and the size of 
   the array.  The lower bound is 0 like the C AST representation.  *)
define_structure `CArray = CA of (num -> 'a) => num`;

val CArray_Ind = prove_induction_thm CArray;

val CArray_Cons = prove_cases_thm CArray_Ind handle e=>Raise e;

rec_define "CArray" `CA_SZ (CA (f:num -> 'a) sz) = sz`;

rec_define "CArray" `CA_FN (CA (f:num -> 'a) sz) = f`;

(* this is the function [X|i:y] given in Reynolds page 112 *)
(* a new array which is the same except at i, which is y *)
rec_define "CArray"
    `CA_PUT (CA (f:num -> 'a) sz) i y =
	CA (\j . (0 <= i /\ i < sz) =>
				((i=j) => y | f j) | (@x.F))
		sz`;

(* a more useful version which takes a variable (rather than a
   constructor) as the array operand *)
val CA_PUT_thm = prove (
    (--`CA_PUT ar i (y:'a) =
	CA (\j . (0 <= i /\ i < CA_SZ ar) =>
				((i=j) => y | ((CA_FN ar) j)) | (@x.F))
		(CA_SZ ar)`--),
    STRIP_ASSUME_TAC (SPEC (--`ar:'a CArray`--) CArray_Cons) THEN
    ASM_REWRITE_TAC [CA_FN,CA_SZ,CA_PUT]
);

(* return the element of the array *)
rec_define "CArray" `CA_IDX (CA (f:num -> 'a) sz) i =
			((0 <= i /\ i < sz) => (f i) | (@ (x:'a) . F))`;

(* WARNING: use ONCE_REWRITE_... with this since it is "recursive" *)
val CArray_Decomp = prove (
    (--`!ar:'a CArray. ar = CA (CA_FN ar) (CA_SZ ar)`--),
    STRIP_TAC THEN
    STRIP_ASSUME_TAC (SPEC (--`ar:'a CArray`--) CArray_Cons) THEN
    ASM_REWRITE_TAC [CArray_Cons,CA_FN,CA_SZ]
);

(*-----------------------------------------------------------------------
		 Convert between HOL and C AST types.
 -----------------------------------------------------------------------*)

(* generalization of map to build comma separated lists, etc. *)
fun mapjoin f joinfn emptyres lst =
    if lst = [] then
	emptyres
    else if length lst < 2 then
	f (hd lst)
    else
	joinfn (f (hd lst)) (mapjoin f joinfn emptyres (tl lst));

(* test

mapjoin I (fn x=>fn y=>x ^ ", " ^ y) "" ["a", "b", "c"]
 = "a, b, c";

mapjoin I (fn x=>fn y=>x ^ ", " ^ y) "" [] = "";

*)

(* convert a HOL type into an equivalent C type.  This should be the
   inverse of ctype2hol *)
fun holtype2c holtype =
    (* hol types carry the *structure* while C types only have
	a name, so change the HOL names to a string *)
let fun holtype2str htype =
    if is_vartype htype then
	(* remove leading apostrophe (') *)
	(implode o tl o explode o dest_vartype) htype
    else
    let val {Args=ars,Tyop=top} = dest_type htype in
	if length ars > 0 then
	    "(" ^ 
	       mapjoin holtype2str (fn x=>fn y=>x^","^y) "" ars ^
	    ")" ^ top
	else
	    top
    end
    fun holtype2Struct htyp = (--`Struct ^(mk_str (holtype2str holtype))`--)
in
if is_vartype holtype then
    holtype2Struct holtype
else
let val {Args=args,Tyop=tyop} = dest_type holtype in
if holtype = (==`:ascii`==)	then (--`Char`--)
else if holtype = (==`:num`==)	then (--`Int`--)
else if holtype = (==`:bool`==)	then (--`Int`--)
else if holtype = (==`:void`==)	then (--`Void`--)
else if holtype = (==`:string`==) then
    (--`Ptr Char`--)
else if tyop = "ptr" then
    (--`Ptr ^(holtype2c (hd args))`--)
else if tyop = "list" then
    (--`Array ^(holtype2c (hd args)) ^unknownArraySize`--)
else if tyop = "fun" then
    (--`Funty ^(holtype2c (el 1 args)) ^(holtype2c (el 2 args))`--)
else
    holtype2Struct holtype
end end;

(* test cases

test_result (holtype2c (==`:num list`==)) (--`Array Int (CCid "UNK")`--);
test_result (holtype2c (==`:'tm ptr`==)) (--`Ptr (Struct "tm")`--);
test_result (holtype2c (==`:string -> ascii`==)) (--`Funty (Ptr Char) Char`--);
test_result (holtype2c (==`:num # 'FILE`==)) (--`Struct "(num,FILE)prod"`--);

*)

local (* for ctype2hol *)

(* divide a list at the first ch.  The character ch is in neither 
   list.  If an open paren is found, take everything to the matching
   closing paren even if there is a ch. *)
fun divnest [] ch = ([],[])
 |  divnest (c1::ct) ch =
	if c1 = ch then
	    ([], ct)
	else if c1 = #"(" then
	    let val (nesthd, nesttl) = divnest ct #")"
		val (divhd, divtl) = divnest nesttl ch in
		(#"("::(append nesthd (#")"::divhd)), divtl)
	    end
	else
	    let val (divhd, divtl) = divnest ct ch in
		(c1::divhd, divtl)
	    end;

(* test

divnest (explode "ab(cd,e(f,g,h)i)j,k") #"," =
	([#"a",#"b",#"(",#"c",#"d",#",",#"e",#"(",#"f",#",",#"g",#",",#"h",
	  #")",#"i",#")",#"j"],[#"k"]);

*)

(* turn a user type name, e.g. "FILE" into a HOL type, e.g., ==`:'FILE`==
   and a complex name, e.g. "(num,FILE)prod" into ==`:num # 'FILE`== *)
fun parsetylist tylist =
    let val (firstAr,restAr) = divnest tylist #"," in
	if restAr = [] then
	    [usrtype2hol firstAr]
	else
	    (usrtype2hol firstAr) :: (parsetylist restAr)
    end
and usrtype2hol unar =
    if hd unar = #"(" then (* type constructor *)
	let val (tyconstructorR,tylistR) = divnest (rev (tl unar)) #")"
	    val tyconstr = implode (rev tyconstructorR)
	    val tylist = parsetylist (rev tylistR)
	in
	    mk_type{Args=tylist, Tyop=tyconstr}
	end
    else
	mk_type{Args=[], Tyop=(implode unar)}
	    handle HOL_ERR _ =>
		mk_vartype ("'" ^ (implode unar));

in

(* convert a C type to the equivalent HOL type *)
fun ctype2hol ctype =
    if is_comb ctype then
	let val (constr,basetype) = strip_comb ctype in
	    if constr = (--`Array`--) then
		let val hbasetype = ctype2hol (hd basetype) in
		    (* change :(ascii)list into :string *)
		    if hbasetype = (==`:ascii`==) then
			(==`:string`==)
		    else
			(==`:^(ty_antiq hbasetype) list`==) 
		end else
	    if constr = (--`Ptr`--) andalso basetype = [(--`Char`--)] then
		(==`:string`==) else
	    if constr = (--`Ptr`--) then
		(==`:^(ty_antiq (ctype2hol (hd basetype))) ptr`==) else
	    if constr = (--`Struct`--) then
		(usrtype2hol o explode o dest_str o hd) basetype else
		(print_term ctype;print "\n";
		    raise Fail "unknown constructor in ctype2hol")
	end
    else
	if ctype = (--`Char`--) then (==`:ascii`==) else
	if ctype = (--`Int`--)  then (==`:num`==)   else
	if ctype = (--`Void`--) then (==`:void`==)  else
	    (print_term ctype;print "\n";
		raise Fail "unknown ctype in ctype2hol")
end;

(* tests

fun test_types ty1 ty2 = test_result (ty_antiq ty1) (ty_antiq ty2);

test_types (ctype2hol (--`Ptr Char`--)) (==`:string`==);
test_types (ctype2hol (--`Ptr Int`--)) (==`:num ptr`==);
test_types (ctype2hol (--`Void`--)) (==`:void`==);

val tt4 = (==`:num # ascii # bool`==);

test_types (ctype2hol (holtype2c tt4)) tt4;

*)

(*-----------------------------------------------------------------------
		Return the type of a C AST expression.
 -----------------------------------------------------------------------*)

local

fun is_boolean opr =
    mem opr [(--`Eq`--),(--`NEq`--),(--`Lt`--),(--`Gt`--),
	     (--`LEq`--),(--`GEq`--),(--`And`--),(--`Or`--)];

in

(* return the C type of the given expression *)
fun ctype_of expr =
let val (marker,terms) = strip_comb expr in
    if marker = (--`Call`--) then
	ctype_of (hd terms)
    else if marker = (--`Assign`--) then
	ctype_of (hd terms)
    else if marker = (--`LUnary`--) then
	ctype_of (el 2 terms)
    else if marker = (--`Unary`--) then
	if el 1 terms = (--`Not`--) then
	    (--`Int`--)
	else
	    ctype_of (el 2 terms)
    else if marker = (--`Binary`--) then
	if is_boolean (el 2 terms) then
	    (* relational, equality, and logical operators return int *)
	    (--`Int`--)
	else
	    (* SKIMP - doesn't do ptr-ptr or casting right *)
	    ctype_of (el 1 terms)
    else if marker = (--`Lval`--) then
	ctype_of (el 1 terms)
    else if marker = (--`Var`--) then
	el 3 terms
    else if marker = (--`Const`--) then
	el 2 terms
    (* Lvalues *)
    else if marker = (--`Vref`--) then
	ctype_of (el 1 terms)
    else if marker = (--`Aryref`--) then
	(* return the base type *)
	(el 1 o strip_op (--`Array`--) o el 3 o strip_op (--`Var`--) o el 1)
							terms
    else if marker = (--`Field`--) then
	ctype_of (el 2 terms)
    else
	(print_term expr; print "\n"; raise Fail "SKIMP ctype_of 1")
end;

end;

(* tests

test_result (ctype_of (--`Binary (Lval (Vref (Var "a" 0 (Ptr Char)))) Gt
				 (Lval (Vref (Var "b" 0 (Ptr Char))))`--))
	    (--`Int`--);

test_result (ctype_of (--`Binary (Lval (Vref (Var "a" 0 Char))) Add
				 (Const (CCid "b") Char)`--))
	    (--`Char`--);

*)

(*-----------------------------------------------------------------------
	  Convert from C AST expressions to equivalent HOL.
 -----------------------------------------------------------------------*)

(* the separator between the name and the variant number *)
val aprime = #"'";

local (* for holvar2c *)

(* divide the array of characters into a string of the characters preceeding
   the marker and an array of everything from the marker onward *)
fun divideat ch strsofar [] = (strsofar, [])
 |  divideat ch strsofar (x::xt) =
	if ch = x then
	    (strsofar, (x::xt))
	else
	    divideat ch (strsofar ^ (str x)) xt;

(* tests

divideat aprime "living" (explode "gary'indiana'usa");

divideat aprime "" (explode "webster");

*)

(* return the last element of a list *)
fun last lst = el (length lst) lst;

(* test

last (explode "fixed");

*)

in

(* convert a HOL variable to a C variable *)
fun holvar2c trm =
let val {Name=vname, Ty=vhtype} = dest_var trm
    val cvty = holtype2c vhtype
    val (basenm,restary) = divideat aprime "" (explode vname)
in
    if null restary orelse restary = [aprime] then (* not a variant *)
	(--`Var ^(mk_str vname) 0 ^cvty`--)
    else (* a variant *)
    let val vary =
	if last restary = aprime then
	    butlast (tl restary)
	else
	    tl restary
    in
	(--`Var ^(mk_str basenm) ^(mk_const{Name=implode vary,Ty=(==`:num`==)})
								^cvty`--)
    end
end;

(* tests

test_result (holvar2c (--`able:num`--))
		(--`Var "able" 0 Int`--);

test_result (holvar2c (mk_var{Name="b'1", Ty=(==`:num`==)}))
		(--`Var "b" 1 Int`--);

test_result (holvar2c (mk_var{Name="b23'34'", Ty=(==`:string`==)}))
		(--`Var "b23" 34 (Ptr Char)`--);

*)

end;
    

(* make sure the expression yields a bool *)
fun castToBool cterm =
    if type_of cterm = (==`:bool`==) then
	cterm
    else if is_var cterm then
	let val vname = (#Name o dest_var) cterm in
	    mk_var{Name=vname, Ty=(==`:bool`==)}
	end
    else
	(--`( ^cterm ) = 0`--);

(* convert a C expression to a HOL expression. *)
fun cexpr2hol ccode =
let val (marker,terms) = strip_comb ccode in
    if marker = (--`Const`--) then
    let val {Rator=copr,Rand=cval} = dest_comb (el 1 terms)
	val valtype = ctype2hol (el 2 terms)
    in
	if copr = (--`CCid`--) then (* symbolic constant *)
	    mk_var{Name=dest_str cval, Ty=valtype}
	else if copr = (--`CCstr`--) then (* some sort of string constant *)
	    if valtype = (==`:ascii`==) then
		(--`CHAR ^cval`--)
	    else
		cval
	else if copr = (--`CCint`--) then (* some sort of numeric constant *)
	    cval
	else (* unknown *)
	    (print "Unknown C expression: "; print_term ccode; print "\n";
	     raise Fail "Unknown Const C expression")
    end
    else if marker = (--`Var`--) then
    let val name = dest_str (el 1 terms)
	val vari = (el 2 terms)
	val variant =
	    if vari = (--`0`--) then
		""
	    else
		(str aprime) ^ (#Name (dest_const vari))
	val variname = name ^ variant
	val rawtype = (el 3 terms)
    in
	if is_comb rawtype andalso (#1 o strip_comb) rawtype=(--`Array`--) then
	    (* an array variable *)
	    let val basetype = strip_op (--`Array`--) rawtype
		val arbasetype = ctype2hol (el 1 basetype)
		val arsize = cexpr2hol (--`Const ^(el 2 basetype) Int`--)
		val arvar = mk_var{Name=variname,
				Ty=(==`:^(ty_antiq arbasetype) CArray`==)}
	    in
		(--`CA (CA_FN ^arvar) ^arsize`--)
	    end
	else
	    (* a plain variable *)
	    mk_var{Name=variname, Ty=ctype2hol rawtype}
    end
    else if marker = (--`Lval`--) then
	    cexpr2hol (hd terms)
    else if marker = (--`Vref`--) then
	    cexpr2hol (hd terms)
    else if marker = (--`Aryref`--) then
	let val ar = cexpr2hol (el 1 terms)
	    val inexp = cexpr2hol (el 2 terms)
	    val arexp =
		(* if array is a string, add conversion to list of ascii *)
		if type_of ar = (==`:string`==) then
		    (--`EXPLODE ^ar`--)
		else
		    ar
	in
	    (--`CA_IDX ^arexp ^inexp`--)
	end
    else if marker = (--`Deref`--) then
	(--`deref ^(cexpr2hol (el 1 terms))`--)
    else if marker = (--`Field`--) then
	let val var = cexpr2hol (el 1 terms)
	    val accessor = cexpr2hol (el 2 terms)
	    val {Name=acnm,Ty=actype} = dest_var accessor
	in
	    mk_comb {Rator=mk_var{Name=acnm,
				  Ty=mk_type{Tyop="fun",
					     Args=[type_of var, actype]}},
		     Rand=var}
	end
    else if marker = (--`LUnary`--) then
	let val [oper,lval] = terms
	    val rhhol = cexpr2hol lval
	in
	    if oper = (--`AdrOf`--) then
		(--`adrof ^rhhol`--)
	    else
		(print_term ccode; print "\n";
		 raise Fail "cexpr2hol SKIMP 2")
	end
    else if marker = (--`Unary`--) then
	let val [oper,rhs] = terms
	    val rhhol = cexpr2hol rhs
	in
	    if oper = (--`Not`--) then
		(--`~ ^(castToBool rhhol)`--)
	    else
		(print_term ccode; print "\n";
		 raise Fail "cexpr2hol SKIMP 5")
	end
    else if marker = (--`Binary`--) then
	let val [lhs,oper,rhs] = terms in
	let val lhhol = cexpr2hol lhs and
		rhhol = cexpr2hol rhs in
	    if oper = (--`Add`--) then
		(--`^lhhol + ^rhhol`--)
	    else if oper = (--`Sub`--) then
		(--`^lhhol - ^rhhol`--)
	    else if oper = (--`Mul`--) then
		(--`^lhhol * ^rhhol`--)
	    else if oper = (--`Div`--) then
		(--`^lhhol DIV ^rhhol`--)
	    else if oper = (--`Mod`--) then
		(--`^lhhol MOD ^rhhol`--)
	    else if oper = (--`ShL`--) then
		(--`^lhhol * 2 EXP ^rhhol`--)
	    else if oper = (--`ShR`--) then
		(--`^lhhol DIV 2 EXP ^rhhol`--)
	    else if oper = (--`Eq`--) then
		(--`^lhhol = ^rhhol`--)
	    else if oper = (--`NEq`--) then
		(--`~(^lhhol = ^rhhol)`--)
	    else if oper = (--`Lt`--) then
		(--`^lhhol < ^rhhol`--)
	    else if oper = (--`Gt`--) then
		(--`^lhhol > ^rhhol`--)
	    else if oper = (--`LEq`--) then
		(--`^lhhol <= ^rhhol`--)
	    else if oper = (--`GEq`--) then
		(--`^lhhol >= ^rhhol`--)
	    else if oper = (--`And`--) then
		(--`^lhhol /\ ^rhhol`--)
	    else if oper = (--`Or`--) then
		(--`^lhhol \/ ^rhhol`--)
	    else if oper = (--`BAnd`--) then
		(--`(BITAND ^lhhol ^rhhol):num`--)
	    else if oper = (--`BOr`--) then
		(--`(BITOR  ^lhhol ^rhhol):num`--)
	    else if oper = (--`BXor`--) then
		(--`(BITXOR ^lhhol ^rhhol):num`--)
	    else
		(print_term ccode;print "\n";
		 raise Fail "cexpr2hol SKIMP 3")
	end end
    else
	(print_term ccode;print "\n";raise Fail "cexpr2hol SKIMP 4")
end;

(* test cases

val _ = " 12 ";
test_result (cexpr2hol (--`Const(CCint 12)Int`--))	(--`12`--);
val _ = " a string constant ";
test_result (cexpr2hol (--`Const(CCstr "(*Y/*)m/(*d *)T") (Ptr Char)`--))
						(--`"(*Y/*)m/(*d *)T"`--);
val _ = " a character constant ";
test_result (cexpr2hol (--`Const (CCstr "a") Char`--)) (--`CHAR "a"`--);
val _ = " complicated type ";
test_result (cexpr2hol (--`Var "j" 0 (Struct "(FILE,(num,ascii)prod)prod")`--))
						(--`j:'FILE # num # ascii`--);
val _ = " str ";
test_result (cexpr2hol (--`Lval (Vref (Var "str" 0 (Ptr Char)))`--))
						(--`str:string`--);
val _ = " void type ";
test_result (cexpr2hol (--`Lval (Vref (Var "novalue" 0 Void))`--))
						(--`novalue:void`--);
val _ = " &y, where y is struct z ";
test_result (cexpr2hol (--`LUnary AdrOf (Vref (Var "y" 0 (Struct "z")))`--))
						(--`(adrof :'z->'z ptr)y`--);
val _ = " ! source'2 ";
test_result (cexpr2hol (--`Unary Not(Lval (Vref(Var "source" 2 Int)))`--))
						(--`~source'2`--);
val _ = " *y <= r ";
test_result (cexpr2hol (--`Binary (Lval (Deref(Lval(Vref(Var"y" 0(Ptr Int))))))
					LEq (Lval (Vref(Var "r" 0 Int)))`--))
					(--`((deref :num ptr->num)y) <= r`--);
val _ = " c != y[j] ";
test_result (cexpr2hol (--`Binary (Lval (Vref(Var "c" 0 Char))) NEq
				(Lval(Aryref(Var"y" 0(Array Char(CCid "MAX")))
					      (Lval(Vref(Var "j"0 Int)))))`--))
			(--`~(c:ascii = CA_IDX (CA (CA_FN y) MAX) j)`--);
val _ = " #define robber ...    person == robber ";
test_result (cexpr2hol
	(--`Binary (Lval (Vref(Var "person" 0 (Ptr(Struct "FILE"))))) Eq
		   (Const (CCid "robber") (Ptr(Struct "FILE")))`--))
				(--`person:'FILE ptr = robber`--);
val _ = " k << (x % 7) ";
test_result (cexpr2hol 
	(--`Binary (Lval (Vref(Var "k" 0 Int))) ShL
		   (Binary (Lval(Vref(Var "x" 0 Int))) Mod
						(Const(CCint 7)Int))`--))
						(--`k * (2 EXP (x MOD 7))`--);
val _ = " j >> (count-1) ";
test_result (cexpr2hol (--`Binary (Lval (Vref (Var "j" 0 Int))) ShR
				  (Binary (Lval (Vref (Var "count" 0 Int)))
				      Sub (Const(CCint 1)Int))`--))
						(--`j DIV (2 EXP(count-1))`--);
val _ = " Si & buf.st_mode ";
test_result (cexpr2hol (--`Binary (Lval (Vref (Var "Si" 0 Int))) BAnd
			(Lval (Field (Vref (Var "buf" 0 (Struct "stat")))
				     (Var "st_mode" 0 Char)))`--))
		(--`(BITAND (Si:num) ((st_mode:'stat -> ascii) buf)):num`--);

print "** Tests done. **\n";

*)

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