Changeset 2708


Ignore:
Timestamp:
Feb 22, 2013, 7:11:30 PM (7 years ago)
Author:
tranquil
Message:

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2705 r2708  
    984984
    985985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
    986 definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
     986definition preamble ≝ list (Identifier × Word).
    987987definition assembly_program ≝ list instruction.
    988988definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
  • src/LIN/LINToASM.ma

    r2490 r2708  
    33include "LIN/LIN.ma".
    44include "ASM/ASM.ma".
     5include "utilities/state.ma".
     6
     7(* utilities to provide Identifier's and addresses  *)
     8record ASM_universe (globals : list ident) : Type[0] :=
     9{ id_univ : universe ASMTag
     10; current_funct : ident
     11; ident_map : identifier_map SymbolTag Identifier
     12; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
     13; address_map : identifier_map SymbolTag Word
     14; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
     15}.
     16
     17definition new_ASM_universe :
     18∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
     19λp.
     20  let globals_addr_internal ≝
     21   λres_offset : identifier_map SymbolTag Word × Z.
     22   λx_size: ident × region × nat.
     23    let 〈res, offset〉 ≝ res_offset in
     24    let 〈x, region, size〉 ≝ x_size in
     25      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in
     26  let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in
     27mk_ASM_universe ? (mk_universe … one)
     28  (an_identifier … one (* dummy *))
     29  (empty_map …) (empty_map …)
     30  (\fst addresses) ?.
     31@hide_prf
     32normalize nodelta
     33cases p -p #vars #functs #main
     34#i #H
     35letin init_val ≝ (〈empty_map ? Word, OZ〉)
     36cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
     37[ %2{H} ] -H
     38lapply i -i lapply init_val -init_val elim vars -vars
     39[2: ** #id #r #v #tl #IH ] #init_val #i
     40[2: * [2: * ] #H @H ]
     41* [2: #H cases (orb_Prop_true … H) -H ] #H
     42@IH
     43[ %1 cases init_val normalize nodelta #init_map #off
     44  >(proj1 ?? (eqb_true ???) H) @mem_set_add_id
     45| %2{H}
     46| %1 cases init_val in H; normalize nodelta #init_map #off #H
     47  >mem_set_add @orb_Prop_r @H
     48]
     49qed.
     50
     51definition Identifier_of_label :
     52  ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
     53λg,l,u.
     54let current ≝ current_funct … u in
     55let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
     56let 〈id, univ, lmap〉 ≝
     57  match lookup … lmap l with
     58  [ Some id ⇒ 〈id, id_univ … u, lmap〉
     59  | None ⇒
     60    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     61    〈id, univ, add … lmap l id〉
     62  ] in
     63〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
     64  (address_map … u) (globals_are_in … u), id〉.
     65
     66definition Identifier_of_ident :
     67  ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
     68λg,i,u.
     69let imap ≝ ident_map … u in
     70let 〈id, univ, imap〉 ≝
     71  match lookup … imap i with
     72  [ Some id ⇒ 〈id, id_univ … u, imap〉
     73  | None ⇒
     74    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     75    〈id, univ, add … imap i id〉
     76  ] in
     77〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
     78  (address_map … u) (globals_are_in … u), id〉.
     79
     80definition start_funct_translation :
     81  ∀globals.(ident × (joint_function LIN globals)) →
     82    state_monad (ASM_universe globals) unit ≝
     83  λg,id_f,u.
     84    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
     85      (address_map … u) (globals_are_in … u), it〉.
     86
     87definition address_of_ident :
     88  ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
     89λglobals,i,prf,u.
     90〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.
     91
     92definition ASM_fresh :
     93  ∀globals.state_monad (ASM_universe globals) Identifier ≝
     94λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     95〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
     96  (address_map … u) (globals_are_in … u), id〉.
    597
    698definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    22114    ]. @I qed.
    23115
    24 let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
    25                     on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
    26   match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
    27   [ nil ⇒ Ⓧ
    28   | cons hd tl ⇒
    29     λprf.
    30     If eq_A a (\fst hd) then \snd hd else with eq_prf do
    31       association … eq_A a tl ?
    32   ].
    33   elim (orb_Prop_true … prf)
    34     [ > eq_prf *
    35     | # H
    36       assumption
    37     ]
    38 qed.
    39 
    40 definition association_ident ≝ association ident nat (eq_identifier ?).
    41 definition association_block ≝ association block Word eq_block.
    42 
    43116definition vector_cast :
    44117∀A,n,m.A → Vector A n → Vector A m ≝
     
    68141definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
    69142
    70 definition statement_labels ≝
    71   λg: list ident.
    72   λs: lin_statement g.
    73   let 〈label, instr〉 ≝ s in
    74   let generated ≝
    75     match instr with
    76     [ sequential instr' _ ⇒
    77       match instr' with
    78       [ step_seq instr'' ⇒
    79         match instr'' with
    80         [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
    81         | _ ⇒ ∅
    82         ]
    83       | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
    84       ]
    85     | final instr' ⇒
    86       match instr' with
    87       [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
    88       | _ ⇒ ∅
    89       ]
    90     ]
    91   in
    92   match label with
    93   [ None ⇒ generated
    94   | Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)
    95   ].
    96 
    97 definition function_labels_internal ≝
    98   λglobals: list ident.
    99   λlabels: identifier_set ?.
    100   λstatement: lin_statement globals.
    101     labels ∪ (statement_labels globals statement).
    102 
    103 (* dpm: A = Identifier *)
    104 definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝
    105   λA: Type[0].
    106   λglobals: list ident.
    107   λf: A × (joint_function LIN globals).
    108   let 〈ignore, fun_def〉 ≝ f in
    109   match fun_def return λ_. identifier_set ? with
    110   [ Internal stmts ⇒
    111       foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)
    112   | External _ ⇒ ∅
    113   ].
    114  
    115 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝
    116   λA: Type[0].
    117   λglobals: list ident.
    118   λlabels: identifier_set ?.
    119   λfunct: A × (joint_function LIN globals).
    120     labels ∪ (function_labels ? globals funct).
    121 
    122 (* CSC: here we are silently throwing away the region information *)
    123 definition program_labels ≝
    124  λprogram: lin_program.
    125     foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
    126               ∅ (prog_funct … program).
    127  
    128143definition data_of_int ≝ λbv. DATA bv.
    129144definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
     
    133148definition asm_other_bit ≝ BIT_ADDR (zero_byte).
    134149
    135 definition translate_statements
    136   λglobals: list (ident × nat).
    137   λglobals_old: list ident.
    138   λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
    139   λstatement: joint_statement LIN globals_old.
    140   match statement  with
     150definition translate_statements :
     151  ∀globals.
     152  joint_statement LIN globals →
     153  state_monad (ASM_universe globals) pseudo_instruction ≝
     154  λglobals,statement.
     155  match statement with
    141156  [ final instr ⇒
    142157    match instr with
    143     [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    144     | RETURN ⇒ Instruction (RET ?)
     158    [ GOTO lbl ⇒
     159      ! lbl' ← Identifier_of_label … lbl ;
     160      return Jmp (toASM_ident ? lbl)
     161    | RETURN ⇒ return Instruction (RET ?)
    145162    | TAILCALL abs _ _ ⇒ Ⓧabs
    146163    ]
     
    152169          match ext with
    153170          [ SAVE_CARRY ⇒
    154             Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
     171            return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
    155172          | RESTORE_CARRY ⇒
    156             Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
     173            return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
     174          | LOW_ADDRESS reg lbl ⇒
     175            ! lbl' ← Identifier_of_label … lbl ;
     176            return MovSuccessor (register_address reg) LOW lbl'
     177          | HIGH_ADDRESS reg lbl ⇒
     178            ! lbl' ← Identifier_of_label … lbl ;
     179            return MovSuccessor (register_address reg) HIGH lbl'
    157180          ]
    158         | COMMENT comment ⇒ Comment comment
    159         | COST_LABEL lbl ⇒ Cost lbl
    160         | POP _ ⇒ Instruction (POP ? accumulator_address)
    161         | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    162         | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    163         | CALL f _ _ ⇒
    164           match f with
    165           [ inl f_id ⇒ Call (toASM_ident ? f_id)
    166           | inr _ ⇒ (* TODO call from ptr in DPTR *)
    167             match not_implemented in False with [ ]
    168           ]
     181        | COMMENT comment ⇒ return Comment comment
     182        | POP _ ⇒ return Instruction (POP ? accumulator_address)
     183        | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address)
     184        | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY)
    169185        | OPACCS accs _ _ _ _ ⇒
    170           match accs with
     186          return match accs with
    171187          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    172188          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    173189          ]
    174190        | OP1 op1 _ _ ⇒
    175           match op1 with
     191          return match op1 with
    176192          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    177193          | Inc ⇒ Instruction (INC ? ACC_A)
     
    179195          ]
    180196        | OP2 op2 _ _ reg ⇒
    181           match arg_address … reg
     197          return match arg_address … reg
    182198          return λx.is_in … [[ acc_a;
    183199                                 direct;
     
    221237          | _ ⇒ Ⓧ
    222238          ] (subaddressing_modein …)
    223         | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    224         | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     239        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     240        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    225241        | ADDRESS addr proof _ _ ⇒
    226           let look ≝ association_ident addr globals (prf ? proof) in
    227             Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     242          ! addr' ← address_of_ident … proof ;
     243          return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
    228244        | SET_CARRY ⇒
    229           Instruction (SETB ? CARRY)
     245          return Instruction (SETB ? CARRY)
    230246        | MOVE regs ⇒
    231           match regs with
     247          return match regs with
    232248          [ to_acc _ reg ⇒
    233249            match register_address reg return λx.is_in … [[ acc_a;
     
    276292          ]
    277293        ]
     294      | CALL f _ _ ⇒
     295        match f with
     296        [ inl id ⇒
     297          ! id' ← Identifier_of_ident … id ;
     298          return Call (toASM_ident ? id')
     299        | inr _ ⇒
     300          return Instruction (JMP … INDIRECT_DPTR)
     301        ]
     302      | COST_LABEL lbl ⇒ return Cost lbl
    278303      | COND _ lbl ⇒
    279         (* dpm: this should be handled in translate_code! *)
    280         Instruction (JNZ ? (toASM_ident ? lbl))
     304        ! l ← Identifier_of_label … lbl;
     305        return Instruction (JNZ ? l)
    281306      ]
     307    | FCOND _ _ lbl_true lbl_false ⇒
     308      ! l1 ← Identifier_of_label … lbl_true;
     309      ! l2 ← Identifier_of_label … lbl_false;
     310      return Jnz ACC_A l1 l2
    282311    ].
    283312  try @I
    284313qed.
    285314
    286 (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
    287 definition ident_of_label: label → Identifier ≝
    288  toASM_ident LabelTag.
    289315
    290316definition build_translated_statement ≝
    291317  λglobals.
    292   λglobals_old.
    293   λprf.
    294   λstatement: lin_statement globals_old.
    295     〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
     318  λstatement: lin_statement globals.
     319  ! stmt ← translate_statements globals (\snd statement) ;
     320  match \fst statement with
     321  [ Some lbl ⇒
     322    ! lbl' ← Identifier_of_label globals lbl ;
     323    return 〈Some ? lbl', stmt〉
     324  | None ⇒
     325    return 〈None ?, stmt〉
     326  ].
    296327
    297328definition translate_code ≝
    298   λglobals: list (ident × nat).
    299   λglobals_old: list ident.
    300   λprf.
    301   λcode: list (lin_statement globals_old).
    302     map ? ? (build_translated_statement globals globals_old prf) code.
     329  λglobals.
     330  λcode: list (lin_statement globals).
     331    m_list_map … (build_translated_statement globals) code.
    303332
    304333definition translate_fun_def ≝
    305   λglobals: list (ident × nat).
    306   λglobals_old.
    307   λprf.
    308   λid_def : ident × (joint_function LIN globals_old).
    309     let 〈id, def〉 ≝ id_def in
    310     match def with
     334  λglobals.
     335  λid_def : ident × (joint_function LIN globals).
     336  !_ start_funct_translation … id_def ;
     337  (* ^ modify current function id ^ *)
     338  match \snd id_def with
    311339    [ Internal int ⇒
    312       let code ≝ joint_if_code LIN globals_old int in
    313       match translate_code globals globals_old prf code with
    314       [ nil ⇒ ⊥
     340      let code ≝ joint_if_code … int in
     341      ! id ← Identifier_of_ident … (\fst id_def) ;
     342      ! code' ← translate_code … code ;
     343      match code' with
     344      [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *)
    315345      | cons hd tl ⇒
    316         let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in
    317           map ? ? (
    318             λr.
    319             match fst ? ? r with
    320             [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉
    321             | None ⇒ 〈None ?, \snd r〉
    322             ]) rest
     346        match \fst hd with
     347        [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl)
     348        | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *)
     349        ]
    323350      ]
    324     | External _ ⇒ [ ]
     351    | External _ ⇒ return [ ]
    325352    ].
    326 cases daemon (*CSC: XXX will be fixed by an invariant later *)
    327 qed.
    328 
    329 include "common/Identifiers.ma".
    330 
    331 let rec flatten_fun_defs
    332   (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    333     (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
    334       on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
    335   match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
    336   [ cons hd tl ⇒
    337     let fun_def ≝ \snd hd in
    338     let fun_id ≝ \fst hd in
    339     let translated ≝ translate_fun_def globals globals_old prf hd in
    340     let size_translated ≝ | translated | in
    341     let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in
    342     let new_hd ≝ translated @ tail_trans in
    343     let new_map ≝ add ? ? tail_map fun_id initial_pc in
    344       〈new_hd, new_map〉
    345   | nil ⇒ 〈[ ], empty_map …〉
    346   ].
    347 
    348 definition translate_functs ≝
    349   λglobals.
    350   λglobals_old.
    351   λprf.
    352   λexit_label.
    353   λmain.
    354   λfuncts : list (ident × (joint_function LIN ?)).
    355   let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    356   let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
    357    〈preamble @ flattened, map〉.
    358 
    359 (*CSC: region silently thrown away here *)
    360 definition globals_addr ≝
    361  λl.
    362   let globals_addr_internal ≝
    363    λres_offset.
    364    λx_size: ident × region × nat.
    365     let 〈res, offset〉 ≝ res_offset in
    366     let 〈x, region, size〉 ≝ x_size in
    367       〈〈x, offset〉 :: res, offset + size〉
    368   in
    369     \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    370 
    371 (* dpm: plays the role of the string "_exit" in the O'caml source *)
    372 axiom identifier_prefix: Identifier.
    373 (*CSC: XXXXXXX wrong anyway since labels from different functions can now
    374   clash with each other and with names of functions *)
    375 axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier.
    376 
    377 (* dpm: fresh prefix stuff needs unifying with brian *)
     353
    378354definition lin_to_asm : lin_program → pseudo_assembly_program ≝
    379355  λp.
    380   let prog_lbls ≝ program_labels … p in
    381   let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    382   let global_addr ≝ globals_addr (prog_vars … p) in
    383   let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
    384   let 〈translated, funct_map〉 ≝
    385     translate_functs global_addr (prog_var_names … p) ? exit_label
    386     (toASM_ident … (prog_main … p)) (prog_funct ?? p) in
    387     〈〈funct_map, global_addr'〉, translated〉.
    388  #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
    389  normalize in match prog_var_names; normalize nodelta
    390  elim (prog_vars … p) //
    391  #hd #tl #IH whd in ⊢ (% → %);
    392  whd in match globals_addr; normalize nodelta
    393  whd in match (foldl ???? (hd::tl)); normalize nodelta
    394  cases hd * #id #reg #size normalize nodelta
    395  cases daemon (*CSC: provable using a pair of lemmas over foldl *)
    396 qed.
     356  state_run ?? (new_ASM_universe p)
     357    (let add_translation ≝
     358      λacc,id_def.
     359      ! code ← translate_fun_def … id_def ;
     360      ! acc ← acc ;
     361      return (code @ acc) in
     362     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
     363     ! exit_label ← ASM_fresh … ;
     364     ! main ← Identifier_of_ident … (prog_main … p) ;
     365     let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     366     (* atm no data identifier is used in the code, so preamble must be empty *)
     367     return 〈[ ], code〉).
  • src/joint/TranslateUtils.ma

    r2688 r2708  
    2727    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    2828     〈set_runiverse … def runiverse, r〉.
    29 
    30 definition state_update : ∀S.(S → S) → state_monad S unit ≝
    31 λS,f,s.〈f s, it〉.
    3229
    3330(* insert into a graph a list of instructions *)
  • src/joint/linearise.ma

    r2702 r2708  
    256256    cases s in H3; [3: *]
    257257    [ * ] normalize nodelta
    258     [2,4: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
    259       inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
     258    [1,2,4: [ #c | #f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
     259      inversion (lookup … visited nxt) in H; [2,4,6: #n'] normalize nodelta
     260      #EQlookup
    260261      normalize nodelta *
    261       [ #EQn' %1 >EQn' %
    262       | #H %2{H}
    263       | #H' lapply (All_nth … H … H')
     262      [1,3,5: #EQn' %1 >EQn' %
     263      |2,4,6: #H %2{H}
     264      |*: #H' lapply (All_nth … H … H')
    264265        whd in ⊢ (?%→?); >EQlookup *
    265266      ]
    266     |3: #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
     267    | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
    267268      inversion (lookup … visited lfalse) in H2;
    268269      [ #ABS * #H' lapply (All_nth … H … H')
     
    270271      | #n' #_ normalize nodelta #EQ >EQ %
    271272      ]
    272     | #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *)
     273    | #s #H @H
    273274    ]
    274275  ]
     
    326327|12: (* add_req_gen utility *)
    327328  #P whd in match add_req_gen;
    328   cases statement [ * [#f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
    329  [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) -H2
    330       cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try %
    331       //
    332  |3,5: normalize nodelta [#_] #H #_ @H %
    333  | normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ
    334    normalize nodelta [ @nxt | @dest ] >EQ try % ]
    335 |14: skip
    336 ] cases daemon (*CSC: XXXXXXXXX
     329  cases statement [ * [ #cost | #f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
     330  normalize nodelta
     331  [3,5: #H #_ @(H I) ]
     332  inversion (nxt ∈ visited') #EQ normalize nodelta
     333  #H1 #H2 [1,3,5: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
    337334|3: elim H #pre ** #H1 #H2 #_
    338335  #i >mem_set_union
     
    341338    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    342339  | >mem_set_union
    343     #H elim (orb_Prop_true … H) -H (*CSC XXXXXXXXXX
     340    #H elim (orb_Prop_true … H) -H
    344341    [ #i_expl %1 @Exists_append_l
    345342      lapply i_expl whd in match translated_statement;
    346       cases statement [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | *] normalize nodelta #H
     343      cases statement [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | *]
     344      normalize nodelta #H
    347345      lapply (mem_list_as_set … H) -H #H
    348       [1,3,4: @Exists_append_r assumption ]
     346      [1,2,4,5: @Exists_append_r assumption ]
    349347      cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]]
    350348      #EQ destruct(EQ) [ %1 % |*: %2 %1 % ]
     
    366364        #i_vis %2 >mem_set_add @orb_Prop_r assumption
    367365      ]
    368     ]*) cases daemon
     366    ]
    369367  ]
    370368|4,5,6: change with reverse in match rev;
     
    423421        lapply (in_map_domain … visited vis_hd)
    424422        >H3 normalize nodelta //
    425       | %{statement}  (*CSC XXXXXXX
     423      | %{statement}
    426424        %
    427425        [ @lookup_eq_safe
     
    429427          change with statement in match (lookup_safe ?????);
    430428          cases statement;
    431           [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
    432           [1,2,3: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
    433           [1,2,5,6: % | %2 | %1 % ]
    434           [1,3,5,7,9,10,12:
     429          [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     430          [1,2,3,4: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
     431          [1,2,3,4,7,8: % | %2 | %1 % ]
     432          [1,3,5,7,9,11,13,14,16:
    435433            >nth_opt_append_r >rev_length <gen_length_prf try %
    436             <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta
    437             >nxt_vis %
     434            <minus_n_n try % try( whd in match graph_to_lin_statement; normalize nodelta
     435            >nxt_vis %)
    438436          |*:
    439437            lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta
    440             [1,3: * #n' ] #EQlookup >EQlookup normalize nodelta
    441             [1,2: %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4: %2 %1 ]
    442               <minus_Sn_n %
    443             |*: %%
    444             ]
    445           ]*) cases daemon
     438            [1,3,5: * #n' ] #EQlookup >EQlookup normalize nodelta
     439            try (%% @False)
     440            %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4,6: %2 %1 ]
     441            <minus_Sn_n %
     442          ]
    446443        ]
    447444      ]
    448445    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
    449       cases daemon (*CSC XXXX
    450446      #Hlookup elim (generated_prf1 … Hlookup)
    451447      #G1 * #s * #G2 #G3
     
    463459        %{G2}
    464460        cases s in G3;
    465         [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
    466         [1,3: * #EQnth_opt #next_spec % | * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
    467         [1,3,5,7: @nth_opt_append_hit_l assumption
    468         |2,4,6: @(eq_identifier_elim … nxt vis_hd)
    469           [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ]
     461        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
     462        [1,2,4: normalize nodelta #H cases H in ⊢ ?; -H
     463          #EQnth_opt #next_spec % |3: normalize nodelta * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
     464        [1,3,5,7,9: @nth_opt_append_hit_l assumption
     465        |2,4,6,8: @(eq_identifier_elim … nxt vis_hd)
     466          [1,3,5,7: #EQ destruct(EQ) >lookup_add_hit whd
     467            [1,2,3: %1]
    470468            lapply (in_map_domain … visited vis_hd)
    471469            >H3 #EQ >EQ in next_spec; * #_ #OK >OK %
    472           |*: #NEQ' >(lookup_add_miss … visited … NEQ')
    473             lapply (in_map_domain … visited nxt)
    474             inversion (nxt ∈ visited) #nxt_vis [1,3: * #n'' ] #EQlookup'
    475             >EQlookup' in next_spec; whd in ⊢ (%→%);
    476             [ * [ #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption
    477             | #H @H
    478             |*: * >H2
     470          |*: #NEQ' >(lookup_add_miss … visited … NEQ') in
     471            ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     472            generalize in match next_spec in ⊢ ?;
     473            inversion (lookup … visited nxt) normalize nodelta
     474            [2,4,6,8: #n'' ] #EQlookup'
     475            [1,2,3: * [1,3,5: #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption
     476            |4: #H @H
     477            |*: * #nxt_visiting @⊥
     478              >H2 in nxt_visiting;
    479479              cases pre in H1;
    480               [1,3: #_
     480              [1,3,5,7: #_
    481481              |*: #frst #pre_tl * #ABS #_
    482482              ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
    483               [1,2: cases NEQ' #ABS cases (ABS ?) %
    484               |*: >nxt_vis in ABS; *
     483              [1,2,3,4: cases NEQ' #ABS cases (ABS ?) %
     484              |*: lapply ABS; whd in ⊢ (?%→?); >EQlookup' *
    485485              ]
    486486            ]
    487487          ]
     488        |10: @nth_opt_append_hit_l assumption
    488489        ]
    489       ] *)
     490      ]
    490491    ]
    491492  | #i whd in match visited';
     
    498499    | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?))
    499500      >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ]
    500       @add_req_gen_prf [ #_ | #s #next #_ #_ ] %
     501      @add_req_gen_prf [ #_ | #s #next #_ ] %
    501502    ]
    502503  ]
    503504| @add_req_gen_prf
    504   [ #K | #s #next #K #next_vis %1 %1 %{(GOTO … next)} % ]
     505  [ #K | #next #K #next_vis %1 %1 %{(GOTO … next)} % ]
    505506  whd in match generated'; whd in match translated_statement;
    506507  normalize nodelta
    507508  change with statement in match (lookup_safe ?????);
    508509  cases statement in K;
    509   [ * [ #s | #a #ltrue ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta
    510   [2: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis
     510  [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta
     511  [3: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis
    511512    [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ]
    512   | #nxt_vis ]
     513  |*: #nxt_vis ]
    513514  %2 % * >nxt_vis *
    514515| whd in match generated';
    515   @add_req_gen_prf [ #_ | #s #next #_ #_ ] normalize >gen_length_prf %
     516  @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf %
    516517|
    517 ]*)
     518]
    518519qed.
    519520
     
    643644           [ sequential s' nxt ⇒
    644645             match s' with
    645              [ step_seq _ ⇒
    646                (stmt_at … c n = Some ? (sequential … s' it)) ∧
     646             [ COND a ltrue ⇒
     647               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
     648               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
     649             | _ ⇒
     650                (stmt_at … c n = Some ? (sequential … s' it)) ∧
    647651                  ((sigma nxt = Some ? (S n)) ∨
    648652                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
    649              | COND a ltrue ⇒
    650                (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
    651                (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
    652              | CALL _ _ _ ⇒
    653                (stmt_at … c n = Some ? (sequential … s' it)) ∧
    654                   ((sigma nxt = Some ? (S n)) ∨
    655                    (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
    656              | COST_LABEL _ ⇒
    657                (stmt_at … c n = Some ? (sequential … s' it)) ∧
    658                   ((sigma nxt = Some ? (S n)) ∨
    659                    (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
    660653             ]
    661654           | final s' ⇒
     
    708701| >commutative_plus change with (? ≤ |g|) %
    709702]
    710 cases daemon qed. (*
    711703**
    712704#visited #required #generated normalize nodelta ****
     
    725717    * #n_lbl #EQsigma
    726718    elim (sigma_prop … EQsigma) #_ * #stmt * #_
    727     cases stmt [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    728     [ * #EQnth_opt #_ | * [ * ] #EQnth_opt [ #_ ] | #EQnth_opt ]
     719    cases stmt [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     720    [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ]
    729721    >(nth_opt_index_of_label ???? n_lbl ? H)
    730     [1,4,7,10: normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
    731     |3: @(sequential … s it) |6: @(sequential … (COND … a ltrue) it)
    732     |9: @(FCOND … I a ltrue nxt) |12: @(final … s)
    733     |2,5,8,11: >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
    734       >H2 %
     722    try (normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption)
     723    [1,3,5,7,9,11:
     724      >nth_opt_filter_labels in ⊢ (??%?);
     725      (* without the try it does not work *)
     726      try >EQnth_opt in ⊢ (??%?);
     727      >m_return_bind in ⊢ (??%?);
     728      >m_return_bind in ⊢ (??%?);
     729      >H2 in ⊢ (??%?); %
     730    |*:
    735731    ]
    736732  | #eq_lookup elim (sigma_prop ?? eq_lookup)
     
    739735    [ @All_append
    740736      [ cases stmt in stmt_spec;
    741         [ * [ #s | #a #ltrue ] #nxt | #s #_ % | * ]
    742         normalize nodelta * [ #stmt_at_EQ * #nxt_spec | * #stmt_at_EQ #nxt_spec | #stmt_at_EQ ]
     737        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ % | * ]
     738        normalize nodelta
     739        [1,2,4: * #stmt_at_EQ * #nxt_spec |3: * [ * ] #stmt_at_EQ [ #nxt_spec ]]
    743740        %{I}
    744         [1,3: >nxt_spec % #ABS destruct(ABS)
    745         |*: lapply (in_map_domain … visited nxt)
    746           >req_vis
    747           [1,3: * #x #EQ >EQ % #ABS destruct(ABS)
    748           |2: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
    749             whd in ⊢ (??%?); >nxt_spec %
    750           |4: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …)))
    751             whd in ⊢ (??%?); >stmt_at_EQ %
    752           ]
     741        try (>nxt_spec % #ABS destruct(ABS) @False)
     742        lapply (in_map_domain … visited nxt)
     743        >req_vis
     744        [1,3,5,7: * #x #EQ >EQ % #ABS destruct(ABS)
     745        |2,4,6: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
     746          whd in ⊢ (??%?); >nxt_spec %
     747        |8: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …)))
     748          whd in ⊢ (??%?); >stmt_at_EQ %
    753749        ]
    754750      | cases stmt in stmt_spec;
    755         [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    756         [ * #EQ #_ | * [ * #EQ #_ | #EQ ] | #EQ ]
     751        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     752        [1,2,4: * #EQ #_ |3: * [ * ] #EQ [ #_ ] |5: #EQ ]
    757753        whd in match stmt_explicit_labels; normalize nodelta
    758         [ @(All_mp … (labels_in_req n (sequential … s it) ?))
     754        [ @(All_mp … (labels_in_req n (sequential … (COST_LABEL … cost) it) ?))
     755        | @(All_mp … (labels_in_req n (sequential … (CALL … f args dest) it) ?))
     756        | @(All_mp … (labels_in_req n (sequential … s it) ?))
    759757        | @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?))
     758        |6: @(All_mp … (labels_in_req n (final … s) ?))
    760759        | cases (labels_in_req n (FCOND … I a ltrue nxt) ?)
    761760          [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue)
    762761            >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ]
    763         | @(All_mp … (labels_in_req n (final … s) ?))
    764762        ]
    765         [1,3,6: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) % #ABS destruct(ABS)
     763        [1,3,5,7,9: #l #l_req >(lookup_eq_safe … (req_vis … l_req))
     764          % #ABS destruct(ABS)
    766765        |*: whd in ⊢ (??%?); >EQ %
    767766        ]
    768767      ]
    769768    | cases stmt in stmt_spec;
    770       [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    771       [ * #EQ #H | * [ * #EQ #H | #EQ ] | #EQ ]
     769      [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     770      [1,2,4: * #EQ #H |3: * [ * ] #EQ [ #H ] |5: #EQ ]
    772771      >stmt_at_filter_labels
    773772      whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta
    774       [ % [%] cases H -H [#H %1{H} | #EQ' %2 >stmt_at_filter_labels whd in ⊢ (??%?); >EQ' % ]
     773      [1,2,3: % [1,3,5: %] cases H -H
     774        #H try (%1{H}) %2 >stmt_at_filter_labels whd in ⊢ (??%?); >H %
    775775      | %1 %{H} %
    776776      | %2 %
     
    796796    cut (|generated| = S i)
    797797    [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) )
    798       elim (option_bind_inverse ????? EQ) #x * #EQ1 #EQ2
     798      whd in EQ : (??%?); inversion (nth_opt ???) in EQ;
     799      [2: #x ] #EQ1 whd in ⊢ (??%%→?); #EQ2 destruct
    799800      <length_reverse
    800801      @(nth_opt_hit_length … EQ1)
     
    843844  〈«mk_joint_internal_function (mk_lin_params p) globals
    844845   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    845    (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    846    (joint_if_stacksize ?? f_sig) code entry, ?»,
     846   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig)
     847   (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?»,
    847848   sigma〉.
    848849normalize nodelta
  • src/joint/semanticsUtils.ma

    r2688 r2708  
    311311* #vars1 #functs1 #main1
    312312* #vars2 #functs2 #main2
    313 * #Mvars #Mfns #EQmain destruct
     313*
     314whd in match prog_var_names;
     315normalize nodelta;
     316#Mvars #Mfns #EQmain destruct
    314317lapply (sym_eq ????)
    315 whd in match prog_var_names in functs2 Mfns ⊢ %;
    316 normalize nodelta in functs2 Mfns ⊢ %; #E
    317 lapply Mfns lapply functs2 -functs2 lapply Mvars -Mvars lapply init_eq -init_eq
     318#E
     319lapply Mfns lapply functs2 -functs2
    318320whd in match globalenv; whd in match globalenv_allocmem;
    319 normalize nodelta
    320 cases daemon
    321 (* TODO I hate coercions *)
     321whd in match prog_var_names in E ⊢ %;
     322normalize nodelta in E ⊢ %;
     323>E normalize nodelta #functs2 #Mfns
     324@add_globals_match [ assumption | % ]
     325@add_functs_match [ assumption ]
     326% try % #p %
    322327qed.
    323328
  • src/utilities/state.ma

    r1976 r2708  
    2424definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
    2525definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
     26definition state_update : ∀S.(S → S) → state_monad S unit ≝ λS,f,s.〈f s, it〉.
    2627
    2728definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
Note: See TracChangeset for help on using the changeset viewer.