Changeset 1607 for src/ASM/Assembly.ma

Timestamp:

Dec 14, 2011, 1:50:23 PM (8 years ago)

Author:

sacerdot

Message:

Porting to new library.

File:

• src/ASM/Assembly.ma (modified) (10 diffs)

src/ASM/Assembly.ma

@@ -1135 +1135 @@
           ]
         ]
-      | >(proj1 ?? (jump_not_in_policy (eject … program) old_policy (|prefix|) ?))
+      | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
         [ //
         | >prf >p1 >nth_append_second [ <minus_n_n
@@ -1248 +1248 @@
    [ >lookup_opt_lookup_miss
      [ @refl
-     | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn))
+     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p2)) n Hn))
        [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))
        | @Hnotjmp
        ]
      ]
-   | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn))
+   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p1)) n Hn))
      [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))
      | @Hnotjmp
@@ -1312 +1312 @@
 lemma stupid:
   ∀program,n.
-  eject … (jump_expansion_step program (jump_expansion_internal program n)) =
-  eject … (jump_expansion_internal program (S n)).
+  pi1 … (jump_expansion_step program (jump_expansion_internal program n)) =
+  pi1 … (jump_expansion_internal program (S n)).
  //
 qed.
@@ -1445 +1445 @@
   policy_equal program policy (jump_expansion_step program policy).
 #program #policy lapply (le_n (|program|)) @(list_ind ?
-  (λx.|x| ≤ |program| → measure_int x (eject … policy) 0 = measure_int x (eject … (jump_expansion_step program policy)) 0 →
-      policy_equal x (eject … policy) (eject … (jump_expansion_step program policy)))
+  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program policy)) 0 →
+      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program policy)))
    ?? program)
  [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
@@ -1513 +1513 @@
 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
   Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
- #program @(dp … (jump_expansion_internal program (2*|program|)))
+ #program @(mk_Sig …(jump_expansion_internal program (2*|program|)))
  @(ex_intro … (2*|program|)) #k #Hk
  cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
@@ -1584 +1584 @@
  λprogram.λpc.
   let policy ≝
-    transform_policy (|\snd program|) (eject … (je_fixpoint (\snd program))) (Stub ??) in
+    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
   lookup ? ? pc policy long_jump.
-/2 by Stub, dp/
+/2 by Stub, mk_Sig/
 qed.
 
@@ -1691 +1691 @@
 
 lemma eject_policy: ∀p. policy p → policy_type.
- #p #pol @(eject … pol)
+ #p #pol @(pi1 … pol)
 qed.
 
@@ -1698 +1698 @@
 definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
  λp,policy.
-  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
+  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    [ None ⇒ λabs. ⊥
    | Some r ⇒ λ_.r] (pi2 … policy).
@@ -1866 +1866 @@
 
 definition construct_costs ≝
- λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
+ λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i).
 
 (*
@@ -1980 +1980 @@
               And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
                 (ppc' = length … pre)) (*∧ *)
-                (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
+                (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
                 (∀id. occurs_exactly_once id pre →
                   lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))