From 2c3ed8d9a2fcf57f1cff5375de4f48dbab321846 Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 25 Dec 2025 21:49:46 +0100 Subject: [PATCH 1/5] Use queue-based algorithm for execution --- src/lsc_eval.ml | 547 ++++------------------------------------------- src/lsc_exec.ml | 237 ++++++++++++++++++++ src/lsc_trace.ml | 250 ++++++++++++++++++++++ 3 files changed, 528 insertions(+), 506 deletions(-) create mode 100644 src/lsc_exec.ml create mode 100644 src/lsc_trace.ml diff --git a/src/lsc_eval.ml b/src/lsc_eval.ml index 8f99f97..cf69583 100644 --- a/src/lsc_eval.ml +++ b/src/lsc_eval.ml @@ -1,529 +1,64 @@ +(* + * lsc_eval.ml - Backwards compatibility wrapper + * + * This module re-exports functionality from lsc_exec and lsc_trace + * to maintain backwards compatibility with existing code. + *) + open Base -open Lsc_ast -open Lsc_ast.StellarRays open Lsc_ast.Raw -let ( let* ) x f = Result.bind x ~f - -(* ---------------------------------------- - Trace mode support - ---------------------------------------- *) - -type source_location = +(* Re-export source_location from lsc_trace *) +type source_location = Lsc_trace.source_location = { filename : string ; line : int ; column : int } -type trace_step = - { step_num : int - ; actions : constellation - ; states : constellation - ; selected_state_idx : int option - ; selected_ray_idx : int option - ; selected_action_idx : int option - ; partner_ray : ray option - ; substitution : substitution option - ; is_final : bool - ; location : source_location option - } - +(* Trace configuration - adapts between old and new APIs *) type trace_config = { enabled : bool - ; mutable step_count : int - ; mutable steps : trace_step list - ; web_mode : bool + ; mutable trace_state : Lsc_trace.trace_state option ; mutable current_location : source_location option - ; mutable current_states : constellation - ; mutable current_actions : constellation - ; mutable fusion_detected : bool } let make_trace_config ?(web_mode = false) enabled = + let mode = + if web_mode then Lsc_trace.WebMode + else if enabled then Lsc_trace.Interactive + else Lsc_trace.Silent + in { enabled - ; step_count = 0 - ; steps = [] - ; web_mode + ; trace_state = Some (Lsc_trace.create ~mode ()) ; current_location = None - ; current_states = [] - ; current_actions = [] - ; fusion_detected = false } -let set_trace_location cfg loc = cfg.current_location <- loc +let set_trace_location cfg loc = + cfg.current_location <- loc; + match cfg.trace_state with + | Some state -> Lsc_trace.set_location state loc + | None -> () -let add_trace_step cfg step = if cfg.enabled then cfg.steps <- step :: cfg.steps - -let get_trace_steps cfg = List.rev cfg.steps - -let get_source_line filename line_num = - try - (* In web mode or when file access fails, gracefully return None *) - let ic = Stdlib.open_in filename in - let rec skip_lines n = - if n <= 1 then () - else - let _ = Stdlib.input_line ic in - skip_lines (n - 1) - in - skip_lines line_num; - let line = Stdlib.input_line ic in - Stdlib.close_in ic; - Some line - with - | Sys_error _ -> None (* File system not available (e.g., web mode) *) - | End_of_file -> None - | _ -> None +let get_trace_steps cfg = + match cfg.trace_state with Some state -> state.collected_steps | None -> [] let format_trace_steps_html steps = - let open Lsc_pretty in - let buffer = Buffer.create 1024 in - - let add_html str = Buffer.add_string buffer str in - let add_line str = - add_html str; - add_html "\n" - in - - let escape_html s = - String.substr_replace_all s ~pattern:"&" ~with_:"&" - |> String.substr_replace_all ~pattern:"<" ~with_:"<" - |> String.substr_replace_all ~pattern:">" ~with_:">" - |> String.substr_replace_all ~pattern:"\"" ~with_:""" - in - - List.iteri steps ~f:(fun _i step -> - add_line "
"; - if step.is_final then ( - add_line - (Printf.sprintf - "
Execution Complete (Step %d)
" - step.step_num ); - add_line "
"; - ( match step.location with - | Some loc -> ( - add_line - (Printf.sprintf "
%s:%d:%d
" loc.filename - loc.line loc.column ); - match get_source_line loc.filename loc.line with - | Some line -> - let trimmed = String.strip line in - if not (String.is_empty trimmed) then - add_line - (Printf.sprintf "
%s
" - (escape_html trimmed) ) - | None -> () ) - | None -> () ); - add_line "
Final Result:
"; - add_line "
"; - List.iteri step.states ~f:(fun idx star -> - add_line - (Printf.sprintf "
[%d] %s
" idx - (string_of_star star) ) ); - add_line "
"; - add_line "
" ) - else ( - add_line - (Printf.sprintf "
Step %d
" step.step_num); - add_line "
"; - ( match step.location with - | Some loc -> ( - add_line - (Printf.sprintf "
%s:%d:%d
" loc.filename - loc.line loc.column ); - match get_source_line loc.filename loc.line with - | Some line -> - let trimmed = String.strip line in - if not (String.is_empty trimmed) then - add_line - (Printf.sprintf "
%s
" - (escape_html trimmed) ) - | None -> () ) - | None -> () ); - - add_line "
"; - add_line "
Actions:
"; - if List.is_empty step.actions then add_line "
{ }
" - else ( - add_line "
"; - List.iteri step.actions ~f:(fun idx star -> - add_line - (Printf.sprintf "
[%d] %s
" idx - (string_of_star star) ) ); - add_line "
" ); - add_line "
"; - - add_line "
"; - add_line "
States:
"; - if List.is_empty step.states then add_line "
{ }
" - else ( - add_line "
"; - List.iteri step.states ~f:(fun idx star -> - add_line - (Printf.sprintf "
[%d] %s
" idx - (string_of_star star) ) ); - add_line "
" ); - add_line "
"; - - add_line "
" ); - add_line "
" ); - - Buffer.contents buffer - -let wait_for_keypress () = - (* Simple version that works everywhere including web *) - let _ = Stdlib.input_line Stdlib.stdin in - () - -let cyan text = "\x1b[36m" ^ text ^ "\x1b[0m" - -let green text = "\x1b[32m" ^ text ^ "\x1b[0m" - -let yellow text = "\x1b[33m" ^ text ^ "\x1b[0m" - -let magenta text = "\x1b[35m" ^ text ^ "\x1b[0m" - -let bold text = "\x1b[1m" ^ text ^ "\x1b[0m" - -let dim text = "\x1b[2m" ^ text ^ "\x1b[0m" - -let print_trace_header step_num location status_msg = - Stdlib.Printf.printf "\n%s\n" (String.make 80 '='); - Stdlib.Printf.printf "%s %s" - (bold (cyan "Step")) - (bold (yellow (Int.to_string step_num))); - ( match status_msg with - | Some msg -> Stdlib.Printf.printf " - %s" (bold msg) - | None -> () ); - ( match location with - | Some loc -> ( - Stdlib.Printf.printf "\n%s %s:%d:%d" (dim "at") loc.filename loc.line - loc.column; - (* Print the source line content *) - match get_source_line loc.filename loc.line with - | Some line -> - let trimmed = String.strip line in - if not (String.is_empty trimmed) then - Stdlib.Printf.printf "\n %s %s" (dim "│") (dim trimmed) - | None -> () ) - | None -> () ); - Stdlib.Printf.printf "\n%s\n" (String.make 80 '=') - -let print_trace_constellation ?(selected_star = None) ?(selected_ray = None) - ?(partner_star = None) ?(partner_ray = None) label constellation = - let open Lsc_pretty in - if List.is_empty constellation then - Stdlib.Printf.printf "%s %s\n" (bold label) (dim "{}") - else begin - Stdlib.Printf.printf "%s\n" (bold label); - List.iteri constellation ~f:(fun i star -> - let is_selected = - match selected_star with Some idx -> idx = i | None -> false - in - let is_partner = - match partner_star with Some idx -> idx = i | None -> false - in - let selected_ray_idx = if is_selected then selected_ray else None in - let partner_ray_idx = if is_partner then partner_ray else None in - let marker = - if is_selected then magenta "◄ " - else if is_partner then green "◄ " - else " " - in - let index_str = - if is_selected then magenta (Printf.sprintf "[%d]" i) - else if is_partner then green (Printf.sprintf "[%d]" i) - else dim (Printf.sprintf "[%d]" i) - in - (* If this star has a selected ray, print rays individually with arrow *) - match (selected_ray_idx, partner_ray_idx) with - | Some ray_idx, _ | _, Some ray_idx -> - Stdlib.Printf.printf "%s%s [" marker index_str; - List.iteri star.content ~f:(fun j ray -> - if j > 0 then Stdlib.Printf.printf " "; - Stdlib.Printf.printf "%s" (string_of_ray ray) ); - if not (List.is_empty star.bans) then - Stdlib.Printf.printf " || %s" - (List.map star.bans ~f:string_of_ban |> String.concat ~sep:" "); - Stdlib.Printf.printf "]\n"; - (* Print arrow pointing to the selected ray *) - let arrow_color = if is_selected then magenta else green in - (* Calculate visual width (accounting for ANSI codes in marker/index_str) *) - let visual_marker_width = 2 in - (* "◄ " or " " *) - let visual_index_width = String.length (Printf.sprintf "[%d]" i) in - let prefix_len = visual_marker_width + visual_index_width + 2 in - (* +2 for " [" *) - let spaces = ref prefix_len in - List.iteri star.content ~f:(fun j ray -> - if j < ray_idx then - (* Add this ray's width + space to position *) - spaces := !spaces + String.length (string_of_ray ray) + 1 - else if j = ray_idx then - (* Print arrow at current position *) - Stdlib.Printf.printf "%s%s\n" (String.make !spaces ' ') - (arrow_color "^") - else () ) - | None, None -> - Stdlib.Printf.printf "%s%s %s\n" marker index_str (string_of_star star) ) - end - -let print_trace_ray label ray = - let open Lsc_pretty in - Stdlib.Printf.printf "%s %s\n" (bold label) (green (string_of_ray ray)) - -let print_trace_fusion_visual step_num location states actions state_idx ray_idx - action_idx action_ray_idx theta = - let open Lsc_pretty in - print_trace_header step_num location (Some (magenta "Fusion detected!")); - Stdlib.Printf.printf "\n"; - print_trace_constellation ~selected_star:(Some state_idx) - ~selected_ray:(Some ray_idx) (cyan "States:") states; - Stdlib.Printf.printf "\n"; - print_trace_constellation ~partner_star:(Some action_idx) - ~partner_ray:(Some action_ray_idx) (cyan "Actions:") actions; - if not (List.is_empty theta) then - Stdlib.Printf.printf "\n %s %s\n" (dim "Substitution:") - (yellow (string_of_subst theta)) - -let print_trace_footer () = - Stdlib.Printf.printf "\n%s\n" (dim "Press Enter to continue..."); - Stdlib.flush Stdlib.stdout; - wait_for_keypress () - -type configuration = constellation * constellation - -let fmap_ban ~f = function - | Ineq (b1, b2) -> Ineq (f b1, f b2) - | Incomp (b1, b2) -> Incomp (f b1, f b2) - -let fusion repl1 repl2 s1 s2 bans1 bans2 theta : star = - let new1 = List.map s1 ~f:repl1 in - let new2 = List.map s2 ~f:repl2 in - let nbans1 = List.map bans1 ~f:(fmap_ban ~f:repl1) in - let nbans2 = List.map bans2 ~f:(fmap_ban ~f:repl2) in - { content = List.map (new1 @ new2) ~f:(subst theta) - ; bans = List.map (nbans1 @ nbans2) ~f:(fmap_ban ~f:(subst theta)) - } - -let group_bans bans = - List.fold bans ~init:([], []) ~f:(fun (inequalities, incompatibles) ban -> - match ban with - | Ineq (b1, b2) -> ((b1, b2) :: inequalities, incompatibles) - | Incomp (b1, b2) -> (inequalities, (b1, b2) :: incompatibles) ) - -let exists_conflicting_incomp_pair (box, slice) incomp_list = - List.exists incomp_list ~f:(fun (other_box, other_slice) -> - equal_ray box other_box && not (equal_ray slice other_slice) ) - -let coherent_incomp incompatible_pairs = - let rec check_all = function - | [] -> true - | head :: tail -> - (not (exists_conflicting_incomp_pair head tail)) && check_all tail - in - check_all incompatible_pairs - -let coherent_bans bans = - let inequalities, incompatibles = group_bans bans in - List.for_all inequalities ~f:(fun (b1, b2) -> not (equal_ray b1 b2)) - && coherent_incomp incompatibles - -let ident_counter = ref 0 - -let classify marked_constellation = - let rec separate_actions_and_states actions states = function - | [] -> (List.rev actions, List.rev states) - | Marked.State s :: rest -> - separate_actions_and_states actions (s :: states) rest - | Marked.Action s :: rest -> - separate_actions_and_states (s :: actions) states rest - in - separate_actions_and_states [] [] marked_constellation - -let extract_intspace (mcs : Marked.constellation) = - ident_counter := 0; - classify mcs - -(* interaction between one selected ray and one selected action *) -let rec interaction ~queue ~trace ~state_idx ~ray_idx ~action_idx repl1 repl2 - (selected_action, other_actions) (selected_ray, other_rays, bans) : - constellation = - match selected_action.content with - | [] -> [] - | r' :: s' when not (is_polarised r') -> - interaction ~queue:(r' :: queue) ~trace ~state_idx ~ray_idx ~action_idx - repl1 repl2 - ({ content = s'; bans }, other_actions) - (selected_ray, other_rays, bans) - | r' :: s' -> ( - match raymatcher (repl1 selected_ray) (repl2 r') with - | None -> - interaction ~queue:(r' :: queue) ~trace ~state_idx ~ray_idx ~action_idx - repl1 repl2 - ({ content = s'; bans }, other_actions) - (selected_ray, other_rays, bans) - (* if there is an actual connection between rays *) - | Some theta -> - let action_ray_idx = List.length queue in - ( match trace with - | Some cfg when cfg.enabled && not cfg.web_mode -> - if not cfg.fusion_detected then ( - cfg.fusion_detected <- true; - print_trace_fusion_visual cfg.step_count cfg.current_location - cfg.current_states cfg.current_actions state_idx ray_idx action_idx - action_ray_idx theta ) - | _ -> () ); - (* action is consumed when execution is linear *) - let next = - interaction ~queue:(r' :: queue) ~trace ~state_idx ~ray_idx ~action_idx - repl1 repl2 - ({ content = s'; bans }, other_actions) - (selected_ray, other_rays, bans) - in - let other_rays' = queue @ s' in - let after_fusion = - fusion repl1 repl2 other_rays other_rays' bans selected_action.bans - theta - in - let res = - if coherent_bans after_fusion.bans then after_fusion :: next else next - in - ident_counter := !ident_counter + 2; - res ) - -(* search partner for a selected ray within a set of available actions *) -let search_partners ~linear ~trace ~state_idx ~ray_idx - (selected_ray, other_rays, bans) actions : star list * star list = - let repl1 = replace_indices !ident_counter in - let rec try_actions acc action_idx actions_list = function - | [] -> ([], acc) - | selected_action :: other_actions -> - let repl2 = replace_indices (!ident_counter + 1) in - let res = - interaction ~queue:[] ~trace ~state_idx ~ray_idx ~action_idx repl1 repl2 - (selected_action, other_actions) - (selected_ray, other_rays, bans) - in - if (not @@ List.is_empty res) && linear then - let next, new_actions = - try_actions acc (action_idx + 1) actions_list other_actions - in - (res @ next, new_actions) - else - let next, new_actions = - try_actions (selected_action :: acc) (action_idx + 1) actions_list - other_actions - in - (res @ next, new_actions) - in - try_actions [] 0 actions actions - -let rec select_ray ~linear ~trace ~state_idx ~ray_idx ~queue actions - other_states (selected_state, bans) : star list option * star list = - match selected_state with - | [] -> (None, actions) - (* if unpolarized, no need to try, try other stars *) - | r :: rs when not (is_polarised r) -> - select_ray ~linear ~trace ~state_idx ~ray_idx:(ray_idx + 1) - ~queue:(r :: queue) actions other_states (rs, bans) - | selected_ray :: other_rays -> ( - (* look for partners for the selected rays in actions *) - match - search_partners ~linear ~trace ~state_idx ~ray_idx - (selected_ray, queue @ other_rays, bans) - actions - with - (* interaction did nothing (no partner), try other rays *) - | [], new_actions -> - select_ray ~linear ~trace ~state_idx ~ray_idx:(ray_idx + 1) - ~queue:(selected_ray :: queue) new_actions other_states - (other_rays, bans) - (* interaction returns a result, keep it for the next round *) - | new_stars, new_actions -> - ( match trace with - | Some cfg when cfg.enabled && not cfg.web_mode -> print_trace_footer () - | _ -> () ); - (Some new_stars, new_actions) ) - -let rec select_star ~linear ~trace ~queue actions : - star list -> star list option * star list = function - | [] -> (None, actions) - (* select a state star and try finding a partner for each ray *) - | selected_state :: other_states -> ( - let state_idx = List.length queue in - match - select_ray ~linear ~trace ~state_idx ~ray_idx:0 ~queue:[] actions - other_states - (selected_state.content, selected_state.bans) - with - (* no success with this star, try other stars *) - | None, new_actions -> - select_star ~linear ~trace new_actions ~queue:(selected_state :: queue) - other_states - (* got new stars to add, construct the result for the next round *) - | Some new_stars, new_actions -> - (Some (List.rev queue @ other_states @ new_stars), new_actions) ) + (* Create a temporary state to format *) + let state = Lsc_trace.create ~mode:WebMode () in + state.collected_steps <- steps; + Lsc_trace.format_html state +(* Main execution function - delegates to lsc_exec *) let exec ?(linear = false) ?(trace = None) mcs : constellation = - (* do a sequence of rounds with a single interaction on state per round *) - let rec loop (actions, states) = - let trace_step_start () = - match trace with - | Some cfg when cfg.enabled -> - cfg.step_count <- cfg.step_count + 1; - cfg.fusion_detected <- false; - (* Store current constellations for fusion visualization *) - cfg.current_states <- states; - cfg.current_actions <- actions; - (* Record trace step for web mode *) - if cfg.web_mode then - add_trace_step cfg - { step_num = cfg.step_count - ; actions - ; states - ; selected_state_idx = None - ; selected_ray_idx = None - ; selected_action_idx = None - ; partner_ray = None - ; substitution = None - ; is_final = false - ; location = cfg.current_location - } - | _ -> () - in - trace_step_start (); - match select_star ~linear ~trace ~queue:[] actions states with - | None, _ -> - ( match trace with - | Some cfg when cfg.enabled -> - if cfg.web_mode then - add_trace_step cfg - { step_num = cfg.step_count + 1 - ; actions - ; states - ; selected_state_idx = None - ; selected_ray_idx = None - ; selected_action_idx = None - ; partner_ray = None - ; substitution = None - ; is_final = true - ; location = cfg.current_location - } - else ( - print_trace_header cfg.step_count cfg.current_location - (Some (green "Execution complete")); - Stdlib.Printf.printf "\n"; - print_trace_constellation (cyan "Final result:") states; - if not cfg.web_mode then print_trace_footer () ) - | _ -> () ); - states (* no more possible interaction *) - | Some res, new_actions -> loop (new_actions, res) - in - let cfg = extract_intspace mcs in - ( match trace with - | Some cfg when cfg.enabled && not cfg.web_mode -> - Stdlib.Printf.printf "%s\n" (bold (magenta "Starting execution trace...")); - Stdlib.Printf.printf "\n" - | _ -> () ); - loop cfg |> List.filter ~f:(fun s -> not @@ List.is_empty s.content) + match trace with + | None -> Lsc_exec.exec ~linear mcs + | Some cfg when cfg.enabled -> ( + match cfg.trace_state with + | Some state -> + (* Set location if available *) + Option.iter cfg.current_location ~f:(fun loc -> + Lsc_trace.set_location state (Some loc) ); + let handler = Lsc_trace.make_handler state in + Lsc_exec.exec ~linear ~on_event:handler mcs + | None -> Lsc_exec.exec ~linear mcs ) + | Some _ -> Lsc_exec.exec ~linear mcs diff --git a/src/lsc_exec.ml b/src/lsc_exec.ml new file mode 100644 index 0000000..a197fbc --- /dev/null +++ b/src/lsc_exec.ml @@ -0,0 +1,237 @@ +(* + * lsc_exec.ml - Queue-based execution engine for star fusion + * + * This module implements the core execution algorithm using an explicit + * work queue approach for clarity and efficiency. + *) + +open Base +open Lsc_ast +open Lsc_ast.StellarRays +open Lsc_ast.Raw + +(* ============================================================ + Type Definitions + ============================================================ *) + +(** A candidate fusion between a state ray and an action ray *) +type fusion_candidate = + { state_idx : int + ; state_ray_idx : int + ; action_idx : int + ; action_ray_idx : int + ; theta : substitution + ; state_star : star + ; action_star : star + ; other_action_rays : ray list (* rays before the matching one *) + } + +(** Result of searching for fusions *) +type fusion_result = + { new_stars : star list + ; remaining_actions : star list + } + +(** Configuration for execution *) +type exec_config = + { linear : bool + ; mutable var_counter : int + } + +(** Observable events during execution (for tracing) *) +type exec_event = + | StepStart of + { step : int + ; actions : constellation + ; states : constellation + } + | FusionFound of fusion_candidate + | StepComplete of + { step : int + ; result : constellation + } + | ExecutionDone of constellation + +(** Event handler type *) +type event_handler = exec_event -> unit + +(* ============================================================ + Core Fusion Logic + ============================================================ *) + +let fmap_ban ~f = function + | Ineq (b1, b2) -> Ineq (f b1, f b2) + | Incomp (b1, b2) -> Incomp (f b1, f b2) + +(** Perform fusion of two stars along matched rays *) +let perform_fusion ~repl1 ~repl2 ~other_state_rays ~other_action_rays + ~state_bans ~action_bans ~theta : star = + let new_state = List.map other_state_rays ~f:repl1 in + let new_action = List.map other_action_rays ~f:repl2 in + let nbans1 = List.map state_bans ~f:(fmap_ban ~f:repl1) in + let nbans2 = List.map action_bans ~f:(fmap_ban ~f:repl2) in + { content = List.map (new_state @ new_action) ~f:(subst theta) + ; bans = List.map (nbans1 @ nbans2) ~f:(fmap_ban ~f:(subst theta)) + } + +(** Check if bans are coherent (no contradictions) *) +let coherent_bans bans = + let inequalities, incompatibles = + List.fold bans ~init:([], []) ~f:(fun (ineqs, incomps) ban -> + match ban with + | Ineq (b1, b2) -> ((b1, b2) :: ineqs, incomps) + | Incomp (b1, b2) -> (ineqs, (b1, b2) :: incomps) ) + in + let ineqs_ok = + List.for_all inequalities ~f:(fun (b1, b2) -> not (equal_ray b1 b2)) + in + let incomps_ok = + let rec check = function + | [] -> true + | (box, slice) :: rest -> + let conflict = + List.exists rest ~f:(fun (b, s) -> + equal_ray box b && not (equal_ray slice s) ) + in + (not conflict) && check rest + in + check incompatibles + in + ineqs_ok && incomps_ok + +(* ============================================================ + Candidate Finding - Queue-Based Approach + ============================================================ *) + +(** Find all fusion candidates between a state ray and an action star. Returns + list of (action_ray_idx, rays_before, theta) *) +let find_action_matches ~repl1 ~repl2 (state_ray : ray) (action : star) : + (int * ray list * substitution) list = + let rec scan idx before = function + | [] -> [] + | r :: rest when not (is_polarised r) -> + (* Skip unpolarized rays *) + scan (idx + 1) (r :: before) rest + | r :: rest -> ( + match raymatcher (repl1 state_ray) (repl2 r) with + | None -> scan (idx + 1) (r :: before) rest + | Some theta -> + (* Found match, continue scanning for more *) + let remaining = scan (idx + 1) (r :: before) rest in + (idx, List.rev before @ rest, theta) :: remaining ) + in + scan 0 [] action.content + +(** Find all fusions for a given state ray against all actions. This is the core + work queue processor for a single ray. *) +let find_ray_fusions ~config ~emit_event ~state_idx ~state_ray_idx ~state_ray + ~other_state_rays ~state_bans (actions : star list) : fusion_result = + let repl1 = replace_indices config.var_counter in + let results = ref [] in + let consumed_actions = ref [] in + + List.iteri actions ~f:(fun action_idx action -> + let repl2 = replace_indices (config.var_counter + 1) in + let matches = find_action_matches ~repl1 ~repl2 state_ray action in + + List.iter matches ~f:(fun (action_ray_idx, other_action_rays, theta) -> + let candidate = + { state_idx + ; state_ray_idx + ; action_idx + ; action_ray_idx + ; theta + ; state_star = + { content = state_ray :: other_state_rays; bans = state_bans } + ; action_star = action + ; other_action_rays + } + in + emit_event (FusionFound candidate); + + let fused = + perform_fusion ~repl1 ~repl2 ~other_state_rays ~other_action_rays + ~state_bans ~action_bans:action.bans ~theta + in + if coherent_bans fused.bans then ( + results := fused :: !results; + config.var_counter <- config.var_counter + 2; + if config.linear then + consumed_actions := action_idx :: !consumed_actions ) ) ); + + let remaining = + if config.linear then + List.filter_mapi actions ~f:(fun i a -> + if List.mem !consumed_actions i ~equal:Int.equal then None else Some a ) + else actions + in + { new_stars = List.rev !results; remaining_actions = remaining } + +(** Try to find fusions for any ray in a state star *) +let try_state_star ~config ~emit_event ~state_idx (state : star) + (actions : star list) : (star list * star list) option = + let rec try_ray ray_idx before = function + | [] -> None + | r :: rest when not (is_polarised r) -> + try_ray (ray_idx + 1) (r :: before) rest + | state_ray :: rest -> + let other_rays = List.rev_append before rest in + let result = + find_ray_fusions ~config ~emit_event ~state_idx ~state_ray_idx:ray_idx + ~state_ray ~other_state_rays:other_rays ~state_bans:state.bans actions + in + if List.is_empty result.new_stars then + try_ray (ray_idx + 1) (state_ray :: before) rest + else Some (result.new_stars, result.remaining_actions) + in + try_ray 0 [] state.content + +(* ============================================================ + Main Execution Loop + ============================================================ *) + +(** Process the work queue: find first state that can interact *) +let rec process_queue ~config ~emit_event ~queue_idx ~before actions = function + | [] -> None + | state :: rest -> ( + match + try_state_star ~config ~emit_event ~state_idx:queue_idx state actions + with + | None -> + process_queue ~config ~emit_event ~queue_idx:(queue_idx + 1) + ~before:(state :: before) actions rest + | Some (new_stars, new_actions) -> + let new_states = List.rev_append before rest @ new_stars in + Some (new_states, new_actions) ) + +(** Main execution function *) +let exec ?(linear = false) ?(on_event = fun _ -> ()) mcs : constellation = + let config = { linear; var_counter = 0 } in + + (* Separate into actions and states *) + let actions, states = + let rec classify acts sts = function + | [] -> (List.rev acts, List.rev sts) + | Marked.State s :: rest -> classify acts (s :: sts) rest + | Marked.Action s :: rest -> classify (s :: acts) sts rest + in + classify [] [] mcs + in + + let rec loop step actions states = + on_event (StepStart { step; actions; states }); + + match + process_queue ~config ~emit_event:on_event ~queue_idx:0 ~before:[] actions + states + with + | None -> + on_event (ExecutionDone states); + states + | Some (new_states, new_actions) -> + on_event (StepComplete { step; result = new_states }); + loop (step + 1) new_actions new_states + in + + loop 1 actions states + |> List.filter ~f:(fun s -> not @@ List.is_empty s.content) diff --git a/src/lsc_trace.ml b/src/lsc_trace.ml new file mode 100644 index 0000000..d610133 --- /dev/null +++ b/src/lsc_trace.ml @@ -0,0 +1,250 @@ +(* + * lsc_trace.ml - Trace visualization for execution + * + * This module provides tracing capabilities that plug into the + * event-based execution engine. + *) + +open Base +open Lsc_ast.Raw +open Lsc_pretty + +(* ============================================================ + Source Location Tracking + ============================================================ *) + +type source_location = + { filename : string + ; line : int + ; column : int + } + +let get_source_line filename line_num = + try + let ic = Stdlib.open_in filename in + let rec skip n = + if n <= 1 then () + else ( + ignore (Stdlib.input_line ic); + skip (n - 1) ) + in + skip line_num; + let line = Stdlib.input_line ic in + Stdlib.close_in ic; + Some line + with _ -> None + +(* ============================================================ + Terminal Colors + ============================================================ *) + +let cyan text = "\x1b[36m" ^ text ^ "\x1b[0m" + +let green text = "\x1b[32m" ^ text ^ "\x1b[0m" + +let yellow text = "\x1b[33m" ^ text ^ "\x1b[0m" + +let magenta text = "\x1b[35m" ^ text ^ "\x1b[0m" + +let bold text = "\x1b[1m" ^ text ^ "\x1b[0m" + +let dim text = "\x1b[2m" ^ text ^ "\x1b[0m" + +(* ============================================================ + Trace State + ============================================================ *) + +type trace_mode = + | Interactive (* Wait for keypress between steps *) + | Batch (* Print all steps without waiting *) + | Silent (* Don't print, just collect *) + | WebMode (* Collect for HTML output *) + +type trace_state = + { mode : trace_mode + ; mutable location : source_location option + ; mutable collected_steps : collected_step list + ; mutable fusion_shown_this_step : bool + } + +and collected_step = + { step_num : int + ; actions : constellation + ; states : constellation + ; is_final : bool + } + +let create ?(mode = Interactive) () = + { mode + ; location = None + ; collected_steps = [] + ; fusion_shown_this_step = false + } + +let set_location state loc = state.location <- loc + +(* ============================================================ + Terminal Output + ============================================================ *) + +let wait_for_keypress () = ignore (Stdlib.input_line Stdlib.stdin) + +let print_header step_num location status = + Stdlib.Printf.printf "\n%s\n" (String.make 80 '='); + Stdlib.Printf.printf "%s %s" + (bold (cyan "Step")) + (bold (yellow (Int.to_string step_num))); + Option.iter status ~f:(fun msg -> Stdlib.Printf.printf " - %s" (bold msg)); + ( match location with + | Some loc -> ( + Stdlib.Printf.printf "\n%s %s:%d:%d" (dim "at") loc.filename loc.line + loc.column; + match get_source_line loc.filename loc.line with + | Some line -> + let trimmed = String.strip line in + if not (String.is_empty trimmed) then + Stdlib.Printf.printf "\n %s %s" (dim "│") (dim trimmed) + | None -> () ) + | None -> () ); + Stdlib.Printf.printf "\n%s\n" (String.make 80 '=') + +let print_constellation label stars = + if List.is_empty stars then + Stdlib.Printf.printf "%s %s\n" (bold label) (dim "{}") + else begin + Stdlib.Printf.printf "%s\n" (bold label); + List.iteri stars ~f:(fun i star -> + Stdlib.Printf.printf " %s %s\n" + (dim (Printf.sprintf "[%d]" i)) + (string_of_star star) ) + end + +let print_footer () = + Stdlib.Printf.printf "\n%s\n" (dim "Press Enter to continue..."); + Stdlib.flush Stdlib.stdout; + wait_for_keypress () + +(* ============================================================ + Event Handler Factory + ============================================================ *) + +let make_handler state : Lsc_exec.event_handler = + let open Lsc_exec in + function + | StepStart { step; actions; states } -> ( + state.fusion_shown_this_step <- false; + match state.mode with + | Silent | WebMode -> + state.collected_steps <- + { step_num = step; actions; states; is_final = false } + :: state.collected_steps + | Interactive | Batch -> () (* We'll print on fusion or completion *) ) + | FusionFound candidate -> ( + match state.mode with + | Silent | WebMode -> () + | (Interactive | Batch) when not state.fusion_shown_this_step -> + state.fusion_shown_this_step <- true; + print_header candidate.state_idx state.location + (Some (magenta "Fusion detected!")); + Stdlib.Printf.printf "\n"; + Stdlib.Printf.printf " State star [%d], ray %d\n" candidate.state_idx + candidate.state_ray_idx; + Stdlib.Printf.printf " Action star [%d], ray %d\n" candidate.action_idx + candidate.action_ray_idx; + if not (List.is_empty candidate.theta) then + Stdlib.Printf.printf " %s %s\n" (dim "θ =") + (yellow (string_of_subst candidate.theta)) + | _ -> () ) + | StepComplete { step = _; result = _ } -> ( + match state.mode with + | Interactive -> print_footer () + | Batch -> Stdlib.Printf.printf "\n" + | Silent | WebMode -> () ) + | ExecutionDone result -> ( + match state.mode with + | Silent | WebMode -> + state.collected_steps <- + { step_num = List.length state.collected_steps + 1 + ; actions = [] + ; states = result + ; is_final = true + } + :: state.collected_steps + | Interactive | Batch -> + print_header + (List.length state.collected_steps + 1) + state.location + (Some (green "Execution complete")); + Stdlib.Printf.printf "\n"; + print_constellation (cyan "Final result:") result; + if phys_equal state.mode Interactive then print_footer () ) + +(* ============================================================ + HTML Output for Web Mode + ============================================================ *) + +let escape_html s = + String.substr_replace_all s ~pattern:"&" ~with_:"&" + |> String.substr_replace_all ~pattern:"<" ~with_:"<" + |> String.substr_replace_all ~pattern:">" ~with_:">" + |> String.substr_replace_all ~pattern:"\"" ~with_:""" + +let format_html state = + let buffer = Buffer.create 1024 in + let add str = Buffer.add_string buffer str in + let add_line str = + add str; + add "\n" + in + + let steps = List.rev state.collected_steps in + List.iter steps ~f:(fun step -> + add_line "
"; + if step.is_final then begin + add_line + (Printf.sprintf + "
Execution Complete (Step %d)
" + step.step_num ); + add_line "
"; + add_line "
Final Result:
"; + add_line "
"; + List.iteri step.states ~f:(fun idx star -> + add_line + (Printf.sprintf "
[%d] %s
" idx + (escape_html (string_of_star star)) ) ); + add_line "
"; + add_line "
" + end + else begin + add_line + (Printf.sprintf "
Step %d
" step.step_num); + add_line "
"; + add_line "
"; + add_line "
Actions:
"; + if List.is_empty step.actions then add_line "
{ }
" + else begin + add_line "
"; + List.iteri step.actions ~f:(fun idx star -> + add_line + (Printf.sprintf "
[%d] %s
" idx + (escape_html (string_of_star star)) ) ); + add_line "
" + end; + add_line "
"; + add_line "
"; + add_line "
States:
"; + if List.is_empty step.states then add_line "
{ }
" + else begin + add_line "
"; + List.iteri step.states ~f:(fun idx star -> + add_line + (Printf.sprintf "
[%d] %s
" idx + (escape_html (string_of_star star)) ) ); + add_line "
" + end; + add_line "
"; + add_line "
" + end; + add_line "
" ); + + Buffer.contents buffer From 7071f2804f50ef23984121e8ab8f78c050ad584c Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 25 Dec 2025 21:58:30 +0100 Subject: [PATCH 2/5] Remove occurrences of failwith --- src/expr.ml | 34 ++++++++++++++++++++++++++++++++-- src/expr_err.ml | 7 +++++++ src/lexer.ml | 4 +++- src/sgen_eval.ml | 23 ++++++++++++++++++++++- src/sgen_parsing.ml | 11 +++++++---- 5 files changed, 71 insertions(+), 8 deletions(-) diff --git a/src/expr.ml b/src/expr.ml index 4896edf..45ea5bc 100644 --- a/src/expr.ml +++ b/src/expr.ml @@ -3,6 +3,8 @@ open Lsc_ast open Sgen_ast open Expr_err +exception MacroError of expr_err * source_location option + let ( let* ) x f = Result.bind x ~f type ident = string @@ -296,7 +298,21 @@ let unfold_decl_def (macro_env : (string * (string list * expr loc list)) list) match arg.content with | Var x -> x | Symbol "..." -> "..." (* Allow ... as a symbol *) - | _ -> failwith "error: syntax declaration must contain variables" ) + | Symbol s -> + raise + (MacroError + ( InvalidMacroArgument + (Printf.sprintf + "macro argument '%s' must be a variable (start with \ + uppercase)" + s ) + , arg.loc ) ) + | List _ -> + raise + (MacroError + ( InvalidMacroArgument + "macro argument must be a variable, not a list" + , arg.loc ) ) ) in (macro_name, (var_args, body)) :: acc | _ -> acc ) @@ -362,7 +378,21 @@ let extract_macros (raw_exprs : Raw.t list) : macro_env = match arg.content with | Var x -> x | Symbol "..." -> "..." (* Allow ... as a symbol *) - | _ -> failwith "error: syntax declaration must contain variables" ) + | Symbol s -> + raise + (MacroError + ( InvalidMacroArgument + (Printf.sprintf + "macro argument '%s' must be a variable (start with \ + uppercase)" + s ) + , arg.loc ) ) + | List _ -> + raise + (MacroError + ( InvalidMacroArgument + "macro argument must be a variable, not a list" + , arg.loc ) ) ) in ((macro_name, (var_args, body)) :: env, acc) | _ -> (env, acc) diff --git a/src/expr_err.ml b/src/expr_err.ml index b145122..0d7c41a 100644 --- a/src/expr_err.ml +++ b/src/expr_err.ml @@ -4,3 +4,10 @@ type expr_err = | InvalidBan of string | InvalidRaylist of string | InvalidDeclaration of string + | InvalidMacroArgument of string + | InvalidBanStructure of string + | CircularImport of string + | FileLoadError of + { filename : string + ; message : string + } diff --git a/src/lexer.ml b/src/lexer.ml index e451bb1..34d3ebb 100644 --- a/src/lexer.ml +++ b/src/lexer.ml @@ -21,7 +21,9 @@ let opposite_delimiter = function | ')' -> '(' | ']' -> '[' | '}' -> '{' - | c -> failwith (Printf.sprintf "Compiler error: '%c' is not a delimiter." c) + | _ -> + (* This case should be unreachable - if hit, it indicates a bug in the lexer *) + assert false let pop_delimiter sym (pos : Lexing.position) = match !delimiters_stack with diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index 6c5924a..05e8b96 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -3,8 +3,11 @@ open Lsc_ast open Lsc_pretty open Lsc_eval open Sgen_ast +open Expr_err open Out_channel +exception EvalError of expr_err * source_location option + let ( let* ) x f = Result.bind x ~f let unifiable r r' = StellarRays.solution [ (r, r') ] |> Option.is_some @@ -118,7 +121,13 @@ and ban_of_term (t : StellarRays.term) : ban = match t with | Func ((Null, "!="), [ r1; r2 ]) -> Ineq (r1, r2) | Func ((Null, "slice"), [ r1; r2 ]) -> Incomp (r1, r2) - | _ -> failwith "Invalid ban structure" + | _ -> + raise + (EvalError + ( InvalidBanStructure + (Printf.sprintf "expected '!=' or 'slice' constraint, got: %s" + (string_of_ray t) ) + , None ) ) (* Global trace config for CLI trace mode *) let cli_trace_config : Lsc_eval.trace_config option ref = ref None @@ -344,6 +353,18 @@ let pp_err error : (string, err) Result.t = | InvalidDeclaration expr -> ( Printf.sprintf "expression '%s' is not a valid declaration" expr , "Declarations must use def, show, ==, or use." ) + | InvalidMacroArgument msg -> + ( Printf.sprintf "invalid macro argument: %s" msg + , "Macro arguments must be variables (start with uppercase)." ) + | InvalidBanStructure msg -> + ( Printf.sprintf "invalid ban structure: %s" msg + , "Ban expressions must use != or 'slice' with two arguments." ) + | CircularImport path -> + ( Printf.sprintf "circular import detected: %s" path + , "Check your import chain for cycles." ) + | FileLoadError { filename; message } -> + ( Printf.sprintf "failed to load file '%s': %s" filename message + , "Check that the file exists and is readable." ) in let header = bold (red "error") ^ ": " ^ bold error_msg in let loc_str = diff --git a/src/sgen_parsing.ml b/src/sgen_parsing.ml index c85a0c3..20bc2aa 100644 --- a/src/sgen_parsing.ml +++ b/src/sgen_parsing.ml @@ -2,6 +2,9 @@ open Base open Lexing open Lexer open Parser +open Expr_err + +exception ImportError of expr_err let red text = "\x1b[31m" ^ text ^ "\x1b[0m" @@ -230,8 +233,7 @@ let rec load_macro_file (filename : string) (current_file : string) (* Check for circular imports *) if List.mem visited resolved_filename ~equal:String.equal then - failwith - (Printf.sprintf "Circular macro import detected: %s" resolved_filename); + raise (ImportError (CircularImport resolved_filename)); let visited = resolved_filename :: visited in @@ -257,8 +259,9 @@ let rec load_macro_file (filename : string) (current_file : string) (* Later imports override earlier ones *) nested_macros @ file_macros with Sys_error msg -> - failwith - (Printf.sprintf "Error loading macro file '%s': %s" resolved_filename msg) + raise + (ImportError + (FileLoadError { filename = resolved_filename; message = msg }) ) (* Preprocess with macro imports *) let preprocess_with_imports (source_file : string) (raw_exprs : Expr.Raw.t list) From 01d27dad3fbfb225a49e2ea12ac198709927a65d Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 25 Dec 2025 22:14:26 +0100 Subject: [PATCH 3/5] Improve handling of I/O --- src/dune | 2 +- src/lsc_trace.ml | 21 ++++++------- src/sgen_eval.ml | 33 ++++++++++---------- src/sgen_parsing.ml | 75 +++++++++++++++++++++++---------------------- 4 files changed, 66 insertions(+), 65 deletions(-) diff --git a/src/dune b/src/dune index 9659380..d322a96 100644 --- a/src/dune +++ b/src/dune @@ -1,6 +1,6 @@ (library (name stellogen) - (libraries base menhirLib) + (libraries base stdio menhirLib) (preprocess (pps sedlex.ppx ppx_deriving.show ppx_deriving.ord ppx_deriving.eq))) diff --git a/src/lsc_trace.ml b/src/lsc_trace.ml index d610133..ba9d8d7 100644 --- a/src/lsc_trace.ml +++ b/src/lsc_trace.ml @@ -6,6 +6,7 @@ *) open Base +open Stdio open Lsc_ast.Raw open Lsc_pretty @@ -21,17 +22,15 @@ type source_location = let get_source_line filename line_num = try - let ic = Stdlib.open_in filename in - let rec skip n = - if n <= 1 then () - else ( - ignore (Stdlib.input_line ic); - skip (n - 1) ) - in - skip line_num; - let line = Stdlib.input_line ic in - Stdlib.close_in ic; - Some line + In_channel.with_file filename ~f:(fun ic -> + let rec skip n = + if n <= 1 then () + else ( + ignore (In_channel.input_line_exn ic); + skip (n - 1) ) + in + skip line_num; + In_channel.input_line ic ) with _ -> None (* ============================================================ diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index 05e8b96..7e487eb 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -1,10 +1,10 @@ open Base +open Stdio open Lsc_ast open Lsc_pretty open Lsc_eval open Sgen_ast open Expr_err -open Out_channel exception EvalError of expr_err * source_location option @@ -226,17 +226,15 @@ let pp_err error : (string, err) Result.t = let get_source_line filename line_num = try - let ic = Stdlib.open_in filename in - let rec skip_lines n = - if n <= 1 then () - else ( - ignore (Stdlib.input_line ic); - skip_lines (n - 1) ) - in - skip_lines line_num; - let line = Stdlib.input_line ic in - Stdlib.close_in ic; - Some line + In_channel.with_file filename ~f:(fun ic -> + let rec skip_lines n = + if n <= 1 then () + else ( + ignore (In_channel.input_line_exn ic); + skip_lines (n - 1) ) + in + skip_lines line_num; + In_channel.input_line ic ) with _ -> None in @@ -491,9 +489,12 @@ let rec eval_sgen_expr (env : env) : let create_start_pos fname = { Lexing.pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 } in - let lexbuf = Sedlexing.Utf8.from_channel (Stdlib.open_in filename) in - Sedlexing.set_position lexbuf (create_start_pos filename); - let expr = Sgen_parsing.parse_with_error filename lexbuf in + let expr = + In_channel.with_file filename ~f:(fun ic -> + let lexbuf = Sedlexing.Utf8.from_channel ic in + Sedlexing.set_position lexbuf (create_start_pos filename); + Sgen_parsing.parse_with_error filename lexbuf ) + in let preprocessed = Sgen_parsing.preprocess_with_imports filename expr in match Expr.program_of_expr preprocessed with | Ok program -> @@ -517,7 +518,7 @@ and eval_program (p : program) = | Ok env -> Ok env | Error e -> let* pp = pp_err e in - output_string stderr pp; + Out_channel.output_string Out_channel.stderr pp; Error e and eval_program_internal (env : env) (p : program) = diff --git a/src/sgen_parsing.ml b/src/sgen_parsing.ml index 20bc2aa..f3f6fc3 100644 --- a/src/sgen_parsing.ml +++ b/src/sgen_parsing.ml @@ -1,4 +1,5 @@ open Base +open Stdio open Lexing open Lexer open Parser @@ -30,18 +31,18 @@ let string_of_token = function let is_end_delimiter = function RPAR | RBRACK | RBRACE -> true | _ -> false let get_line filename line_num = - let ic = Stdlib.open_in filename in - let rec skip_lines n = - if n <= 0 then () - else - match Stdlib.input_line ic with - | exception End_of_file -> () - | _ -> skip_lines (n - 1) - in - skip_lines (line_num - 1); - let result = try Some (Stdlib.input_line ic) with End_of_file -> None in - Stdlib.close_in ic; - result + try + In_channel.with_file filename ~f:(fun ic -> + let rec skip_lines n = + if n <= 0 then () + else + match In_channel.input_line ic with + | None -> () + | Some _ -> skip_lines (n - 1) + in + skip_lines (line_num - 1); + In_channel.input_line ic ) + with Sys_error _ -> None let unexpected_token_msg () = match !last_token with @@ -237,31 +238,31 @@ let rec load_macro_file (filename : string) (current_file : string) let visited = resolved_filename :: visited in - try - let ic = Stdlib.open_in resolved_filename in - let lexbuf = Sedlexing.Utf8.from_channel ic in - Sedlexing.set_filename lexbuf resolved_filename; - - let expr = parse_with_error resolved_filename lexbuf in - Stdlib.close_in ic; - - (* First, recursively load imports from this file *) - let nested_imports = Expr.collect_macro_imports expr in - let nested_macros = - List.concat_map nested_imports ~f:(fun import_path -> - load_macro_file import_path resolved_filename visited ) - in - - (* Then extract macros from this file *) - let file_macros = Expr.extract_macros expr in - - (* Combine nested macros with this file's macros *) - (* Later imports override earlier ones *) - nested_macros @ file_macros - with Sys_error msg -> - raise - (ImportError - (FileLoadError { filename = resolved_filename; message = msg }) ) + let expr = + try + In_channel.with_file resolved_filename ~f:(fun ic -> + let lexbuf = Sedlexing.Utf8.from_channel ic in + Sedlexing.set_filename lexbuf resolved_filename; + parse_with_error resolved_filename lexbuf ) + with Sys_error msg -> + raise + (ImportError + (FileLoadError { filename = resolved_filename; message = msg }) ) + in + + (* First, recursively load imports from this file *) + let nested_imports = Expr.collect_macro_imports expr in + let nested_macros = + List.concat_map nested_imports ~f:(fun import_path -> + load_macro_file import_path resolved_filename visited ) + in + + (* Then extract macros from this file *) + let file_macros = Expr.extract_macros expr in + + (* Combine nested macros with this file's macros *) + (* Later imports override earlier ones *) + nested_macros @ file_macros (* Preprocess with macro imports *) let preprocess_with_imports (source_file : string) (raw_exprs : Expr.Raw.t list) From aa3bca62b48c6db0c3755cf91190611ddf30c085 Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 25 Dec 2025 22:22:19 +0100 Subject: [PATCH 4/5] Refactor macro expansion --- src/expr.ml | 247 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 141 insertions(+), 106 deletions(-) diff --git a/src/expr.ml b/src/expr.ml index 45ea5bc..53ebac1 100644 --- a/src/expr.ml +++ b/src/expr.ml @@ -140,6 +140,141 @@ let rec replace_id (var_from : ident) replacement (expr : expr loc) : expr loc = ; loc = expr.loc } +(* --------------------------------------- + Macro Expansion Helpers + --------------------------------------- *) + +(* Check if a pattern's formal params indicate variadic (ends with Var ...) *) +let is_variadic_pattern (formal_params : string list) : bool = + match List.rev formal_params with "..." :: _ :: _ -> true | _ -> false + +(* Calculate minimum arguments for a pattern *) +let min_args_for_pattern (formal_params : string list) : int = + if is_variadic_pattern formal_params then + match List.rev formal_params with + | "..." :: _var :: rest -> List.length rest + | _ -> List.length formal_params + else List.length formal_params + +(* Check if a pattern matches the given argument count *) +let pattern_matches_args (formal_params : string list) (arg_count : int) : bool + = + let min_args = min_args_for_pattern formal_params in + if is_variadic_pattern formal_params then arg_count >= min_args + else arg_count = min_args + +(* Split formal params into fixed params and optional variadic param name *) +let split_variadic_params (formal_params : string list) : + string list * string option = + if is_variadic_pattern formal_params then + match List.rev formal_params with + | "..." :: var :: rest -> (List.rev rest, Some var) + | _ -> (formal_params, None) + else (formal_params, None) + +(* Find the best matching pattern for a macro name. + Prefers exact (non-variadic) matches over variadic ones. *) +let find_matching_pattern + (all_patterns : (string * (string list * expr loc list)) list) + (arg_count : int) : (string list * expr loc list) option = + (* First try exact (non-variadic) matches *) + match + List.find all_patterns ~f:(fun (_, (params, _)) -> + pattern_matches_args params arg_count && not (is_variadic_pattern params) ) + with + | Some (_, pattern) -> Some pattern + | None -> + (* Then try variadic matches *) + List.find_map all_patterns ~f:(fun ((_, (params, _)) as pattern) -> + if pattern_matches_args params arg_count then Some (snd pattern) else None ) + +(* Apply substitution to an expression, handling variadic splicing. + - subst_pairs: fixed param -> arg mappings + - variadic_param: optional name of variadic param + - rest_args: arguments captured by variadic param *) +let rec apply_variadic_substitution (subst_pairs : (string * expr loc) list) + (variadic_param : string option) (rest_args : expr loc list) (e : expr loc) : + expr loc = + match (e.content, variadic_param) with + | List subexprs, Some vp -> + (* Scan for Var ... pattern and splice *) + let rec splice_list exprs = + match exprs with + | { content = Var v; _ } :: { content = Symbol "..."; _ } :: rest + when String.equal v vp -> + (* Found the pattern - splice in rest_args at this position *) + rest_args @ splice_list rest + | e :: rest -> + (* Recursively substitute in this element, then continue *) + apply_variadic_substitution subst_pairs variadic_param rest_args e + :: splice_list rest + | [] -> [] + in + { content = List (splice_list subexprs); loc = e.loc } + | List subexprs, None -> + (* No variadic param - just recurse *) + { content = + List + (List.map subexprs + ~f: + (apply_variadic_substitution subst_pairs variadic_param rest_args) ) + ; loc = e.loc + } + | Var v, Some vp when String.equal v vp -> + (* Variadic param used alone without ... - wrap rest_args in a list *) + { content = List rest_args; loc = e.loc } + | Var v, _ -> ( + match List.Assoc.find subst_pairs v ~equal:String.equal with + | Some replacement -> { replacement with loc = e.loc } + | None -> e ) + | _, _ -> e + +(* Expand a single matched macro: substitute params and recursively expand *) +let expand_matched_macro + (macro_env : (string * (string list * expr loc list)) list) + (expand_fn : + (string * (string list * expr loc list)) list -> expr loc -> expr loc list + ) (formal_params : string list) (body : expr loc list) + (call_args : expr loc list) (call_loc : source_location option) : + expr loc list = + let fixed_params, variadic_param = split_variadic_params formal_params in + let min_args = List.length fixed_params in + (* First, recursively expand macros in the arguments *) + let expanded_args = + List.map call_args ~f:(fun arg -> + match expand_fn macro_env arg with + | [ single ] -> single + | multiple -> { content = List multiple; loc = arg.loc } ) + in + (* Split into fixed and variadic args *) + let fixed_args, rest_args = List.split_n expanded_args min_args in + (* Build substitution environment *) + let subst_pairs = List.zip_exn fixed_params fixed_args in + (* Apply substitution to body *) + let substituted = + List.map body + ~f:(apply_variadic_substitution subst_pairs variadic_param rest_args) + in + (* Recursively expand macros in the substituted body *) + let expanded = List.concat_map substituted ~f:(expand_fn macro_env) in + (* Attach the call site location to the expanded expressions *) + List.map expanded ~f:(fun e -> { e with loc = call_loc }) + +(* Expand macros in a list of arguments, coalescing results *) +let expand_args_in_list + (macro_env : (string * (string list * expr loc list)) list) + (expand_fn : + (string * (string list * expr loc list)) list -> expr loc -> expr loc list + ) (args : expr loc list) : expr loc list = + List.map args ~f:(fun arg -> + match expand_fn macro_env arg with + | [ single ] -> single + | multiple -> { content = List multiple; loc = arg.loc } ) + +(* --------------------------------------- + Main Macro Expansion + --------------------------------------- *) + (* Recursively expand macros in an expression *) let rec expand_macros_in_expr (macro_env : (string * (string list * expr loc list)) list) (expr : expr loc) @@ -157,112 +292,15 @@ let rec expand_macros_in_expr let all_patterns = List.filter macro_env ~f:(fun (name, _) -> String.equal name macro_name) in - - (* Helper to check if a pattern matches the argument count *) - let pattern_matches (formal_params, _body) = - let is_variadic = - match List.rev formal_params with "..." :: _ :: _ -> true | _ -> false - in - let min_args = - if is_variadic then - match List.rev formal_params with - | "..." :: _var :: rest -> List.length rest - | _ -> List.length formal_params - else List.length formal_params - in - let arg_count = List.length call_args in - if is_variadic then arg_count >= min_args else arg_count = min_args - in - - (* Find the best matching pattern: prefer exact matches (non-variadic) over variadic *) - let matching_pattern = - (* First try exact matches *) - match - List.find all_patterns ~f:(fun (_, pattern) -> - pattern_matches pattern - && not - ( match List.rev (fst pattern) with - | "..." :: _ :: _ -> true - | _ -> false ) ) - with - | Some (_, pattern) -> Some pattern - | None -> - (* Then try variadic matches *) - List.find_map all_patterns ~f:(fun (_, pattern) -> - if pattern_matches pattern then Some pattern else None ) - in - - match matching_pattern with + let arg_count = List.length call_args in + match find_matching_pattern all_patterns arg_count with | Some (formal_params, body) -> - (* Check if this is a variadic macro (ends with ...) *) - let is_variadic = - match List.rev formal_params with "..." :: _ :: _ -> true | _ -> false - in - let fixed_params, variadic_param = - if is_variadic then - match List.rev formal_params with - | "..." :: var :: rest -> (List.rev rest, Some var) - | _ -> (formal_params, None) - else (formal_params, None) - in - let min_args = List.length fixed_params in - (* First, recursively expand macros in the arguments *) - let expanded_args = - List.map call_args ~f:(fun arg -> - match expand_macros_in_expr macro_env arg with - | [ single ] -> single - | multiple -> { content = List multiple; loc = arg.loc } ) - in - (* Split into fixed and variadic args *) - let fixed_args, rest_args = List.split_n expanded_args min_args in - (* Build substitution environment *) - let subst_pairs = List.zip_exn fixed_params fixed_args in - (* Helper to substitute with variadic support *) - let rec apply_substitution_var e = - match (e.content, variadic_param) with - | List subexprs, Some vp -> - (* Scan for Var ... pattern and splice *) - let rec splice_list exprs = - match exprs with - | { content = Var v; _ } :: { content = Symbol "..."; _ } :: rest - when String.equal v vp -> - (* Found the pattern - splice in rest_args at this position *) - rest_args @ splice_list rest - | e :: rest -> - (* Recursively substitute in this element, then continue *) - apply_substitution_var e :: splice_list rest - | [] -> [] - in - { content = List (splice_list subexprs); loc = e.loc } - | List subexprs, None -> - (* No variadic param - just recurse *) - { content = List (List.map subexprs ~f:apply_substitution_var) - ; loc = e.loc - } - | Var v, Some vp when String.equal v vp -> - (* Variadic param used alone without ... - this is an error in most cases, - but we handle it by wrapping rest_args in a list *) - { content = List rest_args; loc = e.loc } - | Var v, _ -> ( - match List.Assoc.find subst_pairs v ~equal:String.equal with - | Some replacement -> { replacement with loc = e.loc } - | None -> e ) - | _, _ -> e - in - let substituted = List.map body ~f:apply_substitution_var in - (* Recursively expand macros in the substituted body *) - let expanded = - List.concat_map substituted ~f:(expand_macros_in_expr macro_env) - in - (* Attach the call site location to the expanded expressions *) - List.map expanded ~f:(fun e -> { e with loc = expr.loc }) + expand_matched_macro macro_env expand_macros_in_expr formal_params body + call_args expr.loc | None -> (* Not a macro - recursively expand in sub-expressions *) let expanded_subexprs = - List.map call_args ~f:(fun arg -> - match expand_macros_in_expr macro_env arg with - | [ single ] -> single - | multiple -> { content = List multiple; loc = arg.loc } ) + expand_args_in_list macro_env expand_macros_in_expr call_args in [ { expr with content = @@ -274,10 +312,7 @@ let rec expand_macros_in_expr (* Regular list - recursively expand in sub-expressions *) | List subexprs -> let expanded_subexprs = - List.map subexprs ~f:(fun sub -> - match expand_macros_in_expr macro_env sub with - | [ single ] -> single - | multiple -> { content = List multiple; loc = sub.loc } ) + expand_args_in_list macro_env expand_macros_in_expr subexprs in [ { expr with content = List expanded_subexprs } ] (* Atoms - no expansion needed *) From 14fd68a2dbd0b0b9868af88862fd1461dbd3be5e Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 25 Dec 2025 22:38:16 +0100 Subject: [PATCH 5/5] Make error messages consistent Add docs Update docs Remove doc Remove docs --- docs/interaction_nets_and_combinators.md | 1496 +++++++++------------- src/lsc_trace.ml | 17 +- src/sgen_eval.ml | 34 +- src/sgen_parsing.ml | 21 +- src/terminal.ml | 43 + 5 files changed, 686 insertions(+), 925 deletions(-) create mode 100644 src/terminal.ml diff --git a/docs/interaction_nets_and_combinators.md b/docs/interaction_nets_and_combinators.md index daf55b4..05bbb60 100644 --- a/docs/interaction_nets_and_combinators.md +++ b/docs/interaction_nets_and_combinators.md @@ -1,1124 +1,872 @@ -# Interaction Nets and Combinators in Stellogen +# Interaction Nets, Proof-Nets, and Stellogen -> **Disclaimer**: This document was written with the assistance of Claude Code and represents exploratory research and analysis. The content may contain inaccuracies or misinterpretations and should not be taken as definitive statements about the Stellogen language implementation. - -**Author:** Research Report -**Date:** 2025-10-12 -**Status:** Research Document - -## Table of Contents - -1. [Introduction](#introduction) -2. [Background: Interaction Nets](#background-interaction-nets) -3. [Interaction Combinators](#interaction-combinators) -4. [Related Projects](#related-projects) -5. [Encoding Interaction Nets in Stellogen](#encoding-interaction-nets-in-stellogen) -6. [Stellogen vs. Traditional Interaction Combinators](#stellogen-vs-traditional-interaction-combinators) -7. [Examples and Analysis](#examples-and-analysis) -8. [Future Directions](#future-directions) -9. [References](#references) +**Research Report: Implementation Directions** +**Date:** 2025-12-25 +**Status:** Technical Analysis with Implementation Insights --- -## Introduction +## 1. Introduction -This document explores the relationship between **interaction nets**, **interaction combinators**, and **Stellogen**. Stellogen's design, based on term unification with polarity and fusion, shares deep conceptual similarities with interaction nets—a graphical model of computation introduced by Yves Lafont. This report: +This document explores how Stellogen relates to **interaction nets** and **proof-nets**, and provides practical insights for implementing interaction combinators. The key thesis is: -1. Explains the theory of interaction nets and interaction combinators -2. Examines how other languages (Par, HVM) compile to interaction combinators -3. Analyzes how Stellogen's primitives (stars, rays, polarity, constellations) naturally encode interaction nets -4. Provides concrete examples from the Stellogen codebase +> **Stellogen already is an interaction net language in disguise.** The primitives (stars, rays, polarity, fusion) directly correspond to interaction net concepts. What's needed is not new mechanisms, but clarity about how to encode the standard constructs. -**Key Insight:** Stellogen can be understood as a textual notation for interaction nets, where stars represent networks of connected agents, rays encode ports with polarity, and constellations define interaction rules. +The connection to **proof-nets** (from linear logic) is particularly illuminating because proof-nets ARE interaction nets—they're the same formalism viewed from different angles. --- -## Background: Interaction Nets - -### Overview - -**Interaction nets** were introduced by French mathematician Yves Lafont in 1990 as a graphical model of computation and a generalization of linear logic proof structures. They provide: - -- **Graph-based computation**: Programs are graphs where nodes interact through local rewriting -- **Inherent parallelism**: Multiple reductions can occur simultaneously with strong confluence -- **Constant-time operations**: Each interaction step is local and happens in constant time -- **Determinism**: The order of reductions doesn't affect the final result - -### Formal Components - -#### 1. Agents and Ports +## 2. The Deep Connection: Proof-Nets = Interaction Nets -An **agent** is a node in the interaction net with: -- **One principal port** (the "active" connection point) -- **Zero or more auxiliary ports** (passive connection points) +### 2.1 Historical Context -Agents are typed by their **signature** (name and arity): -- Signature Σ: The set of all agent types -- Arity: The number of auxiliary ports +Yves Lafont introduced interaction nets in 1990 as a **generalization of proof-nets**. The key realization was that proof-net cut-elimination is a special case of a more general graph-rewriting paradigm. -#### 2. Edges and Wiring +| Proof-Net Concept | Interaction Net Concept | +|-------------------|------------------------| +| Axiom link | Agent with 2 ports | +| Cut | Active pair (principal ports connected) | +| Par (⅋) | Agent with 3 ports (1 principal, 2 auxiliary) | +| Tensor (⊗) | Agent with 3 ports (1 principal, 2 auxiliary) | +| Cut-elimination | Interaction (graph rewriting) | +| Proof | Net in normal form | -- **Edges** connect exactly two ports -- **Free ports** are unconnected ports forming the net's interface -- Ports can be connected to at most one edge +### 2.2 Why This Matters for Stellogen -#### 3. Active Pairs +Your MLL example (`examples/proofnets/mll.sg`) already demonstrates the encoding: -An **active pair** forms when two agents connect at their principal ports. This is the only configuration that can trigger interaction. +```stellogen +' Axiom between vertices a and b = binary positive star +[(+a X) (+b X)] +' Cut between vertices a and b = binary negative star +[(-a X) (-b X)] ``` - [Agent A] [Agent B] - | | - principal principal - └────────────────┘ - active pair -``` - -#### 4. Interaction Rules - -For each pair of agent types (α, β), there is an **interaction rule** that specifies how the active pair rewrites into a new net. Rules are: -- **Local**: Only the two agents and their immediate connections are involved -- **Deterministic**: Each active pair has exactly one rewriting outcome -- **Strongly confluent**: Different reduction orders produce the same result -#### 5. Reduction and Normal Form +This is exactly right. The crucial insight is: -- **Reduction**: Repeatedly find active pairs and apply interaction rules -- **Normal form**: A net with no active pairs (computation complete) -- **Parallel reduction**: Multiple active pairs can be reduced simultaneously +- **Positive rays** = "I provide a connection at this port" +- **Negative rays** = "I request a connection at this port" +- **Fusion** = Cut-elimination (or interaction) -### Properties - -1. **Strong Confluence**: All reduction paths lead to the same normal form -2. **Locality**: Reductions are local graph transformations -3. **Parallelism**: Independent reductions can execute concurrently -4. **Efficiency**: Each step is O(1) in the size of the net +The `[l|X]` and `[r|X]` encoding for binary branching corresponds to how proof-nets encode the two auxiliary ports of par/tensor. --- -## Interaction Combinators - -### The Universal System - -In 1997, Lafont introduced **interaction combinators**—a universal system of interaction nets with only: -- **3 symbols** (agent types) -- **6 interaction rules** - -This minimal system can simulate any interaction net and serves as a universal model of distributed computation. +## 3. Anatomy of Interaction Nets -### The Three Symbols +### 3.1 Agents, Ports, and Wires -Traditional interaction combinators use three agent types: +An **interaction net** consists of: -1. **ε (epsilon)** - Eraser (arity 0) - - Deletes/erases structures - - No auxiliary ports - -2. **δ (delta)** - Duplicator (arity 2) - - Duplicates structures - - Two auxiliary ports - -3. **γ (gamma)** - Constructor (arity 2) - - Constructs/links structures - - Two auxiliary ports - -### The Six Interaction Rules - -The rules define interactions between active pairs: - -#### Annihilation Rules (same symbol types) +1. **Agents**: Nodes with a fixed number of ports +2. **Principal port**: The "active" port (triggers interaction) +3. **Auxiliary ports**: The "passive" ports +4. **Wires**: Connect exactly two ports +5. **Free ports**: Unconnected ports (the interface) ``` -δ --- δ → ══ ══ - ∧ │ │ + aux₁ aux₂ + \ / + \ / + [ Agent ] + | + principal ``` -When two duplicators (or two constructors) connect at their principal ports, they annihilate and connect their corresponding auxiliary ports. +### 3.2 Interaction Rules -#### Commutation Rules (different symbol types) +When two agents connect at their **principal ports**, they form an **active pair** and can **interact** (rewrite). ``` -δ --- γ → δ γ - ∧ │ ╳ │ - γ δ + aux₁ aux₂ aux₃ aux₄ + \ / \ / + \ / \ / + [ Agent α ]------[ Agent β ] + principal ports + ↓ + (interaction rule) + ↓ + (new net) ``` -When a duplicator meets a constructor, they commute: each creates a copy of the other, rotated and reconnected. - -#### Erasure Rules +Key properties: +- **Local**: Only the two agents and their immediate connections change +- **Deterministic**: Each active pair has exactly one rewriting +- **Strongly confluent**: Order of reductions doesn't matter -``` -ε --- δ → ε ε -``` +### 3.3 The Stellogen Correspondence -When an eraser meets a duplicator (or constructor), it propagates erasure to all auxiliary ports. +| Interaction Net | Stellogen | +|-----------------|-----------| +| Agent | Constellation or focused constellation pattern | +| Principal port | The primary ray symbol with polarity | +| Auxiliary ports | Additional rays in the star | +| Active pair | Two rays with opposite polarity that unify | +| Wire | Shared variable between rays | +| Interaction | Star fusion during `exec` or `fire` | +| Free ports | Rays remaining after saturation | -### Universality +--- -This simple system can encode: -- Lambda calculus -- Turing machines -- Any computable function +## 4. Proof-Nets in Stellogen: Current Implementation -The encoding process involves representing computational structures as interaction nets and compiling them to the three basic combinators. +### 4.1 The MLL Encoding ---- +From your `mll.sg`, the encoding strategy is: -## Related Projects +**Axiom** (connects two vertices): +```stellogen +' ax +' __ +'/ \ +'a b -### The Par Language +[(+a X) (+b X)] ' Both ports positive, share variable X +``` -**Par** is an experimental programming language that compiles to interaction combinators. +**Cut** (connects two proofs): +```stellogen +' \__/ +' cut -**Key Features:** -- Based on linear logic -- Automatic concurrent execution -- Type-safe with structural types (pairs, functions, eithers, choices) -- Total and deterministic (mostly) -- Prevents deadlocks through structured concurrency +[(-a X) (-b X)] ' Both ports negative, share variable X +``` -**Compilation Strategy:** -- Uses "CP" (Classical Processes) from Phil Wadler's "Propositions as Sessions" -- Translates programs directly to linear logic proofs -- Compiles to interaction combinators as the execution target +**Par** (⅋) - combines two conclusions into one: +```stellogen +' Transform (+a X) (+b X) into par structure: +[(+(⅋ a b) [l|X]) (+(⅋ a b) [r|X])] -**Philosophy:** Brings linear logic's expressive power into practical programming with emphasis on parallelism and type safety. +' The [l|X] and [r|X] encode left/right auxiliary ports +``` -**Repository:** https://github.com/faiface/par-lang +**Tensor** (⊗) - combines two proofs: +```stellogen +' Transform (+a X) from proof A and (+b X) from proof B: +[(+(⊗ a b) [l|X])] ' From proof A +[(+(⊗ a b) [r|X])] ' From proof B +``` -### HVM (Higher-Order Virtual Machine) & Bend +### 4.2 Cut-Elimination as Interaction -**HVM** is Victor Taelin's massively parallel runtime based on interaction combinators. +The beautiful example from `mll.sg`: -**Key Features:** -- Implements Symmetric Interaction Combinators -- Enables near-ideal speedup on parallel hardware (GPUs) -- Low-level IR for specifying interaction nets -- Compilation target for high-level languages (Python, Haskell, Bend) +```stellogen +' ax ax ax +' _ __ __ +' / \ / \ / \ +' 1 2 3 4 5 6 +' \ / \ / +' ⅋ ⊗ +' |_______| +' cut + +(def x { + [(+(⅋ 1 2) [l|X]) (+(⅋ 1 2) [r|X])] ' Par of 1,2 + [(+3 X) (+(⊗ 4 5) [l|X])] ' Tensor left + [(+(⊗ 4 5) [r|X]) (+6 X)] ' Tensor right + [(-​(⅋ 1 2) X) (-(⊗ 4 5) X)]}) ' Cut! + +' Execution performs cut-elimination: +(def comp (exec #x @[(-3 X) (+3 X)])) +``` -**Node Types in Interaction Calculus:** -- **VAR** - Variables (affine, used once) -- **ERA** - Erasure -- **LAM** - Lambda abstraction -- **APP** - Application -- **SUP** - Superposition -- **DUP** - Duplication +The `exec` command performs cut-elimination by fusing stars. The result is the normal form of the proof-net. -**Interaction Rules Include:** -- APP-LAM: Beta reduction -- APP-SUP: Splits superposition when applied -- DUP-LAM: Handles duplication in lambda terms -- DUP-SUP: Manages duplication/superposition interaction +### 4.3 What Works Well -**Key Innovation:** Uses labels on duplicators to control interaction behavior: -- Matching labels → annihilation -- Different labels → commutation +1. **Polarity is natural**: +/- directly models the two sides of a cut +2. **Variables are wires**: Shared variables connect ports +3. **Fusion is cut-elimination**: The interaction mechanism is correct +4. **Address encoding**: `[l|X]` and `[r|X]` encode port structure -This enables optimal lambda calculus reduction (Lamping's algorithm). +### 4.4 Current Limitations -**Bend** is a high-level parallel programming language that compiles to HVM, providing a more approachable syntax while maintaining automatic parallelization capabilities. +1. **No explicit port arity checking**: Agents don't declare their port count +2. **No interaction rule declaration**: Rules are implicit in constellation structure +3. **No principal port marking**: All rays are equally "principal" +4. **No visualization**: Hard to see the net structure -**Repository:** https://github.com/HigherOrderCO/HVM +--- -### Inpla (Interaction Nets Programming Language) +## 5. Interaction Combinators: The Universal System -**Inpla** is a multi-threaded parallel interpreter for interaction nets that demonstrates competitive performance with established functional languages. +### 5.1 The Three Symbols -**Key Features:** -- **Sequential and parallel modes**: Single-threaded (`make`) and multi-threaded (`make thread`) compilation -- **Automatic parallelization**: Programs scale to multiple cores without modification using POSIX threads -- **Built in C**: Uses flex/bison for parser generation -- **Competitive performance**: Benchmarks show execution times comparable to or faster than Haskell, OCaml, and Standard ML +Lafont's interaction combinators use only **3 agents** and **6 rules** to achieve universality: -**Syntax Elements:** +1. **ε (Eraser)**: Arity 0 (principal port only) +2. **δ (Duplicator)**: Arity 2 (principal + 2 auxiliary) +3. **γ (Constructor)**: Arity 2 (principal + 2 auxiliary) -Rules define agent interactions with pattern matching: -```inpla -gcd(ret) >< (int a, int b) -| b==0 => ret ~ a -| _ => gcd(ret) ~ (b, a%b); ``` - -Nets represent computation instances: -```inpla -gcd(r) ~ (14,21); -r; // outputs: 7 + ε δ γ + | /|\ /|\ + • • | • • | • + aux aux ``` -**Notable Features:** -- Pattern matching with guards (`|` syntax) -- Abbreviation notation (`<<`) for port specifications -- Reuse annotations for memory optimization -- Interactive REPL and batch execution modes -- Built-in agents for common operations +### 5.2 The Six Rules -**Relevance to Stellogen:** Inpla demonstrates that interaction nets can achieve practical performance while maintaining clear, high-level syntax. Its automatic parallelization shows the inherent concurrency benefits of the interaction nets model. +**Annihilation** (same type meeting): +``` +δ ---•--- δ → cross-connect auxiliaries +γ ---•--- γ → cross-connect auxiliaries +ε ---•--- ε → nothing (both erased) +``` -**Repository:** https://github.com/inpla/inpla +**Commutation** (different types meeting): +``` +δ ---•--- γ → 2×2 grid of new agents +``` -### Vine & Ivy +**Erasure**: +``` +ε ---•--- δ → ε connected to each auxiliary +ε ---•--- γ → ε connected to each auxiliary +``` -**Vine** is an experimental multi-paradigm programming language that seamlessly blends functional and imperative patterns. +### 5.3 Encoding in Stellogen -**Architecture:** -- Vine compiles to **Ivy**, a low-level interaction-combinator language -- Ivy executes on the **IVM** (Ivy Virtual Machine), a performant interaction combinator runtime -- Two-stage compilation separates high-level design from low-level optimization +Here's how to encode interaction combinators: -**Implementation:** -- Primarily written in Rust (97.5%) -- Systems-level implementation optimized for performance -- Active development with evolving specification +```stellogen +''' ============================================ ''' +''' INTERACTION COMBINATORS IN STELLOGEN ''' +''' ============================================ ''' + +' AGENT ENCODING: +' - Principal port = the labeled ray +' - Auxiliary ports = additional rays with [l|X] and [r|X] +' - Eraser has no auxiliary ports + +' ERASER (ε): Arity 0 +' Represented as: [(+e Label)] +' or when receiving: [(-e Label)] + +' DUPLICATOR (δ): Arity 2 +' Represented as: [(+d Label [l|X] [r|Y])] +' The label distinguishes different duplicators (for labels/colors) + +' CONSTRUCTOR (γ): Arity 2 +' Represented as: [(+c Label [l|X] [r|Y])] + +''' --------------------------------------------- ''' +''' INTERACTION RULES ''' +''' --------------------------------------------- ''' + +(def interaction-rules { + ' RULE 1: δ-δ Annihilation (same label) + ' Two duplicators with same label meeting → cross-connect + ' + ' a₁ a₂ b₁ b₂ a₁ b₁ + ' \ / \ / | | + ' [δ]------[δ] → | | + ' a₂ b₂ + ' + [(-d L [l|A1] [r|A2]) (-d L [l|B1] [r|B2]) + (+wire A1 B1) (+wire A2 B2)] + + ' RULE 2: γ-γ Annihilation (same label) + [(-c L [l|A1] [r|A2]) (-c L [l|B1] [r|B2]) + (+wire A1 B1) (+wire A2 B2)] + + ' RULE 3: ε-ε Annihilation + [(-e L1) (-e L2)] ' Both erased, nothing remains + + ' RULE 4: δ-γ Commutation (or δ-γ with different labels) + ' Creates 2×2 grid: each aux of δ connects to a new γ, + ' each aux of γ connects to a new δ + ' + ' a₁ a₂ b₁ b₂ a₁ a₂ + ' \ / \ / | | + ' [δ]------[γ] → [γ] [γ] + ' | × | + ' [δ] [δ] + ' | | + ' b₁ b₂ + ' + [(-d Ld [l|A1] [r|A2]) (-c Lc [l|B1] [r|B2]) + ' Create new agents with fresh connections + (+c Lc [l|A1] [r|M1]) ' γ connected to a₁ + (+c Lc [l|A2] [r|M2]) ' γ connected to a₂ + (+d Ld [l|M1] [r|B1]) ' δ connected to b₁ + (+d Ld [l|M2] [r|B2])] ' δ connected to b₂ + + ' RULE 5: ε-δ Erasure + ' Eraser propagates to both auxiliaries + [(-e L) (-d Ld [l|A1] [r|A2]) + (+e A1) (+e A2)] + + ' RULE 6: ε-γ Erasure + [(-e L) (-c Lc [l|A1] [r|A2]) + (+e A1) (+e A2)] +}) + +''' --------------------------------------------- ''' +''' WIRE RESOLUTION ''' +''' --------------------------------------------- ''' + +' Wires need to be resolved to actual connections +(def wire-resolution { + ' When two positive wires meet, connect them + [(+wire X Y) (+wire Y Z) (+wire X Z)] + + ' When wire meets an agent, substitute + [(+wire X X)] ' Identity wire = no-op +}) +``` -**Relevance to Stellogen:** Vine demonstrates a layered approach where a high-level language compiles to interaction combinators. This is similar to how Stellogen could potentially serve as both a high-level notation and a compilation target. +### 5.4 The Challenge: Fresh Name Generation -**Resources:** -- Documentation: https://vine.dev/docs/ -- Repository: https://github.com/VineLang/vine -- Community: Discord server +The commutation rule creates **new agents** with **fresh connections**. In the encoding above, I used variables `M1`, `M2` as intermediaries, but there's a subtlety: -### inet-forth +**Problem**: How do we ensure fresh names don't clash? -**inet-forth** is a Forth-like language implementing interaction nets for automatic parallelization. +**Current Stellogen behavior**: Variables are local to stars, which helps. But when we create new agents, we need to ensure their internal connections are properly scoped. -**Design Philosophy:** -- Addresses post-2003 computing reality: "single-threaded performance halted... increasing performance requires parallelism" -- Combines Forth's stack-based evaluation with node-graph operations -- Graph-structured programs enable automatic multi-core utilization +**Insight**: This is where Stellogen's variable locality actually helps. Each star has its own variable scope, so: -**Core Constructs:** -```forth -define-node -- end -define-rule end -define end -``` +```stellogen +' Star 1 has its own X +[(+agent1 [l|X] [r|Y])] -**Execution Model:** -- Stack-based operations push/pop wires and values -- Node creation takes arguments from the stack -- Interaction rules specify how connected nodes eliminate each other -- Local variables capture disconnected wires during rule application - -**Example - Natural Numbers:** -```forth -define-node zero -- value! end -define-node add1 prev -- value! end -define-node add target! addend -- result end +' Star 2 has a DIFFERENT X (same name, different scope) +[(+agent2 [l|X] [r|Z])] ``` -When `add1` interacts with `add`, the rule: (1) saves wires as local variables, (2) creates new nodes reconnecting the transformed graph. - -**Implementation:** -- Built in C (99.4% of codebase) -- Compiled via Make -- GPLv3 licensed - -**Relevance to Stellogen:** inet-forth shows how interaction nets can be embedded in a concatenative programming paradigm, demonstrating the flexibility of the interaction nets model across different language design philosophies. +The challenge is when we want to **connect** agents created in different stars. This requires explicit wiring. -**Repository:** https://github.com/xieyuheng/inet-forth +--- -### Other Implementations +## 6. What Mechanisms Might Be Needed -Several research implementations exist on GitHub: +### 6.1 Mechanism 1: Agent Declarations -- **nkohen/InteractionCombinators** - Lambda calculus implementations in Java -- **dowlandaiello/ic-sandbox** - Rust-based research sandbox with REPL -- **ia0/lafont** - 3D visualization of Lafont's original system -- **noughtmare/lafont90** - Compiler in Rascal -- **chemlambda/molecular** - Graph rewrite systems with interaction combinators -- **BOHM** - Bologna Optimal Higher-Order Machine -- **Optiscope** - Lévy-optimal lambda calculus reducer +Currently, Stellogen doesn't have explicit agent declarations. This would help: -These projects demonstrate the versatility and ongoing research interest in interaction combinators. +```stellogen +' PROPOSED: Declare agent types with port arities +(agent ε 0) ' Eraser: 0 auxiliary ports +(agent δ 2) ' Duplicator: 2 auxiliary ports +(agent γ 2) ' Constructor: 2 auxiliary ports + +' Benefits: +' - Arity checking at definition time +' - Better error messages +' - Documentation +``` ---- +**Implementation insight**: This could be a macro-level convention rather than a core feature: -## Encoding Interaction Nets in Stellogen +```stellogen +(macro (agent Name Arity) + (def Name (meta arity Arity))) +``` -### Conceptual Mapping +### 6.2 Mechanism 2: Principal Port Marking -Stellogen's design aligns naturally with interaction nets. Here's the correspondence: +Interaction only happens between **principal ports**. Currently, Stellogen uses polarity (+/-) for this, which works but conflates two concepts: -| Interaction Net Concept | Stellogen Equivalent | Notes | -|------------------------|----------------------|-------| -| **Agent** | Constellation or Star | A constellation defines an agent type | -| **Principal Port** | Ray with primary label | The main interaction point (e.g., `add`, `id`) | -| **Auxiliary Ports** | Numbered rays or parameters | Secondary connection points (e.g., `-1`, `+2`, `-3`) | -| **Polarity** | Ray polarity (`+`/`-`) | Built-in mechanism for principal port duality | -| **Active Pair** | Opposite polarity rays | `(+add ...)` and `(-add ...)` can fuse | -| **Interaction Rule** | Constellation clause | Each clause defines how agents interact | -| **Wiring/Edges** | Variables & cons lists | Variables connect ports; `[l\|X]` encodes direction | -| **Network** | Star with multiple rays | A star is a collection of connected agents | +- **Polarity**: Which side of a connection (provider vs. requester) +- **Principal-ness**: Whether this port triggers interaction -### Stars as Blocks of Addresses/Ports +**Insight**: For proof-nets and interaction combinators, these are the same! The principal port of an agent is where it "offers" or "demands" interaction. Polarity already captures this. -The user's insight is key: **Stars can be used as blocks of addresses/ports**. A star represents a network fragment with: +**Conclusion**: No new mechanism needed. Stellogen's polarity IS the principal port marking. -1. **Multiple rays** (ports) that can connect to other agents -2. **Polarity on each ray** indicating whether it's active or passive -3. **Complex address encoding** through structured terms +### 6.3 Mechanism 3: Interaction Rule Definitions -### Port Addressing Schemes +Currently, rules are implicit in constellation structure. An explicit syntax might help: -Stellogen examples demonstrate several encoding strategies: +```stellogen +' PROPOSED: Explicit rule syntax +(rule (δ meets δ) + :when (same-label L) + :pattern [(-d L [l|A1] [r|A2]) (-d L [l|B1] [r|B2])] + :result [(+wire A1 B1) (+wire A2 B2)]) +``` -#### 1. Numeric Addressing (Simple) +**Implementation insight**: This could be sugar over the current approach: ```stellogen -(def agent { - [(-1 X) (+out X)] ' Port 1 connects to output port - [(-2 Y) (+out Y)]}) ' Port 2 connects to output port +(macro (rule Name :when Cond :pattern Pat :result Res) + (def Name { Pat :where Cond Res })) ``` -Ports are numbered: `-1`, `+2`, `-3`, etc. +But the current approach (just define the constellation) is simpler and already works. -#### 2. Direction Encoding with Cons Lists +### 6.4 Mechanism 4: Graph Visualization -```stellogen -(def id { - [(-5 [l|X]) (+1 X)] ' Left branch of port 5 → port 1 - [(-5 [r|X]) (+2 X)] ' Right branch of port 5 → port 2 - [(+5 [l|X]) (+6 [l|X])] ' Connect left branches - [(+5 [r|X]) (+6 [r|X])]}) ' Connect right branches -``` +This is perhaps the most impactful addition. Interaction nets are **inherently graphical**. A visualization tool would: -Uses `[l|X]` for left and `[r|X]` for right, encoding binary tree structure. +1. Show the current net as a graph +2. Highlight active pairs +3. Animate interaction steps +4. Export to DOT/GraphViz format -#### 3. Complex Structured Addressing +**Implementation direction**: ```stellogen -(def var_x [(x (exp X Y)) (+arg (exp [l|X] Y))]) +' Generate DOT format from constellation +(def to-dot { + ' Each star = nodes + edges + [(-star [Ray|Rays]) + (+node (ray-label Ray)) + (+to-dot-rays Rays)] + + [(-to-dot-rays []) + (+done)] + + [(-to-dot-rays [(+ Label X)|Rest]) + (+edge Label X) + (+to-dot-rays Rest)] +}) ``` -Combines multiple levels: `exp` wrapper with depth tracking and directional lists. - -### Polarity as Principal Port Mechanism +### 6.5 Mechanism 5: Labels/Colors on Agents -Stellogen's **polarity** (`+`/`-`) directly models the principal port concept: +HVM and optimal lambda calculus use **labeled duplicators** to control interaction. The label determines whether annihilation or commutation occurs: -- **Positive ray** (`+name`) represents one "side" of the principal port -- **Negative ray** (`-name`) represents the dual "side" -- **Active pair formation**: When `(+name ...)` meets `(-name ...)`, they can fuse -- **Interaction trigger**: Fusion corresponds to applying an interaction rule +``` +δ[a] ---•--- δ[a] → annihilate (same label) +δ[a] ---•--- δ[b] → commute (different labels) +``` -This is a native feature of Stellogen, not requiring explicit encoding. +**Current Stellogen approach**: The label can be part of the term structure: -### Constellations as Interaction Rules +```stellogen +' Labeled duplicator +[(+d a [l|X] [r|Y])] ' Label "a" +[(+d b [l|X] [r|Y])] ' Label "b" -A **constellation** in Stellogen defines the behavior of an agent and its interaction rules: +' Rule checks label equality +[(-d L [l|A1] [r|A2]) (-d L [l|B1] [r|B2]) ' Same L = annihilate + (+wire A1 B1) (+wire A2 B2)] -```stellogen -(def add { - [(+add 0 Y Y)] ' Rule 1: 0 + Y = Y - [(-add X Y Z) (+add (s X) Y (s Z))]}) ' Rule 2: S(X) + Y = S(Z) if X + Y = Z +[(-d L1 [l|A1] [r|A2]) (-d L2 [l|B1] [r|B2]) ' Different = commute + || (!= L1 L2) + ...] ``` -This is equivalent to defining interaction rules: -- When `add` receives arguments `0, Y`, it returns `Y` -- When `add` receives `(s X), Y`, it recursively calls itself - -Each clause is an interaction rule specifying: -1. **Pattern** on input rays (what configuration triggers this rule) -2. **Result** rays (what the net becomes after interaction) +This already works! The `|| (!= L1 L2)` guard handles the distinction. --- -## Stellogen vs. Traditional Interaction Combinators - -### Similarities +## 7. Implementation Strategy -1. **Graph-based computation**: Both models use graphs with nodes and connections -2. **Local rewriting**: Interactions are local transformations -3. **Strong confluence**: Reduction order doesn't matter -4. **Parallelism**: Independent interactions can happen simultaneously -5. **Polarity/Duality**: Both use dual connection points (principal ports vs. +/- polarity) +### 7.1 Level 1: Proof-Net Execution (Already Working) -### Differences +Your `mll.sg` example shows this works. The strategy: -| Aspect | Traditional Interaction Combinators | Stellogen | -|--------|-------------------------------------|-----------| -| **Symbol Set** | Fixed 3 symbols (ε, δ, γ) | User-defined constellations (unlimited) | -| **Rule Count** | Fixed 6 rules | User-defined interaction rules | -| **Encoding** | Everything compiled to 3 symbols | Direct high-level representation | -| **Type System** | Structure-based | Interaction-based (specs as tests) | -| **Polarity** | Implicit in ports | Explicit on rays (`+`/`-`) | -| **Addresses** | Simple port numbers | Flexible: numbers, cons lists, structured terms | -| **Abstraction Level** | Low-level IR | High-level, user-facing | +1. Encode axioms as `[(+a X) (+b X)]` +2. Encode cuts as `[(-a X) (-b X)]` +3. Use `[l|X]` and `[r|X]` for par/tensor structure +4. Run `exec` to perform cut-elimination -### Advantages of Stellogen's Approach +**No changes needed.** This is a proof-of-concept for interaction nets. -1. **Higher abstraction**: No need to compile everything to 3 primitives -2. **Readability**: Programs remain close to their logical structure -3. **Flexibility**: Port addressing can be arbitrarily complex -4. **Logic-agnostic**: Not tied to a specific logical system -5. **Direct encoding**: No intermediate compilation step to interaction combinators +### 7.2 Level 2: Interaction Combinators (Needs Wiring) -Stellogen can be seen as: -- A **generalized interaction net system** where users define their own agents -- A **textual notation** for interaction nets with flexible addressing -- A **meta-level** above interaction combinators, allowing direct expression of computational patterns - ---- +The main challenge is the commutation rule, which creates new agents. Strategy: -## Comparative Analysis: Stellogen Among Interaction Net Languages - -This section compares Stellogen's design decisions with other interaction net implementations. - -### Language Design Spectrum +```stellogen +''' APPROACH 1: Explicit Wiring Phase ''' + +' After interaction, we have "wire" terms that need resolution +(def resolve-wires { + [(+wire X X)] ' Self-loop = delete + [(-wire X Y) (+wire Y X)] ' Symmetry + ' More resolution rules... +}) + +' Execution with wire resolution +(def run-combinators (C) + (exec (exec #C #interaction-rules) #resolve-wires)) +``` -Interaction net languages occupy different points on several design spectra: +```stellogen +''' APPROACH 2: Continuation-Passing ''' -#### Abstraction Level +' Each agent "knows" where its ports connect +' Ports carry their destinations +(def δ-cps + [(+δ (port A1) (port A2) (dest Principal)) + (-Principal connected-to-δ A1 A2)]) ``` -Low-level IR High-level Language -├─────────────┼─────────────┼─────────────┼─────────────┤ -HVM/Ivy inet-forth Inpla Stellogen/Vine -``` - -- **HVM/Ivy**: Bare interaction combinators, compilation target -- **inet-forth**: Stack-based primitives with explicit node/rule definitions -- **Inpla**: Pattern-matching rules with implicit graph operations -- **Stellogen/Vine**: Declarative constellations with term unification -#### Syntax Philosophy - -| Language | Paradigm Base | Syntax Style | Port/Wire Notation | -|----------|--------------|--------------|-------------------| -| **Stellogen** | Logic programming | Declarative, unification-based | Variables + polarity (`+`/`-`) | -| **Inpla** | Multi-paradigm | Imperative-style rules | Explicit agent connections (`~`) | -| **inet-forth** | Concatenative | Stack-based, postfix | Stack operations on wires | -| **Vine** | Multi-paradigm | Functional + imperative blend | (Compiles to Ivy) | -| **HVM** | Functional | Lambda calculus-inspired | Low-level node references | - -#### Parallelization Strategy - -| Language | Parallel Execution | Mechanism | User Control | -|----------|-------------------|-----------|--------------| -| **HVM** | Massively parallel | GPU-optimized runtime | Implicit, automatic | -| **Inpla** | Multi-threaded | POSIX threads | Compile flag (`-t`) | -| **Stellogen** | Potential (not implemented) | Concurrent fusion | Would be implicit | -| **inet-forth** | Designed for parallelism | Graph-based concurrency | Automatic via graph structure | -| **Vine/Ivy** | IVM runtime | Interaction combinator execution | Implicit through compilation | - -### Unique Design Decisions - -#### Stellogen's Distinctive Features - -1. **Explicit Polarity as First-Class Syntax** - - Most languages encode polarity implicitly (principal vs. auxiliary ports) - - Stellogen makes it visible: `(+f X)` vs `(-f X)` - - Enables clear visual distinction between providers and requesters - -2. **Term Unification Foundation** - - Built on Robinson unification rather than graph matching - - Variables are local to stars (constellation clauses) - - Substitution propagates during fusion - -3. **Focus (`@`) Operator** - - Distinguishes **state** (data being computed) from **actions** (rules) - - Non-focused stars can be reused (duplicated during `exec`) - - Focused stars are targets for interaction - - No direct equivalent in other interaction net languages - -4. **Flexible Port Addressing** - - Not limited to numeric ports or fixed conventions - - Supports cons lists: `[l|X]`, `[r|X]` for binary trees - - Allows structured terms: `(exp [r l|X] d)` for complex addressing - - Enables domain-specific encoding schemes - -#### Inpla's Distinctive Features - -1. **Pattern Matching with Guards** - - Conditional rules: `| b==0 => ...` - - Multiple clauses per interaction rule - - Familiar to functional programmers - -2. **Performance Focus** - - Competitive with OCaml/Haskell - - Reuse annotations for memory optimization - - Both interpreted and compiled modes - -3. **Abbreviated Syntax** - - `r << qsort([3,6,1,9,2])` shorthand - - Reduces verbosity for common patterns - -#### inet-forth's Distinctive Features - -1. **Stack-Based Wire Manipulation** - - Wires are values on the stack - - `connect` operation explicitly joins wires - - Natural for Forth programmers - -2. **Explicit Node/Rule Separation** - - `define-node`: declares agent types with port signatures - - `define-rule`: specifies interactions between pairs - - Clear separation of structure and behavior - -3. **Local Variables in Rules** - - Rules capture disconnected wires as locals - - Enables complex rewiring during interaction - -#### Vine/Ivy's Distinctive Features - -1. **Two-Tier Architecture** - - High-level language (Vine) compiles to low-level IR (Ivy) - - Similar to HVM's approach (Bend → HVM) - - Separates language design from runtime optimization - -2. **Multi-Paradigm Integration** - - Seamless functional/imperative interop - - Goal: best of both worlds without artificial boundaries - -### Stellogen's Position in the Ecosystem - -Stellogen occupies a unique niche: - -1. **Closest to Logic Programming** - - Prolog-like declarative style - - Unification-based rather than pattern-matching - - Queries with negative polarity, facts with positive - -2. **Highest Abstraction for Interaction Nets** - - No need to think about low-level combinators - - Direct expression of logical relationships - - Port addressing as complex as needed - -3. **Research/Educational Focus** - - Explores interaction nets as a **foundation** rather than compilation target - - Logic-agnostic philosophy allows experimentation - - Not (yet) optimized for production performance - -4. **Generalized Interaction Rules** - - Not limited to 3 symbols + 6 rules - - Users define domain-specific agents - - Could still serve as compilation target (like Ivy/HVM) - -### Comparison Matrix - -| Feature | Stellogen | Inpla | inet-forth | Vine/Ivy | HVM | -|---------|-----------|-------|------------|----------|-----| -| **Primary Goal** | Logic-agnostic foundation | Practical parallelism | Forth-based nets | Multi-paradigm blend | Optimal λ-calculus | -| **Syntax Inspiration** | Prolog/Datalog | Functional/imperative | Forth | Functional/imperative | Lambda calculus | -| **Polarity** | Explicit (`+`/`-`) | Implicit | Implicit | Implicit | Implicit | -| **Port Addressing** | Flexible terms | Agent ports | Stack wires | Low-level refs | Node IDs | -| **Unification** | Built-in (Robinson) | Pattern matching | Manual in rules | Compiled away | Compiled away | -| **Parallelism** | Theoretical | Multi-threaded (POSIX) | Graph-based | IVM runtime | GPU-optimized | -| **Implementation** | OCaml | C (flex/bison) | C | Rust | Rust | -| **Type System** | Interaction tests | (Not emphasized) | (Not emphasized) | (Under development) | Structural | -| **Focus Operator** | Yes (`@`) | No | No | No | No | -| **Variable Scope** | Star-local | Agent-local | Rule-local | (Depends on Ivy) | Node-local | -| **Production Ready** | No (research) | Yes (benchmarked) | No (research) | No (in development) | Yes | - -### Lessons for Stellogen Development - -From reviewing these implementations, Stellogen could benefit from: - -1. **Performance Benchmarking** (from Inpla) - - Systematic comparison with functional languages - - Identify optimization opportunities - - Measure parallelization benefits - -2. **Explicit Parallelization Flags** (from Inpla) - - Allow users to control thread count - - Single-threaded mode for debugging - - Multi-threaded mode for production +**Insight**: The cleanest approach is probably to use a **two-phase execution**: +1. Phase 1: Interaction (creates new agents and wire placeholders) +2. Phase 2: Wire resolution (connects wires to actual ports) -3. **Compilation to Lower-Level IR** (from Vine/Ivy, HVM/Bend) - - Stellogen → Interaction Combinators → HVM/IVM - - Enables backend optimization without changing syntax - - Could leverage existing runtimes +### 7.3 Level 3: Optimal Lambda Calculus -4. **Stack-Based Operations** (from inet-forth) - - Alternative execution model for imperative patterns - - Could coexist with declarative constellations - - Useful for imperative recipes +This requires labeled duplicators and the "oracle" for managing labels. The Lamping algorithm uses: -5. **Pattern Matching Guards** (from Inpla) - - Inequality constraints (`|| (!= X Y)`) are a start - - Could add numeric comparisons, type guards - - More expressive conditional interactions +- **Fans**: Duplicators with labels +- **Croissants/Brackets**: For handling scope +- **Oracle**: Decides when to annihilate vs. commute -6. **Visual Debugging Tools** (common gap) - - Graph visualization of constellations - - Step-by-step interaction animation - - Wire tracing during reduction +**Implementation sketch**: -### Syntax Comparison: Same Algorithm, Different Languages - -To illustrate the design differences, here's how **GCD (greatest common divisor)** is implemented across interaction net languages: +```stellogen +' Lambda term encoding +(def lambda { + ' Variable: x + [(+var X) ...] + + ' Abstraction: λx.M + [(+lam [var|X] [body|M]) ...] + + ' Application: (M N) + [(+app [func|M] [arg|N]) ...] +}) + +' Translation to interaction combinators +(def to-combinators { + ' λx.M becomes a constructor + [(-lam [var|X] [body|M]) + (+γ [l|X] [r|M])] + + ' (M N) becomes an application node + [(-app [func|M] [arg|N]) + (+@ M N)] + + ' The @ node triggers beta reduction when meeting λ +}) +``` -#### Stellogen (Logic Programming Style) +**Key insight**: Optimal reduction requires tracking "levels" or "depths" to decide annihilation. This can be encoded in the label: ```stellogen -' GCD using declarative rules -(def gcd { - [(+gcd X 0 X)] ' Base case: gcd(X, 0) = X - [(+gcd 0 Y Y)] ' Base case: gcd(0, Y) = Y - [(-gcd X Y R) (+gcd Y (mod X Y) R) ' Recursive: gcd(X, Y) = gcd(Y, X mod Y) - || (!= Y 0)]}) ' Guard: Y ≠ 0 - -' Query -(def query @[(-gcd 14 21 R) (result R)]) -(show (exec #gcd #query)) +' Level-annotated duplicator +[(+δ Level [l|A] [r|B])] + +' Annihilate only at same level +[(-δ L [l|A1] [r|A2]) (-δ L [l|B1] [r|B2]) + (+wire A1 B1) (+wire A2 B2)] + +' Commute at different levels, incrementing +[(-δ L1 [l|A1] [r|A2]) (-δ L2 [l|B1] [r|B2]) + || (!= L1 L2) + ' Create new agents at adjusted levels + ...] ``` -**Characteristics:** -- Declarative rules with polarity -- Variables connect ports implicitly -- Guard syntax with `||` -- Focus `@` marks query +--- -#### Inpla (Pattern Matching Style) +## 8. Concrete Examples -```inpla -gcd(ret) >< (int a, int b) -| b==0 => ret ~ a -| _ => gcd(ret) ~ (b, a%b); +### 8.1 Example: Boolean NOT via Combinators -gcd(r) ~ (14, 21); -r; // outputs: 7 -``` +```stellogen +''' Boolean NOT using interaction combinators ''' -**Characteristics:** -- Explicit agent interaction syntax (`><`) -- Guards with `|` pattern -- Connection operator `~` -- Return port explicitly named +' Encoding: +' true = λx.λy.x +' false = λx.λy.y +' not = λb.b false true -#### inet-forth (Stack-Based Style) +' As combinators (simplified): +(def true-comb [(+true [l|X] [r|Y]) (+result X)]) +(def false-comb [(+false [l|X] [r|Y]) (+result Y)]) -```forth -define-node gcd-base value! -- result! end -define-node gcd-step a b -- result! end +(def not-comb { + ' NOT takes a boolean and applies it to (false, true) + [(-not B) (+apply B false true)] -define-rule gcd-step gcd-base - @b value! ' Get b from gcd-step - dup 0 = if - drop @a result! ' If b=0, return a - else - @a @b % @b swap gcd-step connect result! ' Else gcd(b, a%b) - then -end + ' When B = true, select first = false + [(-apply true X Y) (+result X)] -14 21 gcd-step gcd-base -``` + ' When B = false, select second = true + [(-apply false X Y) (+result Y)] +}) -**Characteristics:** -- Stack operations on wires -- Explicit control flow (`if/then`) -- Manual wire connections -- Postfix notation +' Test: NOT true = false +(def test1 @[(-not true) (-result R) (answer R)]) +(show (exec #not-comb #test1)) ' Should give: (answer false) +``` -#### Comparative Observations +### 8.2 Example: Church Numeral Successor -| Aspect | Stellogen | Inpla | inet-forth | -|--------|-----------|-------|------------| -| **Style** | Declarative | Functional | Imperative | -| **Polarity** | Explicit (`+`/`-`) | Implicit in ports | Implicit in arrows | -| **Guards** | `|| (!= Y 0)` | `\| b==0 =>` | `dup 0 = if` | -| **Connections** | Via variables | Via `~` operator | Via `connect` | -| **Readability** | Mathematical | Functional | Procedural | -| **Verbosity** | Moderate | Low | High | +```stellogen +''' Church numeral successor ''' + +' Church encoding: +' 0 = λf.λx.x +' 1 = λf.λx.f x +' n = λf.λx.f (f ... (f x)) [n times] +' succ = λn.λf.λx.f (n f x) + +' Simplified interaction net encoding: +(def zero { + ' Zero ignores f, returns x + [(+zero [f|F] [x|X]) (+result X)] +}) + +(def succ { + ' Successor duplicates f, applies once more + [(-succ N) (+succ-node N)] + [(-succ-node N [f|F] [x|X]) + ' Need to duplicate F and apply + (+dup F F1 F2) ' Duplicate f + (+apply F1 (N F2 X)) ' f (n f x) + (+result Applied)] +}) + +' This shows the NEED for duplication handling +``` -### Cross-Language Patterns +### 8.3 Example: Linear Identity (No Duplication) -Despite syntactic differences, all three languages express the same **interaction net structure**: +```stellogen +''' Linear identity - simpler because no duplication ''' -1. **Agents** (nodes): - - Stellogen: Constellations `gcd` - - Inpla: Agent definition `gcd(ret) >< (int a, int b)` - - inet-forth: Node types `gcd-base`, `gcd-step` +' Linear lambda: variables used exactly once +' id = λx.x -2. **Ports** (connection points): - - Stellogen: Variables `X`, `Y`, `R` - - Inpla: Named ports `ret`, `a`, `b` - - inet-forth: Stack values and wires +(def linear-id [(+id [l|X]) (+id [r|X])]) -3. **Interaction Rules** (rewrites): - - Stellogen: Constellation clauses - - Inpla: Pattern-match branches with `=>` - - inet-forth: `define-rule` blocks +' Application: id M +(def apply-id { + [(-id X) (-arg X)] + @[(+arg [r|Y]) (result Y)] +}) -4. **Active Pairs** (triggers): - - Stellogen: Opposite polarity rays `(+gcd ...) × (-gcd ...)` - - Inpla: Agent connection `gcd(r) ~ (14, 21)` - - inet-forth: Node connection via `connect` +' Compute: id applied to (value 42) +(def value [(+arg [l|V]) (data V 42)]) -This demonstrates that **interaction nets are the common semantic foundation**, while each language chooses different syntactic surface forms optimized for different programming paradigms. +(show (exec #linear-id #value #apply-id)) +' Result: (result (data 42)) +``` --- -## Examples and Analysis +## 9. Insights and Directions -### Example 1: Linear Logic Identity (from `mll.sg`) +### 9.1 Key Insight 1: Polarity IS Principal Port -```stellogen -(def id { - [(-5 [l|X]) (+1 X)] - [(-5 [r|X]) (+2 X)] - [(-6 [l|X]) (+3 X)] - [(-6 [r|X]) (+4 X)] - [(+5 [l|X]) (+6 [l|X])] - [(+5 [r|X]) (+6 [r|X])]}) -``` +Stellogen's polarity mechanism directly corresponds to the principal port concept in interaction nets. Positive rays "offer" connections, negative rays "demand" them. When they meet with unifiable terms, interaction (fusion) occurs. -**Analysis:** +**No new mechanism needed for this.** -**Ports:** -- Ports 1, 2, 3, 4: Auxiliary ports -- Ports 5, 6: Principal ports (they connect to each other) +### 9.2 Key Insight 2: Variables ARE Wires -**Structure:** -- Port 5 is a binary structure with left and right branches -- When port 5 receives input, it routes based on direction: - - Left branch (`[l|X]`) → Port 1 - - Right branch (`[r|X]`) → Port 2 -- Port 6 mirrors port 5's structure +Shared variables between rays are exactly the wires of interaction nets. When `X` appears in `(+a X)` and `(+b X)`, those two ports are connected. -**Interaction Net Interpretation:** -This encodes the identity agent in multiplicative linear logic (MLL): -- Two principal ports (input and output of the linear arrow) -- The left/right branching represents the proof structure -- Variables X connect corresponding auxiliary ports +**No new mechanism needed for this.** -**Graph Visualization:** -``` - Port 5 (-) - / \ - l r - | | - +1 X +2 X - - Port 6 (-) - / \ - l r - | | - +3 X +4 X - - Port 5 (+l) ←→ Port 6 (+l) - Port 5 (+r) ←→ Port 6 (+r) -``` +### 9.3 Key Insight 3: Cons Lists Encode Port Structure -### Example 2: Cut Elimination (from `mll.sg`) +The `[l|X]` and `[r|X]` pattern elegantly encodes binary port addressing. For agents with more ports, extend the pattern: ```stellogen -(def ps1 { - [+vehicle [ - [(+7 [l|X]) (+7 [r|X])] - @[(3 X) (+8 [l|X])] - [(+8 [r|X]) (6 X)]]] - [+cuts [ - [(-7 X) (-8 X)]]]}) - -(def vehicle (eval (exec #ps1 @[-vehicle]))) -(def cuts (eval (exec #ps1 @[-cuts]))) - -(show (exec #vehicle #cuts)) -``` +' 3-port agent: +[(+agent [1|X] [2|Y] [3|Z])] -**Analysis:** - -**Constellation ps1 defines two agents:** +' Or hierarchical: +[(+agent [l l|X] [l r|Y] [r|Z])] +``` -1. **vehicle agent**: - - Has ports 7 and 8 (both positive) - - Port 7 splits: left and right branches - - Port 8 splits: left and right branches - - Internal wiring connects port 3 and port 6 +**No new mechanism needed for this.** -2. **cuts agent**: - - Has ports 7 and 8 (both negative) - - This forms active pairs with vehicle's ports! +### 9.4 Insight 4: The Commutation Challenge -**Interaction:** -When `vehicle` and `cuts` interact: -- `(+7 X)` from vehicle meets `(-7 X)` from cuts → Active pair -- `(+8 X)` from vehicle meets `(-8 X)` from cuts → Active pair -- These active pairs trigger **cut elimination** (annihilation) +The one genuine challenge is the **commutation rule** which creates new agents with new connections. This requires careful handling of: -**Interaction Net Interpretation:** -This is the classic **cut elimination** from linear logic proof theory: -- A "cut" is a link between a formula and its dual -- Eliminating the cut simplifies the proof net -- The interaction removes the active pair and rewires connections +1. **Fresh names**: Each new agent needs unique identity +2. **Rewiring**: Connections must be properly redirected +3. **Intermediate state**: May need temporary "wire" terms -### Example 3: Linear Lambda Calculus Identity (from `linear_lambda.sg`) +**Potential solution**: A two-phase approach: ```stellogen -' identity function (\x -> x) -(def id [(+id [l|X]) (+id [r|X])]) +' Phase 1: Interaction (may create wire terms) +(def phase1 (exec #net #rules)) -' id id -(def id_arg [(ida [l|X]) (+arg [l r|X])]) +' Phase 2: Wire resolution +(def phase2 (exec #phase1 #wire-rules)) -(def linker [ - [(-id X) (-arg X)] - @[(+arg [r|X]) (out X)]]) - -(show (exec #id #id_arg #linker)) +' Combined: +(def full-run (process #phase1 #phase2)) ``` -**Analysis:** +### 9.5 Insight 5: Labels via Term Structure -**Lambda Term Encoding:** -- Lambda abstraction: Two ports (left for variable binding, right for body) -- Application: Three ports (left for function, right for argument, output) +Labeled agents (needed for optimal reduction) can be encoded naturally: -**id constellation:** -- `(+id [l|X])` and `(+id [r|X])`: Binary structure -- Represents λx.x (identity function) - -**id_arg constellation:** -- Represents the application (id id) -- `[l r|X]`: Nested list structure encoding the application +```stellogen +' Agent with label L +[(+δ L [l|X] [r|Y])] -**linker constellation:** -- Connects the function and argument -- Extracts the result to `out` +' Rules can match on labels +[(-δ L [l|A] [r|B]) (-δ L [l|C] [r|D]) ...] ' Same label +[(-δ L1 ...) (-δ L2 ...) || (!= L1 L2) ...] ' Different labels +``` -**Interaction Net Interpretation:** -This implements lambda calculus using proof-nets: -- Each lambda term is a proof structure -- Reduction corresponds to cut elimination -- The [l|X]/[r|X] structure represents the binary tree of the proof-net +**No new mechanism needed for this.** -### Example 4: Lambda Calculus with Exponentials (from `lambda.sg`) +### 9.6 Insight 6: Focus for Execution Control -```stellogen -(def id [(+id (exp [l|X] d)) (+id [r|X])]) +The `@` focus operator distinguishes what's being computed (state) from how it's computed (actions). For interaction nets: -(def var_x [(x (exp X Y)) (+arg (exp [l|X] Y))]) +- **Focused stars** = The current net (what we're reducing) +- **Unfocused stars** = The interaction rules (how we reduce) -(def lproj { - [(+lproj [l|X])] ' weakening - [(lproj (exp [r l|X] d)) (+lproj [r r|X])]}) +```stellogen +(exec @#net #rules) +' ↑ ↑ +' state actions (can be reused) ``` -**Analysis:** - -**Exponential Modality:** -- `(exp Term Depth)` encodes the exponential modality from linear logic -- Required for non-linear lambda calculus (variables used multiple times) +### 9.7 Insight 7: Fire vs Exec for Resource Control -**id with exponentials:** -- More complex encoding than linear case -- Depth parameter `d` tracks nesting level +- `fire` (linear): Each rule used at most once +- `exec` (non-linear): Rules can be reused -**lproj (left projection):** -- Implements weakening (discarding unused variables) -- `[(+lproj [l|X])]` - erases left branch -- Recursive case handles nested structures - -**Interaction Net Interpretation:** -This is the full lambda calculus encoding using proof-nets with exponentials: -- Exponentials allow contraction and weakening -- Enables non-linear use of variables -- More complex than linear lambda calculus +For interaction nets, you typically want `exec` since rules are reusable. But for proof-nets with linearity constraints, `fire` ensures resources are consumed exactly once. --- -## Future Directions +## 10. Recommended Next Steps -### 1. Formal Encoding of Interaction Combinators in Stellogen +### 10.1 Step 1: Formalize the Basic Combinators -Stellogen could implement the three classic interaction combinators (ε, δ, γ) directly: +Create a standard library file `inet/combinators.sg`: ```stellogen -' Eraser -(def epsilon { - [(+e)]}) ' Erases anything connected to it - -' Duplicator -(def delta { - [(+d [1|X] [2|Y]) (-d [1|X] [2|Y])] ' Annihilation with another delta - [(+d [1|A] [2|B]) (-g [1|X] [2|Y]) ' Commutation with gamma - (+g [1|C] [2|D]) (+d [1|C] [2|D]) - (connect A X) (connect B Y)]}) - -' Constructor -(def gamma { - [(+g [1|X] [2|Y]) (-g [1|X] [2|Y])] ' Annihilation with another gamma - [(+g [1|A] [2|B]) (-d [1|X] [2|Y]) ' Commutation with delta - (+d [1|C] [2|D]) (+g [1|C] [2|D]) - (connect A X) (connect B Y)]}) +' Standard interaction combinator definitions +(def ε-rules { ... }) +(def δ-rules { ... }) +(def γ-rules { ... }) +(def combinator-rules { #ε-rules #δ-rules #γ-rules }) ``` -This would demonstrate that Stellogen can serve as a **host language** for interaction combinators. - -### 2. Optimal Evaluation Strategy - -Stellogen could adopt strategies from HVM: -- **Labeled duplicators** to optimize lambda calculus reduction -- **Parallel reduction** of independent active pairs -- **Symbolic execution** where terms reduce as they're needed +### 10.2 Step 2: Implement Wire Resolution -### 3. Visual Interaction Net Editor +Add a wire resolution phase for handling commutation: -A graphical interface could: -- Visualize Stellogen programs as interaction nets -- Allow direct manipulation of nets (drag-and-drop agents) -- Animate reduction steps -- Generate Stellogen code from visual nets - -### 4. Compilation Targets - -Stellogen programs could compile to: -- **HVM runtime** for massively parallel execution -- **Interaction combinator assembly** for efficient evaluation -- **GPU kernels** for hardware parallelism -- **Distributed systems** leveraging natural concurrency - -### 5. Type System Extensions +```stellogen +(def wire-resolution { ... }) -Stellogen's interaction-based types could incorporate: -- **Session types** (from linear logic / process calculi) -- **Gradual linearity** (mix linear and non-linear code) -- **Dependent interaction types** (types that compute via interaction) +(macro (inet-run Net) + (process (exec @#Net #combinator-rules) #wire-resolution)) +``` -### 6. Proof Net Verification +### 10.3 Step 3: Add Visualization (External Tool) -Tools could verify that Stellogen programs represent valid proof-nets: -- Check correctness criteria (acyclicity, connectedness) -- Verify cut-elimination terminates -- Ensure strong normalization properties +Create a tool that: +1. Parses Stellogen constellations +2. Extracts the graph structure +3. Outputs DOT format or interactive visualization -### 7. Benchmarking and Performance +### 10.4 Step 4: Test with Lambda Calculus -Systematic comparison of Stellogen's evaluation against: -- Traditional lambda calculus interpreters -- HVM runtime -- Par language -- Standard functional languages +Implement the translation from lambda terms to interaction combinators: -### 8. Higher-Order Features +```stellogen +(def lambda-to-inet { ... }) +(def inet-to-lambda { ... }) -Explore encoding: -- **Higher-order functions** with interaction nets -- **Recursive types** and fixpoints -- **Polymorphism** and generics -- **Effects** and computational modalities +' Full pipeline +(macro (optimal-eval Term) + (inet-to-lambda (inet-run (lambda-to-inet #Term)))) +``` -### 9. Practical Applications +### 10.5 Step 5: Benchmark and Compare -Develop real-world programs demonstrating: -- Concurrent algorithms (parallel sorting, search) -- Distributed protocols (consensus, replication) -- Logic programming (Prolog-style querying) -- Functional programming (standard library) +Compare with HVM on standard benchmarks: +- Fibonacci +- Ackermann +- Church numeral operations --- -## References +## 11. Theoretical Perspective: What Stellogen Teaches Us -### Academic Papers +### 11.1 Unification as Interaction -1. **Lafont, Y.** (1990). *Interaction Nets*. In Proceedings of POPL 1990 (Principles of Programming Languages). - https://dl.acm.org/doi/10.1145/96709.96718 +The deepest insight is that **term unification is interaction**. When two terms unify, they're "interacting" to produce a common result. Stellogen makes this explicit: -2. **Lafont, Y.** (1997). *Interaction Combinators*. Information and Computation, 137(1), 69-101. - https://www.sciencedirect.com/science/article/pii/S0890540197926432 +- Unification = finding how two terms can be the same +- Interaction = finding how two agents can combine +- Both are **local**, **deterministic**, and **confluent** -3. **Wadler, P.** (2012). *Propositions as Sessions*. In Proceedings of ICFP 2012. - (Theoretical foundation for Par language) +### 11.2 Polarity as Resource Orientation -### Projects and Implementations +Polarity encodes the **flow of resources**: +- Positive = provides/outputs +- Negative = requires/inputs -1. **Par Language** - https://github.com/faiface/par-lang - Experimental language compiling to interaction combinators +This is exactly the linear logic interpretation, and exactly what interaction nets formalize. -2. **HVM (Higher-Order Virtual Machine)** - https://github.com/HigherOrderCO/HVM - Massively parallel interaction combinator runtime +### 11.3 Proof-Nets as Programs -3. **Victor Taelin's Interaction Calculus** - https://github.com/VictorTaelin/Interaction-Calculus - Optimal lambda calculus reduction system +The connection to proof-nets shows that **proofs are programs** in a very direct sense. A proof-net IS a program; cut-elimination IS execution. Stellogen makes this operational. -4. **Symmetric Interaction Calculus** - https://github.com/VictorTaelin/Symmetric-Interaction-Calculus - Symmetric variant with uniform rules +### 11.4 Logic-Agnostic but Not Logic-Free -5. **Inpla (Interaction Nets Programming Language)** - https://github.com/inpla/inpla - Multi-threaded parallel interpreter with competitive performance +While Stellogen doesn't impose a logic, the mechanisms it provides (polarity, unification, interaction) are the **universal substrate** from which any logic can be built. It's not logic-free; it's pre-logical—the raw material from which logics are constructed. -6. **Vine Language** - https://github.com/VineLang/vine - Multi-paradigm language compiling to Ivy (interaction combinator IR) - -7. **inet-forth** - https://github.com/xieyuheng/inet-forth - Forth-like interaction nets language for automatic parallelization - -8. **Interaction Nets Resources Collection** - https://github.com/etiamz/interaction-net-resources - Curated bibliography and implementation list (1989-2014+) +--- -9. **Interaction Nets Research Sandbox (Rust)** - https://github.com/dowlandaiello/ic-sandbox - REPL for interaction combinators and lambda calculus +## 12. Conclusion -10. **Lafont Animation (3D visualization)** - https://github.com/ia0/lafont - Visual representation of interaction combinator execution +Stellogen is already closer to being an interaction net language than it might appear. The key correspondences are: -11. **BOHM (Bologna Optimal Higher-Order Machine)** - Early implementation of optimal lambda calculus reduction +| Interaction Net | Stellogen | Status | +|-----------------|-----------|--------| +| Agent | Constellation pattern | Working | +| Principal port | Polarized ray | Working | +| Auxiliary ports | Additional rays with address encoding | Working | +| Wire | Shared variable | Working | +| Active pair | Opposite polarity + unification | Working | +| Interaction rule | Constellation clause | Working | +| Net reduction | Star fusion (exec/fire) | Working | +| Labels | Term structure with guards | Working | -12. **Optiscope** - Lévy-optimal lambda calculus reducer +What's needed is not new mechanisms but: -### Articles and Tutorials +1. **A standard library** for interaction combinators +2. **A wire resolution phase** for commutation +3. **Visualization tools** for debugging +4. **Documentation and examples** showing the approach -1. **Interaction Nets, Combinators, and Calculus** - https://zicklag.katharos.group/blog/interaction-nets-combinators-calculus/ - Accessible introduction to the theory +The proof-net examples in your codebase (`mll.sg`, `mall.sg`, `linear_lambda.sg`) already demonstrate the core ideas. Extending this to full interaction combinators is a matter of careful encoding, not fundamental change. -2. **The Symmetric Interaction Calculus** (Medium article) - https://medium.com/@maiavictor/the-abstract-calculus-fe8c46bcf39c - Victor Taelin's explanation of SIC +Stellogen's unique contribution is making interaction nets **textual, executable, and programmable**—moving them from theoretical diagrams to practical computation. -3. **Wikipedia: Interaction Nets** - https://en.wikipedia.org/wiki/Interaction_nets - Comprehensive overview with formal definitions +--- -### Related Stellogen Examples +## References -1. `examples/mll.sg` - Multiplicative linear logic proof-nets -2. `examples/linear_lambda.sg` - Linear lambda calculus with proof-nets -3. `examples/lambda.sg` - Lambda calculus with exponentials -4. `examples/prolog.sg` - Logic programming (related to linear logic) +### Core Theory ---- +1. **Lafont, Y.** (1990). "Interaction Nets." POPL 1990. +2. **Lafont, Y.** (1997). "Interaction Combinators." Information and Computation 137(1). +3. **Girard, J.-Y.** (1987). "Linear Logic." Theoretical Computer Science 50(1). +4. **Girard, J.-Y.** (1996). "Proof-Nets: The Parallel Syntax for Proof-Theory." -## Conclusion +### Optimal Reduction -Stellogen's design naturally aligns with interaction nets and interaction combinators: +5. **Lamping, J.** (1990). "An Algorithm for Optimal Lambda Calculus Reduction." POPL 1990. +6. **Asperti, A., Guerrini, S.** (1998). "The Optimal Implementation of Functional Programming Languages." -1. **Stars** serve as blocks of agents with complex port addressing -2. **Rays** with polarity (`+`/`-`) encode principal and auxiliary ports -3. **Constellations** define interaction rules -4. **Fusion** implements the active pair reduction mechanism -5. **Variables and cons lists** represent wiring/edges +### Modern Implementations -Stellogen operates at a **higher level of abstraction** than traditional interaction combinators: -- Users define domain-specific agents (constellations) -- Port addressing is flexible and expressive -- No need to compile to a fixed 3-symbol system -- Programs remain readable and close to their logical structure +7. **HVM**: https://github.com/HigherOrderCO/HVM +8. **Inpla**: https://github.com/inpla/inpla +9. **Vine/Ivy**: https://github.com/VineLang/vine -At the same time, Stellogen **could** implement interaction combinators directly, serving as a host language for the universal system. This positions Stellogen as: +### Stellogen Examples -- A **generalization** of interaction nets -- A **practical notation** for interaction-based computation -- A **research platform** for exploring new interaction models +10. `examples/proofnets/mll.sg` - MLL proof-structures +11. `examples/proofnets/mall.sg` - MALL proof-structures +12. `examples/lambda/linear_lambda.sg` - Linear lambda calculus +13. `examples/lambda/lambda.sg` - Lambda calculus with exponentials -The connection to projects like Par and HVM suggests exciting future directions: -- Compilation to parallel hardware (GPUs) -- Optimal evaluation strategies -- Formal verification of interaction properties -- Integration with existing interaction combinator ecosystems +--- -Stellogen's **logic-agnostic** philosophy makes it an ideal environment for experimenting with interaction-based computation, free from the constraints of any particular logical system while retaining the benefits of graph-based, parallel, deterministic reduction. +*This document synthesizes theoretical background with practical implementation insights for building interaction net systems in Stellogen.* diff --git a/src/lsc_trace.ml b/src/lsc_trace.ml index ba9d8d7..c37eadb 100644 --- a/src/lsc_trace.ml +++ b/src/lsc_trace.ml @@ -9,6 +9,7 @@ open Base open Stdio open Lsc_ast.Raw open Lsc_pretty +open Terminal (* ============================================================ Source Location Tracking @@ -33,22 +34,6 @@ let get_source_line filename line_num = In_channel.input_line ic ) with _ -> None -(* ============================================================ - Terminal Colors - ============================================================ *) - -let cyan text = "\x1b[36m" ^ text ^ "\x1b[0m" - -let green text = "\x1b[32m" ^ text ^ "\x1b[0m" - -let yellow text = "\x1b[33m" ^ text ^ "\x1b[0m" - -let magenta text = "\x1b[35m" ^ text ^ "\x1b[0m" - -let bold text = "\x1b[1m" ^ text ^ "\x1b[0m" - -let dim text = "\x1b[2m" ^ text ^ "\x1b[0m" - (* ============================================================ Trace State ============================================================ *) diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index 7e487eb..671de11 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -5,6 +5,7 @@ open Lsc_pretty open Lsc_eval open Sgen_ast open Expr_err +open Terminal exception EvalError of expr_err * source_location option @@ -214,14 +215,9 @@ and map_ray env ~f : sgen_expr -> sgen_expr = function | Use id -> Use (f id) let pp_err error : (string, err) Result.t = - let red text = "\x1b[31m" ^ text ^ "\x1b[0m" in - let bold text = "\x1b[1m" ^ text ^ "\x1b[0m" in - let cyan text = "\x1b[36m" ^ text ^ "\x1b[0m" in - let yellow text = "\x1b[33m" ^ text ^ "\x1b[0m" in - let green text = "\x1b[32m" ^ text ^ "\x1b[0m" in - let format_location loc = - Printf.sprintf "%s:%d:%d" (cyan loc.filename) loc.line loc.column + Terminal.format_location ~filename:loc.filename ~line:loc.line + ~column:loc.column in let get_source_line filename line_num = @@ -241,10 +237,8 @@ let pp_err error : (string, err) Result.t = let show_source_location loc = match get_source_line loc.filename loc.line with | Some line -> - let line_num_str = Printf.sprintf "%4d" loc.line in - let pointer = String.make (loc.column - 1) ' ' ^ red "^" in - Printf.sprintf "\n %s %s %s\n %s %s\n" (cyan line_num_str) (cyan "|") - line (cyan "|") pointer + Terminal.format_source_line ~line_num:loc.line ~line_content:line + ~column:loc.column | None -> "" in @@ -252,7 +246,7 @@ let pp_err error : (string, err) Result.t = match error with | ExpectError { got; expected; message = Func ((Null, f), []); location } when String.equal f "default" -> - let header = bold (red "error") ^ ": " ^ bold "assertion failed" in + let header = error_label ^ ": " ^ bold "assertion failed" in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -271,7 +265,7 @@ let pp_err error : (string, err) Result.t = |> Result.return | ExpectError { message = Func ((Null, f), [ term ]); location; _ } when String.equal f "error" -> - let header = bold (red "error") ^ ": " ^ string_of_ray term in + let header = error_label ^ ": " ^ string_of_ray term in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -282,7 +276,7 @@ let pp_err error : (string, err) Result.t = Printf.sprintf "%s\n %s %s\n%s\n" header (cyan "-->") loc_str source |> Result.return | ExpectError { message; location; _ } -> - let header = bold (red "error") ^ ": " ^ string_of_ray message in + let header = error_label ^ ": " ^ string_of_ray message in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -294,7 +288,7 @@ let pp_err error : (string, err) Result.t = |> Result.return | MatchError { term1; term2; message = Func ((Null, f), []); location } when String.equal f "default" -> - let header = bold (red "error") ^ ": " ^ bold "unification failed" in + let header = error_label ^ ": " ^ bold "unification failed" in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -310,7 +304,7 @@ let pp_err error : (string, err) Result.t = (yellow term2_str) |> Result.return | MatchError { message; location; _ } -> - let header = bold (red "error") ^ ": " ^ string_of_ray message in + let header = error_label ^ ": " ^ string_of_ray message in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -321,7 +315,7 @@ let pp_err error : (string, err) Result.t = Printf.sprintf "%s\n %s %s\n%s\n" header (cyan "-->") loc_str source |> Result.return | UnknownID (identifier, location) -> - let header = bold (red "error") ^ ": " ^ bold "identifier not found" in + let header = error_label ^ ": " ^ bold "identifier not found" in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -364,7 +358,7 @@ let pp_err error : (string, err) Result.t = ( Printf.sprintf "failed to load file '%s': %s" filename message , "Check that the file exists and is readable." ) in - let header = bold (red "error") ^ ": " ^ bold error_msg in + let header = error_label ^ ": " ^ bold error_msg in let loc_str = Option.map location ~f:format_location |> Option.value ~default:"" @@ -372,8 +366,8 @@ let pp_err error : (string, err) Result.t = let source = Option.map location ~f:show_source_location |> Option.value ~default:"" in - Printf.sprintf "%s\n %s %s\n%s\n %s %s\n\n" header (cyan "-->") loc_str - source (cyan "help:") hint + Printf.sprintf "%s\n %s %s\n%s\n %s: %s\n\n" header (cyan "-->") loc_str + source hint_label hint |> Result.return let rec eval_sgen_expr (env : env) : diff --git a/src/sgen_parsing.ml b/src/sgen_parsing.ml index f3f6fc3..f4ca398 100644 --- a/src/sgen_parsing.ml +++ b/src/sgen_parsing.ml @@ -4,17 +4,10 @@ open Lexing open Lexer open Parser open Expr_err +open Terminal exception ImportError of expr_err -let red text = "\x1b[31m" ^ text ^ "\x1b[0m" - -let bold text = "\x1b[1m" ^ text ^ "\x1b[0m" - -let cyan text = "\x1b[36m" ^ text ^ "\x1b[0m" - -let yellow text = "\x1b[33m" ^ text ^ "\x1b[0m" - let string_of_token = function | VAR s | SYM s | STRING s -> s | AT -> "@" @@ -53,20 +46,18 @@ let unexpected_token_msg () = let format_location filename pos = let column = pos.pos_cnum - pos.pos_bol + 1 in - Printf.sprintf "%s:%d:%d" (cyan filename) pos.pos_lnum column + Terminal.format_location ~filename ~line:pos.pos_lnum ~column let show_source_location filename pos = match get_line filename pos.pos_lnum with | Some line -> - let line_num_str = Printf.sprintf "%4d" pos.pos_lnum in let column = pos.pos_cnum - pos.pos_bol + 1 in - let pointer = String.make (column - 1) ' ' ^ red "^" in - Printf.sprintf "\n %s %s %s\n %s %s\n" (cyan line_num_str) (cyan "|") - line (cyan "|") pointer + Terminal.format_source_line ~line_num:pos.pos_lnum ~line_content:line + ~column | None -> "" let print_syntax_error pos error_msg filename = - let header = bold (red "error") ^ ": " ^ bold error_msg in + let header = error_label ^ ": " ^ bold error_msg in let loc_str = format_location filename pos in let source = show_source_location filename pos in Stdlib.Printf.eprintf "%s\n %s %s\n%s\n" header (cyan "-->") loc_str source @@ -200,7 +191,7 @@ let parse_with_error_recovery filename lexbuf = List.iter errors ~f:(fun error -> let hint_msg = match error.hint with - | Some h -> "\n " ^ yellow "hint" ^ ": " ^ h + | Some h -> "\n " ^ hint_label ^ ": " ^ h | None -> "" in print_syntax_error error.position error.message filename; diff --git a/src/terminal.ml b/src/terminal.ml new file mode 100644 index 0000000..f3dc754 --- /dev/null +++ b/src/terminal.ml @@ -0,0 +1,43 @@ +(* terminal.ml - Shared terminal formatting utilities *) + +(* ANSI color codes *) +let red text = "\x1b[31m" ^ text ^ "\x1b[0m" + +let green text = "\x1b[32m" ^ text ^ "\x1b[0m" + +let yellow text = "\x1b[33m" ^ text ^ "\x1b[0m" + +let magenta text = "\x1b[35m" ^ text ^ "\x1b[0m" + +let cyan text = "\x1b[36m" ^ text ^ "\x1b[0m" + +let bold text = "\x1b[1m" ^ text ^ "\x1b[0m" + +let dim text = "\x1b[2m" ^ text ^ "\x1b[0m" + +(* Standard error message labels *) +let error_label = bold (red "error") + +let hint_label = yellow "hint" + +(* Format a source location as filename:line:column *) +let format_location ~filename ~line ~column = + Printf.sprintf "%s:%d:%d" (cyan filename) line column + +(* Format a source line with pointer for error display *) +let format_source_line ~line_num ~line_content ~column = + let line_num_str = Printf.sprintf "%4d" line_num in + let pointer = String.make (max 0 (column - 1)) ' ' ^ red "^" in + Printf.sprintf "\n %s %s %s\n %s %s\n" (cyan line_num_str) (cyan "|") + line_content (cyan "|") pointer + +(* Format a complete error message with optional source and hint *) +let format_error ~message ~location ~source ~hint = + let header = error_label ^ ": " ^ bold message in + let loc_line = Printf.sprintf " %s %s" (cyan "-->") location in + let hint_line = + match hint with + | Some h -> Printf.sprintf " %s: %s\n" hint_label h + | None -> "" + in + Printf.sprintf "%s\n%s\n%s%s\n" header loc_line source hint_line