Changeset 777 for src/ASM/Util.ma


Ignore:
Timestamp:
Apr 27, 2011, 5:25:26 PM (9 years ago)
Author:
mulligan
Message:

Lots of work on RTL to ERTL pass from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r764 r777  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4 
     5let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
     6  match n with
     7  [ O ⇒
     8    match l with
     9    [ nil ⇒ [ ]
     10    | cons hd tl ⇒ l
     11    ]
     12  | S n ⇒
     13    match l with
     14    [ nil ⇒ [ ]
     15    | cons hd tl ⇒
     16      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
     17    ]
     18  ].
     19 
     20definition nub_by ≝
     21  λA: Type[0].
     22  λf: A → A → bool.
     23  λl: list A.
     24    nub_by_internal A f l (length ? l).
     25 
     26let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
     27  match l with
     28  [ nil ⇒ false
     29  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
     30  ].
     31 
     32let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
     33  match n with
     34  [ O ⇒ [ ]
     35  | S n ⇒
     36    match l with
     37    [ nil ⇒ [ ]
     38    | cons hd tl ⇒ hd :: take A n tl
     39    ]
     40  ].
     41 
     42let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
     43  match n with
     44  [ O ⇒ l
     45  | S n ⇒
     46    match l with
     47    [ nil ⇒ [ ]
     48    | cons hd tl ⇒ drop A n tl
     49    ]
     50  ].
     51 
     52definition list_split ≝
     53  λA: Type[0].
     54  λn: nat.
     55  λl: list A.
     56    〈take A n l, drop A n l〉.
     57 
     58let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
     59                      (l: list A) on l: list B ≝
     60  match l with
     61  [ nil ⇒ nil ?
     62  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
     63  ]. 
     64
     65definition mapi ≝
     66  λA, B: Type[0].
     67  λf: nat → A → B.
     68  λl: list A.
     69    mapi_internal A B 0 f l.
     70
     71let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
     72  match l with
     73  [ nil ⇒ Some ? (nil (A × B))
     74  | cons hd tl ⇒
     75    match r with
     76    [ nil ⇒ None ?
     77    | cons hd' tl' ⇒
     78      match zip ? ? tl tl' with
     79      [ None ⇒ None ?
     80      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
     81      ]
     82    ]
     83  ].
    484
    585let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
Note: See TracChangeset for help on using the changeset viewer.