Merge pull request #25 from kth-step/dev_select

Set types and select statement

.github/workflows/build.yaml

@@ -32,7 +32,7 @@ jobs:
         uses: actions/cache@v4
         with:
           path: |
-            /home/runner/work/HOL4P4/HOL4P4/scripts
+            /home/runner/work/HOL4P4/HOL4P4/scripts/HOL
           key: os-${{ runner.os }}_polyml-${{ matrix.polyml }}_hol4-${{ matrix.hol4 }}
 
       - name: Prepare cached dependencies

Dockerfile

@@ -17,7 +17,6 @@ RUN apt update && apt-get install -y -q sudo
 # Then, just run the regular install script
 RUN ./HOL4P4/scripts/install.sh
 WORKDIR /HOL4P4/
-RUN ./scripts/install2.sh
 
 # Test compilation
 #RUN export PATH=$PATH:/HOL4P4/HOL/bin && opam exec -- make hol

INSTALL.md

@@ -45,7 +45,7 @@ First, navigate to the directory where you want to put the source code of Poly/M
 		cd ..
 
 3. Install HOL4 Trindemossen-1
-	
+
 		git clone https://github.com/HOL-Theorem-Prover/HOL.git
 		cd HOL
 		git checkout trindemossen-1
@@ -124,4 +124,4 @@ The same tools used to edit HOL4 theories and run the HOL4 REPL can also be used
 
 The `scripts` directory contains installation scripts. These may be run when installing HOL4P4 e.g. on a fresh virtual machine by
 
-	scripts/install.sh && scripts/install2.sh
+	scripts/install.sh

hol/p4Syntax.sig

@@ -15,6 +15,8 @@ val varn_name_tm : term
 val varn_star_tm : term
 val is_varn_star : term -> bool
 
+val v_ty : hol_type
+
 val dest_e_v : term -> term
 val e_v_tm : term
 val is_e_v : term -> bool
@@ -33,6 +35,11 @@ val is_v_bool : term -> bool
 val mk_v_bool : term -> term
 val v_bool_tm : term
 
+val dest_v_ext_ref : term -> term
+val ext_ref_tm : term
+val is_v_ext_ref : term -> bool
+val mk_v_ext_ref : term -> term
+
 val dest_v_str : term -> term
 val is_v_str : term -> bool
 val v_str_tm : term
@@ -45,6 +52,8 @@ val v_struct_tm : term
 
 val mk_v_struct_list : (term * term) list -> term
 
+val dest_v_struct_fields : term -> term list
+
 val dest_v_header : term -> term * term
 val is_v_header : term -> bool
 val mk_v_header : term * term -> term
@@ -183,6 +192,21 @@ val e_header_tm : term
 val is_e_header : term -> bool
 val mk_e_header : term * term -> term
 
+val dest_s_sing : term -> term
+val is_s_sing : term -> bool
+val mk_s_sing : term -> term
+val s_sing_tm : term
+val dest_s_range : term -> term * term
+val is_s_range : term -> bool
+val mk_s_range : term * term -> term
+val s_range_tm : term
+val dest_s_mask : term -> term * term
+val is_s_mask : term -> bool
+val mk_s_mask : term * term -> term
+val s_mask_tm : term
+val s_univ_tm : term
+val is_s_univ : term -> bool
+
 val d_in_tm : term
 val is_d_in : term -> bool
 val d_out_tm : term
@@ -242,8 +266,22 @@ val d_ty : hol_type
 val scope_ty : hol_type
 
 val status_running_tm : term
+val is_status_running : term -> bool
+
+val dest_status_trans : term -> term
+val is_status_trans : term -> bool
+val mk_status_trans : term -> term
+val status_trans_tm : term
+
+val dest_status_returnv : term -> term
+val is_status_returnv : term -> bool
+val mk_status_returnv : term -> term
+val status_returnv_tm : term
+
+val frame_ty : hol_type
 
 val dest_frame : term -> term * term * term
+val mk_frame : term * term * term -> term
 
 val arch_block_pbl_tm : term
 val dest_arch_block_pbl : term -> term * term
@@ -262,19 +300,30 @@ val dest_actx :
    term ->
      term * term * term * term * term * term * term * term * term * term
 val dest_astate : term -> term * term * term * term
+val mk_astate : term * term * term * term -> term
 val dest_aenv : term -> term * term * term * term
-val dest_pblock : term -> term * term * term * term * term
+val mk_aenv : term * term * term * term -> term
+val dest_pblock : term -> term * term * term * term * term * term
 
 val dest_e_red : term -> term * term * term * term * term * term
 val e_red_tm : term
 val is_e_red : term -> bool
 val mk_e_red : term * term * term * term * term * term -> term
 
 val struct_ty_struct_tm : term
+val is_struct_ty_struct : term -> bool
 val struct_ty_header_tm : term
