source: src/utilities/bindLists.ma @ 2896

Last change on this file since 2896 was 2155, checked in by tranquil, 7 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
Line 
1include "utilities/bind_new.ma".
2
3definition bind_list ≝ λB,E.bind_new B (list E).
4
5coercion blist_from_list :
6  ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??.
7
8unification hint 0 ≔ B,E;
9Es ≟ list E
10(*--------------------------*)⊢
11bind_list B E ≡ bind_new B Es.
12
13definition bappend : ∀B,E.bind_list B E → bind_list B E →
14  bind_list B E ≝ λB,E. m_bin_op … (append ?).
15
16include "ASM/Vector.ma".
17interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2).
18
19definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
20  λB,E,e.m_map … (cons … e).
21interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
22
23include "utilities/lists.ma".
24 
25theorem bcompile_append :
26  ∀U, R, E, fresh, bl1, bl2.
27  (bcompile U R (list E) fresh (bl1 @@ bl2)) ≅
28  (
29  ! l1 ← bcompile … fresh bl1 ;
30  ! l2 ← bcompile … fresh bl2 ;
31  return (l1 @ l2)
32  ).
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).
44      #U#R#E#fresh#e#bl2 #u @bcompile_bbind
45qed.
Note: See TracBrowser for help on using the repository browser.