Changeset 1056 for src/Clight/label.ma


Ignore:
Timestamp:
Jul 5, 2011, 4:25:41 PM (9 years ago)
Author:
campbell
Message:

Switch to delayed identifier error scheme.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/label.ma

    r961 r1056  
    11include "Clight/Csyntax.ma".
    22
    3 definition add_cost_before : statement → universe CostTag → res (statement × (universe CostTag)) ≝
     3definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
    44λs,gen.
    5   do 〈l,gen〉 ← fresh … gen;
    6   OK ? 〈Scost l s, gen〉.
     5  let 〈l,gen〉 ≝ fresh … gen in
     6  〈Scost l s, gen〉.
    77
    8 definition add_cost_after : statement → universe CostTag → res (statement × (universe CostTag)) ≝
     8definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝
    99λs,gen.
    10   do 〈l,gen〉 ← fresh … gen;
    11   OK ? 〈Ssequence s (Scost l Sskip), gen〉.
     10  let 〈l,gen〉 ≝ fresh … gen in
     11  〈Ssequence s (Scost l Sskip), gen〉.
    1212
    13 definition add_cost_expr : expr → universe CostTag → res (expr × (universe CostTag)) ≝
     13definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝
    1414λe,gen.
    15   do 〈l,gen〉 ← fresh … gen;
    16   OK ? 〈Expr (Ecost l e) (typeof e), gen〉.
     15  let 〈l,gen〉 ≝ fresh … gen in
     16  〈Expr (Ecost l e) (typeof e), gen〉.
    1717
    1818let rec label_expr (e:expr) (costgen:universe CostTag)
    19         on e : res (expr × (universe CostTag)) ≝
     19        on e : expr × (universe CostTag) ≝
    2020match e with
    21 [ Expr ed ty ⇒ do 〈ed,costgen〉 ← label_expr_descr ed costgen;
    22                OK ? 〈Expr ed ty, costgen〉
     21[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen in
     22               〈Expr ed ty, costgen〉
    2323]
    2424and label_expr_descr (e:expr_descr) (costgen:universe CostTag)
    25     on e : res (expr_descr × (universe CostTag)) ≝
     25    on e : expr_descr × (universe CostTag) ≝
    2626match e with
    2727[ Ederef e' ⇒
    28     do 〈e',costgen〉 ← label_expr e' costgen;
    29     OK ? 〈Ederef e', costgen〉
     28    let 〈e',costgen〉 ≝ label_expr e' costgen in
     29    〈Ederef e', costgen〉
    3030| Eaddrof e' ⇒
    31     do 〈e',costgen〉 ← label_expr e' costgen;
    32     OK ? 〈Eaddrof e', costgen〉
     31    let 〈e',costgen〉 ≝ label_expr e' costgen in
     32    〈Eaddrof e', costgen〉
    3333| Eunop op e' ⇒
    34     do 〈e',costgen〉 ← label_expr e' costgen;
    35     OK ? 〈Eunop op e', costgen〉
     34    let 〈e',costgen〉 ≝ label_expr e' costgen in
     35    〈Eunop op e', costgen〉
    3636| Ebinop op e1 e2 ⇒
    37     do 〈e1,costgen〉 ← label_expr e1 costgen;
    38     do 〈e2,costgen〉 ← label_expr e2 costgen;
    39     OK ? 〈Ebinop op e1 e2, costgen〉
     37    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     38    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     39    〈Ebinop op e1 e2, costgen〉
    4040| Ecast ty e' ⇒
    41     do 〈e',costgen〉 ← label_expr e' costgen;
    42     OK ? 〈Ecast ty e', costgen〉
     41    let 〈e',costgen〉 ≝ label_expr e' costgen in
     42    〈Ecast ty e', costgen〉
    4343| Econdition e' e1 e2 ⇒
    44     do 〈e',costgen〉 ← label_expr e' costgen;
    45     do 〈e1,costgen〉 ← label_expr e1 costgen;
    46     do 〈e1,costgen〉 ← add_cost_expr e1 costgen;
    47     do 〈e2,costgen〉 ← label_expr e2 costgen;
    48     do 〈e2,costgen〉 ← add_cost_expr e2 costgen;
    49     OK ? 〈Econdition e' e1 e2, costgen〉
     44    let 〈e',costgen〉 ≝ label_expr e' costgen in
     45    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     46    let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in
     47    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     48    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
     49    〈Econdition e' e1 e2, costgen〉
    5050(* andbool and orbool are changed to conditionals to capture their
    5151   short-circuiting cost difference *)
    5252| Eandbool e1 e2 ⇒
    53     do 〈e1,costgen〉 ← label_expr e1 costgen;
    54     do 〈e2,costgen〉 ← label_expr e2 costgen;
    55     do 〈e2,costgen〉 ← add_cost_expr e2 costgen;
    56     do 〈ef,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen;
    57     OK ? 〈Econdition e1 e2 ef, costgen〉
     53    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     54    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     55    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
     56    let 〈ef,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen in
     57    〈Econdition e1 e2 ef, costgen〉
    5858| Eorbool e1 e2 ⇒
    59     do 〈e1,costgen〉 ← label_expr e1 costgen;
    60     do 〈et,costgen〉 ← add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen;
    61     do 〈e2,costgen〉 ← label_expr e2 costgen;
    62     do 〈e2,costgen〉 ← add_cost_expr e2 costgen;
    63     OK ? 〈Econdition e1 et e2, costgen〉
     59    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     60    let 〈et,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen in
     61    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     62    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
     63    〈Econdition e1 et e2, costgen〉
    6464
    6565| Efield e' id ⇒
    66     do 〈e',costgen〉 ← label_expr e' costgen;
    67     OK ? 〈Efield e' id, costgen〉
     66    let 〈e',costgen〉 ≝ label_expr e' costgen in
     67    〈Efield e' id, costgen〉
    6868(* The prototype asserts on preexisting cost labels, but I'd quite like to
    6969   keep them. *)
    7070| Ecost l e' ⇒
    71     do 〈e',costgen〉 ← label_expr e' costgen;
    72     OK ? 〈Ecost l e', costgen〉
     71    let 〈e',costgen〉 ≝ label_expr e' costgen in
     72    〈Ecost l e', costgen〉
    7373
    7474(* The remaining expressions don't have subexpressions. *)
    75 | _ ⇒ OK ? 〈e,costgen〉
     75| _ ⇒ 〈e,costgen〉
    7676].
    7777
    7878let rec label_exprs (l:list expr) (costgen:universe CostTag)
    79         on l : res (list expr × (universe CostTag)) ≝
     79        on l : list expr × (universe CostTag) ≝
    8080match l with
    81 [ nil ⇒ OK ? 〈nil ?,costgen〉
     81[ nil ⇒ 〈nil ?,costgen〉
    8282| cons e es ⇒
    83     do 〈e,costgen〉 ← label_expr e costgen;
    84     do 〈es,costgen〉 ← label_exprs es costgen;
    85     OK ? 〈e::es,costgen〉
     83    let 〈e,costgen〉 ≝ label_expr e costgen in
     84    let 〈es,costgen〉 ≝ label_exprs es costgen in
     85    〈e::es,costgen〉
    8686].
    8787
    8888definition label_opt_expr ≝
    8989λoe,costgen. match oe with
    90 [ None ⇒ OK ? 〈None ?, costgen〉
    91 | Some e ⇒ do 〈e,costgen〉 ← label_expr e costgen; OK ? 〈Some ? e,costgen〉
     90[ None ⇒ 〈None ?, costgen〉
     91| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
    9292].
    9393
    9494
    9595let rec label_statement (s:statement) (costgen:universe CostTag)
    96         on s : res (statement × (universe CostTag)) ≝
     96        on s : statement × (universe CostTag) ≝
    9797match s with
    98 [ Sskip ⇒ OK ? 〈Sskip,costgen〉
     98[ Sskip ⇒ 〈Sskip,costgen〉
    9999| Sassign e1 e2 ⇒
    100     do 〈e1,costgen〉 ← label_expr e1 costgen;
    101     do 〈e2,costgen〉 ← label_expr e2 costgen;
    102     OK ? 〈Sassign e1 e2, costgen〉
     100    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     101    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     102    〈Sassign e1 e2, costgen〉
    103103| Scall e_ret e_fn e_args ⇒
    104     do 〈e_ret,costgen〉 ← label_opt_expr e_ret costgen;
    105     do 〈e_fn,costgen〉 ← label_expr e_fn costgen;
    106     do 〈e_args,costgen〉 ← label_exprs e_args costgen;
    107     OK ? 〈Scall e_ret e_fn e_args, costgen〉
     104    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
     105    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
     106    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
     107    〈Scall e_ret e_fn e_args, costgen〉
    108108| Ssequence s1 s2 ⇒
    109     do 〈s1,costgen〉 ← label_statement s1 costgen;
    110     do 〈s2,costgen〉 ← label_statement s2 costgen;
    111     OK ? 〈Ssequence s1 s2, costgen〉
     109    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
     110    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
     111    〈Ssequence s1 s2, costgen〉
    112112| Sifthenelse e s1 s2 ⇒
    113     do 〈e,costgen〉 ← label_expr e costgen;
    114     do 〈s1,costgen〉 ← label_statement s1 costgen;
    115     do 〈s1,costgen〉 ← add_cost_before s1 costgen;
    116     do 〈s2,costgen〉 ← label_statement s2 costgen;
    117     do 〈s2,costgen〉 ← add_cost_before s2 costgen;
    118     OK ? 〈Sifthenelse e s1 s2, costgen〉
     113    let 〈e,costgen〉 ≝ label_expr e costgen in
     114    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
     115    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
     116    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
     117    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
     118    〈Sifthenelse e s1 s2, costgen〉
    119119| Swhile e s' ⇒
    120     do 〈e,costgen〉 ← label_expr e costgen;
    121     do 〈s',costgen〉 ← label_statement s' costgen;
    122     do 〈s',costgen〉 ← add_cost_before s' costgen;
    123     do 〈s,costgen〉 ← add_cost_after (Swhile e s') costgen;
    124     OK ? 〈s,costgen〉
     120    let 〈e,costgen〉 ≝ label_expr e costgen in
     121    let 〈s',costgen〉 ≝ label_statement s' costgen in
     122    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
     123    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
     124    〈s,costgen〉
    125125| Sdowhile e s' ⇒
    126     do 〈e,costgen〉 ← label_expr e costgen;
    127     do 〈s',costgen〉 ← label_statement s' costgen;
    128     do 〈s',costgen〉 ← add_cost_before s' costgen;
    129     do 〈s,costgen〉 ← add_cost_after (Sdowhile e s') costgen;
    130     OK ? 〈s,costgen〉
     126    let 〈e,costgen〉 ≝ label_expr e costgen in
     127    let 〈s',costgen〉 ≝ label_statement s' costgen in
     128    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
     129    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
     130    〈s,costgen〉
    131131| Sfor s1 e s2 s3 ⇒
    132     do 〈e,costgen〉 ← label_expr e costgen;
    133     do 〈s1,costgen〉 ← label_statement s1 costgen;
    134     do 〈s2,costgen〉 ← label_statement s2 costgen;
    135     do 〈s3,costgen〉 ← label_statement s3 costgen;
    136     do 〈s3,costgen〉 ← add_cost_before s3 costgen;
    137     do 〈s,costgen〉 ← add_cost_after (Sfor s1 e s2 s3) costgen;
    138     OK ? 〈s,costgen〉
    139 | Sbreak ⇒ OK ? 〈Sbreak,costgen〉
    140 | Scontinue ⇒ OK ? 〈Scontinue,costgen〉
     132    let 〈e,costgen〉 ≝ label_expr e costgen in
     133    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
     134    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
     135    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
     136    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
     137    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
     138    〈s,costgen〉
     139| Sbreak ⇒ 〈Sbreak,costgen〉
     140| Scontinue ⇒ 〈Scontinue,costgen〉
    141141| Sreturn opt_e ⇒
    142     do 〈opt_e,costgen〉 ← label_opt_expr opt_e costgen;
    143     OK ? 〈Sreturn opt_e,costgen〉
     142    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
     143    〈Sreturn opt_e,costgen〉
    144144| Sswitch e ls ⇒
    145     do 〈e,costgen〉 ← label_expr e costgen;
    146     do 〈ls,costgen〉 ← label_lstatements ls costgen;
    147     OK ? 〈Sswitch e ls, costgen〉
     145    let 〈e,costgen〉 ≝ label_expr e costgen in
     146    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
     147    〈Sswitch e ls, costgen〉
    148148| Slabel l s' ⇒
    149     do 〈s',costgen〉 ← label_statement s' costgen;
    150     do 〈s',costgen〉 ← add_cost_before s' costgen;
    151     OK ? 〈Slabel l s', costgen〉
    152 | Sgoto l ⇒ OK ? 〈Sgoto l, costgen〉
     149    let 〈s',costgen〉 ≝ label_statement s' costgen in
     150    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
     151    〈Slabel l s', costgen〉
     152| Sgoto l ⇒ 〈Sgoto l, costgen〉
    153153
    154154(* The prototype asserts on preexisting cost labels, but I'd quite like to
    155155   keep them. *)
    156156| Scost l s' ⇒
    157     do 〈s',costgen〉 ← label_statement s' costgen;
    158     OK ? 〈Scost l s', costgen〉
     157    let 〈s',costgen〉 ≝ label_statement s' costgen in
     158    〈Scost l s', costgen〉
    159159]
    160160and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
    161         on ls : res (labeled_statements × (universe CostTag)) ≝
     161        on ls : labeled_statements × (universe CostTag) ≝
    162162match ls with
    163163[ LSdefault s ⇒
    164     do 〈s,costgen〉 ← label_statement s costgen;
    165     do 〈s,costgen〉 ← add_cost_before s costgen;
    166     OK ? 〈LSdefault s, costgen〉
     164    let 〈s,costgen〉 ≝ label_statement s costgen in
     165    let 〈s,costgen〉 ≝ add_cost_before s costgen in
     166    〈LSdefault s, costgen〉
    167167| LScase sz i s ls' ⇒
    168     do 〈s,costgen〉 ← label_statement s costgen;
    169     do 〈s,costgen〉 ← add_cost_before s costgen;
    170     do 〈ls',costgen〉 ← label_lstatements ls' costgen;
    171     OK ? 〈LScase sz i s ls', costgen〉
     168    let 〈s,costgen〉 ≝ label_statement s costgen in
     169    let 〈s,costgen〉 ≝ add_cost_before s costgen in
     170    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
     171    〈LScase sz i s ls', costgen〉
    172172].
    173173
    … …  
    175175λf.
    176176  let costgen ≝ new_universe CostTag in
    177   do 〈body,costgen〉 ← label_statement (fn_body f) costgen;
    178   do 〈body,costgen〉 ← add_cost_before body costgen;
     177  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
     178  let 〈body,costgen〉 ≝ add_cost_before body costgen in
     179  do u ← check_universe_ok ? costgen;
    179180  OK ? (mk_function (fn_return f) (fn_params f) (fn_vars f) body).
    180181
Note: See TracChangeset for help on using the changeset viewer.