+val is_struct_ty_header : term  -> bool
+
 val tau_ty : hol_type
 
-val dest_tau_bit : term -> term
+val is_tau_bool : term -> bool
+val tau_bool_tm : term
+
+val is_tau_ext : term -> bool
+val tau_ext_tm : term
+
+val dest_tau_bit : term -> int
 val is_tau_bit : term -> bool
 val mk_tau_bit : int -> term
 val tau_bit_tm : term
@@ -296,6 +345,11 @@ val is_e_lval_tm : term
 val is_is_e_lval : term -> bool
 val mk_is_e_lval : term -> term
 
+val dest_lookup_lval : term -> term * term
+val is_lookup_lval : term -> bool
+val lookup_lval_tm : term
+val mk_lookup_lval : term * term -> term
+
 val dest_lookup_funn_sig : term -> term * term * term * term
 val is_lookup_funn_sig : term -> bool
 val lookup_funn_sig_tm : term
@@ -321,4 +375,9 @@ val is_unred_arg_index : term -> bool
 val mk_unred_arg_index : term * term -> term
 val unred_arg_index_tm : term
 
+val dest_match_all : term -> term
+val is_match_all : term -> bool
+val match_all_tm : term
+val mk_match_all : term -> term
+
 end

hol/p4Syntax.sml

@@ -100,6 +100,9 @@ fun mk_v_biti_arb width =
 val (v_bool_tm, mk_v_bool, dest_v_bool, is_v_bool) =
   syntax_fns1 "p4" "v_bool";
 
