formatted code

alcides · Mar 2, 2024 · e8fc23f · e8fc23f
1 parent 0af82b9
commit e8fc23f
Show file tree

Hide file tree

Showing 5 changed files with 36 additions and 15 deletions.
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -35,7 +35,6 @@ repos:
     hooks:
       - id: ruff
         args: [--fix, --exit-zero]
-      - id: ruff-format
   - repo: https://github.com/regebro/pyroma
     rev: "4.2"
     hooks:

diff --git a/examples/PSB2/solved/basement.ae b/examples/PSB2/solved/basement.ae
@@ -2,9 +2,9 @@ type List;
 
 def List_size: (l:List) -> Int = uninterpreted;
 
-def List_new : {x:List | List_size(x) == 0} = native "[]" ;
+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_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]";

diff --git a/examples/PSB2/solved/shopping.ae b/examples/PSB2/solved/shopping.ae
@@ -3,8 +3,8 @@ 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 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_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)" ;

diff --git a/libraries/List.ae b/libraries/List.ae
@@ -4,13 +4,13 @@ def functools : Bottom = native_import "functools";
 
 def List_size: (l:List) -> Int = uninterpreted;
 
-def List_new : {x:List | List_size(x) == 0} = native "[]" ;
+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_append: (l:List) -> (i: Int) -> {l2:List | List_size l2 == List_size l + 1} = native "lambda xs: lambda x: xs + [x]";
 
 # def List_append: (l:List) -> (i: Int) -> List  = native "lambda xs: lambda x: xs + [x]";
 
-def List_cons: (l:List) -> (i:Int) -> {l2:List | List_size(l2) == (List_size(l) + 1)}  = native "lambda x: lambda xs: [x] + xs";
+def List_cons: (l:List) -> (i:Int) -> {l2:List | List_size l2 == List_size l + 1}  = native "lambda x: lambda xs: [x] + xs";
 
 def List_recursive: (l:List) -> (base:Int) -> (rec:(v:Int) -> (y:Int) -> Int) -> Int = native "lambda l: lambda cb: lambda rec: functools.reduce(lambda seed, next: rec(next)(seed), l, cb)";
 

diff --git a/tests/smt_test.py b/tests/smt_test.py
@@ -19,7 +19,8 @@
     "x",
     t_int,
     LiquidApp("==", [LiquidVar("x"), LiquidLiteralInt(3)]),
-    LiquidConstraint(LiquidApp("==", [LiquidVar("x"), LiquidLiteralInt(3)])),
+    LiquidConstraint(LiquidApp(
+        "==", [LiquidVar("x"), LiquidLiteralInt(3)])),
 )
 
 
@@ -35,7 +36,8 @@ def test_smt_example3():
         "y",
         BaseType("a"),
         LiquidApp("==", [LiquidVar("x"), LiquidVar("y")]),
-        LiquidConstraint(LiquidApp("==", [LiquidVar("x"), LiquidVar("y")])),
+        LiquidConstraint(LiquidApp(
+            "==", [LiquidVar("x"), LiquidVar("y")])),
     ),
 )
 
@@ -44,18 +46,38 @@ def test_other_sorts():
     assert smt_valid(example2)
 
 
-# this test fails with def List_new : {x:List | List_size(x) == 0} ,
-# but with def List_new : {u:List | List_size(u) == 0} works fine
+# this test fails with def List_new : {x:List | List_size x == 0} ,
+# but with def List_new : {u:List | List_size u == 0} works fine
 def test_uninterpreted():
     aeon_code = """
 type List;
 def List_size: (l:List) -> Int = uninterpreted;
 
-def List_new : {x:List | List_size(x) == 0} = native "[]" ;
+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_new : {u:List | List_size(u) == 0} = native "[]" ;
+def main (x:Int) : Unit {
+    empty = List_new;
+    one = List_append empty 3;
+    print(one)
+}"""
+    prog: Program = parse_program(aeon_code)
+    (
+        core_ast,
+        typing_ctx,
+        evaluation_ctx,
+    ) = desugar(prog)
+
+    type_errors = check_type_errors(typing_ctx, core_ast, top)
+    assert len(type_errors) == 0
 
-def List_append: (l:List) -> (i: Int) -> {l2:List | List_size(l2) == (List_size(l) + 1)} = native "lambda xs: lambda x: xs + [x]";
+
+def test_uninterpreted2():
+    aeon_code = """
+type List;
+def List_size: (l:List) -> Int = uninterpreted;
+def List_new : {u:List | List_size u == 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 main (x:Int) : Unit {
     empty = List_new;