Changeset 175 for Csemantics/Csyntax.ma
 Timestamp:
 Oct 13, 2010, 12:19:22 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Csyntax.ma
r156 r175 20 20 include "Coqlib.ma". 21 21 include "Errors.ma". 22 include "CostLabel.ma". 22 23 23 24 (* * * Abstract syntax *) … … 189 190  Eorbool: expr → expr → expr_descr (**r sequential or ([]) *) 190 191  Esizeof: type → expr_descr (**r size of a type *) 191  Efield: expr → ident → expr_descr. (**r access to a member of a struct or union *) 192  Efield: expr → ident → expr_descr (**r access to a member of a struct or union *) 193  Ecost: costlabel → expr → expr_descr. 192 194 193 195 (* * Extract the type part of a typeannotated Clight expression. *) … … 220 222  Slabel : label → statement → statement 221 223  Sgoto : label → statement 224  Scost : costlabel → statement → statement 222 225 223 226 with labeled_statements : Type ≝ (**r cases of a [switch] *) … … 241 244 (Sla:∀l,s. P s → P (Slabel l s)) 242 245 (Sgo:∀l. P (Sgoto l)) 246 (Scs:∀l,s. P s → P (Scost l s)) 243 247 (LSd:∀s. P s → Q (LSdefault s)) 244 248 (LSc:∀i,s,t. P s → Q t → Q (LScase i s t)) … … 249 253  Scall eo e args ⇒ Sca eo e args 250 254  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)255 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 256 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 253 257  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)258 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 259 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 256 260  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)261 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 258 262  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)263 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 260 264  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)265 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1) 266 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2) 267 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3) 264 268  Sbreak ⇒ Sbr 265 269  Scontinue ⇒ Sco 266 270  Sreturn eo ⇒ Sre eo 267 271  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)272 (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls) 269 273  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)274 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 271 275  Sgoto l ⇒ Sgo l 276  Scost l s ⇒ Scs l s 277 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 272 278 ] 273 279 and labeled_statements_ind2 … … 287 293 (Sla:∀l,s. P s → P (Slabel l s)) 288 294 (Sgo:∀l. P (Sgoto l)) 295 (Scs:∀l,s. P s → P (Scost l s)) 289 296 (LSd:∀s. P s → Q (LSdefault s)) 290 297 (LSc:∀i,s,t. P s → Q t → Q (LScase i s t)) … … 292 299 match ls with 293 300 [ 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)301 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 295 302  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)303 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s) 304 (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t) 298 305 ]. 299 306 300 ndefinition 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 307 ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs. 308 statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs 302 309 (λ_,_. I) (λ_,_,_,_,_.I). 303 310
Note: See TracChangeset
for help on using the changeset viewer.