Changeset 1635


Ignore:
Timestamp:
Jan 7, 2012, 12:33:17 AM (8 years ago)
Author:
tranquil
Message:
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
Files:
11 added
5 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1590 r1635  
    285285  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
    286286    MiscPottier.reduce destrs_rest srcrs_rest in
    287   let (def, tmpr) = fresh_reg def in
    288287  let carry_init = match op with
    289288    | I8051.Sub | I8051.Addc ->
  • src/ASM/BitVector.ma

    r1599 r1635  
    5757  λm, n: nat.
    5858  λb: BitVector n. pad_vector ? false m n b.
    59      
     59 
     60let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
     61  match n with
     62  [ O ⇒ VEmpty ?
     63  | S n' ⇒
     64    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
     65  ].
     66 
     67let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
     68  match b with
     69  [ VEmpty ⇒ 0
     70  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
     71
    6072(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    6173(* Other manipulations.                                                       *)
  • src/ASM/I8051.ma

    r1600 r1635  
    2020inductive Op1: Type[0] ≝
    2121  Cmpl: Op1
    22 | Inc: Op1.
     22| Inc: Op1
     23| Rl: Op1. (* TODO: implement left rotation *)
    2324
    2425inductive Op2: Type[0] ≝
  • src/common/Graphs.ma

    r1515 r1635  
    3636    lookup ? ? (add ? ? g l s) l ≠ None ?.
    3737
     38axiom graph_add_eq:
     39  ∀A: Type[0].
     40  ∀g: graph A.
     41  ∀l: label.
     42  ∀s: A.
     43    lookup ? ? (add ? ? g l s) l = Some ? s.
     44
    3845axiom graph_add_lookup:
    3946  ∀A: Type[0].
     
    4350  ∀to_insert: label.
    4451    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
     52   
     53axiom graph_add_preserve :
     54  ∀A: Type[0].
     55  ∀g: graph A.
     56  ∀l: label.
     57  ∀s: A.
     58  ∀to_insert: label.
     59  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
    4560
    4661axiom graph_num_nodes:
  • src/common/Identifiers.ma

    r1631 r1635  
    4040  〈id',u'〉 = fresh tag u →
    4141  fresh_for_univ tag id u'.
    42 #tag * #id * #id' * #u * #u' normalize #H #E destruct /2/
     42#tag * #id * #id' * #u * #u' normalize #H #E destruct /2 by le_S/
    4343qed.
    4444
     
    4747  〈id',u'〉 = fresh tag u →
    4848  id ≠ id'.
    49 #tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2/
     49#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 by absurd/
    5050qed.
    5151
     
    5959  env_fresh_for_univ tag A (〈id,a〉::env) u'.
    6060#tag #A #env * #u * #u' #id #a
    61 #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
     61#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 by fresh_remains_fresh/ ]
    6262qed.
    6363
     
    7777#P #t * #x * #y #T #F
    7878change with (P (eqb ??))
    79 @(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
     79@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
    8080qed.
    8181   
     
    9898
    9999lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
    100 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
     100#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 by not_to_not/
    101101qed.
    102102
     
    105105#E [ % | %2 ]
    106106lapply E @eqb_elim
    107 [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
     107[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 by absurd/ ]
    108108qed.
    109109
     
    123123#tag #A #l elim l
    124124[ //
    125 | * #id #a #tl #IH #r * #H1 #H2 % /2/
     125| * #id #a #tl #IH #r * #H1 #H2 % /2 by All_append_l/
    126126] qed.
    127127
     
    129129#tag #A #l elim l
    130130[ //
    131 | * #id #a #tl #IH #r * #H1 #H2 /2/
     131| * #id #a #tl #IH #r * #H1 #H2 /2 by /
    132132] qed.
    133133
     
    202202  lookup tag A (add tag A m j a) i = lookup tag A m i.
    203203#tag #A * #m * #i * #j #a #H
    204 @lookup_opt_insert_miss /2/
     204@lookup_opt_insert_miss /2 by not_to_not/
    205205qed.
    206206
     
    224224cases (identifier_eq ? i j)
    225225[ #E >E >lookup_add_hit #H %1 destruct % //
    226 | #NE >lookup_add_miss /2/
     226| #NE >lookup_add_miss /2 by or_intror, sym_not_eq/
    227227] qed.
    228228
     
    328328#FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
    329329generalize in ⊢ ((?(??%?) → ?) → ??%?); *
    330 [ // | #a #H @False_ind lapply (H ?) /2/ % #E destruct
     330[ // | #a #H @False_ind lapply (H ?) /2 by absurd/ % #E destruct
    331331qed.
    332332
Note: See TracChangeset for help on using the changeset viewer.