diff --git a/.github/workflows/python-app.yml b/.github/workflows/python-app.yml index 708b534b..a64f966b 100644 --- a/.github/workflows/python-app.yml +++ b/.github/workflows/python-app.yml @@ -50,17 +50,20 @@ jobs: run: | files=$(find examples/core -type f -name '*_main.ae') for file in $files; do + echo "Running $file" python aeon $file --core --log INFO ERROR TYPECHECKER CONSTRAINT done - name: Run Aeon Sugar Files run: | files=$(find examples/sugar -type f -name '*_main.ae') for file in $files; do + echo "Running $file" python aeon $file --log INFO ERROR TYPECHECKER CONSTRAINT done - name: Run PSB2 Solved Problems run: | files=$(find examples/PSB2/solved -type f -name '*.ae') for file in $files; do + echo "Running $file" python aeon $file --log INFO ERROR TYPECHECKER CONSTRAINT done diff --git a/Readme.md b/Readme.md index 6ed9b1a3..31130d57 100644 --- a/Readme.md +++ b/Readme.md @@ -40,7 +40,7 @@ def abs (i:Int) : Int { if i > 0 then i else -i } -def midpoint(a:Int, b:Int) : Int { +def midpoint (a:In) (b:Int) : Int { (a + b) / 2 } diff --git a/aeon/sugar/aeon_sugar.lark b/aeon/sugar/aeon_sugar.lark index 7da5dbb0..32fbf486 100644 --- a/aeon/sugar/aeon_sugar.lark +++ b/aeon/sugar/aeon_sugar.lark @@ -12,7 +12,7 @@ defs : def* -> list type_decl : "type" TYPENAME ";" -> type_decl def : (soft_constraint)* "def" ID ":" type "=" expression ";" -> def_cons - | (soft_constraint)* "def" ID "(" args ")" ":" type "{" expression "}" -> def_fun + | (soft_constraint)* "def" ID args ":" type "{" expression "}" -> def_fun soft_constraint : "@" ID "(" macro_args ")" -> macro @@ -21,9 +21,18 @@ macro_args : -> empty_list args : -> empty_list - | arg ("," arg)* -> args + | arg (arg)* -> args -arg : ID ":" type -> arg +arg : "(" ID ":" type ")" -> arg + | "(" ID ":" type _PIPE expression ")" -> refined_arg + + +type : "{" ID ":" type _PIPE expression "}" -> refined_t // TODO delete later + | "(" ID ":" type ")" "->" type -> abstraction_t + | "(" ID ":" type _PIPE expression ")" "->" type -> abstraction_refined_t + | "forall" ID ":" kind "," type -> polymorphism_t // TODO: desugar + | ID -> simple_t + | "(" type ")" -> same expression : "-" expression_i -> minus @@ -84,11 +93,6 @@ expression_simple : "(" expression ")" -> same | ID -> var | "?" ID -> hole -type : "{" ID ":" type _PIPE expression "}" -> refined_t - | "(" ID ":" type ")" "->" type -> abstraction_t - | "forall" ID ":" kind "," type -> polymorphism_t // TODO: desugar - | ID -> simple_t - | "(" type ")" -> same kind : "B" -> base_kind | "*" -> star_kind diff --git a/aeon/sugar/parser.py b/aeon/sugar/parser.py index 55e215b8..f5fe4108 100644 --- a/aeon/sugar/parser.py +++ b/aeon/sugar/parser.py @@ -6,9 +6,10 @@ from lark import Lark from lark import Tree +from aeon.core.substitutions import liquefy from aeon.core.terms import Abstraction from aeon.core.terms import Annotation -from aeon.core.types import AbstractionType +from aeon.core.types import AbstractionType, RefinedType from aeon.core.types import TypeVar from aeon.frontend.parser import TreeToCore from aeon.sugar.program import Decorator @@ -19,6 +20,7 @@ class TreeToSugar(TreeToCore): + def list(self, args): return args @@ -67,6 +69,13 @@ def args(self, args): def arg(self, args): return (args[0], args[1]) + def refined_arg(self, args): + return args[0], RefinedType(args[0], args[1], liquefy(args[2])) + + def abstraction_refined_t(self, args): + type = RefinedType(args[0], args[1], liquefy(args[2])) + return AbstractionType(str(args[0]), type, args[3]) + def abstraction_et(self, args): return Annotation( Abstraction(args[0], args[2]), diff --git a/aeon/sugar/program.py b/aeon/sugar/program.py index ddd2a94f..981c3585 100644 --- a/aeon/sugar/program.py +++ b/aeon/sugar/program.py @@ -54,7 +54,7 @@ def __repr__(self): return f"def {self.name} : {self.type} = {self.body};" else: args = ", ".join([f"{n}:{t}" for (n, t) in self.args]) - return f"def {self.name} ({args}) -> {self.type} {{\n {self.body} \n}}" + return f"def {self.name} {args} -> {self.type} {{\n {self.body} \n}}" @dataclass diff --git a/aeon/typechecking/typeinfer.py b/aeon/typechecking/typeinfer.py index 8a757861..91accf01 100644 --- a/aeon/typechecking/typeinfer.py +++ b/aeon/typechecking/typeinfer.py @@ -3,7 +3,7 @@ from loguru import logger from aeon.core.instantiation import type_substitution -from aeon.core.liquid import LiquidApp +from aeon.core.liquid import LiquidApp, LiquidHole from aeon.core.liquid import LiquidLiteralBool from aeon.core.liquid import LiquidLiteralFloat from aeon.core.liquid import LiquidLiteralInt @@ -28,16 +28,16 @@ from aeon.core.types import BaseKind from aeon.core.types import BaseType from aeon.core.types import RefinedType -from aeon.core.types import t_bool -from aeon.core.types import t_float -from aeon.core.types import t_int -from aeon.core.types import t_unit from aeon.core.types import Type from aeon.core.types import TypePolymorphism from aeon.core.types import TypeVar from aeon.core.types import args_size_of_type from aeon.core.types import bottom from aeon.core.types import extract_parts +from aeon.core.types import t_bool +from aeon.core.types import t_float +from aeon.core.types import t_int +from aeon.core.types import t_unit from aeon.core.types import type_free_term_vars from aeon.prelude.prelude import ( INTEGER_ARITHMETIC_OPERATORS, @@ -77,10 +77,14 @@ def __str__(self): def argument_is_typevar(ty: Type): - return (isinstance(ty, TypeVar) or isinstance( - ty, - RefinedType, - ) and isinstance(ty.type, TypeVar)) + return ( + isinstance(ty, TypeVar) + or isinstance( + ty, + RefinedType, + ) + and isinstance(ty.type, TypeVar) + ) def prim_litbool(t: bool) -> RefinedType: @@ -154,6 +158,46 @@ def prim_op(t: str) -> Type: ) +def rename_liquid_term(refinement, old_name, new_name): + if isinstance(refinement, LiquidVar): + if refinement.name == old_name: + return LiquidVar(new_name) + else: + return refinement + elif isinstance(refinement, LiquidLiteralBool): + return refinement + elif isinstance(refinement, LiquidLiteralInt): + return refinement + elif isinstance(refinement, LiquidLiteralFloat): + return refinement + elif isinstance(refinement, LiquidApp): + return LiquidApp( + refinement.fun, + [rename_liquid_term(x, old_name, new_name) for x in refinement.args], + ) + elif isinstance(refinement, LiquidHole): + if refinement.name == old_name: + return LiquidHole( + new_name, + [(rename_liquid_term(x, old_name, new_name), t) for (x, t) in refinement.argtypes], + ) + else: + return LiquidHole( + refinement.name, + [(rename_liquid_term(x, old_name, new_name), t) for (x, t) in refinement.argtypes], + ) + else: + assert False + + +def renamed_refined_type(ty: RefinedType) -> RefinedType: + old_name = ty.name + new_name = "_inner_" + old_name + + refinement = rename_liquid_term(ty.refinement, old_name, new_name) + return RefinedType(new_name, ty.type, refinement) + + # patterm matching term def synth(ctx: TypingContext, t: Term) -> tuple[Constraint, Type]: if isinstance(t, Literal) and t.type == t_unit: @@ -178,8 +222,9 @@ def synth(ctx: TypingContext, t: Term) -> tuple[Constraint, Type]: ty = ctx.type_of(t.name) if isinstance(ty, BaseType) or isinstance(ty, RefinedType): ty = ensure_refined(ty) - assert ty.name != t.name - # TODO if the names are equal , we must replace it for another variable + # assert ty.name != t.name + if ty.name == t.name: + ty = renamed_refined_type(ty) # Self ty = RefinedType( ty.name, @@ -200,7 +245,8 @@ def synth(ctx: TypingContext, t: Term) -> tuple[Constraint, Type]: ) if not ty: raise CouldNotGenerateConstraintException( - f"Variable {t.name} not in context", ) + f"Variable {t.name} not in context", + ) return (ctrue, ty) elif isinstance(t, Application): (c, ty) = synth(ctx, t.fun) @@ -222,7 +268,8 @@ def synth(ctx: TypingContext, t: Term) -> tuple[Constraint, Type]: return (c0, t_subs) else: raise CouldNotGenerateConstraintException( - f"Application {t} is not a function.", ) + f"Application {t} is not a function.", + ) elif isinstance(t, Let): (c1, t1) = synth(ctx, t.var_value) nctx: TypingContext = ctx.with_var(t.var_name, t1) @@ -298,8 +345,8 @@ def check_(ctx: TypingContext, t: Term, ty: Type) -> Constraint: @wrap_checks # DEMO1 def check(ctx: TypingContext, t: Term, ty: Type) -> Constraint: if isinstance(t, Abstraction) and isinstance( - ty, - AbstractionType, + ty, + AbstractionType, ): # ??? (\__equal_1__ -> (let _anf_1 = (== _anf_1) in(_anf_1 __equal_1__))) , basetype INT ret = substitution_in_type(ty.type, Var(t.var_name), ty.var_name) c = check(ctx.with_var(t.var_name, ty.var_type), t.body, ret) @@ -325,7 +372,8 @@ def check(ctx: TypingContext, t: Term, ty: Type) -> Constraint: assert liq_cond is not None if not check_type(ctx, t.cond, t_bool): raise CouldNotGenerateConstraintException( - "If condition not boolean", ) + "If condition not boolean", + ) c0 = check(ctx, t.cond, t_bool) c1 = implication_constraint( y, diff --git a/examples/PSB2/annotations/multi_objective/gcd.ae b/examples/PSB2/annotations/multi_objective/gcd.ae index d692785c..316250d6 100644 --- a/examples/PSB2/annotations/multi_objective/gcd.ae +++ b/examples/PSB2/annotations/multi_objective/gcd.ae @@ -4,8 +4,8 @@ # output : integer import PSB2; -def gcd ( n:Int, z:Int) : Int { - if z == 0 then n else (gcd(z)(n % z)) +def gcd (n:Int) (z:Int) : Int { + if z == 0 then n else gcd z (n % z) } def train: TrainData = extract_train_data (load_dataset "gcd" 200 200); @@ -13,7 +13,7 @@ def input_list : List = get_input_list (unpack_train_data train); def expected_values : List = get_output_list (unpack_train_data train); @multi_minimize_float( calculate_list_errors (get_gcd_synth_values input_list synth) (expected_values)) -def synth ( n:Int, z:Int) : Int { +def synth (n:Int) (z:Int) : Int { (?hole:Int) } # def largest_common_divisor ( n :{x:Int | 1 <= x && x <= 1000000}, m :{y:Int | 1 <= y && y <= 1000000}) : Int { gcd n m } diff --git a/examples/PSB2/annotations/single_objective/gcd.ae b/examples/PSB2/annotations/single_objective/gcd.ae index c66b2fd4..11e18221 100644 --- a/examples/PSB2/annotations/single_objective/gcd.ae +++ b/examples/PSB2/annotations/single_objective/gcd.ae @@ -4,7 +4,7 @@ # output : integer import PSB2; -def gcd ( n:Int, z:Int) : Int { +def gcd (n:Int) (z:Int) : Int { if z == 0 then n else (gcd(z)(n % z)) } @@ -13,7 +13,7 @@ def input_list : List = get_input_list ( unpack_train_data train); def expected_values : List = get_output_list ( unpack_train_data train); @minimize_float( mean_absolute_error ( get_gcd_synth_values input_list synth) ( expected_values)) -def synth ( n:Int, z:Int) : Int { +def synth (n:Int) (z:Int) : Int { (?hole:Int) } # def largest_common_divisor ( n :{x:Int | 1 <= x && x <= 1000000}, m :{y:Int | 1 <= y && y <= 1000000}) : Int { gcd n m } diff --git a/examples/PSB2/non_working/gcd.ae b/examples/PSB2/non_working/gcd.ae index 04dfb228..28578138 100644 --- a/examples/PSB2/non_working/gcd.ae +++ b/examples/PSB2/non_working/gcd.ae @@ -5,11 +5,11 @@ # --not- working - recursion problem-- # RecursionError: maximum recursion depth exceeded in comparison -def gcd ( n:Int, z:Int) : Int { - if z == 0 then n else (gcd(z)(n % z)) +def gcd (n:Int) (z:Int) : Int { + if z == 0 then n else gcd z (n % z) } -def synth_gcd ( n:Int, z:Int) : Int { +def synth_gcd (n:Int) (z:Int) : Int { (?hole:Int) } # def largest_common_divisor ( n :{x:Int | 1 <= x && x <= 1000000}, m :{y:Int | 1 <= y && y <= 1000000}) : Int { gcd n m } diff --git a/examples/PSB2/solved/bouncing_balls.ae b/examples/PSB2/solved/bouncing_balls.ae index 86215538..a6055286 100644 --- a/examples/PSB2/solved/bouncing_balls.ae +++ b/examples/PSB2/solved/bouncing_balls.ae @@ -1,7 +1,7 @@ def isZero : (n: Int) -> Bool = \n -> n == 0; -def calculate_distance_helper (b_index: Float, h: Float, n: Int, distance: Float) : Float { +def calculate_distance_helper (b_index: Float) (h: Float) (n: Int) (distance: Float) : Float { if isZero n then distance else @@ -11,7 +11,7 @@ else calculate_distance_helper b_index a n1 d1 } -def bouncing_balls (s_height: Float, b_height:Float , b:Int) : Float{ +def bouncing_balls (s_height: Float) (b_height:Float) (b:Int) : Float{ bounciness_index : Float = s_height /. b_height; calculate_distance_helper bounciness_index s_height b 0.0 } diff --git a/examples/PSB2/solved/bowling.ae b/examples/PSB2/solved/bowling.ae index 38a551cf..b8937b2f 100644 --- a/examples/PSB2/solved/bowling.ae +++ b/examples/PSB2/solved/bowling.ae @@ -17,7 +17,7 @@ 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 create_mapper (scores:String, i:Int) : Int { +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 diff --git a/examples/PSB2/solved/dice_game.ae b/examples/PSB2/solved/dice_game.ae index bbc46f12..3461849c 100644 --- a/examples/PSB2/solved/dice_game.ae +++ b/examples/PSB2/solved/dice_game.ae @@ -4,11 +4,11 @@ def math : Unit = native_import "math"; def Math_toFloat : (i:Int) -> Float = native "lambda i: float(i)" ; def Math_max : (i:Int) -> (j:Int) -> Int = native "lambda i: lambda j: max(i,j)" ; -def peter_wins (n:Int, m:Int) : Int { +def peter_wins (n:Int) (m:Int) : Int { if m == 0 then 0 else Math_max 0 (n - m) + peter_wins n (m - 1) } -def dice_game (n:{x:Int | 1 <= x && x <= 10000}, m:{y:Int | 1 <= y && y <= 10000}) : Float { +def dice_game (n:Int | 1 <= n && n <= 10000) (m:Int | 1 <= m && m <= 10000) : Float { a : Float = Math_toFloat (peter_wins n m); b : Float = Math_toFloat (n * m); c : Float = a /. b; diff --git a/examples/PSB2/solved/find_pair.ae b/examples/PSB2/solved/find_pair.ae index aa4e28a4..c243eb21 100644 --- a/examples/PSB2/solved/find_pair.ae +++ b/examples/PSB2/solved/find_pair.ae @@ -16,7 +16,7 @@ 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]"; #assuming that the list always has at least 2 elements that sum to the target -def find_pair (numbers: List, target: Int) : List { +def find_pair (numbers: List) (target: Int) : List { pairs : List = combinations numbers 2; pred : (s:List) -> Bool = \pair -> List_sum pair == target; matching_pairs : List = List_filter pred pairs; diff --git a/examples/PSB2/solved/gcd.ae b/examples/PSB2/solved/gcd.ae index eb44f0ac..fb17a4e8 100644 --- a/examples/PSB2/solved/gcd.ae +++ b/examples/PSB2/solved/gcd.ae @@ -1,4 +1,4 @@ -def gcd (n:Int, z:Int) : Int { +def gcd (n:Int) (z:Int) : Int { if z == 0 then n else gcd z (n % z) } diff --git a/examples/PSB2/solved/indices_of_substring.ae b/examples/PSB2/solved/indices_of_substring.ae index fe04150a..7ec3d0e4 100644 --- a/examples/PSB2/solved/indices_of_substring.ae +++ b/examples/PSB2/solved/indices_of_substring.ae @@ -10,7 +10,7 @@ def String_equal : (i:String) -> (j:String) -> Bool = native "lambda i: lambda j def String_slice : (i:String) -> (j:Int) -> (l:Int)-> String = native "lambda i: lambda j: lambda l: i[j:l]" ; -def indices_of_substring ( text :String, target: String) : List { +def indices_of_substring ( text :String) (target: String) : List { start: Int = 0; end: Int = (String_len text) - (String_len target) + 1 ; step: Int = 1; diff --git a/examples/PSB2/solved/luhn.ae b/examples/PSB2/solved/luhn.ae index 78782960..4166575b 100644 --- a/examples/PSB2/solved/luhn.ae +++ b/examples/PSB2/solved/luhn.ae @@ -21,7 +21,7 @@ def Range_new : (a:Int) -> (b:Int) -> Range = native "lambda a: lambda b: range( def even : (n:Int) -> Bool = \n -> n % 2 == 0; -def map_digit (x:Int, i:Int) : Int { +def map_digit (x:Int) (i:Int) : Int { if i % 2 != 0 then ( if x * 2 > 9 then (x*2 - 9) else (x*2) : Int) else x } diff --git a/examples/PSB2/solved/mastermind.ae b/examples/PSB2/solved/mastermind.ae index 0301c9ae..8799f145 100644 --- a/examples/PSB2/solved/mastermind.ae +++ b/examples/PSB2/solved/mastermind.ae @@ -21,7 +21,7 @@ def Counter_intersection : (c1:Counter) -> (c2:Counter) -> Counter = native "lam def Counter_values : (c:Counter) -> List = native "lambda c: list(c.values())"; def Tuple : (a:Int) -> (b:Int) -> List = native "lambda a: lambda b: [a,b]"; -def mastermind ( code : String, guess: String ) : List { +def mastermind ( code : String) (guess: String ) : List { items_eq : (x:List) -> Int = \x -> if String_eq (List_get_fst x) (List_get_snd x) then 1 else 0; black_map : List = Map_bool items_eq (String_Zip code guess); black_pegs : Int = List_sum black_map; diff --git a/examples/PSB2/solved/shopping.ae b/examples/PSB2/solved/shopping.ae index b53cb979..6812cbf1 100644 --- a/examples/PSB2/solved/shopping.ae +++ b/examples/PSB2/solved/shopping.ae @@ -16,7 +16,7 @@ def List_map_Int_Int_Int_List: (function: (a: Int) -> (b: Int) -> Int) -> List = native "lambda f: lambda xs: lambda ys: list(map(lambda x, y: f(x)(y), xs, ys))"; -def shopping (prices: List, discounts: List) : Int { +def shopping (prices: List) (discounts: List) : Int { f: (x:Int) -> (y:Int) -> Int = \x -> \y -> x * (1 - y / 100); l: List = List_map_Int_Int_Int_List f prices discounts; List_sum l diff --git a/examples/PSB2/solved/snow_day.ae b/examples/PSB2/solved/snow_day.ae index b374b912..cac3bdb7 100644 --- a/examples/PSB2/solved/snow_day.ae +++ b/examples/PSB2/solved/snow_day.ae @@ -1,6 +1,6 @@ def isZero : (n: Int) -> Bool = \n -> n == 0; -def snow_day ( n: Int, m: Float, t: Float, p: Float) : Float { +def snow_day ( n: Int) ( m: Float) (t: Float) (p: Float) : Float { if isZero 0 then m else diff --git a/examples/PSB2/solved/substitution_cipher.ae b/examples/PSB2/solved/substitution_cipher.ae index f9eec583..17445565 100644 --- a/examples/PSB2/solved/substitution_cipher.ae +++ b/examples/PSB2/solved/substitution_cipher.ae @@ -10,7 +10,7 @@ def Dict_get : (d: Dict) -> (k: String) -> (default: String) -> String = native def Map_String_String: (function: (a:String) -> String) -> (l: String) -> List = native "lambda f:lambda xs: map(f, xs)"; -def cipher (cipher_from: String, cypher_to: String, msg: String) : String { +def cipher (cipher_from: String) ( cypher_to: String) (msg: String) : String { cipher_dict: Dict = Dict_zip (Zip_String_String cipher_from cypher_to); mapper : (x:String) -> String = \x -> Dict_get cipher_dict x x; deciphered_chars: List = Map_String_String mapper msg; diff --git a/examples/PSB2/solved/vector_distance.ae b/examples/PSB2/solved/vector_distance.ae index 390a365d..b90a0347 100644 --- a/examples/PSB2/solved/vector_distance.ae +++ b/examples/PSB2/solved/vector_distance.ae @@ -21,7 +21,7 @@ def List_append_float: (l:List) -> (i: Float) -> {l2:List | List_size l2 == List -def vector_distance (vector1: List, vector2: List) : Float { +def vector_distance (vector1: List) (vector2: List) : Float { mapper : (x:Float) -> (y:Float) -> Float = \x -> \y -> Math_pow_Float (x -. y) 2.0; squared_diffs: List = Map_Float_Float_Float_List_List mapper vector1 vector2; distance = Math_sqrt_Float (List_sum_Float squared_diffs); diff --git a/examples/image/mona.ae b/examples/image/mona.ae deleted file mode 100644 index fd743f20..00000000 --- a/examples/image/mona.ae +++ /dev/null @@ -1,50 +0,0 @@ -import Image; - -def monaLisa : (Image) = Image_load2("examples/sugar/mona.jpg"); - -def random_int_color: {x:Int | 0 <= x && x <= 255} = native "__import__('random').randint(0, 255)"; - -def random_x_coord: Int = native " __import__('random').randint(0, 732)"; -def random_y_coord: Int = native "__import__('random').randint(0, 1024)"; - -#def random_x_coord:(img:Image) -> {x:Int | (x >= 0) && (x <= Image_width(img))} = native " __import__('random').randint(0, 732)"; -#def random_y_coord:(img:Image) -> {y:Int | (y >= 0) && (y <= Image_height(img))} = native "__import__('random').randint(0, 1024)"; - -def random_x1_coord: (x1:Int)-> Int= native "lambda min: __import__('random').randint(min, 732)"; -def random_y1_coord: (y1:Int)-> Int = native "lambda min: __import__('random').randint(min, 1024)"; - -#def random_x1_coord:(img:Image) -> (x1:Int)-> {x:Int | (x >= 0) && (x <= Image_width(img))} = native "lambda min: __import__('random').randint(min, 732)"; -#def random_y1_coord:(img:Image) -> (y1:Int)-> {y:Int | (y >= 0) && (y <= Image_height(img))} = native "lambda min: __import__('random').randint(min, 1024)"; - - -# 732 width, 1024 height - -def canvas : (Image) = (Image_create(732)(1024)); - -def draw : (ImageDraw) = Image_draw(canvas); - -def random_color: (Color) = (Image_makeColor(random_int_color)(random_int_color)(random_int_color)); - - -#def random_coord: (Coordinate) = (Image_makeCoordinate(canvas)(random_x_coord(canvas))(random_y_coord(canvas))(random_x1_coord(canvas)(random_x_coord(canvas)))(random_y1_coord(canvas)(random_y_coord(canvas)))); - -def random_coord: (Coordinate) = (Image_makeCoordinate(canvas)(random_x_coord)(random_y_coord)(random_x1_coord(random_x_coord))(random_y1_coord(random_y_coord))); - - -#def random_rect: ImageDraw= (Image_draw_rectangle(canvas)(random_coord)(random_color)); - -def random_rect: ImageDraw= (Image_draw_rectangle(draw)(random_coord)(random_color)); - -def random_rect2:(x:ImageDraw) -> ImageDraw= \x -> (Image_draw_rectangle(x)(random_coord)(random_color)); - - -def multiple_random_rectangles(count: Int, img:ImageDraw) : ImageDraw { - if (count <= 0 ) then (img) - else (multiple_random_rectangles(c-1)(random_rect2(img))) - -} - - -def multiple_random_rectangles2:(count: Int)-> (x:ImageDraw) -> ImageDraw = -\c -> \img -> if (c <= 0 ) then (img) - else (multiple_random_rectangles2(c-1)(random_rect2(img))); diff --git a/examples/image/mona.jpg b/examples/image/mona.jpg deleted file mode 100644 index f1bb17e3..00000000 Binary files a/examples/image/mona.jpg and /dev/null differ diff --git a/examples/sugar/function_main.ae b/examples/sugar/function_main.ae index e357a76a..17b49b74 100644 --- a/examples/sugar/function_main.ae +++ b/examples/sugar/function_main.ae @@ -1,6 +1,8 @@ def ff : (z:Int) -> (f: (a:{n:Int | 1 <= n && n <= 10000}) ->( b:{m:Int | 0 <=m} ) -> Int ) -> Int = \b-> \a-> b+ a(2)(3); #def fff : (z:Int) -> (f: (a:{n:Int | 0 <=n}) ->( b:{m:Int | 0 <=m} ) -> Int ) -> Int = native "lambda a: lambda b: a+ b(2)(3)"; -def fff : (z:Int) -> (f: (a:{n:Int | 1 <= n && n <= 10000}) ->( b:{m:Int | 0 <=m} ) -> Int ) -> Int = \b-> \a-> b+ a(2)(3); +def fff : (z:Int) -> (f: (a:{k:Int | 1 <= k && k <= 10000}) ->( b:{m:Int | 0 <=m} ) -> Int ) -> Int = \b-> \a-> b+ a(2)(3); +def fff : (z:Int) -> (f: (a:Int | 1 <= a && a <= 10000) -> ( b:Int | 0 <=b) -> Int ) -> Int = \b-> \a-> b+ a(2)(3); + #def fff : (z:Int) -> (f: (a:Int) ->( b:Int ) -> Int ) -> Int = \x -> \y -> x + y; #def fff : (z:Int) -> (f: (u:Int) ->( i:Int ) -> Int ) -> Int = native "lambda a: lambda b: a+ b(2)(3)"; diff --git a/examples/sugar/liquid_types_main.ae b/examples/sugar/liquid_types_main.ae index e32cdfb5..f50e578f 100644 --- a/examples/sugar/liquid_types_main.ae +++ b/examples/sugar/liquid_types_main.ae @@ -1,4 +1,5 @@ def sqrt : (i: {x:Int | x > 0} ) -> Float = native "__import__('math').sqrt"; +def sqrt : (i:Int | i > 0) -> Float = native "__import__('math').sqrt"; def main (i:Int) : Unit { print (sqrt 25) diff --git a/examples/sugar/math_example_main.ae b/examples/sugar/math_example_main.ae index 7dc67012..5af6b006 100644 --- a/examples/sugar/math_example_main.ae +++ b/examples/sugar/math_example_main.ae @@ -2,7 +2,7 @@ def abs (i:Int) : Int { if i > 0 then i else -i } -def midpoint(a:Int, b:Int) : Int { +def midpoint(a:Int) (b:Int) : Int { (a + b) / 2 } diff --git a/examples/sugar/test_list_main.ae b/examples/sugar/test_list_main.ae index 83b6d5cc..200e4b69 100644 --- a/examples/sugar/test_list_main.ae +++ b/examples/sugar/test_list_main.ae @@ -1,5 +1,6 @@ import List; def consume : (l: {x:List | List_size x == 1}) -> Int = \n -> 0; +def consume : (l:List | List_size l == 1) -> Int = \n -> 0; # def neg1 : Int = consume(List_new); diff --git a/examples/sugar/vector_main.ae b/examples/sugar/vector_main.ae index 64a1ee17..f219c3bd 100644 --- a/examples/sugar/vector_main.ae +++ b/examples/sugar/vector_main.ae @@ -10,7 +10,7 @@ def List_cons : (v:Int) -> def List_extract_from_singleton : - (l: {l:List | List_length l == 1}) -> + (l:List | List_length l == 1) -> Int = native "lambda l: l[0]"; def main (i:Int) : Unit { diff --git a/tests/liquid_test.py b/tests/liquid_test.py index 3011a6ee..d069c85b 100644 --- a/tests/liquid_test.py +++ b/tests/liquid_test.py @@ -6,8 +6,18 @@ from aeon.core.substitutions import liquefy from aeon.core.terms import Application from aeon.core.terms import Var +from aeon.core.types import top +from aeon.sugar.desugar import desugar +from aeon.sugar.parser import parse_program +from aeon.typechecking.typeinfer import check_type from aeon.utils.ast_helpers import i1 + +def check_compile(source, ty, res): + p, ctx, ectx = desugar(parse_program(source)) + assert check_type(ctx, p, ty) + + l1 = LiquidLiteralInt(1) lx = LiquidVar("x") lx1 = LiquidApp("x", [l1]) @@ -31,3 +41,16 @@ def test_simple_eq(): [LiquidLiteralInt(2)], ) assert LiquidApp("x", [LiquidLiteralInt(1)]) != LiquidApp("x", [LiquidVar("x2")]) + + +def test_liquid_types_syntax(): + source = r""" + def test (n:Int | n > 0) (z:Int) : Int { + n + z + } + + def main (x:Int) : Unit { + print(test 5 5) + } +""" + check_compile(source, top, 1) diff --git a/tests/recursion_test.py b/tests/recursion_test.py index fbc395b1..50a9e292 100644 --- a/tests/recursion_test.py +++ b/tests/recursion_test.py @@ -14,7 +14,7 @@ def check_compile(source, ty, res): def test_anf(): source = r""" - def gcd ( n:Int, z:Int) : Int { + def gcd ( n:Int) (z:Int) : Int { if z == 0 then n else (gcd(z)(n % z)) }