finger_trees.mlw 1.86 KB
 Martin Clochard committed May 04, 2015 1 2 `````` module FingerTrees `````` Andrei Paskevich committed Jun 11, 2017 3 `````` `````` Andrei Paskevich committed Jun 15, 2018 4 5 6 7 `````` use int.Int use list.List use list.Length use list.Append `````` Andrei Paskevich committed Jun 11, 2017 8 `````` `````` Martin Clochard committed May 04, 2015 9 10 11 12 13 `````` type digit 'a = | One 'a | Two 'a 'a | Three 'a 'a 'a | Four 'a 'a 'a 'a `````` Andrei Paskevich committed Jun 11, 2017 14 `````` `````` Martin Clochard committed May 04, 2015 15 16 17 18 19 20 `````` function d_m (b:digit 'a) : list 'a = match b with | One x -> Cons x Nil | Two y x -> Cons y (Cons x Nil) | Three z y x -> Cons z (Cons y (Cons x Nil)) | Four u z y x -> Cons u (Cons z (Cons y (Cons x Nil))) end `````` Andrei Paskevich committed Jun 11, 2017 21 `````` `````` Martin Clochard committed May 04, 2015 22 23 24 `````` type node 'a = | Node2 'a 'a | Node3 'a 'a 'a `````` Andrei Paskevich committed Jun 11, 2017 25 `````` `````` Martin Clochard committed May 04, 2015 26 27 28 29 `````` function node_cons (nd:node 'a) (l:list 'a) : list 'a = match nd with | Node2 x y -> Cons x (Cons y l) | Node3 x y z -> Cons x (Cons y (Cons z l)) end `````` Andrei Paskevich committed Jun 11, 2017 30 `````` `````` Martin Clochard committed May 04, 2015 31 32 `````` let lemma node_cons_app (nd:node 'a) (p q:list 'a) ensures { node_cons nd (p++q) = node_cons nd p ++ q } `````` Guillaume Melquiond committed Jan 12, 2018 33 `````` = match nd with Node2 _ _ -> [@keep_on_simp] () | _ -> () end `````` Andrei Paskevich committed Jun 11, 2017 34 `````` `````` Martin Clochard committed May 04, 2015 35 36 37 38 `````` function flatten (l:list (node 'a)) : list 'a = match l with | Nil -> Nil | Cons nd q -> node_cons nd (flatten q) end `````` Andrei Paskevich committed Jun 11, 2017 39 `````` `````` Martin Clochard committed May 04, 2015 40 41 42 43 `````` type t 'a = | Empty | Single (digit 'a) | Deep (digit 'a) (t (node 'a)) (digit 'a) `````` Andrei Paskevich committed Jun 11, 2017 44 `````` `````` Martin Clochard committed May 04, 2015 45 46 47 48 49 `````` function t_m (t:t 'a) : list 'a = match t with | Empty -> Nil | Single x -> d_m x | Deep l m r -> d_m l ++ flatten (t_m m) ++ d_m r end `````` Andrei Paskevich committed Jun 11, 2017 50 `````` `````` Andrei Paskevich committed Jun 07, 2018 51 52 `````` let d_cons (x:'a) (d:digit 'a) : (b: digit 'a, o: list (node 'a)) ensures { Cons x (d_m d) = d_m b ++ flatten o /\ length o <= 1 } `````` Martin Clochard committed May 04, 2015 53 `````` = match d with `````` Andrei Paskevich committed Jun 11, 2017 54 55 56 57 `````` | One y -> Two x y , Nil | Two y z -> Three x y z , Nil | Three y z t -> Four x y z t , Nil | Four y z t u -> Two x y , Cons (Node3 z t u) Nil `````` Martin Clochard committed May 04, 2015 58 `````` end `````` Andrei Paskevich committed Jun 11, 2017 59 `````` `````` Martin Clochard committed May 04, 2015 60 61 62 63 64 65 `````` let rec cons (x:'a) (t:t 'a) : t 'a ensures { t_m result = Cons x (t_m t) } variant { t } = match t with | Empty -> Single (One x) | Single d -> Deep (One x) Empty d `````` Andrei Paskevich committed Jun 11, 2017 66 `````` | Deep lf md rg -> let lf2 , rem = d_cons x lf in `````` Martin Clochard committed May 04, 2015 67 68 69 70 71 72 `````` match rem with | Nil -> Deep lf2 md rg | Cons x q -> assert { q = Nil }; Deep lf2 (cons x md) rg end end `````` Andrei Paskevich committed Jun 11, 2017 73 `````` `````` Martin Clochard committed May 04, 2015 74 75 ``````end ``````