+val (ext_ref_tm, mk_v_ext_ref, dest_v_ext_ref, is_v_ext_ref) =
+  syntax_fns1 "p4" "v_ext_ref";
+
 val (v_str_tm, _, dest_v_str, is_v_str) =
   syntax_fns1 "p4" "v_str";
 val mk_v_str = (#2 (syntax_fns1 "p4" "v_str")) o fromMLstring;
@@ -108,6 +111,9 @@ val (v_struct_tm, mk_v_struct, dest_v_struct, is_v_struct) =
   syntax_fns1 "p4" "v_struct";
 fun mk_v_struct_list x_v_l =
   mk_v_struct (listSyntax.mk_list ((map (fn (a, b) => mk_pair (a, b)) x_v_l), ``:(string # v)``));
+fun dest_v_struct_fields strct =
+ (map (snd o dest_pair)) $ fst $ dest_list $ dest_v_struct strct
+;
 
 val (v_header_tm, mk_v_header, dest_v_header, is_v_header) =
   syntax_fns2 "p4" "v_header";
@@ -152,6 +158,8 @@ val (funn_ext_tm, _, dest_funn_ext, is_funn_ext) =
 val mk_funn_ext =
 (#2 (syntax_fns2 "p4" "funn_ext")) o (fn (objname, metname) => (fromMLstring objname, fromMLstring metname));
 
+val funn_ty = mk_type ("funn", []);
+
 (*****)
 (* e *)
 (*****)
@@ -228,6 +236,18 @@ val (e_struct_tm,  mk_e_struct, dest_e_struct, is_e_struct) =
 val (e_header_tm,  mk_e_header, dest_e_header, is_e_header) =
   syntax_fns2 "p4" "e_header";
 
+val (s_sing_tm,  mk_s_sing, dest_s_sing, is_s_sing) =
+  syntax_fns1 "p4" "s_sing";
+
+val (s_range_tm,  mk_s_range, dest_s_range, is_s_range) =
+  syntax_fns2 "p4" "s_range";
+
+val (s_mask_tm,  mk_s_mask, dest_s_mask, is_s_mask) =
+  syntax_fns2 "p4" "s_mask";
+
+val s_univ_tm = prim_mk_const {Name="s_univ", Thy="p4"};
+fun is_s_univ tm = term_eq tm s_univ_tm;
+
 (*****)
 (* d *)
 (*****)
@@ -250,14 +270,24 @@ fun is_d_none tm = term_eq tm d_none_tm;
 (*******)
 
 val struct_ty_struct_tm = prim_mk_const {Name="struct_ty_struct", Thy="p4"};
+fun is_struct_ty_struct tm = term_eq tm struct_ty_struct_tm;
 val struct_ty_header_tm = prim_mk_const {Name="struct_ty_header", Thy="p4"};
+fun is_struct_ty_header tm = term_eq tm struct_ty_header_tm;
 
 val tau_ty = mk_type ("tau", []);
 
-val (tau_bit_tm, mk_tau_bit_tmp, dest_tau_bit, is_tau_bit) =
+val tau_bool_tm = prim_mk_const {Name="tau_bool", Thy="p4"};
+fun is_tau_bool tm = term_eq tm tau_bool_tm;
+
+val tau_ext_tm = prim_mk_const {Name="tau_ext", Thy="p4"};
+fun is_tau_ext tm = term_eq tm tau_ext_tm;
+
+val (tau_bit_tm, mk_tau_bit_tmp, dest_tau_bit_tmp, is_tau_bit) =
   syntax_fns1 "p4" "tau_bit";
 val mk_tau_bit =
   mk_tau_bit_tmp o (fn n => term_of_int n);
+val dest_tau_bit =
+  int_of_term o dest_tau_bit_tmp;
 
 val (tau_xtl_tm, mk_tau_xtl_tmp, dest_tau_xtl, is_tau_xtl) =
   syntax_fns2 "p4" "tau_xtl";
@@ -301,19 +331,34 @@ fun mk_stmt_seq_list [] = stmt_empty_tm
 
 val d_ty = mk_type ("d", []);
 
+val stmt_stack_ty = mk_list_type $ mk_type ("stmt", []);
+
 (*********)
 (* State *)
 (*********)
 
 val scope_ty = mk_list_type $ mk_prod (varn_ty, mk_prod (v_ty, mk_option lval_ty));
+val scope_stack_ty = mk_list_type $ scope_ty;
 
 val status_running_tm = prim_mk_const {Name="status_running", Thy="p4"};
+fun is_status_running tm = term_eq tm status_running_tm;
+
+val (status_trans_tm,  mk_status_trans, dest_status_trans, is_status_trans) =
+  syntax_fns1 "p4" "status_trans";
+
+val (status_returnv_tm,  mk_status_returnv, dest_status_returnv, is_status_returnv) =
+  syntax_fns1 "p4" "status_returnv";
+
+val frame_ty = list_mk_prod [funn_ty, stmt_stack_ty, scope_stack_ty];
 
 fun dest_frame frame =
  case spine_pair frame of
     [funn, stmt_stack, scope_list] => (funn, stmt_stack, scope_list)
   | _ => raise (ERR "dest_frame" ("Unsupported frame shape: "^(term_to_string frame)))
 ;
+fun mk_frame (funn, stmt_stack, scope_stack) =
+ list_mk_pair [funn, stmt_stack, scope_stack]
+;
 
 (********)
 (* Arch *)
@@ -340,6 +385,9 @@ fun dest_astate astate =
     [aenv, g_scope_list, arch_frame_list, status] => (aenv, g_scope_list, arch_frame_list, status)
   | _ => raise (ERR "dest_astate" ("Unsupported astate shape: "^(term_to_string astate)))
 ;
+fun mk_astate (aenv, g_scope_list, arch_frame_list, status) =
+ list_mk_pair [aenv, g_scope_list, arch_frame_list, status]
+;
 (* TODO: Is this a hack? *)
 fun dest_aenv aenv =
  let
@@ -350,15 +398,19 @@ fun dest_aenv aenv =
   (i, io_list, io_list', ascope)
  end
 ;
+fun mk_aenv (i, io_list, io_list', ascope) =
+ list_mk_pair [i, io_list, io_list', ascope]
+;
 
 fun dest_pblock pblock =
  let
   val (pbl_type, pblock') = dest_pair pblock
-  val (b_func_map, pblock'') = dest_pair pblock'
-  val (decl_list, pblock''') = dest_pair pblock''
-  val (pars_map, tbl_map) = dest_pair pblock'''
+  val (params, pblock'') = dest_pair pblock'
+  val (b_func_map, pblock''') = dest_pair pblock''
+  val (decl_list, pblock'''') = dest_pair pblock'''
+  val (pars_map, tbl_map) = dest_pair pblock''''
  in
-  (pbl_type, b_func_map, decl_list, pars_map, tbl_map)
+  (pbl_type, params, b_func_map, decl_list, pars_map, tbl_map)
  end
 ;
 
@@ -384,6 +436,9 @@ val (is_e_lval_tm, mk_is_e_lval, dest_is_e_lval, is_is_e_lval) =
 val (lookup_vexp_tm, mk_lookup_vexp, dest_lookup_vexp, is_lookup_vexp) =
   syntax_fns2 "p4" "lookup_v";
 
+val (lookup_lval_tm, mk_lookup_lval, dest_lookup_lval, is_lookup_lval) =
+  syntax_fns2 "p4" "lookup_lval";
+
 val (lookup_funn_sig_tm, mk_lookup_funn_sig, dest_lookup_funn_sig, is_lookup_funn_sig) =
   syntax_fns4 "p4" "lookup_funn_sig";
 
@@ -399,4 +454,7 @@ val (all_arg_update_for_newscope_tm, mk_all_arg_update_for_newscope, dest_all_ar
 val (unred_arg_index_tm, mk_unred_arg_index, dest_unred_arg_index, is_unred_arg_index) =
   syntax_fns2 "p4" "unred_arg_index";
 
+val (match_all_tm,  mk_match_all, dest_match_all, is_match_all) =
+  syntax_fns1 "p4" "match_all";
+
 end