Changeset 1062


Ignore:
Timestamp:
Jul 11, 2011, 2:09:03 PM (8 years ago)
Author:
mulligan
Message:

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/FoldStuff.ma

    r1014 r1062  
    1 (* RUSSEL **)
    2 
    3 include "basics/jmeq.ma".
    4 include "basics/types.ma".
    5 include "basics/list.ma".
    6 
    7 notation > "hvbox(a break ≃ b)"
    8   non associative with precedence 45
    9 for @{ 'jmeq ? $a ? $b }.
    10 
    11 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
    12   non associative with precedence 45
    13 for @{ 'jmeq $t $a $u $b }.
    14 
    15 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
    16 
    17 lemma eq_to_jmeq:
    18   ∀A: Type[0].
    19   ∀x, y: A.
    20     x = y → x ≃ y.
    21   //
    22 qed.
    23 
    24 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
    25 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
    26 
    27 coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
    28 coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
    29 
    30 (*axiom VOID: Type[0].
    31 axiom assert_false: VOID.
    32 definition bigbang: ∀A:Type[0].False → VOID → A.
    33  #A #abs cases abs
    34 qed.
    35 
    36 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
    37 
    38 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
    39  #A #P #p cases p #w #q @q
    40 qed.
    41 
    42 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
    43  #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
    44 qed.
    45 
    46 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
    47 
    48 (* END RUSSELL **)
    49 
    501include "ASM/Util.ma".
     2include "ASM/JMCoercions.ma".
    513
    524let rec foldl_strong_internal
  • src/ASM/Util.ma

    r1061 r1062  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4
     5include "ASM/JMCoercions.ma".
    46
    57(* let's implement a daemon not used by automation *)
     
    1214 with precedence 10
    1315for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     16
     17definition hd ≝
     18  λA: Type[0].
     19  λl: list A.
     20  λproof: 0 < |l|.
     21  match l return λx. 0 < |x| → A with
     22  [ nil ⇒ λnil_absrd. ?
     23  | cons hd tl ⇒ λcons_prf. hd
     24  ].
     25  normalize in nil_absrd;
     26  cases(not_le_Sn_O 0)
     27  #HYP
     28  cases(HYP nil_absrd)
     29qed.
     30
     31definition tail ≝
     32  λA: Type[0].
     33  λl: list A.
     34  λproof: 0 < |l|.
     35  match l return λx. 0 < |x| → list A with
     36  [ nil ⇒ λnil_absrd. ?
     37  | cons hd tl ⇒ λcons_prf. tl
     38  ].
     39  normalize in nil_absrd;
     40  cases(not_le_Sn_O 0)
     41  #HYP
     42  cases(HYP nil_absrd)
     43qed.
     44
     45let rec split
     46  (A: Type[0]) (l: list A) (index: nat) (proof: index < |l|)
     47    on index ≝
     48  match index return λx. x < |l| → (list A) × (list A) with
     49  [ O ⇒ λzero_prf. 〈[], l〉
     50  | S index' ⇒ λsucc_prf.
     51    match l return λx. S index' < |x| → (list A) × (list A) with
     52    [ nil ⇒ λnil_absrd. ?
     53    | cons hd tl ⇒ λcons_prf.
     54      let 〈l1, l2〉 ≝ split A tl index' ? in
     55        〈hd :: l1, l2〉
     56    ] succ_prf
     57  ] proof.
     58  [1: normalize in nil_absrd;
     59      cases(not_le_Sn_O (S index'))
     60      #HYP
     61      cases(HYP nil_absrd)
     62  |2: normalize in cons_prf;
     63      normalize
     64      @le_S_S_to_le
     65      assumption
     66  ]
     67qed.
    1468
    1569let rec nth_safe
     
    67121  ].
    68122
     123(*
    69124axiom reduce_strong:
    70125  ∀A: Type[0].
     
    72127  ∀right: list A.
    73128    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
    74 
    75 (*
     129*)
     130
     131include "ASM/FoldStuff.ma".
     132
    76133let rec reduce_strong
    77   (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left ≝
     134  (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left
     135  : Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |  ≝
    78136  match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    79137  [ nil ⇒
     
    86144    [ nil ⇒ λcons_nil_absrd_prf. ?
    87145    | cons hd' tl' ⇒ λcons_cons_prf.
    88       let tail_call ≝ reduce_strong A tl tl' ? in ?
     146      let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (*
     147      [ dp clr their_proof ⇒ ? (*
     148        let 〈commonl, commonr〉 ≝ clr in ? *)
     149      ]*)
    89150    ]
    90151  ] prf.
     
    96157  | 3: normalize in cons_nil_absrd_prf;
    97158       destruct(cons_nil_absrd_prf)
     159  | 4:
    98160  ]
    99 qed.
    100 *)   
     161qed.
    101162 
    102163axiom reduce_length:
  • src/RTLabs/RTLAbstoRTL.ma

    r1061 r1062  
    33include "common/AssocList.ma".
    44include "common/Graphs.ma".
    5 (* include "common/IntValue.ma". *)
    65include "common/FrontEndOps.ma".
    76
     
    463462  λdest_lbl.
    464463  λdef.
    465   λprf: | destrs | = | srcrs |.
     464  λprf: |destrs| = |srcrs|.
    466465  match op1 with
    467466  [ intermediate_op1_cast src_size src_sign dest_size ⇒
     
    523522    ]
    524523  ].
    525   [ 1: @third_reduced_proof
    526   | 3: @first_reduced_proof
    527  
    528 let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    529   let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
    530     MiscPottier.reduce srcrs1 srcrs2 in
    531   let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
    532   let ((destrs_common, destrs_rest), _) =
    533     MiscPottier.reduce destrs srcrs1_common in
    534   let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
    535     MiscPottier.reduce destrs_rest srcrs_rest in
    536   let (def, tmpr) = fresh_reg def in
    537   let insts_init =
    538     [RTL.St_clear_carry start_lbl ;
    539      RTL.St_int (tmpr, 0, start_lbl)] in
    540   let f_add destr srcr1 srcr2 =
    541     RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
    542   let insts_add =
    543     MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
    544   let f_add_cted destr srcr =
    545     RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
    546   let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
    547   let f_rest destr =
    548     RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
    549   let insts_rest = List.map f_rest destrs_rest in
    550   adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
    551     start_lbl dest_lbl def
     524cases not_implemented (* problem here with lengths of lists: possible bug? *)
     525qed.
     526
     527let rec translate_mul1
     528  (dummy: register) (tmpr: register) (destrs: list register)
     529  (srcrs1: list register) (srcr2: register) (start_lbl: label)
     530    on srcrs1 ≝
     531  match destrs with
     532  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
     533  | cons destr tl ⇒
     534    match tl with
     535    [ nil ⇒
     536      match srcrs1 with
     537      [ nil ⇒
     538        adds_graph [
     539          rtl_st_int tmpr (zero ?) start_lbl;
     540          rtl_st_op2 Addc destr destr tmpr start_lbl
     541        ] start_lbl
     542      | cons srcr1 tl' ⇒
     543        adds_graph [
     544          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
     545          rtl_st_op2 Addc destr destr tmpr start_lbl
     546        ] start_lbl
     547      ]
     548    | cons destr2 destrs ⇒
     549      match srcrs1 with
     550      [ nil ⇒
     551        add_translates [
     552          adds_graph [
     553            rtl_st_int tmpr (zero ?) start_lbl;
     554            rtl_st_op2 Addc destr destr tmpr start_lbl;
     555            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     556          ];
     557          translate_cst (Ointconst I8 (zero ?)) destrs
     558        ] start_lbl
     559      | cons srcr1 srcrs1 ⇒
     560        match destrs with
     561        [ nil ⇒
     562          add_translates [
     563            adds_graph [
     564              rtl_st_int tmpr (zero ?) start_lbl;
     565              rtl_st_op2 Addc destr destr tmpr start_lbl;
     566              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     567            ];
     568            translate_cst (Ointconst I8 (zero ?)) destrs
     569          ] start_lbl
     570        | cons destr2 destrs ⇒
     571          add_translates [
     572            adds_graph [
     573              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
     574              rtl_st_op2 Addc destr destr tmpr start_lbl
     575            ];
     576            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
     577          ] start_lbl
     578        ]
     579      ]
     580    ]
     581  ].
     582
     583definition translate_muli ≝
     584  λdummy: register.
     585  λtmpr: register.
     586  λdestrs: list register.
     587  λtmp_destrs: list register.
     588  λsrcrs1: list register.
     589  λdummy_lbl: label.
     590  λi: nat.
     591  λtranslates.
     592  λsrcr2i.
     593  let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?.
     594
     595let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
     596    srcr2i =
     597  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
     598  translates @
     599    (match tmp_destrs2 with
     600      | [] -> []
     601      | tmp_destr2 :: tmp_destrs2 ->
     602        [adds_graph [RTL.St_clear_carry dummy_lbl ;
     603                     RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
     604         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
     605         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
     606         adds_graph [RTL.St_clear_carry dummy_lbl] ;
     607         translate_op I8051.Addc destrs destrs tmp_destrs])
    552608
    553609definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.