commit 4f13a98189f7d509bbbd5c5615ecc737792e554a Author: Kacper Marzecki Date: Thu May 29 16:53:36 2025 +0200 asd diff --git a/log.pl b/log.pl new file mode 100644 index 0000000..e416d98 --- /dev/null +++ b/log.pl @@ -0,0 +1,67 @@ +:- module(log, + [ log/1, + debug/1, + log/2, + explain_error/2, + why_failed/2, + set_verbosity/1, + if_verbose/1 + ]). + +:- dynamic verbose_level/1. +verbose_level(0). % Default verbosity: 0 (errors only), 1 (log), 2 (debug) + +set_verbosity(Level) :- + retractall(verbose_level(_)), + assertz(verbose_level(Level)). + +if_verbose(Goal) :- + verbose_level(Level), + Level > 0, + call(Goal). + +log(Message) :- + verbose_level(Level), + Level >= 1, + format(user_error, '[LOG] ~w~n', [Message]). + +debug(Message) :- + verbose_level(Level), + Level >= 2, + format(user_error, '[DEBUG] ~w~n', [Message]). + +log(Phase, Term) :- + verbose_level(Level), + Level >= 1, + format(user_error, '[LOG][~w] ~w~n', [Phase, Term]). + +explain_error(ErrorTerm, Explanation) :- + % Basic error explanation, to be expanded + ( ErrorTerm = type_mismatch(Expected, Actual, Location) -> + format(string(Explanation), "Type mismatch at ~w: Expected ~w, but got ~w.", [Location, Expected, Actual]) + ; ErrorTerm = unification_failure(Term1, Term2, Context) -> + format(string(Explanation), "Unification failed between ~w and ~w in context: ~w.", [Term1, Term2, Context]) + ; ErrorTerm = unbound_variable(Var, Location) -> + format(string(Explanation), "Unbound variable ~w at ~w.", [Var, Location]) + ; ErrorTerm = unknown_predicate(Pred, Location) -> + format(string(Explanation), "Unknown predicate ~w at ~w.", [Pred, Location]) + ; format(string(Explanation), "An error occurred: ~w", [ErrorTerm]) + ), + log(error, Explanation). + +why_failed(ErrorTerm, Details) :- + % Provide more context or steps leading to failure + ( ErrorTerm = type_mismatch(Expected, Actual, _Location) -> + % Placeholder for more detailed logic, e.g., tracing type inference steps + format(string(Details), "Failure due to ~w not being compatible with ~w.", [Actual, Expected]) + ; format(string(Details), "Details for ~w not yet implemented.", [ErrorTerm]) + ), + log(error_details, Details). + +% Example usage (can be removed or moved to tests.pl) +% :- set_verbosity(2). +% :- log('Logging system initialized.'). +% :- debug('This is a debug message.'). +% :- log(parser, 'Parsing phase started.'). +% :- explain_error(type_mismatch(number, string, 'line 5'), Explanation), writeln(Explanation). +% :- why_failed(type_mismatch(number, string, 'line 5'), Details), writeln(Details). diff --git a/parser.pl b/parser.pl new file mode 100644 index 0000000..c9af85a --- /dev/null +++ b/parser.pl @@ -0,0 +1,148 @@ +:- module(parser, + [ parse/2 % parse(-CodeString, -AST) + ]). + +:- use_module(library(dcg/basics)). +:- use_module(log). + +% --- Entry point --- +parse(CodeString, AST) :- + string_codes(CodeString, Codes), + phrase(s_expression(AST), Codes), + log(parser, ast(AST)). + +% --- S-expression parsing --- +s_expression(Ast) --> + ws, "(", ws, s_expression_items(Items), ws, ")", ws, + { build_ast(Items, Ast) }. +s_expression(int(N)) --> integer(N), ws. +s_expression(string_val(S)) --> string_literal(S), ws. +s_expression(bool(true)) --> "true", ws. % Must be before id(Atom) +s_expression(bool(false)) --> "false", ws. % Must be before id(Atom) +s_expression(id(Atom)) --> identifier(Atom), ws. +s_expression(list_nil) --> ws, "(", ws, ")", ws. % Special case for empty list '()' + +s_expression_items([Item | Rest]) --> + s_expression(Item), ws, + ( s_expression_items(Rest) + | {Rest = []} ). +s_expression_items([]) --> []. % For items inside '(...)' + +% --- AST Construction from S-expression items --- +% build_ast(ItemsList, AST) +% ItemsList is a Prolog list of ASTs from inside the parens. +% E.g., for (if c t e), ItemsList = [id(if), AST_c, AST_t, AST_e] + +% Keywords +build_ast([id(if), Cond, Then, Else], if(Cond, Then, Else)) :- !. +build_ast([id(let), id(Var), Value, Body], let(Var, Value, Body)) :- !. + +% Lambda: (lambda (params...) body) -> (lambda (p1 p2) body) +% ParamsSExpr is the AST for (p1 p2 ...), e.g. generic_list([id(p1), id(p2)]) +build_ast([id(lambda), ParamsSExpr, Body], lambda(Params, Body)) :- + extract_lambda_params(ParamsSExpr, Params), !. + +% Match: (match Expr ((Pat1 Body1) (Pat2 Body2) ...)) +% ClausesSExpr is the AST for ((Pat1 Body1) (Pat2 Body2) ...), +% e.g. generic_list([generic_list([Pat1AST, Body1AST]), ...]) +build_ast([id(match), Expr, ClausesSExpr], match(Expr, Clauses)) :- + extract_match_clauses(ClausesSExpr, Clauses), !. + +% Data constructors +build_ast([id(tuple) | Elements], tuple(Elements)) :- !. +build_ast([id(list) | Elements], list_val(Elements)) :- !. + +% Function application (must be last among id-starting rules for simple names) +build_ast([id(FunctorName) | Args], Application) :- + atom(FunctorName), % Ensure FunctorName is an atom, not a complex term + Application =.. [FunctorName | Args], !. + +% Higher-order function application: ((lambda (x) x) 10) or (VarHoldingLambda 10) +% Head of ItemsList is a complex AST (e.g., lambda(...), id(Var)) +build_ast([FunctorSExpr | Args], apply(FunctorSExpr, Args)) :- Args \= [], !. % Ensure there are arguments + +% Generic list structure if not a keyword or application, e.g. for parameters or clause pairs +% Also handles (X) where X is a complex term, parsing to generic_list([X]) +build_ast(Items, generic_list(Items)) :- Items \= [], !. +build_ast([], list_nil) :- !. % Should have been caught by s_expression(list_nil) if it's top-level () + +% --- Helpers for AST construction --- + +% extract_lambda_params(SExpr_representing_param_list, PrologListOfParamNames) +% SExpr for (p1 p2 ...): generic_list([id(p1), id(p2), ...]) +extract_lambda_params(generic_list(IdASTs), ParamNames) :- + maplist(get_id_name_from_ast, IdASTs, ParamNames), !. +extract_lambda_params(list_nil, []) :- !. % (lambda () body) +extract_lambda_params(id(ParamAST_single_param), [ParamName]) :- % (lambda x body) + get_id_name_from_ast(id(ParamAST_single_param), ParamName), !. + +get_id_name_from_ast(id(Name), Name). + +% extract_match_clauses(SExpr_representing_list_of_clauses, PrologListOfClauseASTs) +% SExpr for ((p1 b1) (p2 b2)): generic_list([ ClauseSExpr1, ClauseSExpr2, ... ]) +% ClauseSExpr1 is generic_list([Pat1AST, Body1AST]) +extract_match_clauses(generic_list(ClauseSExprs), ClauseASTs) :- + maplist(parse_one_match_clause, ClauseSExprs, ClauseASTs), !. +extract_match_clauses(list_nil, []) :- !. % (match expr ()) - no clauses + +% parse_one_match_clause(SExpr_for_one_clause, clause(PatternAST, true, BodyAST)) +% SExpr for (pat body): generic_list([RawPatternAST, BodyAST]) +parse_one_match_clause(generic_list([RawPatternAST, BodyAST]), clause(Pattern, true, BodyAST)) :- + ast_to_pattern(RawPatternAST, Pattern). + +ast_to_pattern(id(Name), pvar(Name)) :- Name \= '_', !. +ast_to_pattern(id('_'), pwild) :- !. +ast_to_pattern(int(N), pint(N)) :- !. +ast_to_pattern(string_val(S), pstring(S)) :- !. +ast_to_pattern(bool(B), pbool(B)) :- !. % Pattern for true/false +ast_to_pattern(list_nil, plist([])) :- !. % Pattern for () +ast_to_pattern(tuple(ElementASTs), ptuple(PatternElements)) :- % (tuple p1 p2) + maplist(ast_to_pattern, ElementASTs, PatternElements), !. +ast_to_pattern(list_val(ElementASTs), plist(PatternElements)) :- % (list p1 p2) + maplist(ast_to_pattern, ElementASTs, PatternElements), !. +% For more complex list patterns like (cons head tail) or (list-star p1 p2 ... rest) +% ast_to_pattern(generic_list([id(cons), HAST, TAST]), pcons(HPatt, TPatt)) :- !, +% ast_to_pattern(HAST, HPatt), ast_to_pattern(TAST, TPatt). +% This requires 'cons' to be parsed into generic_list([id(cons),...]) in pattern context. + +% --- Low-level parsers (mostly unchanged) --- +identifier(Atom) --> + [C], { code_type(C, alpha) }, % Simplified: starts with alpha + string_without(" ()", Codes), % Simplified: no spaces or parens in identifier + { atom_codes(Atom, [C|Codes]) }. + +string_literal(String) --> + "\"", string_without("\"", Codes), "\"", + { atom_codes(String, Codes) }. + +ws --> white, ws. +ws --> []. + + +% --- Example Usage (for testing in REPL) --- +% ?- parse("(if (is_number x) x 0)", AST). +% AST = if(is_number(id(x)), id(x), int(0)) +% +% ?- parse("(let y 10 y)", AST). +% AST = let(y, int(10), id(y)) +% +% ?- parse("(match input ((list x y) x))", AST). +% AST = match(id(input), [clause(plist([pvar(x), pvar(y)]), true, id(x))]) +% +% ?- parse("(match data ((tuple a _) a))", AST). +% AST = match(id(data), [clause(ptuple([pvar(a), pwild]), true, id(a))]) +% +% ?- parse("(lambda (x y) (add x y))", AST). +% AST = lambda([x,y], add(id(x),id(y))) +% +% ?- parse("((lambda (x) x) 10)", AST). +% AST = apply(lambda([x],id(x)),[int(10)]) +% +% ?- parse("(list 1 2 3)", AST). +% AST = list_val([int(1), int(2), int(3)]) +% +% ?- parse("(tuple \"a\" true)", AST). +% AST = tuple([string_val("a"), bool(true)]) +% +% ?- parse("()", AST). +% AST = list_nil diff --git a/tests.pl b/tests.pl new file mode 100644 index 0000000..d079f04 --- /dev/null +++ b/tests.pl @@ -0,0 +1,139 @@ +:- module(tests, [run_tests/0]). + +:- use_module(parser). +:- use_module(types). +:- use_module(log). + +run_test(TestName, Env, Code, ExpectedTypeResult) :- + format('--- Test: ~w ---~n', [TestName]), + ( parse(Code, AST) -> + format('Parsed AST: ~w~n', [AST]), + log(test_setup, env(Env)), + ( catch(infer_type(AST, Env, ActualType), Error, ( + log(error, caught_error(Error)), + explain_error(Error, Explanation), + format('Type Error: ~w~n', [Explanation]), + ActualType = error(Error) % Represent error for comparison + )) + -> true + ; ActualType = 'inference_failed_silently' % Should not happen if catch works + ), + format('Inferred Type: ~w~n', [ActualType]), + ( (ActualType == never, ExpectedTypeResult \== never) -> % Explicitly fail if 'never' is inferred unexpectedly + Pass = false, SubMatch = 'unexpected_never' + ; (ExpectedTypeResult = error(_), ActualType = error(_)) -> % Both are errors + Pass = true, SubMatch = 'error_expected_and_received' + ; ExpectedTypeResult == ActualType -> + Pass = true, SubMatch = 'exact_match' + ; unify_types(ExpectedTypeResult, ActualType, ExpectedTypeResult) -> % Actual is subtype of Expected + Pass = true, SubMatch = 'subtype_match' + ; unify_types(ExpectedTypeResult, ActualType, ActualType) -> % Expected is subtype of Actual (and Actual is not 'never' unless Expected is also 'never') + Pass = true, SubMatch = 'supertype_match' + ; Pass = false, SubMatch = 'mismatch' + ), + ( Pass == true -> + format('Status: PASS (~w)~n~n', [SubMatch]) + ; format('Status: FAIL (~w) - Expected: ~w~n~n', [SubMatch, ExpectedTypeResult]) + ) + ; format('Parse FAILED for code: ~s~n~n', [Code]) + ). + +run_tests :- + set_verbosity(1), % Set verbosity: 0 (errors), 1 (log), 2 (debug) + log(tests, 'Starting test suite...'), + initial_env(EmptyEnv), + + run_test('Conditional with is_number/1 (x is number)', + [x:union(number,string)], + "(if (is_number x) x 0)", % x is union(number,string), then branch x is number. else branch x is string. + % 0 is number. So then branch is number, else branch is number. + % Result should be number. + number), % If x is number, then x (number). Else 0 (number). Unified: number. + + run_test('Conditional with is_number/1 (x is string)', + [x:union(number,string)], + "(if (is_number x) 1 \"not num\")", % x:union(number,string). + % Cond: (is_number x) + % Then: x refined to number. Body `1` is number. + % Else: x refined to string. Body `"not num"` is string. + % Result: union(number, string) + union(number, string)), + + run_test('Pattern match list', + [my_list:list(number)], + "(match my_list (((list a b) a)))", % my_list:list(number). a,b become number. returns a (number). + % Pattern (list a b), body a + number), + + run_test('Pattern match tuple', + [my_tuple:tuple([number, string])], + "(match my_tuple (((tuple x y) y)))", % my_tuple:tuple([number, string]). x is number, y is string. returns y (string). + % Pattern (tuple x y), body y + string), + + run_test('Let binding', % z:number, trying to assign string. Current 'let' rebinds. + [z:number], + "(let z \"text\" z)", + string), % With current 'let' semantics (rebinding), z will be string. Env [z:number] is shadowed. + + run_test('Unification in conditional branches', + EmptyEnv, + "(if true 10 \"text\")", % ThenType=number, ElseType=string. unify_types(number,string) -> union(number,string) + union(number,string) + ), + + run_test('Successful refinement (simulated validate_user)', + [user_data:any], + % Using is_number to simulate a predicate that refines type. + % Env: [user_data:any] + % (if (is_number user_data) user_data "not a number") + % Cond: (is_number user_data) -> boolean + % Then branch: user_data refined to number. Body: user_data -> number + % Else branch: user_data refined to not(number). Body: "not a number" -> string + % Result: union(number, string) + "(if (is_number user_data) user_data \"not a number\")", + union(number, string) + ), + + run_test('Lambda expression (syntax check, type not deeply inferred yet)', + EmptyEnv, + "(lambda (x y) (add x y))", % `add` is not a defined function, so type of body is an issue. + % For now, this tests parsing of lambda. + % Expected type depends on how `add` and lambdas are typed. + % Let's expect 'any' or a placeholder function type if types.pl is not updated for lambdas. + % For now, let's assume it's 'any' as `add` is unknown. + any), % Placeholder: Actual type depends on full function type inference. + + run_test('Function application of lambda (syntax check)', + EmptyEnv, + "((lambda (x) x) 10)", + any), % Placeholder: Actual type depends on lambda type inference and application rules. + % If lambda is (T->T) and arg is T, result is T. Here, (any->any) and number -> any. + % If (lambda (x) x) is typed as fun_type([any],any), then apply to int(10) (number) -> any. + + run_test('Empty list literal', + EmptyEnv, + "()", + list(never) % Or some polymorphic list type list(T) if supported. list(never) is common for empty. + ), + + run_test('Boolean true literal', + EmptyEnv, + "true", + boolean + ), + + run_test('Boolean false literal', + EmptyEnv, + "false", + boolean + ), + + log(tests, 'Test suite finished.'). + +% To run: +% ?- consult('log.pl'). +% ?- consult('parser.pl'). +% ?- consult('types.pl'). +% ?- consult('tests.pl'). +% ?- run_tests. diff --git a/types.pl b/types.pl new file mode 100644 index 0000000..7634344 --- /dev/null +++ b/types.pl @@ -0,0 +1,254 @@ +:- module(types, + [ infer_type/3, % infer_type(+AST, +Env, -Type) + unify_types/3, % unify_types(+Type1, +Type2, -UnifiedType) + refine_env/4, % refine_env(+Var, +Type, +EnvIn, -EnvOut) + get_type/3, % get_type(+Var, +Env, -Type) + % Type representations (examples) + type_number/0, type_string/0, type_boolean/0, type_list_nil/0, + type_list/1, type_tuple/1, type_union/2, type_intersection/2, type_negation/1, + type_any/0, type_never/0, + initial_env/1 + ]). + +:- use_module(log). +:- discontiguous unify_types/3. +:- discontiguous infer_type/3. % Added to handle infer_type_arg/3 in between + +% --- Type Representations (as atoms/compound terms) --- +type_number :- _ = number. +type_string :- _ = string. +type_boolean :- _ = boolean. % Represents the type 'boolean' +type_list_nil :- _ = list_nil. % AST node for empty list literal '()' +type_list(_T) :- _ = list(_). % _T is intentionally a singleton, structure check: list(Anything) +type_tuple(Ts) :- _ = tuple(Ts), is_list(Ts). % Ts is used, not singleton +type_union(T1, T2) :- _ = union(T1, T2). % T1, T2 are used, not singletons +type_intersection(T1, T2) :- _ = intersection(T1, T2). % T1, T2 are used, not singletons +type_negation(T) :- _ = negation(T). % T is used, not singleton +type_any :- _ = any. % Top type +type_never :- _ = never. % Bottom type, result of failed branches or contradictions + +% --- Environment --- +% Env is a list of Var:Type pairs. +initial_env([]). + +get_type(Var, [Var:Type | _], Type) :- !. +get_type(Var, [_ | RestEnv], Type) :- get_type(Var, RestEnv, Type). +get_type(Var, [], _) :- + log(error, unbound_variable(Var, 'unknown_location')), % Location should be passed + fail. + +refine_env(Var, Type, EnvIn, [Var:Type | EnvSansOldBinding]) :- + delete(EnvIn, Var:_, EnvSansOldBinding), % EnvSansOldBinding is EnvIn with all Var:_ bindings removed. + log(type_refinement, env_refined(Var, Type)). + + +% --- Type Inference --- +infer_type(int(_), _Env, number) :- log(type_inference, 'Integer literal -> number'). +infer_type(string_val(_), _Env, string) :- log(type_inference, 'String literal -> string'). +infer_type(bool(_), _Env, boolean) :- log(type_inference, 'Boolean literal -> boolean'). +infer_type(list_nil, _Env, list(never)) :- log(type_inference, 'Empty list literal -> list(never)'). % Or a polymorphic list type + +infer_type(id(Var), Env, Type) :- + ( get_type(Var, Env, Type) -> + log(type_inference, id(Var) -> Type) + ; log(error, type_error(unbound_variable(Var), id(Var))), + Type = never, % Or fail, depending on error handling strategy + explain_error(unbound_variable(Var, id(Var)), _Msg) + ). + +infer_type(let(Var, ValueAst, BodyAst), EnvIn, BodyType) :- + log(type_inference, 'Inferring type for let expression'), + infer_type(ValueAst, EnvIn, ValueType), + log(type_inference, let_value(Var, ValueType)), + refine_env(Var, ValueType, EnvIn, EnvMid), + infer_type(BodyAst, EnvMid, BodyType), + log(type_inference, let_body(BodyType)). + +infer_type(if(CondAst, ThenAst, ElseAst), EnvIn, IfType) :- + log(type_inference, 'Inferring type for if expression'), + infer_type(CondAst, EnvIn, CondType), + ( CondType == boolean -> true + ; log(error, type_error(expected_boolean_condition, CondAst)), IfType = never, fail + ), + % Flow-sensitive refinement example: + ( CondAst = is_number(id(X)) -> % If condition is is_number(X) + log(type_inference, flow_refinement_condition(is_number(id(X)))), + refine_env(X, number, EnvIn, EnvThen) % X is number in Then branch + ; EnvThen = EnvIn % No specific refinement from condition structure + ), + infer_type(ThenAst, EnvThen, ThenType), + % For Else branch, if CondAst was `is_number(X)`, then X is `not(number)` + ( CondAst = is_number(id(X)) -> + get_type(X, EnvIn, OriginalXType), % Get original type of X before refinement + refine_env(X, intersection(OriginalXType, negation(number)), EnvIn, EnvElse) + ; EnvElse = EnvIn + ), + infer_type(ElseAst, EnvElse, ElseType), + unify_types(ThenType, ElseType, IfType), % Branches must have compatible types + log(type_inference, if_expression(CondType, ThenType, ElseType) -> IfType). + +% Example: is_number/1 predicate (built-in) +infer_type(is_number(ArgAst), Env, boolean) :- + log(type_inference, 'Inferring type for is_number/1 call'), + infer_type(ArgAst, Env, _ArgType). % ArgType can be anything, is_number checks it. + +% Lambda expressions (placeholder - full function type inference is complex) +infer_type(lambda(_Params, _BodyAst), _Env, any) :- % For (lambda (params...) body) + % A proper implementation would construct a function type: fun_type(ParamTypes, ReturnType) + % This requires inferring types for params (possibly from annotations) and body. + log(type_inference, 'Lambda expression -> any (placeholder)'). + +% General function application (placeholder - requires function type for FunctorSExpr) +infer_type(apply(FunctorSExpr, ArgsSExprs), Env, any) :- % For ((lambda ...) arg) or (f arg) where f is complex + log(type_inference, 'General application (apply/2) -> any (placeholder)'), + infer_type(FunctorSExpr, Env, FunctorType), + % Infer types of ArgsSExprs + maplist(infer_type_arg(Env), ArgsSExprs, ArgTypes), + log(type_inference, apply_functor_type(FunctorType)), + log(type_inference, apply_arg_types(ArgTypes)). + % A proper implementation would: + % 1. Ensure FunctorType is a function type, e.g., fun_type(ExpectedParamTypes, ReturnType). + % 2. Check Arity and if ArgTypes are subtypes of ExpectedParamTypes. + % 3. Return ReturnType. + % For now, it's 'any'. + +infer_type_arg(Env, ArgSExpr, ArgType) :- infer_type(ArgSExpr, Env, ArgType). + + +% Example: validate_user/1 (hypothetical predicate that narrows type) +% Assume validate_user/1 takes 'any' and if it succeeds, the arg is a 'user_record'. +% This would typically be declared elsewhere (e.g. function signatures) +% For now, we simulate its effect. +infer_type(validate_user(ArgAst), Env, boolean) :- % validate_user returns boolean + log(type_inference, 'Inferring type for validate_user/1 call'), + infer_type(ArgAst, Env, _ArgType). + % The actual refinement happens in the 'then' branch of an 'if' or similar construct + % e.g., if validate_user(x) then ... (x is now user_record) + +% Pattern Matching +infer_type(match(ExprAst, Clauses), EnvIn, MatchType) :- + log(type_inference, 'Inferring type for match expression'), + infer_type(ExprAst, EnvIn, ExprType), + infer_clause_types(Clauses, ExprType, EnvIn, ClauseTypes), + ( ClauseTypes = [] -> MatchType = never % Or error: non-exhaustive match if not desired + ; reduce_types(ClauseTypes, MatchType) % Unify all clause body types + ), + log(type_inference, match_result_type(MatchType)). + +infer_clause_types([], _ExprType, _EnvIn, []). +infer_clause_types([clause(Pattern, _Guard, BodyAst) | RestClauses], ExprType, EnvIn, [BodyType | RestBodyTypes]) :- + log(type_inference, inferring_clause_pattern(Pattern)), + refine_env_from_pattern(Pattern, ExprType, EnvIn, EnvPattern), + ( EnvPattern == fail -> % Pattern doesn't match ExprType or is contradictory + log(type_warning, pattern_will_not_match(Pattern, ExprType)), + BodyType = never % This branch is effectively dead + ; infer_type(BodyAst, EnvPattern, BodyType) + ), + infer_clause_types(RestClauses, ExprType, EnvIn, RestBodyTypes). + +% refine_env_from_pattern/4: (+Pattern, +MatchedExprType, +EnvIn, -EnvOutOrFail) +refine_env_from_pattern(pvar(Name), MatchedExprType, EnvIn, EnvOut) :- + !, refine_env(Name, MatchedExprType, EnvIn, EnvOut). +refine_env_from_pattern(pwild, _MatchedExprType, EnvIn, EnvIn) :- !. +refine_env_from_pattern(pint(_), MatchedExprType, EnvIn, EnvIn) :- + ( unify_types(MatchedExprType, number, number) -> true % Check if MatchedExprType is compatible with number + ; log(type_error, pattern_type_mismatch(pint, MatchedExprType)), fail + ). +refine_env_from_pattern(pstring(_), MatchedExprType, EnvIn, EnvIn) :- + ( unify_types(MatchedExprType, string, string) -> true % Check if MatchedExprType is compatible with string + ; log(type_error, pattern_type_mismatch(pstring, MatchedExprType)), fail + ). +refine_env_from_pattern(pbool(_), MatchedExprType, EnvIn, EnvIn) :- % Added for boolean patterns + ( unify_types(MatchedExprType, boolean, boolean) -> true % Check if MatchedExprType is compatible with boolean + ; log(type_error, pattern_type_mismatch(pbool, MatchedExprType)), fail + ). +refine_env_from_pattern(ptuple(Patterns), MatchedExprType, EnvIn, EnvOut) :- + ( MatchedExprType = tuple(ElementTypes) ; MatchedExprType = any ), % Allow matching 'any' as a tuple + ( var(ElementTypes) -> % MatchedExprType was 'any' or tuple(_) + length(Patterns, L), length(ElementTypes, L), % Infer arity + maplist(=(any), ElementTypes) % Assume elements are 'any' if not specified + ; length(Patterns, L1), length(ElementTypes, L2), L1 == L2 % Check arity + ), !, + refine_env_from_patterns(Patterns, ElementTypes, EnvIn, EnvOut). +refine_env_from_pattern(ptuple(_Patterns), MatchedExprType, _EnvIn, fail) :- + log(type_error, pattern_type_mismatch(ptuple, MatchedExprType)), fail. + +refine_env_from_pattern(plist(Patterns), MatchedExprType, EnvIn, EnvOut) :- + ( MatchedExprType = list(ElementType) ; MatchedExprType = any ), + ( var(ElementType) -> ElementType = any ), % If MatchedExprType was 'any' or list(_), treat element type as 'any' + !, + length(Patterns, Len), + length(TypesForPatterns, Len), % Create a list of unbound variables of the same length as Patterns + maplist(=(ElementType), TypesForPatterns), % Unify each variable in TypesForPatterns with ElementType + refine_env_from_patterns(Patterns, TypesForPatterns, EnvIn, EnvOut). +refine_env_from_pattern(plist(_Patterns), MatchedExprType, _EnvIn, fail) :- + \+ (MatchedExprType = list(_); MatchedExprType = any), % Fail only if not a list or any + log(type_error, pattern_type_mismatch(plist, MatchedExprType)), + fail. + + +refine_env_from_patterns([], [], Env, Env). +refine_env_from_patterns([P|Ps], [T|Ts], EnvIn, EnvOut) :- + refine_env_from_pattern(P, T, EnvIn, EnvMid), + ( EnvMid == fail -> EnvOut = fail, ! + ; refine_env_from_patterns(Ps, Ts, EnvMid, EnvOut) + ). + + +% --- Type Unification --- +unify_types(T, T, T) :- !, log(unification, identical(T)). +unify_types(any, T, T) :- !, log(unification, any_with(T) -> T). +unify_types(T, any, T) :- !, log(unification, T -> T). % Corrected T_with_any to T +unify_types(never, _T, never) :- !, log(unification, 'never involved'). % Or should it be T? Depends on meaning. +unify_types(_T, never, never) :- !, log(unification, 'never involved'). + +unify_types(list(T1), list(T2), list(TU)) :- !, + unify_types(T1, T2, TU), + log(unification, list(T1, T2) -> list(TU)). + +unify_types(tuple(Ts1), tuple(Ts2), tuple(TUs)) :- !, + length(Ts1, L), length(Ts2, L), % Tuples must have same arity + maplist(unify_types, Ts1, Ts2, TUs), + log(unification, tuple(Ts1, Ts2) -> tuple(TUs)). + +% Union Type Unification (simplified: create a canonical union) +unify_types(union(A, B), C, union(A, union(B,C))) :- \+ is_union(C), !. % Simplistic, needs canonical form +unify_types(A, union(B, C), union(A, union(B,C))) :- \+ is_union(A), !. +unify_types(union(A1,B1), union(A2,B2), union(A1,union(B1,union(A2,B2)))) :- !. % Very naive + +is_union(union(_,_)). + +% Intersection (placeholder) +unify_types(intersection(A,B), C, intersection(A,intersection(B,C))) :- !. % Needs proper logic + +% Helper to reduce a list of types to a single type (e.g., for match clauses) +reduce_types([T], T) :- !. +reduce_types([T1, T2 | Ts], ResultType) :- + unify_types(T1, T2, UnifiedHead), + ( UnifiedHead == never -> ResultType = never, ! % Propagate failure + ; reduce_types([UnifiedHead | Ts], ResultType) + ). +reduce_types([], never). % Consistent with match behavior for no clauses. + + +% --- Example Predicate for Type Narrowing --- +% This would be part of function signature definitions. +% For 'validate_user(X)', if it returns true, X's type is refined. +% This is usually handled by the 'if' construct using the boolean result. +% e.g. if validate_user(x) then (env refined for x) else (env not refined or negated refinement) + +% Example: +% ?- initial_env(Env), infer_type(if(is_number(id(x)), id(x), string_val("no")), [x:union(number,string)], Type). +% Type = number (because string_val("no") is string, unified with number from then branch, if x is number then x is number, else x is string. +% The unification of number and string should fail, or result in union(number, string). +% The example above needs careful check of unify_types. +% Let's assume unify_types(T1,T2,union(T1,T2)) if they are different base types. + +% Corrected unification for disparate types (common supertype or union) +unify_types(T1, T2, union(T1, T2)) :- + % This is a fallback if no other rule matches and T1, T2 are not 'any' or 'never' + T1 \= any, T2 \= any, T1 \= never, T2 \= never, + T1 \= T2, % Not identical + % Ensure not to double-wrap unions unnecessarily (basic check) + \+ (T1 = union(_,_) ; T2 = union(_,_)), + log(unification, disparate_types(T1, T2) -> union(T1,T2)).