Merge pull request #52 from alcides/psb2

PSB2 examples

examples/PSB2/annotations/multi_objective/basement.ae

@@ -5,18 +5,10 @@ import calculate_basement_errors from "PSB2.ae";
 type List;
 
 def List_size: (l:List) -> Int = uninterpreted;
+def List_len: (l:List) -> Int  = native "lambda x: len(x)";
 def List_new : {x:List | List_size x == 0} = native "[]" ;
 def List_append: (l:List) -> (i: Int) -> {l2:List | List_size l2 == List_size l + 1} = native "lambda xs: lambda x: xs + [x]";
-
-def get_fst: (l:List) -> Int = native "lambda xs: xs[0]";
-def get_snd: (l:List) -> Int = native "lambda xs: xs[1]";
-
-def accumulate_prefix_sum: (l:List)-> (i:Int) -> List = \l -> \i ->
-    extra : Int = if get_fst l + get_snd l >= 0 then 1 else 0;
-    List_append (List_append List_new (get_fst l + get_snd l)) (get_snd l + extra)
-;
-
-def aeon_reduce: (function: (a: List) -> (b: Int) -> List) -> (l: List) -> (l2: List) -> List = native "lambda f: lambda xs: lambda ys: __import__('functools').reduce(lambda x, y:f(x)(y), xs, ys)";
+def List_get: (l:List) -> (i: Int) -> Int = native"lambda xs: lambda i: xs[i]";
 
 
 #PSB2 functions
@@ -27,6 +19,7 @@ def train: TrainData = extract_train_data (load_dataset "basement" 200 200);
             load_dataset,
             train,
             calculate_basement_errors)
+@allow_recursion
 @multi_minimize_float(calculate_basement_errors train synth)
 def synth (nums: List) : Int {
     (?hole : Int)

examples/PSB2/annotations/multi_objective/bouncing_balls.ae

@@ -2,8 +2,6 @@ import "Math.ae";
 
 import extract_train_data from "PSB2.ae";
 import load_dataset from "PSB2.ae";
-#import get_input_list_llist_llist from "PSB2.ae";
-
 
 type List;
 

examples/PSB2/annotations/multi_objective/bowling.ae

@@ -33,57 +33,12 @@ def const2 : String = "/";
 
 def train: TrainData = extract_train_data (load_dataset "bowling" 200 200);
 
-def input_list : List = get_input_list (unpack_train_data train);
-
-def expected_values : List = get_output_list (unpack_train_data train);
 
 @hide(extract_train_data,
-            get_input_list,
-            get_output_list,
-            unpack_train_data,
             load_dataset,
             train,
-            input_list,
-            expected_values,
-            get_bowling_synth_values,
-            calculate_list_errors)
-@multi_minimize_float(calculate_list_errors (get_bowling_synth_values input_list synth) expected_values)
+            calculate_bowling_errors)
+@multi_minimize_float(calculate_bowling_errors train synth)
 def synth (scores: String) : Int {
-    #(?hole: Int)
- 1}
-
-
-def create_mapper (scores:String) (i:Int) : Int {
-    current : String = String_get scores i;
-    next : String = String_get scores (i+1);
-    if String_eq current "X" then
-        next_frame1 : String = String_get scores (i+2);
-        next_frame2 : String = String_get scores (i+3);
-        if String_eq next_frame2 "/" then
-            20
-        else if String_eq next_frame1 "X" then
-            next_next_frame1 : String = String_get scores (i+4);
-            inc : Int = if String_eq next_next_frame1 "X" then 10 else String_to_int next_next_frame1;
-            20 + inc
-        else
-            10 + String_to_int next_frame1 + String_to_int next_frame2
-
-    else if String_eq next "/" then
-        10 + String_to_int (String_get scores (i+2))
-    else
-        String_to_int current + String_to_int next
-}
-
-
-def bowling_score (scores: String) : Int {
-    scores_right_size = String_replace scores "X" "X_";
-    scores_zero = String_replace scores_right_size "-" "0";
-    r : List = List_range_step 0 20 2;
-    mapper : (i:Int) -> Int = create_mapper scores_zero;
-    components : List = List_map mapper r;
-    List_sum components
+    (?hole: Int)
  }
-
-def main (scores: Int) : Unit {
-    print (calculate_bowling_errors train bowling_score)
-}

examples/PSB2/solved/basement.ae

