Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <199304161633.AA11270@panther.cs.uidaho.edu>
To: shb@com.oracorp
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Records in HOL object language?
In-Reply-To: Your message of Fri, 16 Apr 93 12:22:22 -0400. <9304161622.AA13765@sparta.oracorp.com>
Date: Fri, 16 Apr 93 09:33:40 -0700
From: Phil Windley <windley@edu.uidaho.cs.panther>


On Fri, 16 Apr 93 12:22:22 EDT, shb@oracorp.com wrote:
+------------
| What HOL object-language constructs would people recommend that I use
| when what I'd really like are record-valued (in C, structure-valued)
| functions?

I'm not sure its exactly what you're looking for, but I built some
functions on top of the type definition functions that I use when I want a
record.  I'll include the code below.

A call like:

create_record `packet`
    [`p_opcode`,           ":opt_ty";       % opcode %
     `p_blocksize`,        ":bs_ty";        % block size %
     `p_byte_enable_0`,     ":bt4";         % 16 possibilities %      
     `p_dataword_0`,        ":wordn";       % a data word %
     `p_byte_enable_1`,     ":bt4";         % 16 possibilities %
     `p_dataword_1`,        ":wordn";       % a data word %
     `p_byte_enable_2`,     ":bt4";         % 16 possibilities %
     `p_dataword_2`,        ":wordn";       % a data word %
     `p_byte_enable_3`,     ":bt4";         % 16 possibilities %
     `p_dataword_3`,        ":wordn";       % a data word %
    ];;

creates a data type ":packet" as well as a number of selector and mutator
functions.  There are theorems proved about the structure that are handy
for reasoning about it.

The package will also do enumerations and multiarm records (something like
variant records).

--phil--


%----------------------------------------------------------------

   File:         datatypes.ml

   Description:  

   Defines a functions, create_datatype, that uses the abstract 
   type package to create a datatype and prove some useful theorems
   about the datatype.  Datatypes are simply an abstract type with 
   appropriate selector and mutator functions defined.

   Author:       (c) P. J. Windley 1992, 1993

   Modification History:

   09NOV92 [PJW] --- Original file taken from records.ml.

   11NOV92 [PJW] --- Modified to support single arm record declarations.
                     Both multi--arm data structures and single arm
		     records are now supported by the same code.

   08MAR93 [PJW] --- Added create_enum for creating enumerations.

----------------------------------------------------------------%

message `loading datatypes package`;;

begin_section datatypes;;

%----------------------------------------------------------------

 load the patch to concat if the following ml statement prints a 
 number less than 5000 and HOL version <= 2.00.

 lisp `(print call-arguments-limit)`;;


let test_string n = 
    letrec aux s i = 
        (i = 0) => s | aux (`x`^s) (i-1) in
    aux `` n;;

----------------------------------------------------------------%

% message `patching concat`;loadf `concat-patch`;; %

%----------------------------------------------------------------
 define some general list functions
----------------------------------------------------------------%

let int_to_term = (((C (curry mk_const)) ":num") o string_of_int) and
    term_to_int = (int_of_string o fst o dest_const);;

letrec for n lst = 
    (n=0) => []
           | (hd lst).(for (n-1) (tl lst));;


%----------------------------------------------------------------
 define auxilliary functions for new_abstract_representation
----------------------------------------------------------------%

let datatype_type_info = 
       (type_of o snd o dest_comb o 
	fst o dest_eq o snd o strip_forall o hd o conjuncts o snd o 
        strip_forall o snd o dest_abs o snd o dest_comb o 
        snd o strip_forall o concl) ;;

let dest_all_type ty = 
     is_vartype ty => (dest_vartype ty,[]:(type)list) | dest_type ty;;

let string_from_type ty =
    letrec string_aux ty = 
	let s,tl = dest_all_type ty in
	null tl => s |
	let sl = map string_aux tl in
	`(`^(itlist (\x y. x^`,`^y) (butlast sl) (last sl))^`)`^s in
    (string_aux ty)^` `;;


letrec replace (x,y) (lst:(*)list) =
         if (lst = []) then []
         else let (z.zs) = lst in
              if (x = z) then (y.zs)
              else (z.(replace (x,y) zs));;

letrec vector_map fl argl = 
    (null fl) => []
               | (hd fl) (hd argl) . (vector_map (tl fl) (tl argl));;

letrec mult_map fl argl =
    (null fl) => []
               | map (hd fl) argl . (mult_map (tl fl) argl);;

