(* $Header: /users/lal/black/hol/Disser/RCS/c_ast.sml,v 1.22 1997/05/28 15:50:42 black Exp $ *)
(* *created  "Wed Oct  4 10:14:27 1995" *by "Paul E. Black" *)
(* *modified "Wed May 28 09:48:40 1997" *by "Paul E. Black" *)

(*----------------------------------------------------------------------------
	Abstract syntax representation particularly suited to C
 ----------------------------------------------------------------------------*)

system "/bin/rm c_ast.thms";
new_theory "c_ast";

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

(* constants are either #define identifiers or the actual constant value such
   as a number, string, or character.  Identifiers are "carried" by CCid.  
   The others be "carried" by HOL types string or num. *)
val CConst_AX = define_type {
    name = "CConst_AX",
    type_spec =
	`CConst =
	    CCid of string |
	    CCstr of string |
	    CCint of num`,
    fixities = [Prefix, Prefix, Prefix]};

use "proveDistinct.sml";

save_thm("CConsts_all_distinct", prove_all_constructors_distinct CConst_AX);

(* C types are either char, int, void, pointer, array, struct, or functions. *)
(* "Array" means array of CType, size given by the constant. *)
(* SKIMP - float, double, etc. not included
	- short, unsigned, long, etc. not included
	- function declarations are always curried
*)
val CType_AX = define_type {
    name = "CType_AX",
    type_spec =
	`CType =
	    Char |
	    Int  |
	    Void |
	    Ptr of CType  |
	    Array of CType => CConst |
	    Struct of string |
	    Funty of CType => CType`,
    fixities = [Prefix, Prefix, Prefix, Prefix, Prefix, Prefix, Prefix]};

save_thm("CTypes_all_distinct", prove_all_constructors_distinct CType_AX);

(* end-of-string or `\0` byte *)
new_constant{Name = "EOS", Ty = ==`:string`==};

(* carriage return or `\r` byte *)
new_constant{Name = "CR", Ty = ==`:string`==};

(* C variables are a name, a disambiguator, and a type *)
val Cvar_AX = define_type {
    fixities = [Prefix],
    name = "Cvar_AX",
    type_spec =
	`Cvar = Var of string => num => CType`};

save_thm("Var_one_one", prove_constructors_one_one Cvar_AX);

(* C binary operators *)
val Cbinop_AX = define_type {
    name = "Cbinop_AX",
    type_spec =
	`Cbinop = Mul | Div | Mod | Add | Sub |
	      ShL | ShR |
	      Eq | NEq | Lt | Gt | LEq | GEq |
	      And | Or | BAnd | BOr | BXor`,
    fixities = [Prefix, Prefix, Prefix, Prefix, Prefix,
		Prefix, Prefix,
		Prefix, Prefix, Prefix, Prefix, Prefix, Prefix,
		Prefix, Prefix, Prefix, Prefix, Prefix]};

(* C unary operators which take an expression and yield an expression *)
val Cunaryop_AX = define_type {
    name = "Cunaryop_AX",
    type_spec =
	`Cunaryop = Not | BNot`,
    fixities	  = [Prefix, Prefix]};

(* C unary operators which take an lvalue and yield an expression *)
val Clunaryop_AX = define_type {
    name = "Clunaryop_AX",
    type_spec =
	`Clunaryop = AdrOf | PreInc | PostInc | PreDec | PostDec`,
    fixities	   = [Prefix, Prefix, Prefix, Prefix, Prefix]};


(* different C expressions *)

(* must have mutrec.hol_lib in local directory *)
load_library_in_place(find_library "mutrec");

val string_ty = ==`:string`==;
val cconst_ty = ==`:CConst`==;
val ctype_ty = ==`:CType`==;
val cvar_ty = ==`:Cvar`==;
val cbinop_ty = ==`:Cbinop`==;
val cunaryop_ty = ==`:Cunaryop`==;
val clunaryop_ty = ==`:Clunaryop`==;

structure Cexpressions : MutRecTypeInputSig =
struct

structure TypeInfo = TypeInfo

open TypeInfo

(*---------- GRAMMAR ------------------------------------------------

	ParamList = PL <CExpr> <ParamList> |
		PLnull

	Lvalue = Vref <Cvar> |
		Aryref <Cvar> <CExpr> |
		Deref <CExpr> |
		Field <Lvalue> <Cvar> |
		Arrow <Lvalue> <Cvar>

	CExpr = Const <CConst> <CType> |
		Lval <Lvalue> |
		Assign <Lvalue> <CExpr> |
		OpAsgn <Lvalue> <Cbinop> <CExpr> |
		Binary <CExpr> <Cbinop> <CExpr> |
		LUnary <Clunaryop> <Lvalue> |
		Unary <Cunaryop> <CExpr> |
		Condl <CExpr> <CExpr> <CExpr> |
		Comma <CExpr> <CExpr> |
		Call <Cvar> <ParamList>

 --------------------------------------------------------------------*)

