Inline more

khoek · Nov 13, 2018 · fc7c836 · fc7c836
1 parent 8316c16
commit fc7c836
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/src/tidy/lib/table.lean b/src/tidy/lib/table.lean
@@ -3,7 +3,7 @@ import .array
 
 universes u v w z
 
-attribute [inline] bool.decidable_eq option.is_some
+attribute [inline] bool.decidable_eq option.is_some option.is_none list.head
 attribute [inline] array.read array.write
 
 def table_ref : Type := ℕ

diff --git a/src/tidy/rewrite_search/metric/edit_distance.lean b/src/tidy/rewrite_search/metric/edit_distance.lean
@@ -20,7 +20,7 @@ structure ed_partial :=
 def compute_initial_distances_aux (weights : table dnum) : dnum → list table_ref → list dnum
 | _ [] := []
 | so_far (a :: rest) :=
-  let so_far := so_far + (get_weight weights a) in
+  let so_far := so_far + (weights.iget a) in
   list.cons so_far (compute_initial_distances_aux so_far rest)
 
 @[inline] def compute_initial_distances (weights : table dnum) (l : list table_ref) : list dnum :=
@@ -35,20 +35,20 @@ p.distances.zip ((list.cons p.prefix_length p.distances).zip l₂)
 universe u
 
 --TODO explain me
-meta def fold_fn (weights : table dnum) (h : table_ref) (n : dnum × list dnum) : dnum × dnum × table_ref → dnum × list dnum
+@[inline] meta def fold_fn (weights : table dnum) (h : table_ref) (n : dnum × list dnum) : dnum × dnum × table_ref → dnum × list dnum
 | (a, b, r) :=
   let m := if h = r then b else dnum.minl [
-    /- deletion     -/ a + (get_weight weights r),
-    /- substitution -/ b + dnum.max (get_weight weights r) (get_weight weights h),
-    /- insertion    -/ n.2.head + (get_weight weights h)
+    /- deletion     -/ a + (weights.iget r),
+    /- substitution -/ b + dnum.max (weights.iget r) (weights.iget h),
+    /- insertion    -/ n.2.head + (weights.iget h)
   ] in (dnum.min m n.1, list.cons m n.2)
 
 --TODO explain me
 @[inline] meta def improve_bound_once (weights : table dnum) (l r : list table_ref) (cur : dnum) (p : ed_partial) : bound_progress ed_partial :=
   match p.suffix with
     | [] := exactly p.distances.ilast p
     | (h :: t) :=
-      let new_prefix_length := p.prefix_length + (get_weight weights h) in
+      let new_prefix_length := p.prefix_length + (weights.iget h) in
       let initial : dnum × list dnum := (new_prefix_length, [new_prefix_length]) in
       let new_distances : dnum × list dnum := (triples p r).foldl (fold_fn weights h) initial in
       at_least new_distances.1 ⟨ new_prefix_length, t, new_distances.2.reverse.drop 1 ⟩