Changeset 1045


Ignore:
Timestamp:
Jun 29, 2011, 10:47:39 AM (8 years ago)
Author:
mulligan
Message:

resolved conflict in rtlabs

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1043 r1045  
    10681068     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    10691069
    1070 axiom split_elim:
     1070lemma split_zero:
     1071  ∀A,m.
     1072  ∀v: Vector A m.
     1073    〈[[]], v〉 = split A 0 m v.
     1074  #A #m #v
     1075  elim v
     1076  [ %
     1077  | #n #hd #tl #ih
     1078    normalize in ⊢ (???%) %
     1079  ]
     1080qed.
     1081
     1082lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
     1083 #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     1084 #n #hd #tl #abs @⊥ destruct (abs)
     1085qed.
     1086
     1087lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
     1088 ∃hd.∃tl.v ≃ VCons A n hd tl.
     1089 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     1090 [ #abs @⊥ destruct (abs)
     1091 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     1092qed.
     1093
     1094lemma vector_append_zero:
     1095  ∀A,m.
     1096  ∀v: Vector A m.
     1097  ∀q: Vector A 0.
     1098    v = q@@v.
     1099  #A #m #v #q
     1100  >(Vector_O A q) %
     1101qed.
     1102
     1103lemma prod_eq_left:
     1104  ∀A: Type[0].
     1105  ∀p, q, r: A.
     1106    p = q → 〈p, r〉 = 〈q, r〉.
     1107  #A #p #q #r #hyp
     1108  >hyp %
     1109qed.
     1110
     1111lemma prod_eq_right:
     1112  ∀A: Type[0].
     1113  ∀p, q, r: A.
     1114    p = q → 〈r, p〉 = 〈r, q〉.
     1115  #A #p #q #r #hyp
     1116  >hyp %
     1117qed.
     1118
     1119corollary prod_vector_zero_eq_left:
     1120  ∀A, n.
     1121  ∀q: Vector A O.
     1122  ∀r: Vector A n.
     1123    〈q, r〉 = 〈[[ ]], r〉.
     1124  #A #n #q #r
     1125  generalize in match (Vector_O A q …)
     1126  #hyp
     1127  >hyp in ⊢ (??%?)
     1128  %
     1129qed.
     1130
     1131axiom split_succ:
     1132  ∀A, m, n.
     1133  ∀l: Vector A m.
     1134  ∀r: Vector A n.
     1135  ∀v: Vector A (m + n).
     1136  ∀hd: A.
     1137    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
     1138(*
     1139  #A #m
     1140  elim m
     1141  [ #n #l #r #v #hd #equal #hyp
     1142    normalize >(Vector_O A l) >equal
     1143    >(Vector_O A l) %
     1144  | #n' #ih #n #l #r #v #hd
     1145    #equal #hyp
     1146    cases(Vector_Sn A n' l)
     1147    #hd' #exists
     1148    cases exists #tl #jmeq
     1149    >jmeq *)
     1150
     1151lemma split_prod:
     1152  ∀A,m,n.
     1153  ∀p: Vector A (m + n).
     1154  ∀v: Vector A m.
     1155  ∀q: Vector A n.
     1156    p = v@@q → 〈v, q〉 = split A m n p.
     1157  #A #m
     1158  elim m
     1159  [ #n #p #v #q #hyp
     1160    >hyp <(vector_append_zero A n q v)
     1161    >(prod_vector_zero_eq_left A …)
     1162    @split_zero
     1163  | #r #ih #n #p #v #q #hyp
     1164    >hyp
     1165    cases (Vector_Sn A r v)
     1166    #hd #exists
     1167    cases exists
     1168    #tl #jmeq >jmeq
     1169    @split_succ [1: % |2: @ih % ]
     1170  ]
     1171qed.
     1172
     1173lemma split_prod_exists:
     1174  ∀A, m, n.
     1175  ∀p: Vector A (m + n).
     1176  ∃v: Vector A m.
     1177  ∃q: Vector A n.
     1178    〈v, q〉 = split A m n p.
     1179  #A #m #n #p
     1180  elim m
     1181  @ex_intro
     1182  [1:
     1183  |2: @ex_intro
     1184      [1:
     1185      |2:
     1186      ]
     1187  ]
     1188
     1189lemma split_elim:
    10711190 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
    10721191  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
     1192  #A #l #m #v #P #hyp
     1193  normalize
     1194  <(split_prod A l m v ? ? ?)
    10731195
    10741196example half_add_SO:
     
    11101232  | cons hd tl ⇒
    11111233    let 〈new_pc, byte〉 ≝ next code_memory pc in
    1112       hd = byte ∧ encoding_check code_memory new_pc final_pc tl
     1234      hd = byte ∧ encoding_check code_memory new_c final_pc tl
    11131235  ].
    11141236
  • src/RTLabs/RTLAbstoRTL.ma

    r799 r1045  
    2727    match fresh LabelTag (rtl_if_luniverse def) with
    2828    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    29     | Error ⇒ None ?
     29    | Error _ ⇒ None ?
    3030    ].
    3131
     
    917917  ].
    918918
     919axiom translate_op2:
     920  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
     921
    919922definition translate_cond2 ≝
    920923  λop2.
     
    926929  λdef.
    927930  match op2 with
     931  [ op_cmp cmp ⇒
     932    match cmp with
     933    [ Compare_Equal ⇒
     934      let srcr1 ≝ extract_singleton ? srcrs1 in
     935      match srcr1 with
     936      [ None ⇒ None ?
     937      | Some srcr1 ⇒
     938        let srcr2 ≝ extract_singleton ? srcrs2 in
     939        match srcr2 with
     940        [ None ⇒ None ?
     941        | Some srcr2 ⇒
     942          let 〈def, tmpr〉 ≝ fresh_reg def in
     943          adds_graph [
     944            rtl_st_clear_carry start_lbl;
     945            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
     946            rtl_st_cond_acc tmpr lbl_false lbl_true
     947          ] start_lbl start_lbl def
     948        ]
     949      ]
     950    | _ ⇒
     951      let n ≝ length ? srcrs1 + length ? srcrs2 in
     952      match size_of_op2_ret n op2 with
     953      [ None ⇒ None ?
     954      | Some size ⇒
     955        let 〈def, destrs〉 ≝ fresh_regs def size in
     956        let lbl ≝ fresh_label def in
     957        match lbl with
     958        [ None ⇒ None ?
     959        | Some lbl ⇒
     960          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
     961          [ None ⇒ None ?
     962          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
     963          ]
     964        ]
     965      ]
     966    ]
     967  | _ ⇒
     968    let n ≝ length ? srcrs1 + length ? srcrs2 in
     969    match size_of_op2_ret n op2 with
     970    [ None ⇒ None ?
     971    | Some size ⇒
     972      let 〈def, destrs〉 ≝ fresh_regs def size in
     973      let lbl ≝ fresh_label def in
     974      match lbl with
     975      [ None ⇒ None ?
     976      | Some lbl ⇒
     977        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
     978        [ None ⇒ None ?
     979        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
     980        ]
     981      ]
     982    ]
     983  ].
     984
     985let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
     986                           (destr2: ?) (start_lbl: label)
     987                           (dest_lbl: label) (def: rtl_internal_function) ≝
     988  let destrs ≝ [ destr1; destr2 ] in
     989  match mode with
     990  [ Aindexed off ⇒
     991    let srcr12 ≝ extract_singleton ? args in
     992    match srcr12 with
     993    [ None ⇒ None ?
     994    | Some srcr12 ⇒
     995      let srcr12 ≝ extract_pair ? srcr12 in
     996      match srcr12 with
     997      [ None ⇒ None ?
     998      | Some srcr12 ⇒
     999        let 〈srcr1, srcr2〉 ≝ srcr12 in
     1000        let 〈def, tmpr〉 ≝ fresh_reg def in
     1001        add_translates [
     1002          adds_graph [
     1003            rtl_st_int tmpr off start_lbl
     1004          ];
     1005          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
     1006        ] start_lbl dest_lbl def
     1007      ]
     1008    ]
     1009  | Aindexed2 ⇒
     1010    let args_pair ≝ extract_pair ? args in
     1011    match args_pair with
     1012    [ None ⇒ None ?
     1013    | Some args_pair ⇒
     1014      let 〈lft, rgt〉 ≝ args_pair in
     1015      let srcr1112 ≝ extract_pair ? lft in
     1016      let srcr2 ≝ extract_singleton ? rgt in
     1017      match srcr1112 with
     1018      [ None ⇒
     1019        let srcr2 ≝ extract_singleton ? rgt in
     1020        let srcr1112 ≝ extract_pair ? lft in
     1021        match srcr2 with
     1022        [ None ⇒ None ?
     1023        | Some srcr2 ⇒
     1024          match srcr1112 with
     1025          [ None ⇒ None ?
     1026          | Some srcr1112 ⇒
     1027            let 〈srcr11, srcr12〉 ≝ srcr1112 in
     1028            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
     1029          ]
     1030        ]
     1031      | Some srcr1112 ⇒
     1032        let 〈srcr11, srcr12〉 ≝ srcr1112 in
     1033        match srcr2 with
     1034        [ None ⇒ None ?
     1035        | Some srcr2 ⇒
     1036          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
     1037        ]
     1038      ]
     1039    ]
     1040  | Aglobal x off ⇒
     1041    let 〈def, tmpr〉 ≝ fresh_reg def in
     1042    add_translates [
     1043      adds_graph [
     1044        rtl_st_int tmpr off start_lbl;
     1045        rtl_st_addr destr1 destr2 x start_lbl
     1046      ];
     1047      translate_op2 op_addp destrs destrs [ tmpr ]
     1048    ] start_lbl dest_lbl def
     1049  | Abased x off ⇒
     1050    let srcrs ≝ extract_singleton ? args in
     1051    match srcrs with
     1052    [ None ⇒ None ?
     1053    | Some srcrs ⇒
     1054      let 〈def, tmpr1〉 ≝ fresh_reg def in
     1055      let 〈def, tmpr2〉 ≝ fresh_reg def in
     1056      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
     1057      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
     1058      let address_unfold ≝
     1059        let 〈def, tmpr〉 ≝ fresh_reg def in
     1060          add_translates [
     1061            adds_graph [
     1062              rtl_st_int tmpr off start_lbl;
     1063              rtl_st_addr tmpr1 tmpr2 x start_lbl
     1064           ];
     1065            translate_op2 op_addp destrs destrs [ tmpr ]
     1066         ]
     1067      in
     1068      add_translates [
     1069        address_unfold;
     1070        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
     1071      ] start_lbl dest_lbl def
     1072    ]
     1073  | Ainstack off ⇒
     1074    let 〈def, tmpr〉 ≝ fresh_reg def in
     1075    add_translates [
     1076      adds_graph [
     1077        rtl_st_int tmpr off start_lbl;
     1078        rtl_st_stack_addr destr1 destr2 start_lbl
     1079      ];
     1080      translate_op2 op_addp destrs destrs [ tmpr ]
     1081    ] start_lbl dest_lbl def
     1082  | _ ⇒ None ? (* wrong number of arguments *)
     1083  ].
     1084
     1085definition translate_load ≝
     1086  λq.
     1087  λmode.
     1088  λargs.
     1089  λdestrs.
     1090  λstart_lbl: label.
     1091  λdest_lbl: label.
     1092  λdef.
     1093  match q with
    9281094  [
    929   ]
    930 
    931 let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def =
    932   match op2, srcrs1, srcrs2 with
    933 
    934     | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] ->
     1095  ].
     1096
     1097let translate_load q mode args destrs start_lbl dest_lbl def =
     1098  match q, destrs with
     1099
     1100    | Memory.QInt 1, [destr] ->
     1101      let (def, addr1) = fresh_reg def in
     1102      let (def, addr2) = fresh_reg def in
     1103      add_translates
     1104        [addressing_pointer mode args addr1 addr2 ;
     1105         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
     1106        start_lbl dest_lbl def
     1107
     1108    | Memory.QPtr, [destr1 ; destr2] ->
     1109      let (def, addr1) = fresh_reg def in
     1110      let (def, addr2) = fresh_reg def in
     1111      let addr = [addr1 ; addr2] in
    9351112      let (def, tmpr) = fresh_reg def in
    936       adds_graph
    937         [RTL.St_clear_carry start_lbl ;
    938          RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ;
    939          RTL.St_condacc (tmpr, lbl_false, lbl_true)]
    940         start_lbl start_lbl def
    941 
    942     | _, _, _ ->
    943       let n = (List.length srcrs1) + (List.length srcrs2) in
    944       let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
    945       let lbl = fresh_label def in
    946       let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in
    947       translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
     1113      add_translates
     1114        [addressing_pointer mode args addr1 addr2 ;
     1115         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
     1116                     RTL.St_int (tmpr, 1, start_lbl)] ;
     1117         translate_op2 AST.Op_addp addr addr [tmpr] ;
     1118         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
     1119        start_lbl dest_lbl def
     1120
     1121    | _ -> error "Size error in load."
  • src/RTLabs/syntax.ma

    r888 r1045  
    1010include "common/Graphs.ma".
    1111
    12 (* Statements, including the label of successor(s). *)
     12definition immediate : Type[0] ≝ Byte.
     13
     14(* Addressing modes *)
     15
     16inductive addressing : Type[0] ≝
     17(* dpm: changed from int to Byte *)
     18| Aindexed  : immediate → addressing         (* r1 + offset *)
     19| Aindexed2 : addressing                     (* r1 + r2 *)
     20| Aglobal   : ident → immediate → addressing (* global + offset *)
     21| Abased    : ident → immediate → addressing (* global + offset + r1 *)
     22| Ainstack  : immediate → addressing         (* stack + offset *)
     23.
     24
     25definition addr_mode_args : addressing → nat ≝
     26λa. match a with
     27[ Aindexed _  ⇒ 1
     28| Aindexed2   ⇒ 2
     29| Aglobal _ _ ⇒ 0
     30| Abased _ _  ⇒ 1
     31| Ainstack _  ⇒ 0
     32].
     33
     34definition addr ≝ λm.Vector register (addr_mode_args m).
    1335
    1436inductive statement : Type[0] ≝
  • src/common/AST.ma

    r985 r1045  
    6969#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
    7070try ( @Ptrue // )
    71 @Pfalse % #E destruct;
     71@Pfalse % #E destruct
    7272qed.
    7373
     
    274274
    275275definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    276   map ?? (fst ident F) (prog_funct ?? p).
     276  map ? ? (fst ident F) (prog_funct ?? p).
    277277
    278278definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
     
    594594
    595595
    596 
    597596(* Partially merged stuff derived from the prototype cerco compiler. *)
    598597
     598(*
    599599definition bool_to_Prop ≝
    600600 λb. match b with [ true ⇒ True | false ⇒ False ].
    601601
    602602coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     603*)
    603604
    604605(* dpm: should go to standard library *)
Note: See TracChangeset for help on using the changeset viewer.