Changeset 1515 for src/Clight


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
Location:
src/Clight
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r1401 r1515  
    11
    22include "Clight/Csyntax.ma".
     3include "utilities/extranat.ma".
    34
    45axiom TypeMismatch : String.
     
    1011definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    1112#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    12 
    13 definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
    14 #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
    15 [ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed.
    1613
    1714let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
  • src/Clight/fresh.ma

    r1207 r1515  
    1111λa,b. match a with [ an_identifier a ⇒
    1212      match b with [ an_identifier b ⇒
    13         an_identifier ? (max_u ? a b)
     13        an_identifier ? (max a b)
    1414      ]].
    1515
    1616definition max_id_of_env : list (ident × type) → ident ≝
    17 foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? (zero ?)).
     17foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one).
    1818
    1919definition max_id_of_fn : function → ident ≝
     
    2727
    2828definition max_id_of_functs : list (ident × clight_fundef) → ident ≝
    29 foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? (zero ?)).
     29foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one).
    3030
    3131definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝
    32 foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? (zero ?)).
     32foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one).
    3333
    3434definition max_id_of_program : clight_program → ident ≝
     
    3939definition universe_for_program : clight_program → universe SymbolTag ≝
    4040λp. match max_id_of_program p with [ an_identifier i ⇒
    41       let next ≝ increment ? i in
    42       mk_universe SymbolTag next (eq_bv ? next (zero ?))
     41      let next ≝ succ i in
     42      mk_universe SymbolTag next
    4343    ].
  • src/Clight/label.ma

    r1224 r1515  
    172172].
    173173
    174 definition label_function : function → res function ≝
     174definition label_function : function → function ≝
    175175λf.
    176176  let costgen ≝ new_universe CostTag in
    177177  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
    178178  let 〈body,costgen〉 ≝ add_cost_before body costgen in
    179   do u ← check_universe_ok ? costgen;
    180   OK ? (mk_function (fn_return f) (fn_params f) (fn_vars f) body).
     179    mk_function (fn_return f) (fn_params f) (fn_vars f) body.
    181180
    182 definition label_fundef : clight_fundef → res clight_fundef ≝
     181definition label_fundef : clight_fundef → clight_fundef ≝
    183182λf. match f with
    184 [ CL_Internal f ⇒ do f ← label_function f; OK ? (CL_Internal f)
    185 | CL_External id args ty ⇒ OK ? (CL_External id args ty)
     183[ CL_Internal f ⇒ CL_Internal (label_function f)
     184| CL_External id args ty ⇒ CL_External id args ty
    186185].
    187186
    188 definition clight_label : clight_program → res clight_program ≝
    189  λp. transform_partial_program … p label_fundef.
     187definition clight_label : clight_program → clight_program ≝
     188 λp. transform_program … p label_fundef.
  • src/Clight/test/insertsort.test.ma

    r1513 r1515  
    2626
    2727example labelled_exec:
    28   (do p ← clight_label myprog;
     28  (let p ≝ clight_label myprog in
    2929   do s ← exec_up_to clight_fullexec p 1000
    3030     [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];
  • src/Clight/toCminor.ma

    r1369 r1515  
    125125cases (identifier_eq ? id id')
    126126[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
    127 | #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
     127| #NE >lookup_add_miss /2/
    128128] qed.
    129129
     
    134134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
    135135>lookup_add_miss
    136 [ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
     136[ #H @H | /2/ ]
    137137qed.
    138138
     
    737737  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
    738738#tmp #g #g' #vars #q
    739 whd in ⊢ (???% → ?)
    740 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
    741 * #tmp' #u whd in ⊢ (???% → ?) #E
    742 destruct
     739whd in ⊢ (???% → ?) #E
    743740#id #H
     741cases (identifier_eq ? id tmp)
     742destruct #E
    744743whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
    745 cases (identifier_eq ? id tmp')
    746 [ #E1 >E1 >lookup_add_hit @I
    747 | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1)
     744[ >E >lookup_add_hit @I
     745| cases E #NE >lookup_add_miss [ @H | /2/
    748746] qed.
    749747
     
    770768cases (identifier_eq ? id id')
    771769[ #E >E >lookup_add_hit @I
    772 | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)
     770| #NE >lookup_add_miss [ @H | /2/
    773771] qed.
    774772
     
    793791  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    794792#tmp #u #q #u0 #vars
    795 whd in ⊢ (???% → ?)
    796 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
    797 * #tmp' #u' whd in ⊢ (???% → ?) #E
     793whd in ⊢ (???% → ?) #E
    798794destruct
    799795whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     
    997993  l0 ≠ l →
    998994  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
    999 #lbls #l #l' #l0 * #NE
     995#lbls #l #l' #l0 #NE
    1000996whd in ⊢ (??%%)
    1001997>lookup_add_miss
    1002 [ @refl | @(eq_identifier_elim ?? l0 l)
    1003   [ #E cases (NE E)
    1004   | #_ @I
    1005   ]
    1006 ]
     998[ @refl | @NE ]
    1007999qed. 
    10081000
     
    10481040  cases (identifier_eq ? i id)
    10491041  [ #E >E #H %2 whd %1 @refl
    1050   | * #NE #H cases (IH ?)
     1042  | #NE #H cases (IH ?)
    10511043    [ #H' %1 @H'
    10521044    | #H' %2 %2 @H'
    10531045    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
    1054       >lookup_add_miss in H; [ #H @H | @eq_identifier_elim // #E cases (NE E) ]
     1046      >lookup_add_miss in H; [ #H @H | @NE ]
    10551047    ]
    10561048  ]
Note: See TracChangeset for help on using the changeset viewer.