Changeset 478


Ignore:
Timestamp:
Jan 25, 2011, 5:30:36 PM (6 years ago)
Author:
campbell
Message:

Prevent clashes between names in AST and other parts of the development.
(Noticed when trying a large example file.)

Location:
Deliverables/D3.1/C-semantics
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/AST.ma

    r467 r478  
    5555
    5656ninductive typ : Type ≝
    57   | Tint : typ
    58   | Tfloat : typ.
     57  | ASTint : typ
     58  | ASTfloat : typ.
    5959
    6060ndefinition typesize : typ → Z ≝ λty.
    61   match ty return λ_.Z with  [ Tint ⇒ 4 | Tfloat ⇒ 8 ].
     61  match ty return λ_.Z with  [ ASTint ⇒ 4 | ASTfloat ⇒ 8 ].
    6262
    6363nlemma typesize_pos: ∀ty. typesize ty > 0.
     
    8787ndefinition proj_sig_res : signature → typ ≝ λs.
    8888  match sig_res s with
    89   [ None ⇒ Tint
     89  [ None ⇒ ASTint
    9090  | Some t ⇒ t
    9191  ].
     
    415415  ef_sig: signature
    416416}.
    417 
     417(*
    418418ninductive fundef (F: Type): Type ≝
    419419  | Internal: F → fundef F
     
    433433  | External ef ⇒ External ? ef
    434434  ].
    435 
     435*)
    436436(*
    437437End TRANSF_FUNDEF.
  • Deliverables/D3.1/C-semantics/Animation.ma

    r409 r478  
    99λo,ev.
    1010match io_in_typ o return λt. res (eventval_type t) with
    11 [ Tint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
    12 | Tfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
     11[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
     12| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
    1313].
    1414
     
    3030].
    3131
    32 ndefinition exec_up_to : program → nat → list eventval → res (trace × state) ≝
     32ndefinition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝
    3333λp,n,i. up_to_nth_step n i (exec_inf p) E0.
    3434
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r457 r478  
    471471
    472472ndefinition eventval_type : ∀ty:typ. Type ≝
    473 λty. match ty with [ Tint ⇒ int | Tfloat ⇒ float ].
     473λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
    474474
    475475ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    476 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ Tint ⇒ λv.EVint v | Tfloat ⇒ λv.EVfloat v ].
     476λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
    477477
    478478ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝
    479 λty:typ. match ty return λty'.eventval_type ty' → val with [ Tint ⇒ λv.Vint v | Tfloat ⇒ λv.Vfloat v ].
     479λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
    480480
    481481nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
     
    486486λev,ty.
    487487match ty with
    488 [ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
    489 | Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
     488[ ASTint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
     489| ASTfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
    490490| _ ⇒ Some ? (Error ?)
    491491]. nwhd; //; nqed.
     
    494494λv,ty.
    495495match ty with
    496 [ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
    497 | Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
     496[ ASTint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
     497| ASTfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
    498498| _ ⇒ Some ? (Error ?)
    499499]. nwhd; //; nqed.
     
    694694].
    695695
    696 nlet rec make_initial_state (p:program) : res state ≝
     696nlet rec make_initial_state (p:clight_program) : res state ≝
    697697  let ge ≝ globalenv Genv ?? p in
    698698  let m0 ≝ init_mem Genv ?? p in
     
    769769
    770770
    771 ndefinition exec_inf : program → execution ≝
     771ndefinition exec_inf : clight_program → execution ≝
    772772λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
    773773
  • Deliverables/D3.1/C-semantics/Csem.ma

    r474 r478  
    14811481  without arguments and with an empty continuation. *)
    14821482
    1483 ninductive initial_state (p: program): state -> Prop :=
     1483ninductive initial_state (p: clight_program): state -> Prop :=
    14841484  | initial_state_intro: ∀b,f.
    14851485      let ge := globalenv Genv ?? p in
     
    15001500  behavior. *)
    15011501
    1502 ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
     1502ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    15031503  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
    15041504(*
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r474 r478  
    339339  data.  See module [AST] for more details. *)
    340340
    341 ndefinition program : Type ≝ program fundef type.
     341ndefinition clight_program : Type ≝ program fundef type.
    342342
    343343(* * * Operations over types *)
     
    890890(* * Translating Clight types to Cminor types, function signatures,
    891891  and external functions. *)
    892 (* XXX: is this the best way to access these? *)
    893 alias id "ASTint" = "cic:/matita/c-semantics/AST/typ.con(0,1,0)".
    894 alias id "ASTfloat" = "cic:/matita/c-semantics/AST/typ.con(0,2,0)".
    895892
    896893ndefinition typ_of_type : type → typ ≝ λt.
  • Deliverables/D3.1/C-semantics/Events.ma

    r474 r478  
    189189ninductive eventval_match: eventval -> typ -> val -> Prop :=
    190190  | ev_match_int:
    191       ∀i. eventval_match (EVint i) Tint (Vint i)
     191      ∀i. eventval_match (EVint i) ASTint (Vint i)
    192192  | ev_match_float:
    193       ∀f. eventval_match (EVfloat f) Tfloat (Vfloat f).
     193      ∀f. eventval_match (EVfloat f) ASTfloat (Vfloat f).
    194194
    195195ninductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
  • Deliverables/D3.1/C-semantics/Values.ma

    r456 r478  
    6464  match v with
    6565  [ Vundef ⇒ True
    66   | Vint _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
    67   | Vfloat _ ⇒ match t with [ Tfloat ⇒ True | _ ⇒ False ]
    68   | Vptr _ _ _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
     66  | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
     67  | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
     68  | Vptr _ _ _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
    6969  | _ ⇒ False
    7070  ].
Note: See TracChangeset for help on using the changeset viewer.