Changeset 1640 for src/RTL

Timestamp:

Jan 11, 2012, 5:41:45 PM (8 years ago)

Author:

tranquil

Message:

• finished fork of semantics.ma
• unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material

File:

• src/RTL/RTL_paolo.ma (modified) (7 diffs)

src/RTL/RTL_paolo.ma

@@ -25 +25 @@
   | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
 
-  
-inductive rtl_move : Type[0] ≝
-  | CARRY : bool → rtl_move
-  | REG : register → rtl_argument → rtl_move.
-  
-(* avoid expansion *)
-definition rtl_params : graph_params ≝ mk_graph_params
+definition rtl_params ≝ mk_graph_params (mk_unserialized_params
   (mk_inst_params
     (* acc_a_reg ≝ *) register
@@ -42 +36 @@
     (* dph_arg   ≝ *) rtl_argument
     (* snd_arg   ≝ *) rtl_argument
-    (* operator1 ≝ *) Op1
-    (* operator2 ≝ *) Op2
-    (* pair_move ≝ *) rtl_move
+    (* pair_move ≝ *) (register × rtl_argument)
     (* call_args ≝ *) (list rtl_argument)
     (* call_dest ≝ *) (list register)
@@ -53 +45 @@
       (* resultT ≝ *) (list register)
       (* paramsT ≝ *) (list register))
-      (* localsT ≝ *) (list register)).
+      (* localsT ≝ *) (list register))).
+
+interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
 
 (* aid unification *)
@@ -59 +53 @@
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_reg (g_inst_pars rtl_params) ≡ register.
+acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_reg (g_inst_pars rtl_params) ≡ register.
+acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg (g_inst_pars rtl_params) ≡ rtl_argument.
+acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_arg (g_inst_pars rtl_params) ≡ rtl_argument.
+acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_reg (g_inst_pars rtl_params) ≡ register.
+dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_reg (g_inst_pars rtl_params) ≡ register.
+dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_arg (g_inst_pars rtl_params) ≡ rtl_argument.
+dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_arg (g_inst_pars rtl_params) ≡ rtl_argument.
+dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-snd_arg (g_inst_pars rtl_params) ≡ rtl_argument.
+snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-operator1 (g_inst_pars rtl_params) ≡ Op1.
+pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-operator2 (g_inst_pars rtl_params) ≡ Op2.
+call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-pair_move (g_inst_pars rtl_params) ≡ rtl_move.
-unification hint 0 ≔
-(*---------------*) ⊢
-call_args (g_inst_pars rtl_params) ≡ list rtl_argument.
-unification hint 0 ≔
-(*---------------*) ⊢
-call_dest (g_inst_pars rtl_params) ≡ list register.
+call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
 
-check (λglobals,r.OP2 rtl_params globals Or r r r)
 
 definition rtl_instruction ≝ joint_instruction rtl_params.
-definition rtl_statement ≝ joint_statement rtl_params.
-
-
-definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝
-  λglobals,r,k.
-  MOVE rtl_params globals (REG r (imm_nat k)).
-
-definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝
-  λglobals,r,k.
-  MOVE rtl_params globals (REG r (Imm k)).
-
-definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝
-  λglobals,r,k.
-  MOVE … (REG r (Reg k)).
-
-definition set_carry : ∀globals.rtl_instruction globals ≝
-  λglobals.MOVE … (CARRY true).
-
-definition clear_carry : ∀globals.rtl_instruction globals ≝
-  λglobals.MOVE … (CARRY false).
-  
+(* Paolo: can't understand why coercions do not compose implicitly here *)
+definition rtl_statement ≝ joint_statement (rtl_params : params).
 
 definition rtl_internal_function ≝
@@ -136 +104 @@
   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
 
-definition rtlntc_params : graph_params ≝ mk_graph_params
+definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
   (mk_inst_params
     (* acc_a_reg ≝ *) register
@@ -147 +115 @@
     (* dph_arg   ≝ *) rtl_argument
     (* snd_arg   ≝ *) rtl_argument
-    (* operator1 ≝ *) Op1
-    (* operator2 ≝ *) Op2
-    (* pair_move ≝ *) rtl_move
+    (* pair_move ≝ *) (register × rtl_argument)
     (* call_args ≝ *) (list rtl_argument)
     (* call_dest ≝ *) (list register)
@@ -158 +124 @@
       (* resultT ≝ *) (list register)
       (* paramsT ≝ *) (list register))
-      (* localsT ≝ *) (list register)).
+      (* localsT ≝ *) (list register))).
 
-definition rtlntc_statement ≝ joint_statement rtlntc_params.
+definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
 
 definition rtlntc_internal_function ≝