Changeset 700


Ignore:
Timestamp:
Mar 18, 2011, 4:28:26 PM (9 years ago)
Author:
campbell
Message:

Get Clight semantics going again (except for problems CexecEquiv? that I caused
earlier).

Location:
src
Files:
22 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r698 r700  
    123123        false) b c.
    124124
    125 (* dpm: commented out to get our stuff to typecheck
    126125lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
    127126  (x = y → P true) →
     
    131130#Q * *; normalize /3/
    132131qed.
    133 *)
    134132
    135133let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
  • src/ASM/BitVectorZ.ma

    r697 r700  
    11
    2 include "binary/Z.ma".
    3 include "cerco/BitVector.ma".
    4 include "cerco/Arithmetic.ma".
     2include "utilities/binary/Z.ma".
     3include "ASM/BitVector.ma".
     4include "ASM/Arithmetic.ma".
    55
    66let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
  • src/ASM/Vector.ma

    r698 r700  
    1212include "arithmetics/nat.ma".
    1313
    14 (* include "oldlib/eq.ma". *)
     14include "utilities/oldlib/eq.ma".
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    469469*)
    470470
    471 (* dpm: commented out to get out stuff to typecheck
     471(* dpm: commented out to get out stuff to typecheck *)
    472472lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
    473473  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     
    486486  ]
    487487] qed.
    488 *)
    489488
    490489(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • src/Clight/AST.ma

    r636 r700  
    1818
    1919include "basics/types.ma".
    20 include "extralib.ma".
    21 include "Integers.ma".
    22 include "Floats.ma".
    23 include "binary/positive.ma".
     20include "utilities/extralib.ma".
     21include "common/Integers.ma".
     22include "common/Floats.ma".
     23include "utilities/binary/positive.ma".
    2424
    2525(* * * Syntactic elements *)
  • src/Clight/Animation.ma

    r693 r700  
    11
    2 include "Cexec.ma".
     2include "Clight/Cexec.ma".
    33
    44(* Functions to allow programs to be executed up to some number of steps, given
  • src/Clight/Cexec.ma

    r693 r700  
    11
    22
    3 include "extralib.ma".
    4 include "IOMonad.ma".
    5 include "SmallstepExec.ma".
    6 include "Csem.ma".
     3include "utilities/extralib.ma".
     4include "common/IOMonad.ma".
     5include "common/SmallstepExec.ma".
     6include "Clight/Csem.ma".
    77
    88(*
  • src/Clight/CexecComplete.ma

    r500 r700  
    1 include "Cexec.ma".
     1include "Clight/Cexec.ma".
    22
    33definition yields ≝ λA.λa:res A.λv':A.
  • src/Clight/CexecEquiv.ma

    r487 r700  
    1 include "CexecComplete.ma".
    2 include "CexecSound.ma".
    3 include "extralib.ma".
     1include "Clight/CexecComplete.ma".
     2include "Clight/CexecSound.ma".
     3include "utilities/extralib.ma".
    44
    55include "basics/jmeq.ma".
     
    1010| se_step : trace → state → s_execution → s_execution
    1111| se_wrong : s_execution
    12 | se_interact : ∀o:io_out. (io_in o → execution) → io_in o → s_execution → s_execution.
    13 
    14 coinductive single_exec_of : execution → s_execution → Prop ≝
    15 | seo_stop : ∀tr,r,m. single_exec_of (e_stop tr r m) (se_stop tr r m)
     12| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.
     13
     14coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
     15| seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m)
    1616| seo_step : ∀tr,s,e,se.
    1717    single_exec_of e se →
    18     single_exec_of (e_step tr s e) (se_step tr s se)
    19 | seo_wrong : single_exec_of e_wrong se_wrong
     18    single_exec_of (e_step ??? tr s e) (se_step tr s se)
     19| seo_wrong : single_exec_of (e_wrong ???) se_wrong
    2020| seo_interact : ∀o,k,i,se.
    2121    single_exec_of (k i) se →
    22     single_exec_of (e_interact o k) (se_interact o k i se).
     22    single_exec_of (e_interact ??? o k) (se_interact o k i se).
    2323
    2424(* starting after state s, zero or more steps of execution e reach state s'
     
    4949] qed.
    5050
    51 lemma exec_e_step: ∀ge,x,tr,s,e.
    52   exec_inf_aux ge x = e_step tr s e →
    53   exec_inf_aux ge (exec_step ge s) = e.
    54 #ge #x #tr #s #e
     51lemma exec_e_step: ∀p,ge,x,tr,s,e.
     52  exec_inf_aux (clight_exec p) ge x = e_step ??? tr s e →
     53  exec_inf_aux (clight_exec p) ge (exec_step ge s) = e.
     54#p #ge #x #tr #s #e
    5555>(exec_inf_aux_unfold …) cases x;
    5656[ #o #k #EXEC whd in EXEC:(??%?); destruct
    57 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
     57| #y cases y; #tr' #s' whd in ⊢ (??%? → ?); >(?:? (clight_exec p) s' = is_final s'); whd in match (? (clight_exec) s') in ⊢ %; whd in ⊢ (??%? → ?);
    5858    cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
    5959    @refl
  • src/Clight/CexecSound.ma

    r500 r700  
    1 include "Cexec.ma".
     1include "Clight/Cexec.ma".
    22
    33(*include "Plogic/connectives.ma".*)
  • src/Clight/CostLabel.ma

    r487 r700  
    1 include "AST.ma".
     1include "Clight/AST.ma".
    22
    33definition costlabel ≝ ident.
  • src/Clight/Csem.ma

    r648 r700  
    2323(*include "AST.ma".*)
    2424(*include "Mem.ma".*)
    25 include "Globalenvs.ma".
    26 include "Csyntax.ma".
    27 include "Maps.ma".
     25include "common/Globalenvs.ma".
     26include "Clight/Csyntax.ma".
     27include "common/Maps.ma".
    2828(*include "Events.ma".*)
    29 include "Smallstep.ma".
     29include "common/Smallstep.ma".
    3030
    3131(* * * Semantics of type-dependent operations *)
  • src/Clight/Csyntax.ma

    r498 r700  
    1717
    1818(*include "Integers.ma".*)
    19 include "AST.ma".
    20 include "Coqlib.ma".
    21 include "Errors.ma".
    22 include "CostLabel.ma".
     19include "Clight/AST.ma".
     20include "utilities/Coqlib.ma".
     21include "common/Errors.ma".
     22include "Clight/CostLabel.ma".
    2323
    2424(* * * Abstract syntax *)
  • src/common/Events.ma

    r695 r700  
    2121(*include "Integers.ma".*)
    2222(*include "Floats.ma".*)
    23 include "Values.ma".
     23include "common/Values.ma".
    2424include "basics/list.ma".
    25 include "extralib.ma".
    26 include "CostLabel.ma".
     25include "utilities/extralib.ma".
     26include "Clight/CostLabel.ma".
    2727
    2828(* * The observable behaviour of programs is stated in terms of
  • src/common/Floats.ma

    r695 r700  
    2121  and the associated operations.  *)
    2222
    23 include "Coqlib.ma".
    24 include "Integers.ma".
     23include "utilities/Coqlib.ma".
     24include "common/Integers.ma".
    2525
    2626axiom float: Type[0].
  • src/common/Globalenvs.ma

    r695 r700  
    3434  system. *)
    3535
    36 include "Errors.ma".
    37 include "AST.ma".
     36include "common/Errors.ma".
     37include "Clight/AST.ma".
    3838(*include "Values.ma".*)
    39 include "Mem.ma".
     39include "common/Mem.ma".
    4040
    4141(* FIXME: unimplemented stuff in AST.ma
  • src/common/IOMonad.ma

    r695 r700  
    1 include "extralib.ma".
    2 include "Errors.ma".
     1include "utilities/extralib.ma".
     2include "common/Errors.ma".
    33
    44(* IO monad *)
  • src/common/Integers.ma

    r697 r700  
    2020include "utilities/extralib.ma".
    2121
    22 include "cerco/BitVector.ma".
    23 include "cerco/BitVectorZ.ma".
    24 include "cerco/Arithmetic.ma".
     22include "ASM/BitVector.ma".
     23include "ASM/BitVectorZ.ma".
     24include "ASM/Arithmetic.ma".
    2525
    2626(* * * Comparisons *)
  • src/common/Maps.ma

    r695 r700  
    3333*)
    3434
    35 include "Coqlib.ma".
     35include "utilities/Coqlib.ma".
    3636(* XXX: For ident type; should maybe follow original and use positives *)
    37 include "AST.ma".
     37include "Clight/AST.ma".
    3838
    3939(*
  • src/common/Mem.ma

    r695 r700  
    3232
    3333(*include "Coqlib.ma".*)
    34 include "Values.ma".
     34include "common/Values.ma".
    3535(*include "AST.ma".*)
    36 include "extralib.ma".
     36include "utilities/extralib.ma".
    3737
    3838definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝
  • src/common/Smallstep.ma

    r695 r700  
    2727Require Import AST.
    2828*)
    29 include "Events.ma".
     29include "common/Events.ma".
    3030(*
    3131Require Import Globalenvs.
  • src/common/SmallstepExec.ma

    r695 r700  
    11
    2 include "extralib.ma".
    3 include "IOMonad.ma".
    4 include "Integers.ma".
    5 include "Events.ma".
    6 include "Mem.ma".
     2include "utilities/extralib.ma".
     3include "common/IOMonad.ma".
     4include "common/Integers.ma".
     5include "common/Events.ma".
     6include "common/Mem.ma".
    77
    88record execstep : Type[1] ≝
  • src/common/Values.ma

    r695 r700  
    1717  semantics of all our intermediate languages. *)
    1818
    19 include "Coqlib.ma".
    20 include "AST.ma".
    21 include "Integers.ma".
    22 include "Floats.ma".
    23 include "Errors.ma".
    24 
    25 include "cerco/Vector.ma".
     19include "utilities/Coqlib.ma".
     20include "Clight/AST.ma".
     21include "common/Integers.ma".
     22include "common/Floats.ma".
     23include "common/Errors.ma".
     24
     25include "ASM/Vector.ma".
    2626
    2727include "basics/logic.ma".
Note: See TracChangeset for help on using the changeset viewer.