Changeset 1640 for src/RTLabs


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (8 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1636 r1640  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
    10 
    11 
    12 (* Paolo: to be moved elsewhere *)
    13 
    14 notation "r ← a1 .op. a2" with precedence 50 for
    15   @{'op2 $op $r $a1 $a2}.
    16 notation "r ← . op . a" with precedence 50 for
    17   @{'op1 $op $r $a}.
    18 notation "r ← a" with precedence 50 for
    19   @{'mov $r $a}.
    20 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
    21   @{'opaccs $op $r $s $a1 $a2}.
    22 
    23 interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
    24 interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
    25 interpretation "move" 'mov r a = (MOVE ? ? (REG r a)).
    26 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    2710
    2811
     
    141124    eqb m n = true → m = n.
    142125    #m#n@eqb_elim // #_ #F destruct(F) qed.
    143    
     126
    144127definition translate_op:
    145128  ∀globals. Op2 →
     
    161144  (* first, clear carry if op relies on it *)
    162145  match op with
    163   [ Addc ⇒ [clear_carry ?]
    164   | Sub ⇒ [clear_carry ?]
     146  [ Addc ⇒ [CLEAR_CARRY ??]
     147  | Sub ⇒ [CLEAR_CARRY ??]
    165148  | _ ⇒ [ ]
    166149  ] @
     
    228211      match split_into_bytes size const with
    229212      [ mk_Sig bytes bytes_length_proof ⇒
    230         map2 … (reg_from_byte globals) destrs bytes ?
     213        map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs bytes ?
    231214      ]
    232215    | Ofloatconst float ⇒ λ_.⊥
     
    374357    | cons srcr srcrs' ⇒
    375358      let f : register → rtl_instruction globals ≝
    376         λr. OP2 ?? Or destr (Reg destr) (Reg r) in
    377       reg_from_reg … srcr destr ::
     359        λr. destr ← destr .Or. r in
     360      MOVE rtl_params globals 〈destr,srcr〉 ::
    378361      map … f srcrs' @
    379362      (* now destr is non-null iff srcrs was non-null *)
    380       clear_carry … ::
     363      CLEAR_CARRY ? ? ::
    381364      (* many uses of 0, better not use immediates *)
    382365      ν tmp in
     
    420403  ]
    421404qed.
     405
     406include alias "arithmetics/nat.ma".
    422407
    423408let rec range_strong_internal (start : ℕ) (count : ℕ)
     
    615600          acc in
    616601        let epilogue : list (rtl_instruction globals) ≝
    617           [ clear_carry … ;
     602          [ CLEAR_CARRY … ;
    618603            tmpr ← 0 .Sub. destr ;
    619604            (* now carry bit is 1 iff destrs != 0 *)
     
    782767  | cons srcr srcrs' ⇒
    783768    ν tmpr in
    784     let f ≝ λr. OP2 rtl_params globals Or tmpr (Reg tmpr) (Reg r) in
    785     reg_from_reg globals tmpr srcr ::
     769    let f : register → rtl_instruction globals ≝
     770      λr. tmpr ← tmpr .Or. r in
     771    MOVE rtl_params globals 〈tmpr,srcr〉 ::
    786772    map … f srcrs' @
    787     [ COND tmpr lbl_true ]
     773    [ COND ?? tmpr lbl_true ]
    788774  ].
    789775
     
    926912  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    927913    (f_params def @ f_locals def) (f_result def) in
    928   let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
     914  let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in
    929915  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
    930916  let result ≝
     
    939925  let runiverse' ≝ runiverse in
    940926  let result' ≝ result in
    941   let params' ≝ params in
     927  let params' ≝ parameters in
    942928  let locals' ≝ locals in
    943929  let stack_size' ≝ f_stacksize def in
    944930  let entry' ≝ f_entry def in
    945931  let exit' ≝ f_exit def in
    946   let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params globals entry') in
    947   let graph' ≝ add LabelTag ? graph' exit' (RETURN rtl_params globals) in
     932  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry'
     933    (GOTO (rtl_params : params) globals entry') in
     934  let graph' ≝ add LabelTag ? graph' exit'
     935    (RETURN (rtl_params : params) globals) in
    948936  let res ≝
    949937    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
Note: See TracChangeset for help on using the changeset viewer.