Changeset 1056


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

Switch to delayed identifier error scheme.

Location:
src
Files:
5 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
  • src/Cminor/toRTLabs.ma

    r961 r1056  
    66definition env ≝ identifier_map SymbolTag register.
    77definition label_env ≝ identifier_map SymbolTag label.
    8 definition populate_env : env → universe RegisterTag → list (ident × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝
     8definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
    99λen,gen. foldr ??
    1010 (λidt,rsengen.
    1111   let 〈id,ty〉 ≝ idt in
    12    do 〈rs,en,gen〉 ← rsengen;
    13    do 〈r,gen'〉 ← fresh … gen;
    14    OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
    15 
    16 definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
     12   let 〈rs,en,gen〉 ≝ rsengen in
     13   let 〈r,gen'〉 ≝ fresh … gen in
     14     〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
     15
     16definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝
    1717λen,gen. foldr ??
    1818 (λid,engen.
    19    do 〈en,gen〉 ← engen;
    20    do 〈r,gen'〉 ← fresh … gen;
    21    OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).
     19   let 〈en,gen〉 ≝ engen in
     20   let 〈r,gen'〉 ≝ fresh … gen in
     21     〈add ?? en id r, gen'〉) 〈en, gen〉.
    2222
    2323(* Add a statement to the graph, *without* updating the entry label. *)
     
    3737(* Add a statement with a fresh label to the start of the function.  The
    3838   statement is parametrised by the *next* instruction's label. *)
    39 definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝
     39definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝
    4040λs,f.
    41   do 〈l,g〉 ← fresh … (f_labgen f);
     41  let 〈l,g〉 ≝ fresh … (f_labgen f) in
    4242  let s' ≝ s (f_entry f) in
    43   OK ? (mk_internal_function g (f_reggen f)
     43    (mk_internal_function g (f_reggen f)
    4444                       (f_result f) (f_params f) (f_locals f)
    4545                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
     
    4747(* Generate a fresh label and use it as a dangling entry point, to be filled in
    4848   later with the loop head. *)
    49 definition add_loop_label_to_graph : internal_function → res internal_function ≝
     49definition add_loop_label_to_graph : internal_function → internal_function ≝
    5050λf.
    51   do 〈l,g〉 ← fresh … (f_labgen f);
    52   OK ? (mk_internal_function g (f_reggen f)
     51  let 〈l,g〉 ≝ fresh … (f_labgen f) in
     52    (mk_internal_function g (f_reggen f)
    5353                       (f_result f) (f_params f) (f_locals f)
    5454                       (f_stacksize f) (f_graph f) l (f_exit f)).
    5555
    56 definition fresh_reg : internal_function → typ → res (register × internal_function)
     56definition fresh_reg : internal_function → typ → register × internal_function
    5757λf,ty.
    58   do 〈r,g〉 ← fresh … (f_reggen f);
    59   OK ? 〈r, mk_internal_function (f_labgen f) g
     58  let 〈r,g〉 ≝ fresh … (f_reggen f) in
     59    〈r, mk_internal_function (f_labgen f) g
    6060                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
    6161                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
     
    7070      OK ? 〈r, f〉
    7171  | _ ⇒
    72       fresh_reg f ty
     72      OK ? (fresh_reg f ty)
    7373  ].
    7474
     
    8888    match register_eq r dst with
    8989    [ inl _ ⇒ OK ? f
    90     | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
     90    | inr _ ⇒ OK ? (add_fresh_to_graph (St_op1 Oid dst r) f)
    9191    ]
    92 | Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
     92| Cst _ c ⇒ OK ? (add_fresh_to_graph (St_const dst c) f)
    9393| Op1 _ _ op e' ⇒
    9494    do 〈r,f〉 ← choose_reg env ? e' f;
    95     do f ← add_fresh_to_graph (St_op1 op dst r) f;
     95    let f ≝ add_fresh_to_graph (St_op1 op dst r) f in
    9696    add_expr env ? e' r f
    9797| Op2 _ _ _ op e1 e2 ⇒
    9898    do 〈r1,f〉 ← choose_reg env ? e1 f;
    9999    do 〈r2,f〉 ← choose_reg env ? e2 f;
    100     do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
     100    let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in
    101101    do f ← add_expr env ? e2 r2 f;
    102102    add_expr env ? e1 r1 f
    103103| Mem _ _ q e' ⇒
    104104    do 〈r,f〉 ← choose_reg env ? e' f;
    105     do f ← add_fresh_to_graph (St_load q r dst) f;
     105    let f ≝ add_fresh_to_graph (St_load q r dst) f in
    106106    add_expr env ? e' r f
    107107| Cond _ _ _ e' e1 e2 ⇒
     
    109109    do f ← add_expr env ? e2 dst f;
    110110    let lfalse ≝ f_entry f in
    111     do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
     111    let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in
    112112    do f ← add_expr env ? e1 dst f;
    113113    do 〈r,f〉 ← choose_reg env ? e' f;
    114     do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;
     114    let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in
    115115    add_expr env ? e' r f
    116116| Ecost _ l e' ⇒
    117117    do f ← add_expr env ? e' dst f;
    118     add_fresh_to_graph (St_cost l) f
     118    OK ? (add_fresh_to_graph (St_cost l) f)
    119119].
    120120
     
    146146    do 〈val_reg, f〉 ← choose_reg env ? e2 f;
    147147    do 〈addr_reg, f〉 ← choose_reg env ? e1 f;
    148     do f ← add_fresh_to_graph (St_store q addr_reg val_reg) f;
     148    let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in
    149149    do f ← add_expr env ? e1 addr_reg f;
    150150    add_expr env ? e2 val_reg f
     
    158158    do f ←
    159159      match e with
    160       [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
     160      [ Id _ id ⇒ OK ? (add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f)
    161161      | _ ⇒
    162162        do 〈fnr, f〉 ← choose_reg env ? e f;
    163         do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
     163        let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in
    164164        add_expr env ? e fnr f
    165165      ];
     
    169169    do f ←
    170170      match e with
    171       [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
     171      [ Id _ id ⇒ OK ? (add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f)
    172172      | _ ⇒
    173173        do 〈fnr, f〉 ← choose_reg env ? e f;
    174         do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
     174        let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
    175175        add_expr env ? e fnr f
    176176      ];
     
    183183    do f ← add_stmt env label_env s2 exits f;
    184184    let l2 ≝ f_entry f in
    185     do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
     185    let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in
    186186    do f ← add_stmt env label_env s1 exits f;
    187187    do 〈r,f〉 ← choose_reg env ? e f;
    188     do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;
     188    let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in
    189189    add_expr env ? e r f
    190190| St_loop s ⇒
    191     do f ← add_loop_label_to_graph f;
     191    let f ≝ add_loop_label_to_graph f in
    192192    let l_loop ≝ f_entry f in
    193193    do f ← add_stmt env label_env s exits f;
     
    197197| St_exit n ⇒
    198198    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    199     add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
     199    OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
    200200| St_switch sz sg e tab n ⇒
    201201    do 〈r,f〉 ← choose_reg env ? e f;
    202202    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    203     do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
     203    let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
    204204    do f ← foldr ?? (λcs,f.
    205205      do f ← f;
    206206      let 〈i,n〉 ≝ cs in
    207       do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
    208       do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);
     207      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
     208      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
    209209      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    210       do f ← add_fresh_to_graph (St_cond br l_case) f;
    211       do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
    212       add_fresh_to_graph (St_const cr (Ointconst ? i)) f) (OK ? f) tab;
     210      let f ≝ add_fresh_to_graph (St_cond br l_case) f in
     211      let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
     212        OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
    213213    add_expr env ? e r f
    214214| St_return opt_e ⇒
    215     do f ← add_fresh_to_graph (λ_. St_return) f;
     215    let f ≝ add_fresh_to_graph (λ_. St_return) f in
    216216    match opt_e with
    217217    [ None ⇒ OK ? f
     
    228228| St_goto l ⇒
    229229    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    230     add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
     230    OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
    231231| St_cost l s' ⇒
    232232    do f ← add_stmt env label_env s' exits f;
    233     add_fresh_to_graph (St_cost l) f
     233    OK ? (add_fresh_to_graph (St_cost l) f)
    234234].
    235235[ @(λ_. St_skip l_next)
     
    258258let reggen0 ≝ new_universe RegisterTag in
    259259let cminor_labels ≝ labels_of (f_body f) in
    260 do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
    261 do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
    262 do 〈result, locals, reggen〉 ←
     260let 〈params, env1, reggen1〉 ≝ populate_env (empty_map …) reggen0 (f_params f) in
     261let 〈locals0, env, reggen2〉 ≝ populate_env env1 reggen1 (f_vars f) in
     262let 〈result, locals, reggen〉 ≝
    263263  match f_return f with
    264   [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
     264  [ None ⇒ 〈None ?, locals0, reggen2〉
    265265  | Some ty ⇒
    266       do 〈r,gen〉 ← fresh … reggen2;
    267       OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];
    268 do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
    269 do 〈l,labgen〉 ← fresh … labgen1;
     266      let 〈r,gen〉 ≝ fresh … reggen2 in
     267        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
     268let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
     269let 〈l,labgen〉 ≝ fresh … labgen1 in
    270270let emptyfn ≝
    271271  mk_internal_function
     
    279279    l
    280280    l in
    281   add_stmt env label_env (f_body f) [ ] emptyfn
     281do f ← add_stmt env label_env (f_body f) [ ] emptyfn;
     282do u1 ← check_universe_ok ? (f_labgen f);
     283do u2 ← check_universe_ok ? (f_reggen f);
     284OK ? f
    282285.
    283286
  • src/RTLabs/import.ma

    r898 r1056  
    22include "RTLabs/semantics.ma".
    33
    4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝
     4let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
    55match n with
    6 [ O ⇒ OK ? 〈[[ ]], g〉
    7 | S m ⇒ do 〈ls, g'〉 ← n_idents m tag g;
    8         do 〈l, g''〉 ← fresh ? g';
    9         OK ? 〈l:::ls, g''〉
     6[ O ⇒ 〈[[ ]], g〉
     7| S m ⇒ let 〈ls, g'〉 ≝ n_idents m tag g in
     8        let 〈l, g''〉 ≝ fresh ? g' in
     9        〈l:::ls, g''〉
    1010].
    1111
     
    2424definition make_register :
    2525  (pre_register → option register) → pre_register → universe RegisterTag →
    26   res ((nat → option register) × (universe RegisterTag) × register)
     26  (nat → option register) × (universe RegisterTag) × register
    2727λm,reg,g.
    2828  match m reg with
    29   [ Some r' ⇒ OK ? 〈〈m,g〉,r'〉
    30   | None ⇒ do 〈r',g'〉 ← fresh ? g;
    31            OK ? 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
     29  [ Some r' ⇒ 〈〈m,g〉,r'〉
     30  | None ⇒ let 〈r',g'〉 ≝ fresh ? g in
     31             〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
    3232  ]
    3333.
     
    3535definition make_registers_list :
    3636  (nat → option register) → list (pre_register × typ) → universe RegisterTag →
    37   res ((nat → option register) × (universe RegisterTag) × (list (register×typ))) ≝
     37    (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝
    3838λm,lrs,g.
    39 foldr ?? (λrst,acc. do 〈acc',l〉 ← acc;
    40                    let 〈rs,ty〉 ≝ rst in
    41                    let 〈m,g〉 ≝ acc' in
    42                    do 〈mg,rs'〉 ← make_register m rs g;
    43                    OK ? 〈mg,〈rs',ty〉::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
     39foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in
     40                    let 〈rs,ty〉 ≝ rst in
     41                    let 〈m,g〉 ≝ acc' in
     42                    let 〈mg,rs'〉 ≝ make_register m rs g in
     43                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
    4444
    4545axiom MissingRegister : String.
    4646axiom MissingLabel : String.
    4747
     48(* Doesn't check for identifier overflow, but don't really need to care here. *)
    4849definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
    4950λpre_f.
    5051  let rgen0 ≝ new_universe RegisterTag in
    51   do 〈rmapgen1, result〉 ← match pf_result pre_f with
    52                           [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
    53                           | Some rt ⇒ do 〈x,y〉 ← make_register (λ_.None ?) (\fst rt) rgen0; OK ? 〈x,Some ? 〈y,\snd rt〉〉
    54                           ];
     52  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
     53                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
     54                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
     55                           ] in
    5556  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
    56   do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
     57  let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in
    5758  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
    58   do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
     59  let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in
    5960  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
    6061  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
    6162  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    62   do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
     63  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
    6364  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    6465  do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
  • src/RTLabs/syntax.ma

    r1051 r1056  
    1313| St_skip : label → statement
    1414| St_cost : costlabel → label → statement
    15 | St_const : register → cast → label → statement
     15| St_const : register → constant → label → statement
    1616| St_op1 : unary_operation → register → register → label → statement
    1717| St_op2 : binary_operation → register → register → register → label → statement
  • src/common/Identifiers.ma

    r1055 r1056  
    2222  λtag. mk_universe tag (zero ?) false.
    2323
    24 definition fresh ≝
     24(* Fresh identifier generation uses delayed overflow checking.  To make sure
     25   that the identifiers really were fresh, use the check_universe_ok function
     26   below afterwards. *)
     27definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
    2528  λtag.
    2629  λuniv: universe tag.
     
    3235  //
    3336qed.
     37
     38axiom TooManyIdentifiers : String.
     39
     40definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
     41  λtag, univ.
     42  if counter_overflow ? univ
     43  then Error ? (msg TooManyIdentifiers)
     44  else OK ? it.
    3445
    3546definition eq_identifier ≝
Note: See TracChangeset for help on using the changeset viewer.