Changeset 1884


Ignore:
Timestamp:
Apr 9, 2012, 3:07:06 PM (8 years ago)
Author:
campbell
Message:

Syntax changes to fit Paolo's commit.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1878 r1884  
    122122    let 〈c,stack_high〉 ≝
    123123      (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *)
    124       if always_alloc ty ∨ mem_set ? mem_vars id then
     124      if always_alloc ty ∨ id ∈ mem_vars then
    125125        〈Stack stack_high,stack_high + sizeof ty〉
    126126      else
     
    177177  #H >(contract_pair var_types nat ?) in E;
    178178  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    179   cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     179  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    180180  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    181181  cases (identifier_eq ? i id)
     
    212212  #H >(contract_pair var_types nat ?) in E;
    213213  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    214   cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     214  cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    215215  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    216216
  • src/Cminor/toRTLabs.ma

    r1878 r1884  
    431431
    432432lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
    433   choose_regs le env es f p = ❬f',rs❭ → |es| = |rs|.
     433  choose_regs le env es f p = ❬f',rs❭ → |es| = length … rs.
    434434#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
    435435qed.
     
    571571
    572572let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    573                   (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le env)
     573                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
    574574                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
    575575match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
Note: See TracChangeset for help on using the changeset viewer.