Changeset 341


Ignore:
Timestamp:
Nov 30, 2010, 3:06:51 PM (9 years ago)
Author:
sacerdot
Message:

A simple version of assembly (no labels) implemented.

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

Legend:

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

    r316 r341  
    479479;;
    480480*)
     481
     482ndefinition assembly: List instruction → List Byte ≝
     483 fold_right … (λi,l. assembly1 i @ l) [].
  • Deliverables/D4.1/Matita/Interpret.ma

    r338 r341  
    11include "Status.ma".
    2 (* include "Fetch.ma". *)
     2include "Fetch.ma".
    33include "Cartesian.ma".
    44include "Arithmetic.ma".
    55include "List.ma".
    6 
    7 naxiom fetch: BitVectorTrie Byte sixteen → Word → (preinstruction [[relative]]) × Word × Nat.
    86
    97alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
  • Deliverables/D4.1/Matita/depends

    r334 r341  
     1Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    13Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
    6 Universes.ma
    76Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    87Either.ma Bool.ma Maybe.ma Universes.ma
     8Universes.ma
    99ASM.ma BitVectorTrie.ma Either.ma String.ma
     10Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1011Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1112Char.ma Universes.ma
    12 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
     13Test.ma Assembly.ma
    1314Connectives.ma Plogic/equality.ma
    1415Bool.ma Universes.ma
    1516Assembly.ma ASM.ma
    1617List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     18Util.ma Nat.ma
    1719Interpret.ma Arithmetic.ma Cartesian.ma List.ma Status.ma
    18 Util.ma Nat.ma
     20BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1921Compare.ma Universes.ma
    20 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    2122String.ma Char.ma List.ma
    2223Plogic/equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.