@@ -1,28 +1,25 @@
 type List;
 
 def List_size: (l:List) -> Int = uninterpreted;
-
+def List_len: (l:List) -> Int  = native "lambda x: len(x)";
 def List_new : {x:List | List_size x == 0} = native "[]" ;
-
 def List_append: (l:List) -> (i: Int) -> {l2:List | List_size l2 == List_size l + 1} = native "lambda xs: lambda x: xs + [x]";
+def List_get: (l:List) -> (i: Int) -> Int = native"lambda xs: lambda i: xs[i]";
 
-def get_fst: (l:List) -> Int = native "lambda xs: xs[0]";
-def get_snd: (l:List) -> Int = native "lambda xs: xs[1]";
-
-def accumulate_prefix_sum: (l:List)-> (i:Int) -> List = \l -> \i ->
-    extra : Int = if get_fst l + get_snd l >= 0 then 1 else 0;
-    List_append (List_append List_new (get_fst l + get_snd l)) (get_snd l + extra)
-;
-
-def aeon_reduce: (function: (a: List) -> (b: Int) -> List) -> (l: List) -> (l2: List) -> List = native "lambda f: lambda xs: lambda ys: __import__('functools').reduce(lambda x, y:f(x)(y), xs, ys)";
+def fst_negative (l:List) (i:Int)(u:Int) : Int {
+    if (i >= (List_len l)) then
+        i
+     else if (u < 0) then
+        i
+     else
+        fst_negative l (i + 1) (u + (List_get l (i + 1)))
+     }
 
 def basement (nums: List) : Int {
-    get_snd (
-        aeon_reduce accumulate_prefix_sum nums (List_append (List_append List_new 0) 0)
-        )
- }
+     fst_negative nums 0 (List_get nums 0)
+     }
 
 
 def main (args:Int): Unit {
-    print (aeon_reduce (accumulate_prefix_sum) (List_append List_new 0) (List_append (List_append List_new 0) 0 ))
+    print (basement (List_append List_new (-100)) )
 }

examples/PSB2/solved/bouncing_balls.ae

@@ -5,9 +5,9 @@ def calculate_distance_helper (b_index: Float) (h: Float) (n: Int) (distance: Fl
 if isZero n then
     distance
 else
-    a: Float = b_index *. h;
+    a: Float = h /. b_index;
     n1: Int = n - 1;
-    d1: Float = distance +. h +. b_index *. h;
+    d1: Float = (distance +. h) +. a;
     calculate_distance_helper b_index a n1 d1
 }
 
@@ -18,5 +18,5 @@ def bouncing_balls (s_height: Float) (b_height:Float) (b:Int) : Float{
 
 
 def main (x: Int) : Unit {
-    print(bouncing_balls 60.567 37.053 1)
+    print(bouncing_balls 15.319 5.635 1) # 20.954
  }

examples/PSB2/solved/bowling.ae

@@ -17,6 +17,17 @@ def String_eq : (s:String) -> (s2:String) -> Bool = native "lambda s: lambda s2:
 
 def List_range_step : (start:Int) -> (end:Int) -> (step:Int) -> List = native "lambda s: lambda e: lambda st: list(range(s, e, st))";
 
+ def convert_bowling(score: String) : Int {
+ if String_eq score "X" then
+    10
+ else
+    if String_eq score "/" then
+        10
+    else
+        String_to_int score
+ }
+
+
 def create_mapper (scores:String) (i:Int) : Int {
     current : String = String_get scores i;
     next : String = String_get scores (i+1);
@@ -30,12 +41,13 @@ def create_mapper (scores:String) (i:Int) : Int {
             inc : Int = if String_eq next_next_frame1 "X" then 10 else String_to_int next_next_frame1;
             20 + inc
         else
-            10 + String_to_int next_frame1 + String_to_int next_frame2
+            10 + convert_bowling next_frame1 + convert_bowling next_frame2
 
     else if String_eq next "/" then
-        10 + String_to_int (String_get scores (i+2))
+        next_next : String = String_get scores (i+2);
+        10 + (convert_bowling next_next)
     else
-        String_to_int current + String_to_int next
+        String_to_int current + convert_bowling next
 }
 
 

run_examples.sh

@@ -36,7 +36,7 @@ do
 done
 
 # TODO: add pbt PSB2
-for folder in ffi image imports list syntax synthesis;
+for folder in ffi image imports list syntax synthesis "PSB2/solved";
 do
     for entry in examples/$folder/*.ae
     do