letrec map3 (f:(*#**#***)->****) lst = 
       (null (fst lst)) => [] | 
	   let head = (hd # (hd # hd)) lst and
	       rest = (tl # (tl # tl)) lst in
	   (f head) . (map3 f rest);;

%----------------------------------------------------------------
 function to create a multiarm (variant) record
----------------------------------------------------------------%

let create_datatype name recs =
    let cons_names, lsts = split recs in
    let nls,tls = split(map split lsts) in
    let ty_str_lsts = map (map string_from_type) tls in
    let cons_strs =
	map2  (\nl, sl . nl^` `^(itlist (\x y. x^`  `^y) sl ``)) 
	      (cons_names,ty_str_lsts) in
    let ty_str = 
	name^` = `^(itlist (\x y.x^` | `^y) 
			   (butlast cons_strs) 
			    (last cons_strs)) in
    let ty_axiom = 
        % print_string `.`; %
        define_type name ty_str in
    let cons_terms = 
       map (snd o dest_comb o fst o dest_eq o snd o strip_forall)
           ((conjuncts o snd o dest_abs o snd o dest_comb o snd o 
	     strip_forall o concl) ty_axiom) in
    let make_rec_def cons_term (x, y) =
        % print_string `.`; %
	new_recursive_definition false ty_axiom x 
	"^(mk_var (x,mk_type(`fun`,[type_of cons_term;
                                    type_of y]))) ^cons_term = ^y" in
    let rec_thml = 
	vector_map (map map2 (map make_rec_def cons_terms))
		   (combine(nls,map (snd o strip_comb) cons_terms)) in
    let selectors = 
	save_thm(name^`_selectors`,
		 LIST_CONJ(itlist (curry $@) rec_thml [])) in
    let make_update_def cons_term (x,y) = 
        % print_string `.`; %
        let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
	let new_name = x^`_update` in 
	let new_y = variant cons_term_vars y in
	let new_cons_term = subst [new_y,y] cons_term in
	let update_type = 
	    mk_type(`fun`,[type_of y;
			   mk_type(`fun`,[type_of cons_term;
					  type_of cons_term])]) in
	new_recursive_definition false ty_axiom new_name 
	   "^(mk_var (new_name,update_type))
	    ^new_y
	    ^cons_term = ^new_cons_term" in
    let update_thml = 
	vector_map (map map2 (map make_update_def cons_terms))
		   (combine(nls,map (snd o strip_comb) cons_terms)) in
    let updates = 
	save_thm(name^`_updates`,
		 LIST_CONJ(itlist (curry $@) update_thml [])) in
    let make_pred_def name cons_term =
        let pred_name = `IS_`^name in
        let ((cons_rator,_),_) = ((dest_const # I) o strip_comb) cons_term in
        let boolval = if (cons_rator = name) then "T" else "F" in
        "^(mk_var (pred_name,
                   mk_type(`fun`,[type_of cons_term;":bool"]))) 
         ^cons_term = ^boolval" in
    let pred_terms = 
         map list_mk_conj 
             (mult_map (map make_pred_def cons_names) cons_terms) in
    let pred_thm = 
        map2 (\x,y.new_recursive_definition false ty_axiom (`IS_`^x) y)
             (cons_names, pred_terms) in
   letrec mk_func_vars n = 
       (n = 0) => []
		| (`f` ^ (string_of_int n)) . (mk_func_vars (n-1)) in
   let mk_func_comb (str, tm) = 
       mk_comb(mk_var(str,mk_type(`fun`,[type_of tm;type_of tm])),
	       tm) in
   let mk_func_tms (str,tm) =
       mk_var(str,mk_type(`fun`,[type_of tm;type_of tm])) in
   let func_combs cons_term = 
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       map2 mk_func_comb 
		 (rev(mk_func_vars(length(cons_term_vars))),
		 cons_term_vars) in
   let func_tms cons_term = 
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       map2 mk_func_tms 
	    (rev(mk_func_vars(length(cons_term_vars))),
             cons_term_vars) in
   let new_cons_term cons_term = 
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       subst (combine (func_combs cons_term,cons_term_vars)) cons_term in
   letrec mk_func_comb_type lst end =
	 (null lst) => mk_type(`fun`,[type_of end; type_of end]) |
	 let head.rest = lst in
	 mk_type(`fun`,[mk_type (`fun`,[type_of head;type_of head]);
		       mk_func_comb_type rest end]) in
   let update_lhs (name, cons_term) = 
       let update_rec_name = `Update_`^name in
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       list_mk_comb(mk_var (update_rec_name,
			    mk_func_comb_type cons_term_vars cons_term),
		    ((func_tms cons_term) @ [cons_term])) in
   let update_tm (name, cons_term) = 
       let tm = mk_eq(update_lhs (name, cons_term),
                      new_cons_term cons_term) in
       (`Update_`^name,tm) in
   let update_tms = map2 update_tm (cons_names,cons_terms) in
   let update_rec_thms = 
       map (uncurry (new_recursive_definition false ty_axiom))
           update_tms in
   let update_rec_thm = 
       save_thm(`Update_`^name^`_thm`, LIST_CONJ update_rec_thms) in
   let one_one_thm = 
       % print_string `.`; %
       save_thm(name^`_one_one`,prove_constructors_one_one ty_axiom) in
   let cases_thm = 
       % print_string `.`; %
       save_thm(name^`_cases`,
                     prove_cases_thm(prove_induction_thm ty_axiom)) in
   let distinct_thm = 
       (length recs) > 1 => 
          let thl = CONJUNCTS (prove_constructors_distinct ty_axiom) in
          save_thm(name^`_distinct`, LIST_CONJ(thl @ (map GSYM thl))) |
          BOOL_CASES_AX in
   let rec_type = datatype_type_info ty_axiom in
   let var_name = "x:^rec_type" in
   let selector_terms = 
       map(map (fst o strip_comb o fst o 
            dest_eq o snd o strip_forall o concl)) rec_thml in
   let selector_apps = map(map (\tm . mk_comb(tm,var_name))) selector_terms in
   let mk_pred name cons_term =
        let pred_name = `IS_`^name in
        let ((cons_rator,_),_) = ((dest_const # I) o strip_comb) cons_term in
        (mk_const (pred_name,
                   mk_type(`fun`,[type_of cons_term;":bool"]))) in
   let selector_goal_arm (name,cons_term, selector_app) = 
       let (cons_term_rator,_) = strip_comb cons_term in
       let pred = mk_comb(mk_pred name cons_term,var_name) in
       let eq_tm = mk_eq(var_name, 
			 list_mk_comb(cons_term_rator,selector_app)) in
       (length recs > 1) => mk_imp(pred,eq_tm)
	                  | eq_tm in
   let selector_goals = 
       map3 selector_goal_arm (cons_names,cons_terms,selector_apps) in
   let goal = 
       mk_forall(var_name,
                 itlist (curry mk_disj) 
	                (butlast selector_goals) 
	                (last selector_goals)) in
   let selector_tactic = 
       GEN_TAC
       THEN STRUCT_CASES_TAC 
	       (SPEC var_name cases_thm)
       THEN REWRITE_TAC ([selectors] @ pred_thm) in
   let selectors_work_thm = 
       % print_string `.`; %
       prove_thm(name^`_selectors_work`,
                 goal,
                 selector_tactic) in
    let mk_update_commutes_tm (name,cons_term) (x, y, z) = 
        let update_rec_name = `Update_`^name in
        let (_,cons_term_vars) = strip_comb cons_term in
 	let selector_tm =  
            (mk_const (x,mk_type(`fun`,[type_of cons_term; y]))) in
	let update_x = 
	    list_mk_comb(mk_const (update_rec_name,
				 mk_func_comb_type cons_term_vars cons_term),
			    ((func_tms cons_term) @ ["x:^rec_type"])) in
        let pred = mk_comb(mk_pred name cons_term,"x:^rec_type") in
        let eq_tm = "(^selector_tm ^update_x = ^z (^selector_tm x))" in
	let commute_tm = (length recs > 1) => mk_imp(pred,eq_tm) 
	                                    | eq_tm in
	list_mk_forall(frees commute_tm,commute_tm) in
    let commute_goals = 
	let goal_list_list =
            map2 (uncurry map3)
	     ((map2 mk_update_commutes_tm (cons_names, cons_terms)),
	      (combine(nls,combine(tls, (map func_tms cons_terms))))) in
        itlist (curry $@) goal_list_list [] in
    let commute_TAC =
        REPEAT GEN_TAC
        THEN STRUCT_CASES_TAC (SPEC "x:^rec_type" cases_thm)
	THEN REWRITE_TAC ([update_rec_thm;selectors] @ pred_thm) in
    let commute_thms = 
        save_thm(name^`_Update_commute_thms`,
                 LIST_CONJ(map (\goal . PROVE(goal,commute_TAC)) 
                               commute_goals)) in
   (length recs) > 1 => 
      ([ty_axiom;selectors;updates;one_one_thm;cases_thm;
	selectors_work_thm; update_rec_thm; commute_thms] @ 
       pred_thm @ [distinct_thm]) |
      ([ty_axiom;selectors;updates;one_one_thm;cases_thm;
	selectors_work_thm; update_rec_thm; commute_thms] @ pred_thm);;


let create_record name lst = 
    create_datatype name [name,lst];;

let create_enum name recs =
    let ty_str = 
	name^` = `^recs in
    let ty_axiom = 
        define_type name ty_str in
    let induct_thm = 
        save_thm(name^`_induct`,
                 prove_induction_thm ty_axiom) in
   let cases_thm = 
       save_thm(name^`_cases`,
                prove_cases_thm induct_thm) in
   let thl = CONJUNCTS (prove_constructors_distinct ty_axiom) in
   let distinct_thm = 
       save_thm(name^`_distinct`,LIST_CONJ(thl @ (map GSYM thl))) in
   ([ty_axiom;induct_thm;cases_thm;distinct_thm]);;


%----------------------------------------------------------------
create_enum `error` `ALREADY_EXISTS | NOT_FOUND | SUCCESS`;;
----------------------------------------------------------------%

%----------------------------------------------------------------
 Bind exportable functions to it
----------------------------------------------------------------%
(create_datatype,create_record,create_enum);;

end_section datatypes;;

%----------------------------------------------------------------
 Recover exportable functions from it.
----------------------------------------------------------------%
let (create_datatype, create_record, create_enum) = it;;