Changeset 887 for src/Cminor


Ignore:
Timestamp:
Jun 6, 2011, 3:55:23 PM (8 years ago)
Author:
campbell
Message:

Start bringing RTLabs into line with the prototype compiler:

  • a coarse-grained type is associated with every register
  • the special addressing modes have been removed
Location:
src/Cminor
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r881 r887  
    5555          match f' with
    5656          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
    57                                            (f_sig f)
     57                                           (f_return f)
    5858                                           (f_params f)
    5959                                           (f_vars f)
    60                                            (f_ptrs f)
    6160                                           (f_stacksize f)
    6261                                           (St_seq s (f_body f)))〉
  • src/Cminor/toRTLabs.ma

    r881 r887  
    66definition env ≝ identifier_map SymbolTag register.
    77definition label_env ≝ identifier_map SymbolTag label.
    8 definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝
     8definition populate_env : env → universe RegisterTag → list (ident × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝
    99λen,gen. foldr ??
    10  (λid,rsengen.
     10 (λidt,rsengen.
     11   let 〈id,ty〉 ≝ idt in
    1112   do 〈rs,en,gen〉 ← rsengen;
    1213   do 〈r,gen'〉 ← fresh … gen;
    13    OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
     14   OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
    1415
    1516definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
     
    2324definition fill_in_statement : label → statement → internal_function → internal_function ≝
    2425λl,s,f.
    25   mk_internal_function (f_labgen f) (f_reggen f) (f_sig f)
    26                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     26  mk_internal_function (f_labgen f) (f_reggen f)
     27                       (f_result f) (f_params f) (f_locals f)
    2728                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
    2829
     
    3031definition add_to_graph : label → statement → internal_function → internal_function ≝
    3132λl,s,f.
    32   mk_internal_function (f_labgen f) (f_reggen f) (f_sig f)
    33                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     33  mk_internal_function (f_labgen f) (f_reggen f)
     34                       (f_result f) (f_params f) (f_locals f)
    3435                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
    3536
     
    4041  do 〈l,g〉 ← fresh … (f_labgen f);
    4142  let s' ≝ s (f_entry f) in
    42   OK ? (mk_internal_function g (f_reggen f) (f_sig f)
    43                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     43  OK ? (mk_internal_function g (f_reggen f)
     44                       (f_result f) (f_params f) (f_locals f)
    4445                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
    4546
     
    4950λf.
    5051  do 〈l,g〉 ← fresh … (f_labgen f);
    51   OK ? (mk_internal_function g (f_reggen f) (f_sig f)
    52                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     52  OK ? (mk_internal_function g (f_reggen f)
     53                       (f_result f) (f_params f) (f_locals f)
    5354                       (f_stacksize f) (f_graph f) l (f_exit f)).
    5455
    55 definition fresh_reg : internal_function → res (register × internal_function) ≝
    56 λf.
     56definition fresh_reg : internal_function → typ → res (register × internal_function) ≝
     57λf,ty.
    5758  do 〈r,g〉 ← fresh … (f_reggen f);
    58   OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f)
    59                        (f_result f) (f_params f) (r::(f_locals f)) (f_ptrs f)
     59  OK ? 〈r, mk_internal_function (f_labgen f) g
     60                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
    6061                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    6162
    62 definition fresh_ptr_reg : internal_function → res (register × internal_function) ≝
    63 λf.
    64   do 〈r,g〉 ← fresh … (f_reggen f);
    65   OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f)
    66                        (f_result f) (f_params f) (r::(f_locals f)) (r::(f_ptrs f))
    67                        (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    68 
    69 let rec expr_yields_pointer (ty:typ) (e:expr ty) (ptrs:list ident) on e : bool ≝
    70 match e with
    71 [ Id _ i ⇒ exists ? (eq_identifier ? i) ptrs
    72 | Cst _ c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ]
    73 | Op1 _ _ op e' ⇒
    74     match op with
    75     [ Oid ⇒ expr_yields_pointer ? e' ptrs
    76     | Optrofint _ ⇒ true
    77     | _ ⇒ false
    78     ]
    79 | Op2 _ _ _ op e1 e2 ⇒
    80     match op with
    81     [ Oaddp ⇒ true
    82     | Osubpi ⇒ true
    83     | _ ⇒ false
    84     ]
    85 | Mem _ _ q e' ⇒
    86     match q with
    87     [ Mpointer _ ⇒ true
    88     | _ ⇒ false
    89     ]
    90 (* Both branches ought to be the same? *)
    91 | Cond _ _ _ e' e1 e2 ⇒ (expr_yields_pointer ? e1 ptrs) ∨ (expr_yields_pointer ? e2 ptrs)
    92 | Ecost _ _ e' ⇒ expr_yields_pointer ? e' ptrs
    93 ].
    94 
    9563axiom UnknownVariable : String.
    9664
    97 definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝
    98 λenv,ty,e,ptrs,f.
     65definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function) ≝
     66λenv,ty,e,f.
    9967  match e with
    10068  [ Id _ i ⇒
     
    10270      OK ? 〈r, f〉
    10371  | _ ⇒
    104       if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f
     72      fresh_reg f ty
    10573  ].
    10674
    107 definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝
    108 λenv,es,ptrs,f.
     75definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝
     76λenv,es,f.
    10977  foldr (Σt:typ.expr t) ?
    11078    (λe,acc. do 〈rs,f〉 ← acc;
    111              do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ];
     79             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ];
    11280             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
    11381
    11482axiom BadCminorProgram : String.
    11583
    116 let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
     84let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (f:internal_function) on e: res internal_function ≝
    11785match e with
    11886[ Id _ i ⇒
     
    12492| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
    12593| Op1 _ _ op e' ⇒
    126     do 〈r,f〉 ← choose_reg env ? e' ptrs f;
     94    do 〈r,f〉 ← choose_reg env ? e' f;
    12795    do f ← add_fresh_to_graph (St_op1 op dst r) f;
    128     add_expr env ? e' r ptrs f
     96    add_expr env ? e' r f
    12997| Op2 _ _ _ op e1 e2 ⇒
    130     do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
    131     do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
     98    do 〈r1,f〉 ← choose_reg env ? e1 f;
     99    do 〈r2,f〉 ← choose_reg env ? e2 f;
    132100    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
    133     do f ← add_expr env ? e2 r2 ptrs f;
    134     add_expr env ? e1 r1 ptrs f
    135 | Mem _ _ q e' ⇒
    136     add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e')
     101    do f ← add_expr env ? e2 r2 f;
     102    add_expr env ? e1 r1 f
     103| Mem _ _ q e' ⇒
     104    do 〈r,f〉 ← choose_reg env ? e' f;
     105    do f ← add_fresh_to_graph (St_load q r dst) f;
     106    add_expr env ? e' r f
    137107| Cond _ _ _ e' e1 e2 ⇒
    138108    let resume_at ≝ f_entry f in
    139     do f ← add_expr env ? e2 dst ptrs f;
     109    do f ← add_expr env ? e2 dst f;
    140110    let lfalse ≝ f_entry f in
    141111    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
    142     do f ← add_expr env ? e1 dst ptrs f;
    143     add_branch_internal env ? e' (f_entry f) lfalse ptrs f (add_expr env ? e')
     112    do f ← add_expr env ? e1 dst f;
     113    add_branch_internal env ? e' (f_entry f) lfalse f (add_expr env ? e')
    144114| Ecost _ l e' ⇒
    145     do f ← add_expr env ? e' dst ptrs f;
     115    do f ← add_expr env ? e' dst f;
    146116    add_fresh_to_graph (St_cost l) f
    147117   
     
    150120   add_<whatever> afterwards. *)
    151121]
    152 and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty)
    153                           (s:∀m:addressing. addr m → label → statement)
    154                           (ptrs:list ident)
    155                           (f:internal_function)
    156                           (termination_hack:register → list ident → internal_function → res internal_function)
    157                           on e : res internal_function ≝
    158 let add_default : unit → res internal_function ≝ λ_.
    159     do 〈r, f〉 ← choose_reg env ? e ptrs f;
    160     do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
    161     termination_hack r ptrs f
    162 in
    163 match e with
    164 [ Cst _ c ⇒
    165     match c with
    166     [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
    167     | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
    168     | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
    169     ]
    170 | Op2 _ _ _ op e1 e2 ⇒
    171     match op with
    172     [ Oaddp ⇒
    173         let add_generic_addp : unit → res internal_function ≝ λ_.
    174           do 〈r1, f〉 ← choose_reg env ? e1 ptrs f;
    175           do 〈r2, f〉 ← choose_reg env ? e2 ptrs f;
    176           do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
    177           do f ← add_expr env ? e2 r2 ptrs f;
    178           add_expr env ? e1 r1 ptrs f
    179         in
    180         match e1 with
    181         [ Cst _ c ⇒
    182             match c with
    183             [ Oaddrsymbol id i ⇒
    184                 do 〈r, f〉 ← choose_reg env ? e ptrs f;
    185                 do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
    186                 add_expr env ? e2 r ptrs f
    187             | _ ⇒ add_generic_addp it
    188             ]
    189         | _ ⇒ add_generic_addp it
    190         ]
    191     | _ ⇒ add_default it
    192     ]
    193 | _ ⇒ add_default it
    194 ]
    195 (* and again *)
    196 and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
    197         (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
     122and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (f:internal_function)
     123        (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
    198124match e with
    199125[ Id _ i ⇒
     
    203129    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    204130| Op1 _ _ op e' ⇒
    205     do 〈r,f〉 ← choose_reg env ? e' ptrs f;
     131    do 〈r,f〉 ← choose_reg env ? e' f;
    206132    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    207     add_expr env ? e' r ptrs f
     133    add_expr env ? e' r f
    208134| Op2 _ _ _ op e1 e2 ⇒
    209     do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
    210     do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
     135    do 〈r1,f〉 ← choose_reg env ? e1 f;
     136    do 〈r2,f〉 ← choose_reg env ? e2 f;
    211137    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    212     do f ← add_expr env ? e2 r2 ptrs f;
    213     add_expr env ? e1 r1 ptrs f
     138    do f ← add_expr env ? e2 r2 f;
     139    add_expr env ? e1 r1 f
    214140| _ ⇒
    215     do 〈r,f〉 ← choose_reg env ? e ptrs f;
     141    do 〈r,f〉 ← choose_reg env ? e f;
    216142    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    217     termination_hack_add_expr r ptrs f
     143    termination_hack_add_expr r f
    218144].
    219145
    220146(* See comment above. *)
    221 definition add_with_addressing ≝
    222 λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e).
    223147definition add_branch ≝
    224 λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e).
     148λenv,ty,e,ltrue,lfalse,f. add_branch_internal env ty e ltrue lfalse f (add_expr env ty e).
    225149
    226150(* This shouldn't occur; maybe use vectors? *)
    227151axiom WrongNumberOfArguments : String.
    228152
    229 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
     153let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (f:internal_function) on es: res internal_function ≝
    230154match es with
    231155[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
     
    234158    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
    235159    | cons r rt ⇒
    236         do f ← add_exprs env et rt ptrs f;
    237         match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ]
     160        do f ← add_exprs env et rt f;
     161        match e with [ dp ty e ⇒ add_expr env ty e r f ]
    238162    ]
    239163].
     
    242166axiom ReturnMismatch : String.
    243167
    244 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝
     168let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
    245169match s with
    246170[ St_skip ⇒ OK ? f
    247171| St_assign _ x e ⇒
    248172    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    249     add_expr env ? e dst ptrs f
     173    add_expr env ? e dst f
    250174| St_store _ _ q e1 e2 ⇒
    251     do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f;
    252     do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f;
    253     add_expr env ? e2 val_reg ptrs f
     175    do 〈val_reg, f〉 ← choose_reg env ? e2 f;
     176    do 〈addr_reg, f〉 ← choose_reg env ? e1 f;
     177    do f ← add_fresh_to_graph (St_store q addr_reg val_reg) f;
     178    do f ← add_expr env ? e1 addr_reg f;
     179    add_expr env ? e2 val_reg f
    254180| St_call return_opt_id e args ⇒
    255181    do return_opt_reg ←
     
    258184      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
    259185      ];
    260     do 〈args_regs, f〉 ← choose_regs env args ptrs f;
     186    do 〈args_regs, f〉 ← choose_regs env args f;
    261187    do f ←
    262188      match e with
    263189      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    264190      | _ ⇒
    265         do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
     191        do 〈fnr, f〉 ← choose_reg env ? e f;
    266192        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
    267         add_expr env ? e fnr ptrs f
     193        add_expr env ? e fnr f
    268194      ];
    269     add_exprs env args args_regs ptrs f
     195    add_exprs env args args_regs f
    270196| St_tailcall e args ⇒
    271     do 〈args_regs, f〉 ← choose_regs env args ptrs f;
     197    do 〈args_regs, f〉 ← choose_regs env args f;
    272198    do f ←
    273199      match e with
    274200      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    275201      | _ ⇒
    276         do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
     202        do 〈fnr, f〉 ← choose_reg env ? e f;
    277203        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
    278         add_expr env ? e fnr ptrs f
     204        add_expr env ? e fnr f
    279205      ];
    280     add_exprs env args args_regs ptrs f
     206    add_exprs env args args_regs f
    281207| St_seq s1 s2 ⇒
    282     do f ← add_stmt env label_env s2 exits ptrs f;
    283     add_stmt env label_env s1 exits ptrs f
     208    do f ← add_stmt env label_env s2 exits f;
     209    add_stmt env label_env s1 exits f
    284210| St_ifthenelse _ _ e s1 s2 ⇒
    285211    let l_next ≝ f_entry f in
    286     do f ← add_stmt env label_env s2 exits ptrs f;
     212    do f ← add_stmt env label_env s2 exits f;
    287213    let l2 ≝ f_entry f in
    288214    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    289     do f ← add_stmt env label_env s1 exits ptrs f;
    290     add_branch env ? e (f_entry f) l2 ptrs f
     215    do f ← add_stmt env label_env s1 exits f;
     216    add_branch env ? e (f_entry f) l2 f
    291217| St_loop s ⇒
    292218    do f ← add_loop_label_to_graph f;
    293219    let l_loop ≝ f_entry f in
    294     do f ← add_stmt env label_env s exits ptrs f;
     220    do f ← add_stmt env label_env s exits f;
    295221    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
    296222| St_block s ⇒
    297     add_stmt env label_env s ((f_entry f)::exits) ptrs f
     223    add_stmt env label_env s ((f_entry f)::exits) f
    298224| St_exit n ⇒
    299225    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    300226    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    301 | St_switch _ _ e tab n ⇒
    302     do 〈r,f〉 ← choose_reg env ? e ptrs f;
     227| St_switch sz sg e tab n ⇒
     228    do 〈r,f〉 ← choose_reg env ? e f;
    303229    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    304230    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
     
    306232      do f ← f;
    307233      let 〈i,n〉 ≝ cs in
    308       do 〈cr,f〉 ← fresh_reg … f;
     234      do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
    309235      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    310236      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
    311237      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    312     add_expr env ? e r ptrs f
     238    add_expr env ? e r f
    313239| St_return opt_e ⇒
    314240    do f ← add_fresh_to_graph (λ_. St_return) f;
     
    318244        match f_result f with
    319245        [ None ⇒ Error ? (msg ReturnMismatch)
    320         | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ]
     246        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f ]
    321247        ]
    322248    ]
    323249| St_label l s' ⇒
    324     do f ← add_stmt env label_env s' exits ptrs f;
     250    do f ← add_stmt env label_env s' exits f;
    325251    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    326252    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
     
    329255    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
    330256| St_cost l s' ⇒
    331     do f ← add_stmt env label_env s' exits ptrs f;
     257    do f ← add_stmt env label_env s' exits f;
    332258    add_fresh_to_graph (St_cost l) f
    333259].
     
    360286do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
    361287do 〈result, locals, reggen〉 ←
    362   match sig_res (f_sig f) with
     288  match f_return f with
    363289  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
    364   | Some _
     290  | Some ty
    365291      do 〈r,gen〉 ← fresh … reggen2;
    366       OK ? 〈Some ? r, r::locals0, gen〉 ];
    367 do ptrs ← mmap ?? (λid. opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id)) (f_ptrs f);
     292      OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];
    368293do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
    369294do 〈l,labgen〉 ← fresh … labgen1;
     
    372297    labgen
    373298    reggen
    374     (f_sig f)
    375299    result
    376300    params
    377301    locals
    378     ptrs
    379302    (f_stacksize f)
    380303    (add ?? (empty_map …) l St_return)
    381304    l
    382305    l in
    383   add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
     306  add_stmt env label_env (f_body f) [ ] emptyfn
    384307.
    385308
Note: See TracChangeset for help on using the changeset viewer.