Changeset 1056 for src/Cminor


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

Switch to delayed identifier error scheme.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.