source: src/utilities/bindLists.ma @ 2919

Last change on this file since 2919 was 2155, checked in by tranquil, 8 years ago

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File size: 1.3 KB
RevLine 
[1882]1include "utilities/bind_new.ma".
[1635]2
[1882]3definition bind_list ≝ λB,E.bind_new B (list E).
[1635]4
[1647]5coercion blist_from_list :
[1882]6  ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??.
[1635]7
[1882]8unification hint 0 ≔ B,E;
9Es ≟ list E
10(*--------------------------*)⊢
11bind_list B E ≡ bind_new B Es.
[1635]12
[1882]13definition bappend : ∀B,E.bind_list B E → bind_list B E →
14  bind_list B E ≝ λB,E. m_bin_op … (append ?).
[1635]15
[1882]16include "ASM/Vector.ma".
17interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2).
[1635]18
[1882]19definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
[2155]20  λB,E,e.m_map … (cons … e).
[1882]21interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
[1635]22
[1882]23include "utilities/lists.ma".
[1635]24 
25theorem bcompile_append :
[1882]26  ∀U, R, E, fresh, bl1, bl2.
27  (bcompile U R (list E) fresh (bl1 @@ bl2)) ≅
[1635]28  (
29  ! l1 ← bcompile … fresh bl1 ;
30  ! l2 ← bcompile … fresh bl2 ;
31  return (l1 @ l2)
32  ).
[1882]33  #U#R#E#fresh#bl1#bl2
34  #u >bcompile_bbind normalize @pair_elim
35  #u' #l' normalize @pair_elim
36  #u'' #l'' normalize >bcompile_bbind #EQ #EQ'
37  normalize >EQ normalize //
38qed.
39
40theorem bcompile_cons :
41  ∀U, R, E, fresh, e, bl2.
42  (bcompile U R (list E) fresh (e ::: bl2)) ≅
43    ! l ← bcompile … fresh bl2 ; return (e :: l).
[2155]44      #U#R#E#fresh#e#bl2 #u @bcompile_bbind
[1635]45qed.
Note: See TracBrowser for help on using the repository browser.