Changeset 1515


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 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
Files:
1 added
26 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1493 r1515  
    11include "ASM/BitVector.ma".
    2 
    3 definition Identifier ≝ Word.
     2include "common/Identifiers.ma".
     3include "common/CostLabel.ma".
     4
     5axiom ASMTag : String.
     6definition Identifier ≝ identifier ASMTag.
     7definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
    48
    59inductive addressing_mode: Type[0] ≝
     
    194198  | Instruction: preinstruction Identifier → pseudo_instruction
    195199  | Comment: String → pseudo_instruction
    196   | Cost: Identifier → pseudo_instruction
     200  | Cost: costlabel → pseudo_instruction
    197201  | Jmp: Identifier → pseudo_instruction
    198202  | Call: Identifier → pseudo_instruction
  • src/ASM/Erase.ma

    r1463 r1515  
    11include "ASM/ASM.ma".
    2 include "ASM/BitVectorTrie.ma".
    3      
     2
    43let rec pre_erase
    54  (the_program: list labelled_instruction) (labels: list Identifier)
    6     on the_program: ((BitVectorTrie Identifier 16) × (list labelled_instruction)) ≝
     5    on the_program: ((identifier_map ASMTag Identifier) × (list labelled_instruction)) ≝
    76  match the_program with
    87  [ nil        ⇒
    98    match labels with
    10     [ nil ⇒ 〈Stub Identifier 16, [ ]〉 (* XXX: labels should be empty *)
     9    [ nil ⇒ 〈empty_map ??, [ ]〉 (* XXX: labels should be empty *)
    1110    | _   ⇒ ⊥
    1211    ]
     
    2524        | _ ⇒
    2625          let 〈maps, the_program〉 ≝ pre_erase tl [ ] in
    27           let maps ≝ foldr … (λl. λmap. insert … l label map) maps (label::labels) in
     26          let maps ≝ foldr ?? (λl. λmap. add … map l label) maps (label::labels) in
    2827            〈maps, the_program〉
    2928        ]
     
    3332qed.
    3433
    35 definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16 → preinstruction Identifier ≝
     34definition relabel_instruction: preinstruction Identifier → identifier_map ASMTag Identifier → preinstruction Identifier ≝
    3635  λpre.
    3736  λmap.
    3837  match pre with
    3938  [ JC ident ⇒
    40     let located ≝ lookup … ident map ident in
     39    let located ≝ lookup_def … map ident ident in
    4140      JC … located
    4241  | JNC ident ⇒
    43     let located ≝ lookup … ident map ident in
     42    let located ≝ lookup_def … map ident ident in
    4443      JNC … located
    4544  | JB bit ident ⇒
    46     let located ≝ lookup … ident map ident in
     45    let located ≝ lookup_def … map ident ident in
    4746      JB … bit located
    4847  | JNB bit ident ⇒
    49     let located ≝ lookup … ident map ident in
     48    let located ≝ lookup_def … map ident ident in
    5049      JNB … bit located
    5150  | JBC bit ident ⇒
    52     let located ≝ lookup … ident map ident in
     51    let located ≝ lookup_def … map ident ident in
    5352      JBC … bit located
    5453  | JZ ident ⇒
    55     let located ≝ lookup … ident map ident in
     54    let located ≝ lookup_def … map ident ident in
    5655      JZ … located
    5756  | JNZ ident ⇒
    58     let located ≝ lookup … ident map ident in
     57    let located ≝ lookup_def … map ident ident in
    5958      JNZ … located
    6059  | CJNE src ident ⇒
    61     let located ≝ lookup … ident map ident in
     60    let located ≝ lookup_def … map ident ident in
    6261      CJNE … src located
    6362  | DJNZ src ident ⇒
    64     let located ≝ lookup … ident map ident in
     63    let located ≝ lookup_def … map ident ident in
    6564      DJNZ … src located
    6665  (* XXX: no identifiers in rest of instructions *)
     
    6867  ].
    6968
    70 definition relabel_pseudo_instruction: pseudo_instruction → BitVectorTrie Identifier 16 → pseudo_instruction ≝
     69definition relabel_pseudo_instruction: pseudo_instruction → identifier_map ASMTag Identifier → pseudo_instruction ≝
    7170  λpseudo.
    7271  λmap.
     
    7675  | Comment comment ⇒ Comment comment
    7776  | Jmp ident ⇒
    78     let located ≝ lookup … ident map ident in
     77    let located ≝ lookup_def … map ident ident in
    7978      Jmp located
    8079  | Call ident ⇒
    81     let located ≝ lookup … ident map ident in
     80    let located ≝ lookup_def … map ident ident in
    8281      Call located
    8382  | Mov dptr ident ⇒
    84     let located ≝ lookup … ident map ident in
     83    let located ≝ lookup_def … map ident ident in
    8584      Mov dptr located
    8685  ].
    8786     
    8887let rec relabel
    89   (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16)
     88  (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier)
    9089    on the_program: list labelled_instruction ≝
    9190  match the_program with
     
    9796      match label with
    9897      [ None ⇒ None …
    99       | Some label ⇒ Some … (lookup … ident map ident)
     98      | Some label ⇒ Some … (lookup_def … map ident ident)
    10099      ]
    101100    in
  • src/ASM/I8051.ma

    r1416 r1515  
    77include "utilities/Compare.ma".
    88include "joint/BEValues.ma".
     9include "ASM/BitVectorTrie.ma".
    910
    1011definition int_size ≝ bitvector_of_nat 8 1.
  • src/ASM/Interpret.ma

    r1514 r1515  
    686686      let preamble ≝ \fst (code_memory ? s) in
    687687      let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
    688         set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
     688        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
    689689    ]
    690690  in
  • src/ASM/Interpret2.ma

    r1478 r1515  
    2323 let s ≝ execute_1_pseudo_instruction ticks_of s in
    2424 match instr with
    25  [ Cost cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉
     25 [ Cost cst ⇒ ret … 〈Echarge cst, s〉
    2626 | _ ⇒ ret ? 〈E0, s〉 ].
    2727
     
    3737
    3838(*CSC: move this definition elsewhere *)
    39 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie Identifier 16).
     39definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    4040
    41 definition make_global: object_code → BitVectorTrie Identifier 16 ≝ \snd.
     41definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4242
    4343definition execute_1_instruction:
    44  BitVectorTrie Identifier 16 → Status → IO io_out io_in (trace × Status) ≝
     44 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
    4545λcosts,s.
    4646 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
     
    4949 match lookup_opt … pc costs with
    5050 [ None ⇒ ret … 〈E0, s〉
    51  | Some cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉 ].
     51 | Some cst ⇒ ret … 〈Echarge cst, s〉 ].
    5252
    53 axiom is_final: BitVectorTrie Identifier 16 → Status → option int.
     53axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
    5454
    5555definition exec: trans_system io_out io_in ≝
  • src/ASM/Status.ma

    r1459 r1515  
    702702  λr: BitVector 3.
    703703    let address ≝ bit_address_of_register ? s r in
    704       lookup address (low_internal_ram ? s) (zero 8).
     704      lookup ?? address (low_internal_ram ? s) (zero 8).
    705705     
    706706definition set_register ≝
     
    717717  λM: Type[0].
    718718  λs: PreStatus M.
    719     let 〈 nu, nl 〉 ≝ split 4 4 (get_8051_sfr ? s SFR_SP) in
     719    let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in
    720720    let m ≝ get_index_v … nu O ? in
    721721    let r1 ≝ get_index_v … nu 1 ? in
     
    804804        λext_indirect_dptr: True.
    805805          let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    806             lookup 16 address (external_ram ? s) (zero 8)
     806            lookup ? 16 address (external_ram ? s) (zero 8)
    807807      | EXT_INDIRECT e ⇒
    808808        λext_indirect: True.
    809809          let address ≝ get_register ? s [[ false; false; e ]]  in
    810810          let padded_address ≝ pad 8 8 address in
    811             lookup 16 padded_address (external_ram ? s) (zero 8)
     811            lookup ? 16 padded_address (external_ram ? s) (zero 8)
    812812      | ACC_DPTR ⇒
    813813        λacc_dptr: True.
     
    815815          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    816816          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
    817             lookup 16 address (external_ram ? s) (zero 8)
     817            lookup ? 16 address (external_ram ? s) (zero 8)
    818818      | ACC_PC ⇒
    819819        λacc_pc: True.
    820820          let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in
    821821          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in
    822             lookup 16 address (external_ram ? s) (zero 8)
     822            lookup ? 16 address (external_ram ? s) (zero 8)
    823823      | DIRECT d ⇒
    824824        λdirect: True.
    825           let 〈 nu, nl 〉 ≝ split 4 4 d in
     825          let 〈 nu, nl 〉 ≝ split ? 4 4 d in
    826826          let bit_one ≝ get_index_v ? ? nu 0 ? in
    827827          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     
    836836          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in
    837837          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    838           let bit_1 ≝ get_index_v bit_one_v O ? in
     838          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    839839          match  bit_1 with
    840840            [ false ⇒
     
    10021002                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10031003                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1004                 let trans ≝ lookup 7 address' (low_internal_ram ? s) (zero 8) in
     1004                let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    10051005                  ¬(get_index_v … trans (modulus address 8) ?)
    10061006              ]
     
    10381038                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    10391039                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1040                 let t ≝ lookup 7 address' (low_internal_ram ? s) (zero 8) in
     1040                let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in
    10411041                let n_bit ≝ set_index … t (modulus address 8) v ? in
    10421042                let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in
     
    10961096    match \fst x with
    10971097    [ None ⇒ false
    1098     | Some x ⇒ eq_bv ? x y
     1098    | Some x ⇒ eq_identifier ? x y
    10991099    ].
    11001100
     
    11141114lemma does_not_occur_Some:
    11151115 ∀id,id',i,list_instr.
    1116   eq_bv ? id' id = false →
     1116  eq_identifier ? id' id = false →
    11171117   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    11181118    does_not_occur id list_instr.
     
    11261126  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    11271127 #id #i #list_instr elim list_instr
    1128   [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
    1129     >eq_bv_refl %
     1128  [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
     1129    >eq_identifier_refl %
    11301130  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
    11311131qed.
     
    11511151lemma occurs_exactly_once_Some:
    11521152 ∀id,id',i,prefix.
    1153   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
     1153  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
    11541154 #id #id' #i #prefix elim prefix
    1155   [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    1156     change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
     1155  [ whd in ⊢ (?% → ?)
     1156    change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) with (eq_identifier ? id' id)
     1157    @eq_identifier_elim normalize nodelta; /2/
    11571158  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    11581159    cases he; normalize nodelta
    11591160     [ #H @ (IH H)
    1160      | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1161        change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
    1162        [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
    1163         /2/ #H >does_not_occur_Some //
     1161     | #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id)
     1162       @eq_identifier_elim #E normalize nodelta
     1163       [ destruct @eq_identifier_elim normalize nodelta;
     1164        /2/ #H >does_not_occur_Some /2/
    11641165       | #H @IH @H]]]
    11651166qed.
     
    11681169  ∀id,id',i,prefix.
    11691170    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
    1170     (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
    1171     (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
     1171    (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
     1172    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    11721173 #id #id' #i #prefix elim prefix
    1173  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
    1174   change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
     1174 [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?) with (eq_identifier ???)
     1175   @eq_identifier_elim #E
    11751176  [ normalize //
    11761177  | normalize #H @⊥ @H 
     
    11791180   cases he; normalize nodelta
    11801181   [ #H @ (IH H)
    1181    | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1182      generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
    1183      cases (eq_bv ???) in ⊢ (???% → %) #Heq
    1184      [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
    1185        [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
     1182   | #x @eq_identifier_elim #Heq
     1183     [ @eq_identifier_elim normalize nodelta
     1184       [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
    11861185       | #H >(does_not_occur_Some)
    1187          [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    1188            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    1189            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
    1190            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
    1191          | @(sym_eq … H)
     1186         [ #H2 whd in match (does_not_occur ??)
     1187           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1188           >Heq >eq_identifier_refl normalize nodelta
     1189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??)
     1190           change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1191           >eq_identifier_refl
     1192           normalize nodelta @H2 
     1193         | /2/
    11921194         ]
    11931195       ]
    1194      | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
    1195        generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
    1196        #Heq2
    1197        [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
    1198          whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    1199          change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    1200          cases (does_not_occur id tl) in Hor; normalize nodelta //
     1196     | normalize nodelta #H lapply (IH H) -IH -H;
     1197       @eq_identifier_elim #Heq2
     1198       #Hor @orb_elim
     1199       [ <Heq2 in Hor; #Hor normalize in Hor;
     1200         whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1201         >eq_identifier_false // normalize nodelta
     1202         cases (does_not_occur id' tl) in Hor; normalize nodelta //
    12011203       | normalize nodelta whd in match (occurs_exactly_once ??)
    1202          whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
    1203          >Heq normalize nodelta <Heq2 in Hor; normalize //
     1204         change in match (instruction_matches_identifier ??) with (eq_identifier ???)
     1205         >eq_identifier_false //
    12041206       ]
    12051207     ] 
     
    12411243
    12421244lemma index_of_internal_Some_miss: ∀i,id,id'.
    1243  eq_bv ? id' id = false →
     1245 eq_identifier ? id' id = false →
    12441246 ∀instr_list,n.
    12451247 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     
    12591261  = |instr_list| + n.
    12601262 #i #id #instr_list elim instr_list
    1261   [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
     1263  [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
    12621264  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    1263     [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
     1265    [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
    12641266qed.
    12651267
     
    12781280
    12791281lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1280  eq_bv ? id' id = false →
     1282 eq_identifier ? id' id = false →
    12811283  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    12821284   address_of_word_labels_code_mem instr_list id =
    12831285   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    12841286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1285  >(index_of_internal_Some_miss … H) //
     1287 >(index_of_internal_Some_miss … H) [ @refl | // ]
    12861288qed.
    12871289
     
    12911293   = bitvector_of_nat … (|instr_list|).
    12921294 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
    1293  >(index_of_internal_Some_hit … H) //
     1295 >(index_of_internal_Some_hit … H) <plus_n_O @refl
    12941296qed.
    12951297
     
    13011303definition construct_datalabels ≝
    13021304  λpreamble.
    1303     \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
     1305    \fst (foldl ((identifier_map ASMTag Word) × nat) ? (
    13041306    λt. λpreamble.
    13051307      let 〈datalabels, addr〉 ≝ t in
    13061308      let 〈name, size〉 ≝ preamble in
    13071309      let addr_16 ≝ bitvector_of_nat 16 addr in
    1308         〈insert ? ? name addr_16 datalabels, addr + size〉)
    1309           〈(Stub ? ?), 0〉 preamble).
     1310        〈add ? ? datalabels name addr_16, addr + size〉)
     1311          〈empty_map …, 0〉 preamble).
  • src/ASM/StatusProofs.ma

    r1014 r1515  
    182182lemma get_8051_sfr_write_at_stack_pointer:
    183183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
    184  #T #s #x #y whd in ⊢ (??%%) //
     184 #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
    185185qed.
    186186
  • 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  ]
  • 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)
  • src/ERTL/ERTLToLTL.ma

    r1424 r1515  
    380380  ].
    381381
    382 definition bvt_fold ≝
    383   λa, b: Type[0].
    384   λf: label → a → b → b.
    385   λtrie: BitVectorTrie a 16.
    386   λseed: b.
    387     let f' ≝ λbv: BitVector 16. λa. λb.
    388       f (an_identifier LabelTag bv) a b
    389     in
    390       bvtfold_aux a b f' seed 16 ? trie [[]].
    391   //
    392 qed.
    393 
    394382definition graph_fold ≝
    395383  λglobals.
     
    398386  λgraph: graph (ertl_statement globals).
    399387  λseed : b.
    400   match graph with
    401   [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed
    402   ]. 
     388    foldi (ertl_statement globals) b ? f graph seed.
    403389
    404390definition translate_internal: ∀globals: list ident.
  • src/LIN/LINToASM.ma

    r1379 r1515  
    3333    [ sequential instr' _ ⇒
    3434      match instr' with
    35       [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    36       | COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | _ ⇒ set_empty ?
     35      [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
     36      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
     37      | _ ⇒
    3838      ]
    39     | RETURN ⇒ set_empty ?
    40     | GOTO lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
     39    | RETURN ⇒
     40    | GOTO lbl ⇒ {(toASM_ident ? lbl)} ]
    4141  in
    4242  match label with
    4343  [ None ⇒ generated
    44   | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated
     44  | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
    4545  ].
    4646
    4747definition function_labels_internal ≝
    4848  λglobals: list ident.
    49   λlabels: BitVectorTrieSet ?.
     49  λlabels: identifier_set ?.
    5050  λstatement: lin_statement globals.
    51     set_union ? labels (statement_labels globals statement).
     51    labels ∪ (statement_labels globals statement).
    5252
    5353(* dpm: A = Identifier *)
    54 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
     54definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
    5555  λA: Type[0].
    5656  λglobals: list ident.
    5757  λf: A × (lin_function globals).
    5858  let 〈ignore, fun_def〉 ≝ f in
    59   match fun_def return λ_. BitVectorTrieSet ? with
     59  match fun_def return λ_. identifier_set ? with
    6060  [ Internal stmts ⇒
    61       foldl ? ? (function_labels_internal globals) (set_empty ?) (joint_if_code ?? stmts)
    62   | External _ ⇒ set_empty ?
     61      foldl ? ? (function_labels_internal globals) (joint_if_code ?? stmts)
     62  | External _ ⇒
    6363  ].
    6464 
    65 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝
     65definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
    6666  λA: Type[0].
    6767  λglobals: list ident.
    68   λlabels: BitVectorTrieSet ?.
     68  λlabels: identifier_set ?.
    6969  λfunct: A × (lin_function globals).
    70     set_union ? labels (function_labels ? globals funct).
     70    labels ∪ (function_labels ? globals funct).
    7171
    7272(* CSC: here we are silently throwing away the region information *)
     
    7474 λprogram: lin_program.
    7575    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
    76               (set_empty …) (prog_funct … program).
     76              (prog_funct … program).
    7777 
    7878definition data_of_int ≝ λbv. DATA bv.
     
    8686  λstatement: pre_lin_statement globals_old.
    8787  match statement with
    88   [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl)
     88  [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    8989  | RETURN ⇒ Instruction (RET ?)
    9090  | sequential instr _ ⇒
     
    9292      [ extension ext ⇒ ⊥
    9393      | COMMENT comment ⇒ Comment comment
    94       | COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl)
     94      | COST_LABEL lbl ⇒ Cost (toASM_ident ? lbl)
    9595      | POP _ ⇒ Instruction (POP ? accumulator_address)
    9696      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    9797      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    98       | CALL_ID f _ _ ⇒ Call (word_of_identifier ? f)
     98      | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
    9999      | OPACCS accs _ _ _ _ ⇒
    100100        match accs with
     
    236236      | COND _ lbl ⇒
    237237        (* dpm: this should be handled in translate_code! *)
    238         Instruction (JNZ ? (word_of_identifier ? lbl))
     238        Instruction (JNZ ? (toASM_ident ? lbl))
    239239      | SET_CARRY ⇒
    240240        Instruction (SETB ? CARRY)
     
    246246
    247247(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
    248 definition ident_of_label: label → ident
    249  λl. an_identifier … (word_of_identifier … l).
     248definition ident_of_label: label → Identifier
     249 toASM_ident LabelTag.
    250250
    251251definition build_translated_statement ≝
     
    275275      [ nil ⇒ ⊥
    276276      | cons hd tl ⇒
    277         let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
     277        let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
    278278          map ? ? (
    279279            λr.
    280280            match fst ? ? r with
    281             [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉
     281            [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
    282282            | None ⇒ 〈None ?, \snd r〉
    283283            ]) rest
     
    287287cases daemon (*CSC: XXX will be fixed by an invariant later *)
    288288qed.
    289    
     289
    290290definition translate_functs ≝
    291291  λglobals.
     
    312312
    313313(* dpm: plays the role of the string "_exit" in the O'caml source *)
    314 axiom identifier_prefix: Word.
     314axiom identifier_prefix: Identifier.
    315315(*CSC: XXXXXXX wrong anyway since labels from different functions can now
    316316  clash with each other and with names of functions *)
    317 axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
     317axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
    318318
    319319(* dpm: fresh prefix stuff needs unifying with brian *)
     
    323323  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    324324  let global_addr ≝ globals_addr (prog_vars … p) in
    325   let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
    326     〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
     325  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x,off〉) global_addr in
     326    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p)〉.
    327327 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
    328328 normalize in match prog_var_names normalize nodelta
  • src/LTL/LTLToLIN.ma

    r1379 r1515  
    2020let rec visit
    2121  (globals: list ident) (g: label → option (ltl_statement globals))
    22   (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
     22  (required: identifier_set LabelTag) (visited: identifier_set LabelTag)
    2323  (generated: list (lin_statement globals)) (l: label) (n: nat)
    24     on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
     24    on n: identifier_set LabelTag × (list (lin_statement globals)) ≝
    2525  match n with
    2626  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    2727  | S n' ⇒
    28     if set_member … (word_of_identifier … l) visited then
    29      〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉
     28    if mem_set … visited l then
     29     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
    3030    else
    31      let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
    32      match g (an_identifier LabelTag (word_of_identifier … l)) with
     31     let visited' ≝ add_set ? visited l in
     32     match g l with
    3333     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
    3434     | Some statement ⇒
     
    4141            let 〈required', generated''〉 ≝
    4242             visit globals g required visited' generated' l2 n' in
    43             let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
    44              if set_member … (word_of_identifier … l1) visited' then
     43            let required'' ≝ add_set ? required' l1 in
     44             if mem_set … visited' l1 then
    4545               〈required', generated''〉
    4646             else
     
    6262 λglobals,entry,labels_upper_bound,g.
    6363  let g ≝ branch_compress ? g in
    64   let visited ≝ set_empty ? in
    65   let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
     64  let visited ≝ in
     65  let required ≝ { (entry) } in
    6666  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
    6767  let reversed ≝ rev ? translated in
     
    7171       [ None ⇒ 〈None …,x〉
    7272       | Some l ⇒
    73           〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
     73          〈if mem_set … required' l then Some ? l else None ?,
    7474           x〉])
    7575    reversed.
     
    8383  mk_joint_internal_function globals (lin_params globals)
    8484   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
    85     (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
     85    (translate_graph globals (joint_if_entry ?? f) (nat_of_pos … (next_identifier … (joint_if_luniverse … f)))
    8686     (lookup ?? (joint_if_code … f)))
    8787    ??.
  • src/RTLabs/RTLabsToRTL.ma

    r1408 r1515  
    5959  | register_ptr: register → register → register_type.
    6060
    61 definition local_env ≝ BitVectorTrie (list register) 16.
     61definition local_env ≝ identifier_map RegisterTag (list register).
    6262
    6363definition mem_local_env : register → local_env → bool ≝
    64   λr. member … (word_of_identifier … r).
     64  λr,e. member … e r.
    6565
    6666definition add_local_env : register → list register → local_env → local_env ≝
    67   λr. insert … (word_of_identifier … r).
     67  λr,v,e. add … e r v.
    6868
    6969definition find_local_env : register → local_env → list register ≝
    70   λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
     70  λr: register.λenv. lookup_def … env r [].
    7171
    7272definition initialize_local_env_internal ≝
     
    8989    ]
    9090  in
    91     foldl … initialize_local_env_internal 〈Stub …,runiverse〉 registers.
     91    foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.
    9292
    9393definition map_list_local_env_internal ≝
  • src/common/Graphs.ma

    r1253 r1515  
    2626  λseed: B.
    2727  match graph with
    28   [ an_id_map map ⇒ fold A B 16 f map seed
     28  [ an_id_map map ⇒ fold A B f map seed
    2929  ].
    3030
  • src/common/Identifiers.ma

    r1316 r1515  
    11include "basics/types.ma".
    22include "ASM/String.ma".
    3 include "ASM/Arithmetic.ma".
     3include "utilities/binary/positive.ma".
    44include "common/Errors.ma".
    55include "utilities/option.ma".
     
    1010(* in common/PreIdentifiers.ma, via Errors.ma.
    1111inductive identifier (tag:String) : Type[0] ≝
    12   an_identifier : Word → identifier tag.
     12  an_identifier : Pos → identifier tag.
    1313*)
    1414
    1515record universe (tag:String) : Type[0] ≝
    1616{
    17   next_identifier : Word;
    18   counter_overflow: bool
     17  next_identifier : Pos
    1918}.
    2019
    2120definition new_universe : ∀tag:String. universe tag ≝
    22   λtag. mk_universe tag (zero ?) false.
     21  λtag. mk_universe tag one.
    2322
    2423(* Fresh identifier generation uses delayed overflow checking.  To make sure
     
    2827  λtag.
    2928  λuniv: universe tag.
    30   let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
    31     if get_index_v … carries 0 ? then
    32       〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
    33     else
    34       〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
    35   //
    36 qed.
    37 
    38 axiom TooManyIdentifiers : String.
    39 
    40 definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
    41   λtag, univ.
    42   if counter_overflow ? univ
    43   then Error ? (msg TooManyIdentifiers)
    44   else OK ? it.
     29  let id ≝ next_identifier ? univ in
     30  〈an_identifier tag id, mk_universe tag (succ id)〉.
    4531
    4632definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     
    5036    match r with
    5137    [ an_identifier r' ⇒
    52       eq_bv ? l' r'
     38      eqb l' r'
    5339    ]
    5440  ].
     
    5844  P (eq_identifier t x y).
    5945#P #t * #x * #y #T #F
    60 change with (P (eq_bv ???))
    61 @eq_bv_elim [ /2/ | * #H @F % #E destruct /2/ ]
     46change with (P (eqb ??))
     47@(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
    6248qed.
    6349   
     
    6955  ].
    7056
     57lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
     58#tag * #id whd in ⊢ (??%?) >eqb_n_n @refl
     59qed.
     60
     61lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
     62#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
     63qed.
     64
    7165definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
    72 #tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
     66#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
    7367#E [ % | %2 ]
    74 lapply E @eq_bv_elim
     68lapply E @eqb_elim
    7569[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
    7670qed.
    7771
    7872definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
    79   λtag,n. an_identifier tag (bitvector_of_nat ? n).
     73  λtag,n. an_identifier tag (succ_pos_of_nat n).
    8074
    8175
    8276(* Maps from identifiers to arbitrary types. *)
    8377
    84 include "ASM/BitVectorTrie.ma".
     78include "common/PositiveMap.ma".
    8579
    8680inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
    87   an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     81  an_id_map : positive_map A → identifier_map tag A.
    8882 
    8983definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
    90   λtag,A. an_id_map tag A (Stub A 16).
    91 
    92 definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
    93   λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
    94                               (match m with [ an_id_map m' ⇒ m' ]).
     84  λtag,A. an_id_map tag A (pm_leaf A).
     85
     86let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝
     87  lookup_opt A (match l with [ an_identifier l' ⇒ l' ])
     88               (match m with [ an_id_map m' ⇒ m' ]).
     89
     90definition lookup_def ≝
     91λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
     92
     93let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
     94  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
    9595
    9696(* Always adds the identifier to the map. *)
    97 definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
    98 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    99                                            (match m with [ an_id_map m' ⇒ m' ])).
     97let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝
     98  an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a
     99                            (match m with [ an_id_map m' ⇒ m' ])).
    100100
    101101lemma lookup_add_hit : ∀tag,A,m,i,a.
     
    106106
    107107lemma lookup_add_miss : ∀tag,A,m,i,j,a.
    108   (notb (eq_identifier tag i j))
     108  i ≠ j
    109109  lookup tag A (add tag A m j a) i = lookup tag A m i.
    110 #tag #A * #m * #i * #j #a
    111 change with (notb (eq_bv ???) → ?)
    112 @lookup_opt_insert_miss
     110#tag #A * #m * #i * #j #a #H
     111@lookup_opt_insert_miss /2/
    113112qed.
    114113
     
    117116  lookup tag A (add tag A m j a) i ≠ None ?.
    118117#tag #A #m #i #j #a #H
    119 lapply (lookup_add_miss … m i j a)
    120 @eq_identifier_elim
    121 [ #E #_ >E >lookup_add_hit % #N destruct
    122 | #_ #H' >H' //
     118cases (identifier_eq ? i j)
     119[ #E >E >lookup_add_hit % #N destruct
     120| #NE >lookup_add_miss //
    123121] qed.
    124122
     
    129127cases (identifier_eq ? i j)
    130128[ #E >E >lookup_add_hit #H %1 destruct % //
    131 | #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
     129| #NE >lookup_add_miss /2/
    132130] qed.
    133131
     
    135133definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
    136134λtag,A,m.
    137   fold ??? (λl,a,el. 〈an_identifier tag l, a〉::el)
    138            (match m with [ an_id_map m' ⇒ m' ]) [ ].
     135  fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el)
     136          (match m with [ an_id_map m' ⇒ m' ]) [ ].
    139137
    140138axiom MissingId : String.
     
    143141definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
    144142λtag,A,m,l,a.
    145   match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    146                     (match m with [ an_id_map m' ⇒ m' ]) with
     143  match update A (match l with [ an_identifier l' ⇒ l' ]) a
     144                 (match m with [ an_id_map m' ⇒ m' ]) with
    147145  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
    148146  | Some m' ⇒ OK ? (an_id_map tag A m')
     
    155153λA,B,tag,f,m,b.
    156154  match m with
    157   [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
     155  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
    158156
    159157(* A predicate that an identifier is in a map, and a failure-avoiding lookup
     
    162160definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
    163161λtag,A,m,i. lookup … m i ≠ None ?.
     162
     163lemma member_present : ∀tag,A,m,id.
     164  member tag A m id = true → present tag A m id.
     165#tag #A * #m #id normalize cases (lookup_opt A ??) normalize
     166[ #E destruct
     167| #x #E % #E' destruct
     168] qed.
     169
     170include "ASM/Util.ma".
    164171
    165172definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
     
    171178  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
    172179  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
    173   let u' ≝ update A 16 l' a m' in
    174   match u' return λx. update ????? = x → ? with
     180  let u' ≝ update A l' a m' in
     181  match u' return λx. update ???? = x → ? with
    175182  [ None ⇒ λE.⊥
    176183  | Some m' ⇒ λ_. an_id_map tag A m'
    177184  ] (refl ? u').
    178 whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
    179 cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
     185cases l in p E; cases m; -l' -m' #m' #l'
     186whd in ⊢ (% → ?)
     187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
    180188#NL #U cases NL #H @H @(update_fail … U)
    181189qed.
     
    188196whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
    189197cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
    190 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
     198[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
    191199  % #E' destruct
    192 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
    193   <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
     200| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
     201  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    194202] qed.
    195203
     
    197205
    198206inductive identifier_set (tag:String) : Type[0] ≝
    199   an_id_set : BitVectorTrie unit 16 → identifier_set tag.
     207  an_id_set : positive_map unit → identifier_set tag.
    200208
    201209definition empty_set : ∀tag:String. identifier_set tag ≝
    202 λtag. an_id_set tag (Stub unit 16).
     210λtag. an_id_set tag (pm_leaf unit).
    203211
    204212let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
    205   an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
    206                              it (match s with [ an_id_set s' ⇒ s' ])).
     213  an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
     214                          it (match s with [ an_id_set s' ⇒ s' ])).
    207215
    208216definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
     
    210218
    211219let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
    212   match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
    213                         (match s with [ an_id_set s' ⇒ s' ]) with
     220  match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
     221                     (match s with [ an_id_set s' ⇒ s' ]) with
    214222  [ None ⇒ false
    215223  | Some _ ⇒ true
     
    217225
    218226let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
    219   an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
    220                                (match s' with [ an_id_set s1 ⇒ s1 ])).
     227  an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
     228                            (match s' with [ an_id_set s1 ⇒ s1 ])).
    221229
    222230interpretation "identifier set union" 'union a b = (union_set ? a b).
     
    231239
    232240lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    233 #tag * #s cases (BitVectorTrie_Sn … s)
    234 [ * #x * #y #E >E //
    235 | #E >E //
    236 ] qed.
     241#tag * * // qed.
  • src/common/PreIdentifiers.ma

    r797 r1515  
    77include "basics/types.ma".
    88include "ASM/String.ma".
    9 include "ASM/Arithmetic.ma".
     9include "utilities/binary/positive.ma".
    1010
    1111(* identifiers and their generators are tagged to differentiate them, and to
     
    1313
    1414inductive identifier (tag:String) : Type[0] ≝
    15   an_identifier : Word → identifier tag.
     15  an_identifier : Pos → identifier tag.
  • src/joint/Erasure.ma

    r1472 r1515  
    55  (globals: list ident) (the_program: list (lin_statement globals))
    66    (labels: list label)
    7       on the_program: ((BitVectorTrie Word 16) × (list (lin_statement globals))) ≝
     7      on the_program: ((identifier_map ? label) × (list (lin_statement globals))) ≝
    88  match the_program with
    99  [ nil        ⇒
    1010    match labels with
    11     [ nil ⇒ 〈Stub Word 16, [ ]〉 (* XXX: labels should be empty *)
     11    [ nil ⇒ 〈empty_map …, [ ]〉 (* XXX: labels should be empty *)
    1212    | _   ⇒ ⊥
    1313    ]
     
    2626          ]
    2727      | Some lbl ⇒
    28         let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    2928        match instr with
    3029        [ sequential seq l ⇒
     
    3332          | _ ⇒
    3433            let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
    35             let maps ≝ foldr ? ? (λl. λmap.
    36               match l with
    37               [ an_identifier l ⇒ insert … l lbl' map
    38               ]) maps (lbl :: labels)
     34            let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
    3935            in
    4036              〈maps, instructions〉
     
    4238        | _ ⇒
    4339          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
    44           let maps ≝ foldr ? ? (λl. λmap.
    45             match l with
    46             [ an_identifier l ⇒ insert … l lbl' map
    47             ]) maps (lbl :: labels)
     40          let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
    4841          in
    4942            〈maps, instructions〉
     
    6255    ∀globals: list ident.
    6356    ∀params: params_.
    64       BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝
     57      identifier_map LabelTag label → joint_instruction params globals → joint_instruction params globals ≝
    6558  λglobals: list ident.
    6659  λparams.
     
    6962  match instr with
    7063  [ COND acc_a lbl ⇒
    71     let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    72     let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
     64    let located ≝ lookup_def ?? map lbl lbl in
    7365      COND params globals acc_a located
    7466  | _ ⇒ instr
     
    7870  ∀globals: list ident.
    7971  ∀params: params_.
    80     BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝
     72    identifier_map LabelTag label → joint_statement params globals → joint_statement params globals ≝
    8173  λglobals: list ident.
    8274  λparams: params_.
    83   λmap: BitVectorTrie Word 16.
     75  λmap: identifier_map LabelTag label.
    8476  λstmt: joint_statement params globals.
    8577  match stmt with
     
    8981  | RETURN ⇒ RETURN params globals
    9082  | GOTO l ⇒
    91     let l ≝ match l with [ an_identifier l ⇒ l ] in
    92     let located ≝ an_identifier LabelTag (lookup … l map l) in
     83    let located ≝ lookup_def ?? map l l in
    9384      GOTO params globals located
    9485  ].
    9586
    9687let rec relabel_lin_internal_function'
    97   (globals: list ident) (map: BitVectorTrie Word 16)
     88  (globals: list ident) (map: identifier_map LabelTag label)
    9889    (program: list (lin_statement globals))
    9990      on program: list (lin_statement globals) ≝
     
    10798      [ None ⇒ None …
    10899      | Some label ⇒
    109         let label ≝ match label with [ an_identifier l ⇒ l ] in
    110           Some … (an_identifier LabelTag (lookup … label map label))
     100          Some … (lookup_def ?? map label label)
    111101      ]
    112102    in
     
    122112definition empty_graph ≝
    123113  λa: Type[0].
    124     an_id_map LabelTag a (Stub a 16).
     114    empty_map LabelTag a.
    125115
    126116let rec pre_erase_graph_internal_function'
    127117  (params1: params1) (globals: list ident)
    128118    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
    129       (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)
    130         (visited: BitVectorTrie bool 16)
    131           on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝
    132   match size_counter return λ_.  ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     119      (entry_point: label) (size_counter: nat) (map: identifier_map LabelTag label)
     120        (visited: identifier_map LabelTag bool)
     121          on size_counter: ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) ≝
     122  match size_counter return λ_.  ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    133123  [ O ⇒
    134124    match labels with
     
    137127    ]
    138128  | S size_counter ⇒
    139     let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
    140129    let statement ≝ lookup LabelTag ? the_graph entry_point in
    141     match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     130    match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    142131    [ None ⇒ ⊥ (* XXX: should not happen *)
    143132    | Some statement ⇒
    144       let entered_previously ≝ bvt_lookup … entry_point' visited false in
    145       match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     133      let entered_previously ≝ lookup_def … visited entry_point false in
     134      match entered_previously return λe: bool. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    146135      [ true ⇒ 〈map, visited, the_graph〉
    147136      | false ⇒ (* XXX: never visited here before *)
    148         let visited ≝ insert … entry_point' true visited in
    149         match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     137        let visited ≝ add … visited entry_point true in
     138        match statement return λs: joint_statement (graph_params params1 globals) globals. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    150139        [ sequential seq l ⇒
    151140          match seq with
     
    155144            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    156145            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] cond_label size_counter map visited in
    157             let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     146            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    158147              〈map, visited, the_graph〉
    159148          | _ ⇒
    160149            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    161             let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     150            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    162151              〈map, visited, the_graph〉
    163152          ]
    164153        | RETURN ⇒
    165           let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     154          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    166155            〈map, visited, the_graph〉
    167156        | GOTO l ⇒
    168157          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    169           let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     158          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    170159            〈map, visited, the_graph〉
    171160        ]
     
    183172  [ dp entry entry_proof ⇒
    184173    let code ≝ joint_if_code … int_fun in
    185     let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (Stub …) (Stub …) in
     174    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (empty_map …) (empty_map …) in
    186175      〈map, the_graph〉
    187176  ].
     
    189178let rec relabel_graph'
    190179  (params1: params1) (globals: list ident)
    191     (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)
    192       (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)
     180    (the_graph: codeT globals (graph_params params1 globals)) (map: identifier_map LabelTag label)
     181      (visited: identifier_map LabelTag bool) (entry_point: label) (size_counter: nat)
    193182        on size_counter: codeT globals (graph_params params1 globals) ≝
    194183  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
    195184  [ O ⇒ empty_graph …
    196185  | S size_counter ⇒
    197     let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
    198     let relabelled_entry_point ≝ an_identifier LabelTag (bvt_lookup … entry_point' map entry_point') in
     186    let relabelled_entry_point ≝ lookup_def … map entry_point entry_point in
    199187    let statement ≝ lookup LabelTag ? the_graph entry_point in
    200188    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
    201189    [ None ⇒ ⊥ (* XXX: should not happen *)
    202190    | Some statement ⇒
    203       let entered_previously ≝ (bvt_lookup … entry_point' visited false) in
     191      let entered_previously ≝ lookup_def … visited entry_point false in
    204192      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
    205193      [ true ⇒ the_graph
    206194      | false ⇒ (* XXX: never visited here before *)
    207         let visited ≝ insert … entry_point' true visited in
     195        let visited ≝ add … visited entry_point true in
    208196        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
    209197        [ sequential seq l ⇒
    210           let l' ≝ match l with [ an_identifier l ⇒ l ] in
    211198          let 〈the_graph, new_seq〉 ≝
    212199            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
    213200            [ COND acc_a cond_label ⇒
    214               let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
    215               let relabelled ≝ an_identifier LabelTag (bvt_lookup … cond_label' map cond_label') in
     201              let relabelled ≝ lookup_def … map cond_label cond_label in
    216202              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
    217203                〈tail_graph, COND … acc_a relabelled〉
     
    220206          in
    221207            let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
    222             let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
     208            let relabelled ≝ lookup_def … map l l in
    223209              add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
    224210        | RETURN ⇒ the_graph
    225211        | GOTO l ⇒
    226           let l' ≝ match l with [ an_identifier l ⇒ l ] in
    227           let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
     212          let relabelled ≝ lookup_def … map l l in
    228213            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
    229214        ]
     
    237222  λglobals: list ident.
    238223  λparams1: params1.
    239   λmap: BitVectorTrie Word 16.
     224  λmap: identifier_map LabelTag label.
    240225  λint_fun: joint_internal_function globals (graph_params params1 globals).
    241226    match joint_if_entry … int_fun with
    242227    [ dp entry entry_prf ⇒
    243228      let code ≝ joint_if_code … int_fun in
    244         relabel_graph' … code map (Stub …) entry (graph_num_nodes … code)
     229        relabel_graph' … code map (empty_map …) entry (graph_num_nodes … code)
    245230    ].
    246231   
     
    248233  λglobals: list ident.
    249234  λpars: params globals.
    250   λerasure_function: joint_internal_function globals pars → (BitVectorTrie Word 16) × (codeT … pars).
    251   λrelabelling_function: BitVectorTrie Word 16 → joint_internal_function globals pars → codeT … pars.
     235  λerasure_function: joint_internal_function globals pars → (identifier_map LabelTag label) × (codeT … pars).
     236  λrelabelling_function: identifier_map LabelTag label → joint_internal_function globals pars → codeT … pars.
    252237  λint_fun: joint_internal_function globals pars.
    253238  match joint_if_entry … int_fun with
     
    255240    match joint_if_exit … int_fun with
    256241    [ dp exit exit_prf ⇒
    257       let exit' ≝ word_of_identifier … exit in
    258       let entry' ≝ word_of_identifier … entry in
    259242      let 〈maps, code〉 ≝ erasure_function int_fun in
    260243      let int_fun ≝ set_joint_code globals pars int_fun code entry exit in
    261244      let code ≝ relabelling_function maps int_fun in
    262         set_joint_code globals pars int_fun code (an_identifier … (bvt_lookup … entry' maps entry'))
    263         (an_identifier … (bvt_lookup … exit' maps exit'))
     245        set_joint_code globals pars int_fun code (lookup_def … maps entry entry)
     246        (lookup_def … maps exit exit)
    264247    ]
    265248  ].
  • src/joint/SemanticUtils.ma

    r1452 r1515  
    2525 λoldpc,l.
    2626  mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (nat_of_bitvector ? (word_of_identifier … l))).
     27   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
    2828// qed.
    2929
     
    3434
    3535definition graph_label_of_pointer: pointer → res label ≝
    36  λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))).
     36 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    3737
    3838(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
  • src/joint/TranslateUtils.ma

    r1352 r1515  
    2424    cases (fresh_regs pars0 globals def m) normalize nodelta
    2525    #def' #regs #EQ change in EQ with (|regs| = m) <EQ
    26     change with
    27     (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?)
    28     cases (fresh … (joint_if_runiverse … def')) normalize // ]
     26    @refl
     27 ]
    2928qed.
    3029
  • src/utilities/binary/positive.ma

    r1330 r1515  
    656656definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
    657657
    658 interpretation "natural minus" 'minus x y = (minus x y).
     658interpretation "positive minus" 'minus x y = (minus x y).
    659659
    660660lemma partialminus_S: ∀n,m:Pos.
     
    942942  ].
    943943
    944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.
     944theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0].
    945945(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
    946946#n elim n;
     
    11591159
    11601160definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
     1161
     1162
     1163
     1164definition max : Pos → Pos → Pos ≝
     1165λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
  • src/utilities/extralib.ma

    r1350 r1515  
    389389definition mod ≝ λm,n. snd ?? (divide m n).
    390390
    391 lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
     391lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).
    392392@pos_elim /3/;
    393393qed.
  • src/utilities/extranat.ma

    r961 r1515  
     1include "basics/types.ma".
    12include "arithmetics/nat.ma".
    23
     
    3637[ //
    3738| #m' #IH whd in ⊢ (??%?) > IH @refl
     39] qed.
     40
     41
     42let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
     43match n return λn.Sum (n=m) (n≠m) with
     44[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
     45| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒
     46           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
     47].
     48[ 1,2: % #E destruct
     49| >E @refl
     50| % #E destruct cases NE /2/
    3851] qed.
    3952
Note: See TracChangeset for help on using the changeset viewer.