Changeset 414 for Deliverables


Ignore:
Timestamp:
Dec 13, 2010, 6:03:05 PM (9 years ago)
Author:
mulligan
Message:

Got a few more cases working.

Location:
Deliverables/D4.1/Matita
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r410 r414  
    430430          let 〈name, size〉 ≝ preamble in
    431431          let addr_sixteen ≝ bitvector_of_nat sixteen addr in
    432             〈insert ? ? addr_sixteen name datalabels, addr + size〉)
     432            〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉)
    433433              〈(Stub ? ?), Z〉 preamble in
    434434    let 〈pc_labels, costs〉 ≝
     
    440440              [ Instruction instr ⇒
    441441                let code_memory ≝ load_code_memory (assembly1 instr) in
    442                 let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
     442                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
    443443                let 〈instr', program_counter'〉 ≝ instr_pc' in
    444444                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
     
    446446              | Label label ⇒
    447447                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
    448                   〈〈program_counter, (insert ? ? program_counter_bv label labels)〉, costs〉
     448                  〈〈program_counter, (insert ? ? (bitvector_of_string ? label) program_counter_bv labels)〉, costs〉
    449449              | Cost cost ⇒
    450450                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
     
    479479                  | Call call ⇒
    480480                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
    481                     let address ≝ ADDR16 (bitvector_of_nat sixteen pc_offset) in
    482                       assembly1 (LCALL address)
    483                   | _ ⇒ ?
     481                    let address ≝ ADDR16 pc_offset in
     482                      assembly1 (LCALL ? address)
     483                  | Mov d trgt ⇒
     484                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
     485                    let address ≝ DATA16 pc_offset in
     486                      assembly1 (MOV ? (Right ? ?(Right ? ? (Right ? ? (Right ? ? (Right ? ? 〈DPTR, address〉))))))
     487                  | Instruction instr ⇒ ?
     488                  | Jmp jmp ⇒
     489                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
     490                    let address ≝ ADDR16 pc_offset in
     491                      assembly1 (LJMP ? address)
     492                  | WithLabel jmp ⇒ ?
    484493                  ]
    485494            ) instr_list
  • Deliverables/D4.1/Matita/Map.ma

    r410 r414  
    11include "Universes.ma".
    22include "Compare.ma".
     3include "Maybe.ma".
    34
    45ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝
     
    78| Node: A → B → Map A B → Map A B → Map A B.
    89
     10(* Greater than or equal to the right, less than to the left.  *)
     11
    912nlet rec insert (A: Type[0]) (B: Type[0])
    10                 (key: A) (f: A → A → Compare) (value: B) (map: Map A B)
     13                (key: A) (f: A → A → Compare) (value: B) (map: Map A B) on map
    1114  match map with
    12     [ Empty ⇒ Leaf key value
     15    [ Empty ⇒ Leaf key value
    1316    | Leaf key' value' ⇒
    1417      match f key key' with
    15         [ Equal ⇒ ?
    16         | Less ⇒ ?
    17         | Greater ⇒ ?
     18        [ Equal ⇒ Node … key' value' (Empty …) (Leaf … key value)
     19        | Less ⇒ Node … key' value' (Leaf … key value) (Empty …)
     20        | Greater ⇒ Node … key' value' (Empty …) (Leaf … key value)
    1821        ]
    19     | Node key' value'
     22    | Node key' value' left right
    2023      match f key key' with
    21         [ Equal ⇒ ?
    22         | Less ⇒ ?
    23         | Greater ?
     24        [ Equal ⇒ Node A B key' value' left (insert A B key f value right)
     25        | Less ⇒ Node A B key' value' (insert A B key f value left) right
     26        | Greater ⇒ Node A B key' value' left (insert A B key f value right)
    2427        ]
    2528    ].
     29   
     30nlet rec lookup (A: Type[0]) (B: Type[0])
     31                (key: A) (f: A → A → Compare) (map: Map A B) on map ≝
     32  match map with
     33    [ Empty ⇒ Nothing ?
     34    | Leaf key' value' ⇒
     35      match f key key' with
     36        [ Equal ⇒ Just ? value'
     37        | _ ⇒ Nothing ?
     38        ]
     39    | Node key' value' left right ⇒
     40      match f key key' with
     41        [ Equal ⇒ Just ? value'
     42        | Less ⇒ lookup A B key f left
     43        | Greater ⇒ lookup A B key f right
     44        ]
     45    ].
  • Deliverables/D4.1/Matita/String.ma

    r329 r414  
    11include "Char.ma".
    22include "List.ma".
     3include "Compare.ma".
    34
    45ndefinition String ≝ List Char.
     6
     7naxiom string_lexicographic_ordering: String → String → Compare.
  • Deliverables/D4.1/Matita/depends

    r410 r414  
    99DoTest.ma Assembly.ma Interpret.ma Test.ma
    1010ASM.ma BitVector.ma Either.ma String.ma
     11Map.ma Compare.ma Maybe.ma Universes.ma
    1112Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1213Char.ma Universes.ma
     
    1516Connectives.ma Plogic/equality.ma
    1617Bool.ma Universes.ma
    17 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
     18Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Map.ma Status.ma
    1819List.ma Maybe.ma Util.ma
    1920Interpret.ma Fetch.ma Status.ma
    2021Util.ma Nat.ma
     22Compare.ma Universes.ma
    2123BitVector.ma String.ma Vector.ma
    2224String.ma Char.ma List.ma
Note: See TracChangeset for help on using the changeset viewer.