Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

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

    r485 r487  
    1717  the abstract syntax trees of many of the intermediate languages. *)
    1818
    19 include "datatypes/sums.ma".
     19include "basics/types.ma".
    2020include "extralib.ma".
    2121include "Integers.ma".
     
    2828  etc) are represented by the type [positive] of positive integers. *)
    2929
    30 ndefinition ident ≝ Pos.
    31 
    32 ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
    33 #x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y);
    34 ##[ #H; @2; /2/; ##| #H; @1; //; ##| #H; @2; /2/ ##] nqed.
     30definition ident ≝ Pos.
     31
     32definition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
     33#x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
     34[ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
    3535
    3636(*
    3737(* XXX: we use nats for now, but if in future we use binary like compcert
    3838        then the maps will be easier to define. *)
    39 ndefinition ident ≝ nat.
    40 ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
    41 #x; nelim x;
    42 ##[ #y; ncases y; /3/;
    43 ##| #x'; #IH; #y; ncases y;
    44   ##[ @2; @; #H; ndestruct
    45   ##| #y'; nelim (IH y');
    46     ##[ #e; ndestruct; /2/
    47     ##| #ne; @2; /2/;
    48     ##]
    49   ##]
    50 ##] nqed.
     39definition ident ≝ nat.
     40definition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
     41#x elim x;
     42[ #y cases y; /3/;
     43| #x' #IH #y cases y;
     44  [ %{2} % #H destruct
     45  | #y' elim (IH y');
     46    [ #e destruct; /2/
     47    | #ne %{2} /2/;
     48    ]
     49  ]
     50] qed.
    5151*)
    5252(* * The intermediate languages are weakly typed, using only two types:
     
    5454  numbers. *)
    5555
    56 ninductive typ : Type
     56inductive typ : Type[0]
    5757  | ASTint : typ
    5858  | ASTfloat : typ.
    5959
    60 ndefinition typesize : typ → Z ≝ λty.
     60definition typesize : typ → Z ≝ λty.
    6161  match ty return λ_.Z with  [ ASTint ⇒ 4 | ASTfloat ⇒ 8 ].
    6262
    63 nlemma typesize_pos: ∀ty. typesize ty > 0.
    64 #ty; ncases ty; //; nqed.
    65 
    66 nlemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    67 #t1;#t2;ncases t1;ncases t2;/2/; @2; napply nmk; #H; ndestruct; nqed.
    68 
    69 nlemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
    70 #t1;#t2;ncases t1;ncases t2;/2/;
    71 ##[ ##1,2: #ty; @2; napply nmk; #H; ndestruct;
    72 ##| #ty1;#ty2; nelim (typ_eq ty1 ty2); /2/; #neq; @2; napply nmk;
    73     #H; ndestruct; /2/;
    74 ##] nqed.
     63lemma typesize_pos: ∀ty. typesize ty > 0.
     64#ty cases ty; //; qed.
     65
     66lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
     67#t1 #t2 cases t1;cases t2;/2/; %2 @nmk #H destruct; qed.
     68
     69lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     70#t1 #t2 cases t1;cases t2;/2/;
     71[ 1,2: #ty %2 @nmk #H destruct;
     72| #ty1 #ty2 elim (typ_eq ty1 ty2); /2/; #neq %2 @nmk
     73    #H destruct; /2/;
     74] qed.
    7575
    7676(* * Additionally, function definitions and function calls are annotated
     
    8080  for the function. *)
    8181
    82 nrecord signature : Type ≝ {
     82record signature : Type[0] ≝ {
    8383  sig_args: list typ;
    8484  sig_res: option typ
    8585}.
    8686
    87 ndefinition proj_sig_res : signature → typ ≝ λs.
     87definition proj_sig_res : signature → typ ≝ λs.
    8888  match sig_res s with
    8989  [ None ⇒ ASTint
     
    9393(* Memory spaces *)
    9494
    95 ninductive region : Type
     95inductive region : Type[0]
    9696  | Any : region
    9797  | Data : region
     
    101101  | Code : region.
    102102
    103 ndefinition eq_region : region → region → bool ≝
     103definition eq_region : region → region → bool ≝
    104104λr1,r2.
    105105  match r1 with
     
    112112  ].
    113113
    114 nlemma eq_region_elim : ∀P:bool → Type. ∀r1,r2.
     114lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
    115115  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
    116116  P (eq_region r1 r2).
    117 #P r1 r2; ncases r1; ncases r2; #Ptrue Pfalse;
    118 ntry ( napply Ptrue // );
    119 napply Pfalse; @; #E; ndestruct;
    120 nqed.
    121 
    122 ndefinition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
    123 #r1 r2; napply (eq_region_elim ? r1 r2); /2/; nqed.
     117#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
     118try ( @Ptrue // )
     119@Pfalse % #E destruct;
     120qed.
     121
     122definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
     123#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    124124
    125125(* * Memory accesses (load and store instructions) are annotated by
     
    127127  chunk of memory being accessed. *)
    128128
    129 ninductive memory_chunk : Type[0] ≝
     129inductive memory_chunk : Type[0] ≝
    130130  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
    131131  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
     
    139139(* * Initialization data for global variables. *)
    140140
    141 ninductive init_data: Type[0] ≝
     141inductive init_data: Type[0] ≝
    142142  | Init_int8: int → init_data
    143143  | Init_int16: int → init_data
     
    160160programs are common to all languages. *)
    161161
    162 nrecord program (F,V: Type) : Type := {
     162record program (F,V: Type[0]) : Type[0] := {
    163163  prog_funct: list (ident × F);
    164164  prog_main: ident;
     
    166166}.
    167167
    168 ndefinition prog_funct_names ≝ λF,V: Type. λp: program F V.
     168definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    169169  map ?? (fst ident F) (prog_funct ?? p).
    170170
    171 ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
     171definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    172172  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
    173173(*
     
    184184*)
    185185
    186 ndefinition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
     186definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
    187187λA,B,transf,l.
    188188  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
    189189
    190 ndefinition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
     190definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
    191191λA,B,V,transf,p.
    192192  mk_program B V
     
    194194    (prog_main A V p)
    195195    (prog_vars A V p).
    196 
    197 nlemma transform_program_function:
     196(*
     197lemma transform_program_function:
    198198  ∀A,B,V,transf,p,i,tf.
    199199  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
    200200  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
    201 nnormalize; #A B V transf p i tf H; nelim (list_in_map_inv ????? H);
    202 #x; nelim x; #i' tf'; *; #e H; ndestruct; @tf'; /2/;
    203 nqed.
    204 
     201normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
     202#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
     203qed.
     204*)
    205205(*
    206206End TRANSF_PROGRAM.
     
    432432  a type for such functions and some generic transformation functions. *)
    433433
    434 nrecord external_function : Type ≝ {
     434record external_function : Type[0] ≝ {
    435435  ef_id: ident;
    436436  ef_sig: signature
    437437}.
    438438(*
    439 ninductive fundef (F: Type): Type ≝
     439inductive fundef (F: Type): Type ≝
    440440  | Internal: F → fundef F
    441441  | External: external_function → fundef F.
     
    448448Variable transf: A -> B.
    449449*)
    450 ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
     450definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
    451451λA,B,transf,fd.
    452452  match fd with
Note: See TracChangeset for help on using the changeset viewer.