Changeset 698 for src/ASM


Ignore:
Timestamp:
Mar 18, 2011, 1:47:53 PM (9 years ago)
Author:
mulligan
Message:

Commit with changes to files to get our files to typecheck.

Location:
src/ASM
Files:
11 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r690 r698  
    1 include "cerco/BitVector.ma".
    2 include "cerco/String.ma".
     1include "common/AST.ma".
    32
    43inductive addressing_mode: Type[0] ≝
     
    65| INDIRECT: Bit → addressing_mode
    76| EXT_INDIRECT: Bit → addressing_mode
    8 | REGISTER: BitVector (S (S (S O))) → addressing_mode
     7| REGISTER: BitVector 3 → addressing_mode
    98| ACC_A: addressing_mode
    109| ACC_B: addressing_mode
     
    191190inductive labelled_instruction: Type[0] ≝
    192191  Instruction: instruction → labelled_instruction
    193 | Cost: String → labelled_instruction
    194 | Jmp: String → labelled_instruction
    195 | Call: String → labelled_instruction
    196 | Mov: [[dptr]] → String → labelled_instruction
    197 | Label: String → labelled_instruction
    198 | WithLabel: jump String → labelled_instruction.
    199 
    200 definition preamble ≝ list (String × nat).
     192| Cost: Identifier → labelled_instruction
     193| Jmp: Identifier → labelled_instruction
     194| Call: Identifier → labelled_instruction
     195| Mov: [[dptr]] → Identifier → labelled_instruction
     196| Label: Identifier → labelled_instruction
     197| WithLabel: jump Identifier → labelled_instruction.
     198
     199definition preamble ≝ list (Identifier × nat).
    201200
    202201definition assembly_program ≝ preamble × (list labelled_instruction).
  • src/ASM/Arithmetic.ma

    r697 r698  
    1 include "cerco/BitVector.ma".
    2 include "cerco/Util.ma".
     1include "ASM/BitVector.ma".
     2include "ASM/Util.ma".
    33
    44definition nat_of_bool ≝
  • src/ASM/BitVector.ma

    r697 r698  
    88include "arithmetics/nat.ma".
    99
    10 include "cerco/Util.ma".
    11 include "cerco/Vector.ma".
    12 include "cerco/String.ma".
     10include "ASM/Util.ma".
     11include "ASM/Vector.ma".
     12include "ASM/String.ma".
    1313
    1414(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    123123        false) b c.
    124124
     125(* dpm: commented out to get our stuff to typecheck
    125126lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
    126127  (x = y → P true) →
     
    130131#Q * *; normalize /3/
    131132qed.
     133*)
    132134
    133135let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
  • src/ASM/BitVectorTrie.ma

    r697 r698  
    11include "basics/types.ma".
    22
    3 include "cerco/BitVector.ma".
     3include "ASM/BitVector.ma".
    44
    55inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
  • src/ASM/Fetch.ma

    r690 r698  
    1 include "cerco/BitVectorTrie.ma".
    2 include "cerco/Arithmetic.ma".
    3 include "cerco/ASM.ma".
     1include "ASM/BitVectorTrie.ma".
     2include "ASM/Arithmetic.ma".
     3include "ASM/ASM.ma".
    44
    55include "basics/pairs.ma".
  • src/ASM/I8051.ma

    r696 r698  
    22include "basics/jmeq.ma".
    33
    4 include "cerco/String.ma".
    5 include "cerco/ASM.ma".
    6 include "cerco-intermediate-languages/utilities/Compare.ma".
     4include "ASM/String.ma".
     5include "ASM/ASM.ma".
     6include "utilities/Compare.ma".
    77
    88(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
  • src/ASM/Interpret.ma

    r690 r698  
    1 include "cerco/Status.ma".
    2 include "cerco/Fetch.ma".
     1include "ASM/Status.ma".
     2include "ASM/Fetch.ma".
    33
    44definition sign_extension: Byte → Word ≝
  • src/ASM/Status.ma

    r690 r698  
    33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    44
    5 include "cerco/ASM.ma".
    6 include "cerco/Arithmetic.ma".
    7 include "cerco/BitVectorTrie.ma".
     5include "ASM/ASM.ma".
     6include "ASM/Arithmetic.ma".
     7include "ASM/BitVectorTrie.ma".
    88
    99definition Time ≝ nat.
  • src/ASM/String.ma

    r690 r698  
    11include "basics/list.ma".
    22
    3 include "cerco/Char.ma".
     3include "ASM/Char.ma".
    44
    55definition String ≝ list Char.
  • src/ASM/Util.ma

    r697 r698  
    22include "basics/list.ma".
    33include "basics/types.ma".
     4
     5let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
     6  match l with
     7  [ nil ⇒ a
     8  | cons hd tl ⇒ foldl A B f (f a hd) tl
     9  ].
     10
     11definition flatten ≝
     12  λA: Type[0].
     13  λl: list (list A).
     14    foldl ? ? (append ?) [ ] l.
    415
    516definition if_then_else ≝
  • src/ASM/Vector.ma

    r697 r698  
    88include "basics/types.ma".
    99
    10 include "cerco/Util.ma".
     10include "ASM/Util.ma".
    1111
    1212include "arithmetics/nat.ma".
    1313
    14 include "oldlib/eq.ma".
     14(* include "oldlib/eq.ma". *)
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    469469*)
    470470
     471(* dpm: commented out to get out stuff to typecheck
    471472lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
    472473  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     
    485486  ]
    486487] qed.
     488*)
    487489
    488490(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.