Changeset 700 for src/Clight


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/Clight
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • 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 *)
Note: See TracChangeset for help on using the changeset viewer.