Ignore:
Timestamp:
Dec 19, 2011, 2:48:37 PM (9 years ago)
Author:
campbell
Message:

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1630 r1631  
    11701170  let tmp ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
    11711171  do s ← translate_statement vartypes lbls tmp (fn_body f);
    1172    do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
     1172  do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
     1173  let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
     1174  let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f) in
     1175  do D ← check_distinct_env ?? (params @ vars);
    11731176  OK ? (mk_internal_function
    11741177    (opttyp_of_type (fn_return f))
    1175     (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    1176     ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f)))
     1178    params
     1179    vars
     1180    D
    11771181    stacksize
    11781182    s ?).
     
    11901194                  | * #id #ty * #E1 #E2 <E1 <E2 @refl
    11911195                  ]
    1192     | #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
     1196    | #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
    11931197    ]
    11941198  | @(stmt_labels_mp … H2)
Note: See TracChangeset for help on using the changeset viewer.