Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/ClassifyOp.ma

    r1872 r2176  
    1414*)
    1515
    16 definition ptr_type ≝ λr,ty,n. match n with [ None ⇒ Tpointer r ty | Some n' ⇒ Tarray r ty n' ].
     16definition ptr_type ≝ λty,n. match n with [ None ⇒ Tpointer  ty | Some n' ⇒ Tarray ty n' ].
    1717
    1818inductive classify_add_cases : type → type → Type[0] ≝
    1919  (* integer addition is always done on a single type, the parser will insert any
    2020     necessary casts *)
    21   | add_case_ii: ∀sz,sg.          classify_add_cases (Tint sz sg)      (Tint sz sg)      (*Tint sz sg*)
    22   | add_case_ff: ∀sz.             classify_add_cases (Tfloat sz)       (Tfloat sz)       (*Tfloat sz*)
    23   | add_case_pi: ∀n,r,ty,sz,sg.   classify_add_cases (ptr_type r ty n) (Tint sz sg)      (*ptr_type r ty n*)
    24   | add_case_ip: ∀n,sz,sg,r,ty.   classify_add_cases (Tint sz sg)      (ptr_type r ty n) (*ptr_type r ty n*)
    25   | add_default: ∀ty1,ty2.        classify_add_cases ty1 ty2 (*ty'*).
     21  | add_case_ii: ∀sz,sg.      classify_add_cases (Tint sz sg)     (Tint sz sg)     (*Tint sz sg*)
     22  | add_case_ff: ∀sz.         classify_add_cases (Tfloat sz)      (Tfloat sz)      (*Tfloat sz*)
     23  | add_case_pi: ∀n,ty,sz,sg. classify_add_cases (ptr_type  ty n) (Tint sz sg)     (*ptr_type r ty n*)
     24  | add_case_ip: ∀n,sz,sg,ty. classify_add_cases (Tint sz sg)     (ptr_type ty n) (*ptr_type r ty n*)
     25  | add_default: ∀ty1,ty2.    classify_add_cases ty1 ty2 (*ty'*).
    2626
    2727definition classify_add : ∀ty1,ty2. classify_add_cases ty1 ty2 ≝ λty1: type. λty2: type.
     
    3030    match ty2 return λty2. classify_add_cases ? ty2 with
    3131    [ Tint sz2 sg2 ⇒ inttyp_eq_elim' sz1 sz2 sg1 sg2 (λsz1,sg1,sz2,sg2. classify_add_cases (Tint sz1 sg1) (Tint sz2 sg2)) (add_case_ii sz1 ?) (add_default ??)
    32     | Tpointer _ ty ⇒ add_case_ip (None ?) …
    33     | Tarray _ ty n ⇒ add_case_ip (Some ? n) …
     32    | Tpointer ty ⇒ add_case_ip (None ?) …
     33    | Tarray ty n ⇒ add_case_ip (Some ? n) …
    3434    | _ ⇒ add_default … ]
    3535  | Tfloat sz1 ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [ Tfloat sz2 ⇒ floatsize_eq_elim sz1 sz2 (λsz1,sz2. classify_add_cases (Tfloat sz1) (Tfloat sz2)) (add_case_ff sz1) (add_default …) | _ ⇒ add_default … ]
    36   | Tpointer _ ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
    37   | Tarray _ ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
     36  | Tpointer ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
     37  | Tarray ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
    3838  | _ ⇒ add_default …
    3939  ].
    4040
    4141inductive classify_sub_cases : type → type → Type[0] ≝
    42   | sub_case_ii: ∀sz,sg.        classify_sub_cases (Tint sz sg)      (Tint sz sg)
    43   | sub_case_ff: ∀sz.           classify_sub_cases (Tfloat sz)       (Tfloat sz)
    44   | sub_case_pi: ∀n,r,ty,sz,sg. classify_sub_cases (ptr_type r ty n) (Tint sz sg)
    45   | sub_case_pp: ∀n1,n2,r1,ty1,r2,ty2. classify_sub_cases (ptr_type r1 ty1 n1) (ptr_type r2 ty2 n2)
     42  | sub_case_ii: ∀sz,sg.         classify_sub_cases (Tint sz sg)       (Tint sz sg)
     43  | sub_case_ff: ∀sz.            classify_sub_cases (Tfloat sz)        (Tfloat sz)
     44  | sub_case_pi: ∀n,ty,sz,sg.    classify_sub_cases (ptr_type  ty n)  (Tint sz sg)
     45  | sub_case_pp: ∀n1,n2,ty1,ty2. classify_sub_cases (ptr_type  ty1 n1) (ptr_type ty2 n2)
    4646  | sub_default: ∀ty1,ty2. classify_sub_cases ty1 ty2.
    4747
     
    5050  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_sub_cases ty1 ty2) (sub_case_ii sz1 sg1) (sub_default …)
    5151  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_sub_cases ty1 ty2) (sub_case_ff sz1) (sub_default …)
    52   | Tpointer _ ty ⇒
     52  | Tpointer ty ⇒
    5353    match ty2 return λty2. classify_sub_cases ? ty2 with
    5454    [ Tint sz sg ⇒ sub_case_pi …
    55     | Tpointer _ _ ⇒ sub_case_pp (None ?) (None ?) …
    56     | Tarray _ _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
     55    | Tpointer _ ⇒ sub_case_pp (None ?) (None ?) …
     56    | Tarray _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
    5757    | _ ⇒ sub_default …]
    58   | Tarray _ ty n1 ⇒
     58  | Tarray ty n1 ⇒
    5959    match ty2 return λty2. classify_sub_cases ? ty2 with
    6060    [ Tint _ _ ⇒ sub_case_pi …
    61     | Tpointer _ _ ⇒ sub_case_pp (Some ? n1) (None ?) …
    62     | Tarray _ _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
     61    | Tpointer _ ⇒ sub_case_pp (Some ? n1) (None ?) …
     62    | Tarray _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
    6363    | _ ⇒ sub_default … ]
    6464  | _ ⇒ sub_default …
     
    8484inductive classify_cmp_cases : type → type → Type[0] ≝
    8585  | cmp_case_ii: ∀sz,sg.  classify_cmp_cases (Tint sz sg)      (Tint sz sg)
    86   | cmp_case_pp: ∀n,r,ty. classify_cmp_cases (ptr_type r ty n) (ptr_type r ty n)
     86  | cmp_case_pp: ∀n,ty.   classify_cmp_cases (ptr_type  ty n)  (ptr_type ty n)
    8787  | cmp_case_ff: ∀sz.     classify_cmp_cases (Tfloat sz)       (Tfloat sz)
    8888  | cmp_default: ∀ty,ty'. classify_cmp_cases ty ty'.
     
    9292  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) (cmp_case_ii sz1 sg1) (cmp_default …)
    9393  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_ff sz1) (cmp_default …)
    94   | Tpointer r1 ty1' ⇒ if_type_eq (Tpointer r1 ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
    95   | Tarray r1 ty1' n1 ⇒ if_type_eq (Tarray r1 ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
     94  | Tpointer  ty1' ⇒ if_type_eq (Tpointer ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
     95  | Tarray  ty1' n1 ⇒ if_type_eq (Tarray ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
    9696  | _ ⇒ cmp_default …
    9797  ].
     
    104104  match ty with
    105105  [ Tfunction args res ⇒ fun_case_f args res
    106   | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
    107                                     | _ ⇒ fun_default
    108                                     ]
     106  | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
     107                                  | _ ⇒ fun_default
     108                                  ]
    109109  | _ ⇒ fun_default
    110110  ].
Note: See TracChangeset for help on using the changeset viewer.