Changeset 24 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Aug 27, 2010, 1:21:50 PM (10 years ago)
Author:
campbell
Message:

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r4 r24  
    224224  | LSdefault: statement → labeled_statements
    225225  | LScase: int → statement → labeled_statements → labeled_statements.
     226
     227nlet rec statement_ind2
     228  (P:statement → Prop) (Q:labeled_statements → Prop)
     229  (Ssk:P Sskip)
     230  (Sas:∀e1,e2. P (Sassign e1 e2))
     231  (Sca:∀eo,e,args. P (Scall eo e args))
     232  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
     233  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
     234  (Swh:∀e,s. P s → P (Swhile e s))
     235  (Sdo:∀e,s. P s → P (Sdowhile e s))
     236  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     237  (Sbr:P Sbreak)
     238  (Sco:P Scontinue)
     239  (Sre:∀eo. P (Sreturn eo))
     240  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
     241  (Sla:∀l,s. P s → P (Slabel l s))
     242  (Sgo:∀l. P (Sgoto l))
     243  (LSd:∀s. P s → Q (LSdefault s))
     244  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     245  (s:statement) on s : P s ≝
     246match s with
     247[ Sskip ⇒ Ssk
     248| Sassign e1 e2 ⇒ Sas e1 e2
     249| Scall eo e args ⇒ Sca eo e args
     250| Ssequence s1 s2 ⇒ Ssq s1 s2
     251    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
     252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     253| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
     254    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
     255    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     256| Swhile e s ⇒ Swh e s
     257    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     258| Sdowhile e s ⇒ Sdo e s
     259    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     260| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
     261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
     262    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     263    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s3)
     264| Sbreak ⇒ Sbr
     265| Scontinue ⇒ Sco
     266| Sreturn eo ⇒ Sre eo
     267| Sswitch e ls ⇒ Ssw e ls
     268    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc ls)
     269| Slabel l s ⇒ Sla l s
     270    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     271| Sgoto l ⇒ Sgo l
     272]
     273and labeled_statements_ind2
     274  (P:statement → Prop) (Q:labeled_statements → Prop)
     275  (Ssk:P Sskip)
     276  (Sas:∀e1,e2. P (Sassign e1 e2))
     277  (Sca:∀eo,e,args. P (Scall eo e args))
     278  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
     279  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
     280  (Swh:∀e,s. P s → P (Swhile e s))
     281  (Sdo:∀e,s. P s → P (Sdowhile e s))
     282  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     283  (Sbr:P Sbreak)
     284  (Sco:P Scontinue)
     285  (Sre:∀eo. P (Sreturn eo))
     286  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
     287  (Sla:∀l,s. P s → P (Slabel l s))
     288  (Sgo:∀l. P (Sgoto l))
     289  (LSd:∀s. P s → Q (LSdefault s))
     290  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     291  (ls:labeled_statements) on ls : Q ls ≝
     292match ls with
     293[ LSdefault s ⇒ LSd s
     294    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     295| LScase i s t ⇒ LSc i s t
     296    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     297    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc t)
     298].
     299
     300ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo.
     301  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo
     302  (λ_,_. I) (λ_,_,_,_,_.I).
    226303
    227304(* * ** Functions *)
Note: See TracChangeset for help on using the changeset viewer.