Changeset 1633 for src/RTLabs


Ignore:
Timestamp:
Jan 4, 2012, 7:19:09 PM (8 years ago)
Author:
campbell
Message:

Update Cminor pretty printer and examples.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r1226 r1633  
    136136
    137137let print_statement lookup_type = function
    138   | RTLabs.St_skip lbl -> "make_St_skip " ^ (print_label lbl)
     138  | RTLabs.St_skip lbl
     139  | RTLabs.St_ind_0 (_, lbl)
     140  | RTLabs.St_ind_inc (_, lbl)
     141     -> "make_St_skip " ^ (print_label lbl)
    139142  | RTLabs.St_cost (cost_lbl, lbl) ->
    140       Printf.sprintf "make_St_cost C%s %s" cost_lbl (print_label lbl)
     143      Printf.sprintf "make_St_cost C%s %s"
     144        cost_lbl.CostLabel.name (print_label lbl)
    141145  | RTLabs.St_cst (dests, cst, lbl) ->
    142146      Printf.sprintf "make_St_const %s (%s) %s"
     
    198202        (Register.print rs)
    199203        (print_table tbl)
    200   | RTLabs.St_return rs -> "make_St_return" (* rs should always be the function's result register, anyway *)
     204  | RTLabs.St_return -> "make_St_return"
    201205
    202206let print_cost_labels n c =
  • src/RTLabs/import.ma

    r1612 r1633  
    1717; pf_locals    : list (pre_register × typ)
    1818; pf_stacksize : nat
    19 ; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
     19; pf_graph     : list (nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement))
    2020; pf_entry     : nat
    2121; pf_exit      : nat
     
    2323
    2424definition make_register :
    25   (pre_register → option register) → pre_register → universe RegisterTag →
    26   (nat → option register) × (universe RegisterTag) × register ≝
    27 λm,reg,g.
     25  (pre_register → option (register×typ)) → pre_register → typ → universe RegisterTag →
     26  (nat → option (register×typ)) × (universe RegisterTag) × register ≝
     27λm,reg,ty,g.
    2828  match m reg with
    29   [ Some r' ⇒ 〈〈m,g〉,r'〉
     29  [ Some r' ⇒ 〈〈m,g〉,\fst r'〉
    3030  | None ⇒ let 〈r',g'〉 ≝ fresh ? g in
    31              〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
     31             〈〈λn. if eqb reg n then Some ? 〈r',ty〉 else m n,g'〉,r'〉
    3232  ]
    3333.
    3434
    3535definition make_registers_list :
    36   (nat → option register) → list (pre_register × typ) → universe RegisterTag →
    37     (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝
     36  (nat → option (register×typ)) → list (pre_register × typ) → universe RegisterTag →
     37    (nat → option (register×typ)) × (universe RegisterTag) × (list (register×typ)) ≝
    3838λm,lrs,g.
    3939foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in
    4040                    let 〈rs,ty〉 ≝ rst in
    4141                    let 〈m,g〉 ≝ acc' in
    42                     let 〈mg,rs'〉 ≝ make_register m rs g in
     42                    let 〈mg,rs'〉 ≝ make_register m rs ty g in
    4343                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
    4444
     
    5252  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
    5353                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
    54                            | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
     54                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) (\snd rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
    5555                           ] in
    5656  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
     
    6363  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
    6464  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    65   do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
     65  do graph ← foldr ?? (λp:nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement).λg0.
    6666                         do g ← g0;
    6767                         let 〈l,s〉 ≝ p in
     
    8888         (pf_stacksize pre_f)
    8989         graph
     90         ?
     91         ?
    9092         (mk_Sig ?? entry p)
    9193         (mk_Sig ?? exit q)
    9294         )))
    9395   .
    94 % #E destruct (E)
     96[ 1,2: % #E destruct (E)
     97| 3,4: cases daemon
     98]
    9599qed.
    96100
    97 definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
    98 λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
     101definition make_reg_list : (nat → res (register×typ)) → list pre_register → res (list register) ≝
     102λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do 〈r,t〉 ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
    99103
    100104(* XXX move somewhere sensible *)
     
    107111].
    108112
    109 definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
    110 λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
     113definition make_opt_reg : (pre_register → res (register×typ)) → option pre_register → res (option register) ≝
     114λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do 〈r',t'〉 ← m r; OK ? (Some ? r') ].
    111115
    112 let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
    113 let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
    114 let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
    115 let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src' ← r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
    116 let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src1' ← r src1; do src2' ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
    117 let rec make_St_load chunk addr dst l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do dst' ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
    118 let rec make_St_store chunk addr src l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do src' ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
    119 let rec make_St_call_id id args dst l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
    120 let rec make_St_call_ptr frs args dst l ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
    121 let rec make_St_tailcall_id id args ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
    122 let rec make_St_tailcall_ptr frs args ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
    123 let rec make_St_cond src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
    124 let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
    125 definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
     116inductive pre_op1 : Type[0] ≝
     117  | POcastint: intsize → signedness → intsize → pre_op1
     118  | POnegint:  pre_op1
     119  | POnotbool: pre_op1
     120  | POnotint:  pre_op1
     121  | POid: pre_op1
     122  | POptrofint: pre_op1
     123  | POintofptr: pre_op1
     124.
    126125
     126axiom TypeMismatch : String.
     127
     128(* duplicated from Clight/toCminor.ma. *)
     129definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
     130* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     131qed.
     132
     133definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
     134* [ #sz1 #sg1 | #r1 | #sz1 ]
     135* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
     136[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
     137  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     138| *; #P #p @(region_should_eq r1 ?? p)
     139| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     140] qed.
     141
     142definition is_bool_src : ∀ty. res (boolsrc ty) ≝
     143λty. match ty return λt.res (boolsrc t) with [ ASTint _ _ ⇒ OK ? I | ASTptr _ ⇒ OK ? I | _ ⇒ Error ? (msg TypeMismatch) ].
     144
     145definition make_op1 : ∀t,t'. pre_op1 → res (unary_operation t' t) ≝
     146λt,t',op.
     147  match op with
     148  [ POcastint sz sg sz' ⇒
     149      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     150        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Ocastint sz sg sz' sg2);
     151               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
     152      | _ ⇒ Error ? (msg TypeMismatch) ]
     153  | POnegint ⇒
     154      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     155        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onegint sz2 sg2);
     156               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
     157      | _ ⇒ Error ? (msg TypeMismatch) ]
     158  | POnotbool ⇒
     159      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     160        do p ← is_bool_src t';
     161               OK ? (Onotbool t' sz2 sg2 p)
     162      | _ ⇒ Error ? (msg TypeMismatch) ]
     163  | POnotint ⇒
     164      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     165        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onotint sz2 sg2);
     166               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
     167      | _ ⇒ Error ? (msg TypeMismatch) ]
     168  | POid ⇒ typ_should_eq t t' (λt'. unary_operation t' t) (Oid t)
     169  | POptrofint ⇒
     170      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     171      match t return λt. res (unary_operation ? t) with [ ASTptr r1 ⇒
     172        OK ? (Optrofint …)
     173      | _ ⇒ Error ? (msg TypeMismatch) ]
     174      | _ ⇒ Error ? (msg TypeMismatch) ]
     175  | POintofptr ⇒
     176      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
     177      match t' return λt'. res (unary_operation t' ?) with [ ASTptr r1 ⇒
     178        OK ? (Ointofptr …)
     179      | _ ⇒ Error ? (msg TypeMismatch) ]
     180      | _ ⇒ Error ? (msg TypeMismatch) ]
     181  ].
     182
     183let rec make_St_skip l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_skip l').
     184let rec make_St_cost cl l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
     185let rec make_St_const rs cst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',ty'〉 ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
     186let rec make_St_op1 op dst src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src',sty〉 ← r src; do l' ← f l; do op ← make_op1 dty sty op; OK ? (St_op1 dty sty op dst' src' l').
     187let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src1',sty1〉 ← r src1; do 〈src2',sty2〉 ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
     188let rec make_St_load chunk addr dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈dst',dty〉 ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
     189let rec make_St_store chunk addr src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈src',sty〉 ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
     190let rec make_St_call_id id args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
     191let rec make_St_call_ptr frs args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
     192let rec make_St_tailcall_id id args ≝ λr:nat → res (register×typ).λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
     193let rec make_St_tailcall_ptr frs args ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
     194let rec make_St_cond src ltrue lfalse ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈src',sty〉 ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
     195let rec make_St_jumptable rs ls ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',rty〉 ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
     196definition make_St_return ≝ λr:nat → res (register×typ).λf:nat → res label. OK statement St_return.
     197
Note: See TracChangeset for help on using the changeset viewer.