Changeset 698


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
Files:
17 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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • src/LIN/LIN.ma

    r696 r698  
    1818
    1919inductive LINStatement (globals: list (Identifier × nat)): Type[0] ≝
    20   | LIN_St_Goto: Label → LINStatement globals
    21   | LIN_St_Label: Label → LINStatement globals
     20  | LIN_St_Goto: Identifier → LINStatement globals
     21  | LIN_St_Label: Identifier → LINStatement globals
    2222  | LIN_St_Comment: String → LINStatement globals
    2323  | LIN_St_CostLabel: CostLabel → LINStatement globals
     
    3535  | LIN_St_Store: LINStatement globals
    3636  | LIN_St_CallId: Identifier → LINStatement globals
    37   | LIN_St_CondAcc: Label → LINStatement globals
     37  | LIN_St_CondAcc: Identifier → LINStatement globals
    3838  | LIN_St_Return: LINStatement globals.
    3939 
  • src/LIN/LINToASM.ma

    r696 r698  
    1 include "cerco/Util.ma".
    2 include "cerco-intermediate-languages/utilities/BitVectorTrieSet.ma".
    3 include "cerco-intermediate-languages/LIN/LIN.ma".
     1include "ASM/Util.ma".
     2include "utilities/BitVectorTrieSet.ma".
     3include "LIN/LIN.ma".
    44 
    55let rec association (i: Identifier) (l: list (Identifier × nat))
     
    267267  λl.
    268268    foldl ? ? globals_addr_internal 〈[ ], 0〉 l.
    269        
     269     
     270(*   
    270271definition translate ≝
    271272  λp.
     
    284285      ASM.phas_main = p.LIN.main <> None } in
    285286  ASMInterpret.assembly p
     287  *)
  • src/common/AST.ma

    r491 r698  
    11include "arithmetics/nat.ma".
    22
    3 include "cerco/String.ma".
    4 include "cerco/BitVector.ma".
    5 include "cerco-intermediate-languages/utilities/Compare.ma".
    6 include "cerco-intermediate-languages/common/CostLabel.ma".
     3include "ASM/String.ma".
     4include "ASM/BitVector.ma".
     5include "utilities/Compare.ma".
     6include "common/CostLabel.ma".
    77
    88definition Identifier ≝ Byte.
  • src/common/CostLabel.ma

    r491 r698  
    1 include "cerco/BitVector.ma".
    2 include "cerco-intermediate-languages/utilities/StringTools.ma".
     1include "ASM/BitVector.ma".
     2include "utilities/StringTools.ma".
    33
    44definition CostLabel ≝ Byte.
  • src/utilities/BitVectorTrieSet.ma

    r491 r698  
    1 include "cerco/BitVectorTrie.ma".
     1include "ASM/BitVectorTrie.ma".
    22
    33definition BitVectorTrieSet ≝ BitVectorTrie unit.
  • src/utilities/StringTools.ma

    r491 r698  
    1 include "cerco/String.ma".
    2 include "cerco-intermediate-languages/utilities/Compare.ma".
     1include "ASM/String.ma".
     2include "utilities/Compare.ma".
    33
    44axiom compare: String → String → Compare.
Note: See TracChangeset for help on using the changeset viewer.