Changeset 2645 for src/LIN

Timestamp:

Feb 7, 2013, 9:22:22 PM (7 years ago)

Author:

sacerdot

Message:

1. some broken back-end files repaires, several still to go
2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files

Location:

src/LIN

Files:

• joint_LTL_LIN.ma (modified) (1 diff)
• joint_LTL_LIN_semantics.ma (modified) (5 diffs)

src/LIN/joint_LTL_LIN.ma

@@ -36 +36 @@
     (* ext_seq_labels ≝ *) ltl_lin_seq_labels
     (* has_tailcalls ≝ *) false
-    (* paramsT ≝ *) unit
-    (* localsT ≝ *) void.
+    (* paramsT ≝ *) unit.
 
 interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).

src/LIN/joint_LTL_LIN_semantics.ma

@@ -1 +1 @@
 include "LIN/joint_LTL_LIN.ma".
-include "joint/SemanticUtils.ma".
+include "joint/semanticsUtils.ma".
 
 definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
@@ -7 +7 @@
   λl,a.match a with
   [ Reg r ⇒ hw_reg_retrieve l r
-  | Imm b ⇒ OK … b
+  | Imm b ⇒ OK … (BVByte b)
   ].
 
@@ -17 +17 @@
   hw_reg_store RegisterA (hwreg_retrieve e r) e
 | int_to_reg r v ⇒
-  hw_reg_store r v e
+  hw_reg_store r (BVByte v) e
 | int_to_acc _ v ⇒
-  hw_reg_store RegisterA v e
+  hw_reg_store RegisterA (BVByte v) e
 ].
 
@@ -55 +55 @@
   (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
   (* pair_reg_move_     ≝ *) eval_registers_move
-  (* fetch_ra           ≝ *) (load_ra …)
+(*  (* fetch_ra           ≝ *) (load_ra …)
   (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
-  (* save_frame         ≝ *) (λp.λ_.λst.save_ra … st p)
+*)  (* save_frame         ≝ *) ?(*(λp.λ_.λst.save_ra … st p)*)
   (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
-  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
+  (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*)
   (* set_result         ≝ *) ltl_lin_set_result
   (* call_args_for_main ≝ *) 0
@@ -65 +65 @@
   (* read_result        ≝ *) (λ_.λ_.λ_.
   λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
-  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
-  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
+  (* eval_ext_seq       ≝ *) ?(*(λ_.λ_.λs.λ_.eval_ltl_lin_seq s)*)
+(*  (* eval_ext_tailcall  ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*)
   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
-  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
-  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
+*)  (* pop_frame          ≝ *) ?(*(λ_.λ_.λ_.λst.return st)*)
+(*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).