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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1464 r1515  
    4747  lapply (refl ? (populate_env e u tl))
    4848  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
    49   >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E
    50   whd in E:(??%?)
    51   >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
     49  >E0 in E; whd in ⊢ (??%? → ?) #E
     50  destruct
    5251  #i #H @lookup_add_oblivious @(IH … E0) @H
    5352] qed.
     
    6968  lapply (refl ? (populate_label_env lbls u t))
    7069  cases (populate_label_env lbls u t) in ⊢ (???% → %)
    71   #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
    72   #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
     70  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?)
     71  #E destruct
    7372  #l *
    7473  [ #El <El whd >lookup_add_hit % #Er destruct
     
    8685  lapply (refl ? (populate_label_env lbls u t))
    8786  cases (populate_label_env lbls u t) in ⊢ (???% → %)
    88   #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
    89   #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
     87  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?)
     88  #E destruct
    9089  #l #H cases (identifier_eq ? l h)
    9190  [ #El %1 %1 @El
    9291  | #NE cases (IH … E1 l ?)
    93     [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/ ]
     92    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H // ]
    9493  ]
    9594] qed.
     
    154153| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
    155154  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    156   | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
     155  | >lookup_add_miss in H /2/
    157156  ]
    158157] qed.
     
    210209| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
    211210  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    212   | >lookup_add_miss in H // @eq_identifier_elim // #E cases NE /2/
     211  | >lookup_add_miss in H /2/
    213212  ]
    214213] qed.
     
    680679    l in
    681680do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
    682 do u1 ← check_universe_ok ? (pf_labgen ? f);
    683 do u2 ← check_universe_ok ? (pf_reggen ? f);
    684681OK ? (mk_internal_function
    685682    (pf_labgen ? f)
Note: See TracChangeset for help on using the changeset viewer.