(* The specification of the type *)

val mut_rec_ty_spec =
[{type_name = "ParamList",
  constructors = 
      [{name = "PL",	    arg_info = [being_defined "CExpr",
					being_defined "ParamList"]},
       {name = "PLnull",    arg_info = []}]},
 {type_name = "Lvalue",
  constructors =
      [{name = "Vref",      arg_info = [existing cvar_ty]},
       {name = "Aryref",    arg_info = [existing cvar_ty,
					being_defined "CExpr"]},
       {name = "Deref",     arg_info = [being_defined "CExpr"]},
       {name = "Field",	    arg_info = [being_defined "Lvalue",
					existing cvar_ty]},
       {name = "Arrow",	    arg_info = [being_defined "Lvalue",
					existing cvar_ty]}]},
 {type_name = "CExpr",
  constructors =
      [{name = "Const",	    arg_info = [existing cconst_ty,
					existing ctype_ty]},
       {name = "Lval",	    arg_info = [being_defined "Lvalue"]},
       {name = "Assign",    arg_info = [being_defined "Lvalue",
					being_defined "CExpr"]},
       {name = "OpAsgn",    arg_info = [being_defined "Lvalue",
					existing cbinop_ty,
					being_defined "CExpr"]},
       {name = "Binary",    arg_info = [being_defined "CExpr",
					existing cbinop_ty,
					being_defined "CExpr"]},
       {name = "LUnary",    arg_info = [existing clunaryop_ty,
					being_defined "Lvalue"]},
       {name = "Unary",	    arg_info = [existing cunaryop_ty,
					being_defined "CExpr"]},
       {name = "Condl",     arg_info = [being_defined "CExpr",
					being_defined "CExpr",
					being_defined "CExpr"]},
       {name = "Comma",     arg_info = [being_defined "CExpr",
					being_defined "CExpr"]},
       {name = "Call",	    arg_info = [existing cvar_ty,
					being_defined "ParamList"]}]}
]

val New_Ty_Existence_Thm_Name = "cexprs_existence_thm"
val New_Ty_Induct_Thm_Name = "cexprs_induction_thm"
val New_Ty_Uniqueness_Thm_Name = "cexprs_uniqueness_thm"
val Constructors_One_One_Thm_Name = "cexprs_constructors_one_one"
val Constructors_Distinct_Thm_Name = "cexprs_constructors_distinct"
val Cases_Thm_Name = "cexprs_cases"

end; (* struct *)

structure Cexpressions_Def = MutRecTypeFunc (Cexpressions);

(*---------- Convert a ParamList into a list of CExpr's. -------------------*)

val _ = define_mutual_functions
{name = "PL2CEL_DEF",
 rec_axiom = cexprs_existence_thm,
 fixities = NONE,
 def =
    (--`(PL2CEL PLnull = ([]:CExpr list)) /\
	(PL2CEL (PL h l) = (CONS h (PL2CEL l)))`--)
};


(* C statements *)
val CStmt_AX = define_type {
    name = "CStmt_AX",
    type_spec =
	`CStmt = EmptyStmt |
	    Simple of CExpr |
	    If of CExpr => CStmt |
	    IfElse of CExpr => CStmt => CStmt |
	    CWhile of CExpr => CStmt |
	    DoWhile of CStmt => CExpr |
	    Seq of CStmt => CStmt |
	    Block of Cvar list => CStmt |
	    Ret of CExpr |
	    EmptyRet |
	    Break |
	    Cont`,
    fixities = [Prefix, Prefix, Prefix, Prefix, Prefix, Prefix,
		Prefix, Prefix, Prefix, Prefix, Prefix, Prefix]};

(* Optional body type *)
val Cbody_AX = define_type {
    name = "Cbody_AX",
    type_spec =
	`Cbody = SOMEBody of CStmt |
		 NOBody`,
    fixities = [Prefix, Prefix]};

(* Function declaration.  A function is
	- function name and return type,
	- a list of paramaters,
	- the set (list) of globals (potentially) read or written,
	- an (optional) body
 *)
val Cfunction_AX = define_type {
    name = "Cfunction_AX",
    type_spec =
	`Cfunction = Func of Cvar => Cvar list => Cvar list => Cbody`,
    fixities = [Prefix]};

(* A C file consists of variable declarations and function definitions *)
val Cfile_AX = define_type {
    name = "Cfile_AX",
    type_spec =
	`Cfile = EndOfCFile |
	    Cfdcl of Cvar list => Cfile |
	    Cffun of Cfunction => Cfile`,
    fixities = [Prefix, Prefix, Prefix]};

close_theory();
export_theory();

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