examples updated

examples/PSB2/annotations/basement.ae

@@ -16,16 +16,17 @@ def accumulate_prefix_sum: (l:List)-> (i:Int) -> List = \l -> \i ->
       List_append(List_append(List_new)(get_fst(l)+get_snd(l)))(get_snd(l))
 ;
 
-
 def aeon_reduce: (function: (a: List) -> (b: Int) -> List) -> (l: List) -> (l2: List) -> List = native "lambda f: lambda xs: lambda ys: __import__('functools').reduce(f, xs, ys)";
 
 def basement (nums: List) : Int {
     get_snd(
-        aeon_reduce
-            accumulate_prefix_sum
-            (nums)
-            (List_append (List_append List_new 0) 0)
+        aeon_reduce(accumulate_prefix_sum) (nums) (List_append (List_append List_new 0) 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) ))
+}
+
 #TypeError: eval.<locals>.v() takes 1 positional argument but 2 were given

examples/PSB2/annotations/coin_sum.ae

@@ -16,3 +16,7 @@ def coin_sum (cents: Int) : List {
   pennies:Int = ((cents % 25) % 10) % 5;
   List_append(List_append (List_append ( List_append(List_new)(quarters)) (dimes)) (nickels))(pennies)
  }
+
+ def main (args:Int): Unit {
+    print( coin_sum(5))
+    }

examples/PSB2/annotations/fuel_cost.ae

@@ -1,13 +1,22 @@
 type List;
 
+def List_size: (l:List) -> Int = uninterpreted;
+def List_length: (l:List) -> Int = native "lambda list: len(list)";
+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 sum: (l:List) -> Int = native "lambda xs: sum(xs)";
 def Math_max : (i:Int) -> (j:Int) -> Int = native "lambda i: lambda j: max(i,j)" ;
 def Math_floor_division : (i:Int) -> (j:Int)-> Int = native "lambda i: lambda j: i // j" ;
 
-def map_Int_Int_List: (function:(a: Int) -> Int) -> (l: List) -> List = native "lambda f, xs: map(f, xs)";
+def map_Int_Int_List: (function:(a: Int) -> Int) -> (l: List) -> List = native "lambda f:lambda xs: map(f, xs)";
 
 def fuel_cost  (xs: List) : Int {
  sum(
     map_Int_Int_List (( \x -> Math_max (Math_floor_division(x)(3) - 2)(0)) : (x: Int) -> Int) (xs)
     )
  }
+
+def main (args:Int) : Unit {
+    print(fuel_cost(List_append(List_append(List_new)(1))(9)))
+}

examples/PSB2/annotations/paired_digits.ae

@@ -13,14 +13,14 @@ def filter :  (f: (s:String) -> Bool) -> (l:List) -> List = native "lambda f: la
 def filter2 :  (f: (s:String) -> Bool) -> (l:List) -> List = native "lambda f: lambda xs: filter(f, xs)";
 
 def sum: (l:List) -> Int = native "lambda xs: sum(xs)";
-def map_String_Int_List: (function:(a: String) -> Int) -> (l: List) -> List = native "lambda f, xs: map(f, xs)";
+def map_String_Int_List: (function:(a: String) -> Int) -> (l: List) -> List = native "lambda f: lambda xs: map(f, xs)";
 
 def paired_digits (nums: String) : Int {
     pairs: List = String_to_List(String_zip (nums)(String_slice(nums)(1)(String_len(nums))));
-    matching_pairs : List = filter2 ((\x -> get_fst(x) == get_snd(x)):((x:String) -> Bool)) (pairs);
+    matching_pairs : List = filter2 ((\x -> get_fst(x) == get_snd(x)):((x:String) -> Bool)) (pairs); # z3.z3types.Z3Exception: sort mismatch
     total_sum : Int = sum(map_String_Int_List ((\x -> String_to_Int(get_fst(x))) : (x: String) -> Int) (matching_pairs));
     total_sum
  }
-
-# Type not freshable: ?t <class 'aeon.core.types.TypeVar'> [FIXED]
-# z3.z3types.Z3Exception: sort mismatch
+def main (args:Int) : Unit {
+    print (paired_digits("99"))
+}

examples/PSB2/annotations/shopping.ae

@@ -1,15 +1,28 @@
 type List;
+type Map;
+
+def List_size: (l:List) -> Int = uninterpreted;
+def List_length: (l:List) -> Int = native "lambda list: len(list)";
+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 sum: (l:List) -> Int = native "lambda xs: sum(xs)";
 def Math_max : (i:Int) -> (j:Int) -> Int = native "lambda i: lambda j: max(i,j)" ;
 def Math_floor_division : (i:Int) -> (j:Int)-> Int = native "lambda i: lambda j: i // j" ;
-def map_Int_Int_Int_List_List: (function: (a: Int) -> (b: Int) -> Int) -> (l: List) -> (l2: List) -> List = native "lambda f, xs: map(f, xs)";
+def Map_Int_Int_Int_List_List: (function: (a: Int) -> (b: Int) -> Int) -> (l: List) -> (l2: List) -> Map = native "lambda f: lambda xs: map(f, xs)";
+def Map_to_list: (m: Map) -> List = native "lambda m: list(m)";
 
 def shopping  (prices: List, discounts: List) : Int {
- sum(
-    map_Int_Int_Int_List_List
-        (( \x -> (\y -> x * (1 - y / 100))): (x:Int) -> (y:Int) -> Int) (prices) (discounts)
-    )
+    m: Map= Map_Int_Int_Int_List_List(( \x -> (\y -> x * (1 - y / 100))): (x:Int) -> (y:Int) -> Int) (prices) (discounts);
+    l: List = Map_to_list(m);
+    sum(l)
+
  }
 
-# Type not freshable: ?t <class 'aeon.core.types.TypeVar'>
+def main (args:Int) : Unit {
+    l1: List = List_append(List_append(List_new) (50)) (0);
+    l2: List = List_append(List_append(List_new) (10)) (0);
+    print (shopping(l1)(l2))
+}
+
+# TypeError: 'map' object is not callable