Ignore:
Timestamp:
Sep 3, 2012, 12:42:47 PM (8 years ago)
Author:
boender
Message:
  • now it compiles
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2316 r2318  
    182182definition sigma_compact ≝
    183183 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    184  ∀n.n < |program| →
     184 ∀datalabels.∀n.n < |program| →
    185185  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    186186  [ None ⇒ False
     
    190190    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    191191       pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    192          (λx.zero ?)
     192         datalabels
    193193         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    194194         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
     
    615615  sigma_compact program (create_label_map program) sigma.
    616616  #program cases program -program #program #Hprogram #old_sigma #sigma
    617   #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #i #Hi
     617  #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #dlbl #i #Hi
    618618  lapply (Hcp_unsafe i Hi) -Hcp_unsafe lapply (Hsafe i Hi) -Hsafe
    619619  inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))
Note: See TracChangeset for help on using the changeset viewer.