From 7e1d9e8870f3e84e805be622164d4c76f250f515 Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 19:41:37 +0200 Subject: [PATCH 1/7] Refactoring (use PPX) and separate files --- src/dune | 2 +- src/expr.ml | 12 +- src/lsc_ast.ml | 325 ++++----------------------------------------- src/lsc_eval.ml | 167 +++++++++++++++++++++++ src/lsc_pretty.ml | 59 ++++++++ src/sgen_eval.ml | 11 +- src/unification.ml | 32 ++--- 7 files changed, 274 insertions(+), 334 deletions(-) create mode 100644 src/lsc_eval.ml create mode 100644 src/lsc_pretty.ml diff --git a/src/dune b/src/dune index e15b5f4..9659380 100644 --- a/src/dune +++ b/src/dune @@ -2,7 +2,7 @@ (name stellogen) (libraries base menhirLib) (preprocess - (pps sedlex.ppx))) + (pps sedlex.ppx ppx_deriving.show ppx_deriving.ord ppx_deriving.eq))) (env (dev diff --git a/src/expr.ml b/src/expr.ml index 89fd5e1..abde414 100644 --- a/src/expr.ml +++ b/src/expr.ml @@ -23,6 +23,7 @@ type expr = | Symbol of string | Var of ident | List of expr list + [@@derive eq] let primitive = String.append "%" @@ -73,14 +74,6 @@ let rec expand_macro : Raw.t -> expr = function List.fold_left t ~init:(expand_macro h) ~f:(fun acc e -> List [ expand_macro e; acc ] ) -let rec equal_expr x y = - match (x, y) with - | Var x1, Var x2 | Symbol x1, Symbol x2 -> equal_string x1 x2 - | List es1, List es2 -> begin - try List.for_all2_exn es1 es2 ~f:equal_expr with _ -> false - end - | _ -> false - let rec replace_id (xfrom : ident) xto e = match e with | Var x when equal_string x xfrom -> xto @@ -159,7 +152,6 @@ let rec star_of_expr : expr -> marked_star = function | e -> Unmarked { content = raylist_of_expr e; bans = [] } let rec constellation_of_expr : expr -> marked_constellation = function - | Symbol k when equal_string k nil_op -> [] | Symbol s -> [ Unmarked { content = [ var (s, None) ]; bans = [] } ] | Var x -> [ Unmarked { content = [ var (x, None) ]; bans = [] } ] | List [ Symbol s; h; t ] when equal_string s cons_op -> @@ -172,6 +164,8 @@ let rec constellation_of_expr : expr -> marked_constellation = function let rec sgen_expr_of_expr (e : expr) : sgen_expr = match e with + | Symbol k when equal_string k nil_op -> + Raw [ Unmarked { content = []; bans = [] } ] (* ray *) | Var _ | Symbol _ -> Raw [ Unmarked { content = [ ray_of_expr e ]; bans = [] } ] diff --git a/src/lsc_ast.ml b/src/lsc_ast.ml index 4f81d15..47b1a25 100644 --- a/src/lsc_ast.ml +++ b/src/lsc_ast.ml @@ -1,35 +1,30 @@ open Base -let ( let* ) x f = Result.bind x ~f - type polarity = | Pos | Neg | Null +[@@deriving eq] module StellarSig = struct type idvar = string * int option type idfunc = polarity * string - let equal_idvar (s, i) (s', i') = - match (i, i') with - | None, None -> equal_string s s' - | Some j, Some j' -> - equal_string (s ^ Int.to_string j) (s' ^ Int.to_string j') - | None, Some j' -> equal_string s (s' ^ Int.to_string j') - | Some j, None -> equal_string (s ^ Int.to_string j) s' - - let equal_idfunc (p, f) (p', f') = - match (p, p') with - | Pos, Pos | Neg, Neg | Null, Null -> equal_string f f' - | _ -> false - - let compatible f g = - match (f, g) with - | (Pos, f), (Neg, g) | (Neg, f), (Pos, g) -> equal_string f g - | (Null, f), (Null, g) -> equal_string f g - | _ -> false + let string_of_idvar (s, i) = + match i with None -> s | Some j -> s ^ Int.to_string j + + let equal_idvar x y = equal_string (string_of_idvar x) (string_of_idvar y) + + let equal_idfunc ((p, f) : idfunc) ((p', f') : idfunc) = + equal_polarity p p' && equal_string f f' + + let compatible (p1, f1) (p2, f2) = + let ( = ) = equal_polarity in + equal_string f1 f2 + && ( (p1 = Pos && p2 = Neg) + || (p1 = Neg && p2 = Pos) + || (p1 = Null && p2 = Null) ) end module StellarRays = Unification.Make (StellarSig) @@ -46,49 +41,20 @@ let fresh_placeholder () = counter_placeholder := !counter_placeholder + 1; Int.to_string r -type ray = term +type ray = term [@@deriving eq] type ban = | Ineq of ray * ray | Incomp of ray * ray +[@@deriving eq] type star = { content : ray list ; bans : ban list } +[@@deriving eq] -type constellation = star list - -let rec compare_ray r1 r2 = - match (r1, r2) with - | Var (x, i), Var (y, j) -> - let i' = Option.value (Option.map i ~f:Int.to_string) ~default:"" in - let j' = Option.value (Option.map j ~f:Int.to_string) ~default:"" in - String.compare (x ^ i') (y ^ j') - | Func _, Var _ -> 1 - | Var _, Func _ -> -1 - | Func (pf1, args1), Func (pf2, args2) -> begin - match (pf1, pf2) with - | pf1, pf2 when StellarSig.equal_idfunc pf1 pf2 -> - List.compare compare_ray args1 args2 - | (Null, f1), (Null, f2) | (Neg, f1), (Neg, f2) | (Pos, f1), (Pos, f2) -> - String.compare f1 f2 - | (Null, _), (_, _) -> -1 - | (Pos, _), (_, _) -> 1 - | (Neg, _), (Null, _) -> 1 - | (Neg, _), (Pos, _) -> -1 - end - -let compare_star = List.compare compare_ray - -let equal_ray = equal_term - -let sort_rays = List.sort ~compare:compare_ray - -let equal_star s1 s2 = - let s1 = sort_rays s1.content in - let s2 = sort_rays s2.content in - List.equal equal_ray s1 s2 +type constellation = star list [@@deriving eq] let to_var x = Var (x, None) @@ -126,61 +92,13 @@ let replace_indices (i : int) : ray -> ray = let raymatcher r r' : substitution option = if is_polarised r && is_polarised r' then solution [ (r, r') ] else None -(* --------------------------------------- - Pretty Printer - --------------------------------------- *) - -let string_of_polarity = function Pos -> "+" | Neg -> "-" | Null -> "" - -let string_of_polsym (p, f) = string_of_polarity p ^ f - -let string_of_var (x, i) = - match i with None -> x | Some i' -> x ^ Int.to_string i' - -let rec string_of_ray = function - | Var xi -> string_of_var xi - | Func (pf, []) -> string_of_polsym pf - | Func (pf, ts) -> - Printf.sprintf "(%s %s)" (string_of_polsym pf) - (List.map ~f:string_of_ray ts |> String.concat ~sep:" ") - -let string_of_subst sub = - Printf.sprintf "{%s}" - (List.fold sub ~init:"" ~f:(fun _ (x, r) -> - string_of_var x ^ "->" ^ string_of_ray r ) ) - -let string_of_ban = function - | Ineq (b1, b2) -> - Printf.sprintf "(!= %s %s)" (string_of_ray b1) (string_of_ray b2) - | Incomp (b1, b2) -> - Printf.sprintf "(slice %s %s)" (string_of_ray b1) (string_of_ray b2) - -let string_of_star s = - match s.content with - | [] -> "[]" - | _ -> - Printf.sprintf "[%s%s]" - (List.map ~f:string_of_ray s.content |> String.concat ~sep:" ") - ( if List.is_empty s.bans then "" - else - Printf.sprintf " || %s" - (List.map ~f:string_of_ban s.bans |> String.concat ~sep:" ") ) - -let string_of_constellation = function - | [] -> "{}" - | [ h ] -> Printf.sprintf "%s" (string_of_star h) - | h :: t -> - let string_h = "{ " ^ string_of_star h ^ " " in - List.fold_left t - ~init:(List.length t, string_h, String.length string_h) - ~f:(fun (i, acc, size) s -> - let string_s = string_of_star s in - let new_size = size + String.length string_s in - if equal_int i 1 then (0, acc ^ string_s, 0) - else if new_size < 80 then (i - 1, acc ^ string_s ^ " ", new_size) - else (i - 1, acc ^ string_s ^ "...\n", 0) ) - |> fun (_, x, _) -> - x |> fun x -> String.append x " }" +let fresh_var vars = + let rec aux i = + if not @@ List.mem vars ("X", Some i) ~equal:StellarSig.equal_idvar then + ("X", Some i) + else aux (i + 1) + in + aux 0 (* --------------------------------------- Operation on marked stars @@ -189,25 +107,9 @@ let string_of_constellation = function type marked_star = | Marked of star | Unmarked of star +[@@deriving eq] -type marked_constellation = marked_star list - -let compare_mstar ms ms' = - match (ms, ms') with - | Marked _, Unmarked _ -> 1 - | Unmarked _, Marked _ -> -1 - | Marked s, Marked s' | Unmarked s, Unmarked s' -> - compare_star s.content s'.content - -let equal_mstar ms ms' = equal_int (compare_mstar ms ms') 0 - -let fresh_var vars = - let rec aux i = - if not @@ List.mem vars ("X", Some i) ~equal:StellarSig.equal_idvar then - ("X", Some i) - else aux (i + 1) - in - aux 0 +type marked_constellation = marked_star list [@@deriving eq] let map_mstar ~f : marked_star -> marked_star = function | Marked s -> Marked { content = List.map ~f s.content; bans = s.bans } @@ -230,11 +132,6 @@ let normalize_vars (mcs : marked_constellation) = let sub = List.zip_exn vars new_vars in subst_all_vars sub mcs -let equal_mconstellation mcs mcs' = - let smcs = List.sort ~compare:compare_mstar mcs in - let smcs' = List.sort ~compare:compare_mstar mcs' in - List.equal equal_mstar (normalize_vars smcs) (normalize_vars smcs') - let unmark = function s -> Unmarked s let mark = function s -> Marked s @@ -249,169 +146,3 @@ let unmark_all = List.map ~f:(fun s -> Unmarked s) let remove_mark_all : marked_constellation -> constellation = List.map ~f:remove_mark - -let ident_counter = ref 0 - -let classify = - let rec aux (cs, space) = function - | [] -> (List.rev cs, List.rev space) - | Marked s :: t -> aux (cs, s :: space) t - | Unmarked s :: t -> aux (s :: cs, space) t - in - aux ([], []) - -let extract_intspace (mcs : marked_constellation) = - ident_counter := 0; - classify mcs - -(* --------------------------------------- - Execution - --------------------------------------- *) - -type configuration = constellation * constellation - -let unpolarized_star s = List.for_all ~f:(Fn.compose not is_polarised) s.content - -let kill : constellation -> constellation = List.filter ~f:unpolarized_star - -let clean : constellation -> constellation = - List.filter ~f:(fun s -> List.is_empty s.content) - -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 = - List.fold_left ~init:([], []) ~f:(function ineq, incomp -> - (function - | Ineq (b1, b2) -> ((b1, b2) :: ineq, incomp) - | Incomp (b1, b2) -> (ineq, (b1, b2) :: incomp) ) ) - -let exists_incomp_pair (box, slice) = - List.exists ~f:(fun (box', slice') -> - equal_ray box box' && (not @@ equal_ray slice slice') ) - -let coherent_incomp incomp = - let aux others res = function - | [] -> res - | h :: t -> res && (not @@ exists_incomp_pair h (others @ t)) - in - aux [] true incomp - -let coherent_bans bans = - let ineq, incomp = group_bans bans in - List.for_all ineq ~f:(fun (b1, b2) -> not @@ equal_ray b1 b2) - && coherent_incomp incomp - -(* interaction between one selected ray and one selected action *) -let rec interaction ~queue repl1 repl2 (selected_action, other_actions) - (selected_ray, other_rays, bans) : star list = - match selected_action.content with - | [] -> [] - | r' :: s' when not (is_polarised r') -> - interaction ~queue:(r' :: queue) 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) repl1 repl2 - ({ content = s'; bans }, other_actions) - (selected_ray, other_rays, bans) - (* if there is an actual connection between rays *) - | Some theta -> - (* action is consumed when execution is linear *) - let next = - interaction ~queue:(r' :: queue) 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 (selected_ray, other_rays, bans) actions : - star list * star list = - let repl1 = replace_indices !ident_counter in - let rec try_actions acc = function - | [] -> ([], acc) - | selected_action :: other_actions -> - let repl2 = replace_indices (!ident_counter + 1) in - let res = - interaction ~queue:[] 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 other_actions in - (res @ next, new_actions) - else - let next, new_actions = - try_actions (selected_action :: acc) other_actions - in - (res @ next, new_actions) - in - try_actions [] actions - -let rec select_ray ~linear ~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 ~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 (selected_ray, queue @ other_rays, bans) actions - with - (* interaction did nothing (no partner), try other rays *) - | [], new_actions -> - select_ray ~linear ~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 -> (Some new_stars, new_actions) ) - -let rec select_star ~linear ~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 -> ( - match - select_ray ~linear ~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 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) ) - -let exec ?(linear = false) mcs : constellation = - (* do a sequence of rounds with a single interaction on state per round *) - let rec loop (actions, states) = - match select_star ~linear ~queue:[] actions states with - | None, _ -> states (* no more possible interaction *) - | Some res, new_actions -> loop (new_actions, res) - in - let cfg = extract_intspace mcs in - loop cfg diff --git a/src/lsc_eval.ml b/src/lsc_eval.ml new file mode 100644 index 0000000..aa5881f --- /dev/null +++ b/src/lsc_eval.ml @@ -0,0 +1,167 @@ +open Base +open Lsc_ast +open Lsc_ast.StellarRays + +let ( let* ) x f = Result.bind x ~f + +type configuration = constellation * constellation + +let unpolarized_star s = List.for_all ~f:(Fn.compose not is_polarised) s.content + +let kill : constellation -> constellation = List.filter ~f:unpolarized_star + +let clean : constellation -> constellation = + List.filter ~f:(fun s -> List.is_empty s.content) + +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 = + List.fold_left ~init:([], []) ~f:(function ineq, incomp -> + (function + | Ineq (b1, b2) -> ((b1, b2) :: ineq, incomp) + | Incomp (b1, b2) -> (ineq, (b1, b2) :: incomp) ) ) + +let exists_incomp_pair (box, slice) = + List.exists ~f:(fun (box', slice') -> + equal_ray box box' && (not @@ equal_ray slice slice') ) + +let coherent_incomp incomp = + let aux others res = function + | [] -> res + | h :: t -> res && (not @@ exists_incomp_pair h (others @ t)) + in + aux [] true incomp + +let coherent_bans bans = + let ineq, incomp = group_bans bans in + List.for_all ineq ~f:(fun (b1, b2) -> not @@ equal_ray b1 b2) + && coherent_incomp incomp + +let ident_counter = ref 0 + +let classify = + let rec aux (cs, space) = function + | [] -> (List.rev cs, List.rev space) + | Marked s :: t -> aux (cs, s :: space) t + | Unmarked s :: t -> aux (s :: cs, space) t + in + aux ([], []) + +let extract_intspace (mcs : marked_constellation) = + ident_counter := 0; + classify mcs + +(* interaction between one selected ray and one selected action *) +let rec interaction ~queue repl1 repl2 (selected_action, other_actions) + (selected_ray, other_rays, bans) : star list = + match selected_action.content with + | [] -> [] + | r' :: s' when not (is_polarised r') -> + interaction ~queue:(r' :: queue) 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) repl1 repl2 + ({ content = s'; bans }, other_actions) + (selected_ray, other_rays, bans) + (* if there is an actual connection between rays *) + | Some theta -> + (* action is consumed when execution is linear *) + let next = + interaction ~queue:(r' :: queue) 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 (selected_ray, other_rays, bans) actions : + star list * star list = + let repl1 = replace_indices !ident_counter in + let rec try_actions acc = function + | [] -> ([], acc) + | selected_action :: other_actions -> + let repl2 = replace_indices (!ident_counter + 1) in + let res = + interaction ~queue:[] 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 other_actions in + (res @ next, new_actions) + else + let next, new_actions = + try_actions (selected_action :: acc) other_actions + in + (res @ next, new_actions) + in + try_actions [] actions + +let rec select_ray ~linear ~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 ~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 (selected_ray, queue @ other_rays, bans) actions + with + (* interaction did nothing (no partner), try other rays *) + | [], new_actions -> + select_ray ~linear ~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 -> (Some new_stars, new_actions) ) + +let rec select_star ~linear ~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 -> ( + match + select_ray ~linear ~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 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) ) + +let exec ?(linear = false) mcs : constellation = + (* do a sequence of rounds with a single interaction on state per round *) + let rec loop (actions, states) = + match select_star ~linear ~queue:[] actions states with + | None, _ -> states (* no more possible interaction *) + | Some res, new_actions -> loop (new_actions, res) + in + let cfg = extract_intspace mcs in + loop cfg diff --git a/src/lsc_pretty.ml b/src/lsc_pretty.ml new file mode 100644 index 0000000..ef6f519 --- /dev/null +++ b/src/lsc_pretty.ml @@ -0,0 +1,59 @@ +open Base +open Lsc_ast +open Lsc_ast.StellarRays + +let string_of_polarity = function Pos -> "+" | Neg -> "-" | Null -> "" + +let string_of_polsym (p, f) = string_of_polarity p ^ f + +let string_of_var (x, i) = + match i with None -> x | Some i' -> x ^ Int.to_string i' + +let rec string_of_ray = function + | Var xi -> string_of_var xi + | Func (pf, []) -> string_of_polsym pf + | Func (pf, ts) -> + Printf.sprintf "(%s %s)" (string_of_polsym pf) + (List.map ~f:string_of_ray ts |> String.concat ~sep:" ") + +let string_of_subst sub = + Printf.sprintf "{%s}" + (List.fold sub ~init:"" ~f:(fun _ (x, r) -> + string_of_var x ^ "->" ^ string_of_ray r ) ) + +let string_of_ban = function + | Ineq (b1, b2) -> + Printf.sprintf "(!= %s %s)" (string_of_ray b1) (string_of_ray b2) + | Incomp (b1, b2) -> + Printf.sprintf "(slice %s %s)" (string_of_ray b1) (string_of_ray b2) + +let string_of_star s = + match s.content with + | [] -> "[]" + | _ -> + Printf.sprintf "[%s%s]" + (List.map ~f:string_of_ray s.content |> String.concat ~sep:" ") + ( if List.is_empty s.bans then "" + else + Printf.sprintf " || %s" + (List.map ~f:string_of_ban s.bans |> String.concat ~sep:" ") ) + +let string_of_constellation = function + | [] -> "{}" + | [ x ] -> begin + match x with + | { content = [ x ]; bans = _ } -> Printf.sprintf "%s" (string_of_ray x) + | _ -> Printf.sprintf "%s" (string_of_star x) + end + | h :: t -> + let string_h = "{ " ^ string_of_star h ^ " " in + List.fold_left t + ~init:(List.length t, string_h, String.length string_h) + ~f:(fun (i, acc, size) s -> + let string_s = string_of_star s in + let new_size = size + String.length string_s in + if i = 1 then (0, acc ^ string_s, 0) + else if new_size < 80 then (i - 1, acc ^ string_s ^ " ", new_size) + else (i - 1, acc ^ string_s ^ "...\n", 0) ) + |> fun (_, x, _) -> + x |> fun x -> String.append x " }" diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index 5764f85..406fc61 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -1,5 +1,7 @@ open Base open Lsc_ast +open Lsc_pretty +open Lsc_eval open Sgen_ast open Out_channel @@ -128,10 +130,9 @@ let rec eval_sgen_expr (env : env) : and expr_of_ray = function | Var (x, None) -> Expr.Var x | Var (x, Some i) -> Expr.Var (x ^ Int.to_string i) - | Func (pf, []) -> Symbol (Lsc_ast.string_of_polsym pf) + | Func (pf, []) -> Symbol (string_of_polsym pf) | Func (pf, args) -> - Expr.List - (Symbol (Lsc_ast.string_of_polsym pf) :: List.map ~f:expr_of_ray args) + Expr.List (Symbol (string_of_polsym pf) :: List.map ~f:expr_of_ray args) let rec eval_decl env : declaration -> (env, err) Result.t = function | Def (x, e) -> @@ -155,8 +156,8 @@ let rec eval_decl env : declaration -> (env, err) Result.t = function let* eval_e1 = eval_sgen_expr env e1 in let* eval_e2 = eval_sgen_expr env e2 in let normalize x = x |> remove_mark_all |> unmark_all in - if not @@ equal_mconstellation (normalize eval_e1) (normalize eval_e2) then - Error (ExpectError (eval_e1, eval_e2, message)) + if not @@ equal_marked_constellation (normalize eval_e1) (normalize eval_e2) + then Error (ExpectError (eval_e1, eval_e2, message)) else Ok env | Use path -> let open Lsc_ast.StellarRays in diff --git a/src/unification.ml b/src/unification.ml index 4d650cb..b541539 100644 --- a/src/unification.ml +++ b/src/unification.ml @@ -20,17 +20,7 @@ module Make (Sig : Signature) = struct type term = | Var of Sig.idvar | Func of Sig.idfunc * term list - - let rec equal_term t u = - match (t, u) with - | Var x, Var y -> Sig.equal_idvar x y - | Func (f, ts), Func (g, us) -> begin - try - Sig.equal_idfunc f g - && List.for_all2_exn ~f:(fun t u -> equal_term t u) ts us - with _ -> false - end - | _ -> false + [@@deriving eq] type substitution = (Sig.idvar * term) list @@ -48,7 +38,7 @@ module Make (Sig : Signature) = struct | Var x -> fbase x | Func (g, ts) -> Func (fnode g, List.map ~f:(map fnode fbase) ts) - let skip = fun _ acc -> acc + let skip _ acc = acc let exists_var pred = fold skip (fun y acc -> pred y || acc) false @@ -69,11 +59,9 @@ module Make (Sig : Signature) = struct Unification algorithm --------------------------------------- *) - let lift_pairl f (x, y) = (f x, y) - - let lift_pairr f (x, y) = (x, f y) + let map_snd f (x, y) = (x, f y) - let lift_pair f p = p |> lift_pairl f |> lift_pairr f + let map_pair f (x, y) = (f x, f y) let rec solve sub : problem -> substitution option = function | [] -> Some sub @@ -82,18 +70,18 @@ module Make (Sig : Signature) = struct (* Orient + Replace *) | (Var x, t) :: pbs | (t, Var x) :: pbs -> elim x t pbs sub (* Open *) - | (Func (f, ts), Func (g, us)) :: pbs - when Sig.compatible f g && List.length ts = List.length us -> begin - solve sub (List.zip_exn ts us @ pbs) - end + | (Func (f, ts), Func (g, us)) :: pbs when Sig.compatible f g -> ( + match List.zip ts us with + | Ok zipped -> solve sub (zipped @ pbs) + | Unequal_lengths -> None ) | _ -> None (* Replace *) and elim x t pbs sub : substitution option = if occurs x t then None (* Circularity *) else - let new_prob = List.map ~f:(lift_pair (subst [ (x, t) ])) pbs in - let new_sub = (x, t) :: List.map ~f:(lift_pairr (subst [ (x, t) ])) sub in + let new_prob = List.map ~f:(map_pair (subst [ (x, t) ])) pbs in + let new_sub = (x, t) :: List.map ~f:(map_snd (subst [ (x, t) ])) sub in solve new_sub new_prob let solution : problem -> substitution option = solve [] From 95655c845d226a2ad74d38731f97e96e31815441 Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 19:47:17 +0200 Subject: [PATCH 2/7] Add ppx_deriving dependency --- dune-project | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dune-project b/dune-project index bedde37..a6bf5a6 100644 --- a/dune-project +++ b/dune-project @@ -19,7 +19,7 @@ (name stellogen) (synopsis "Stellogen is a minimalistic and logic-agnostic programming language based on term unification.") - (depends base menhir (alcotest :with-test) sedlex) + (depends base menhir (alcotest :with-test) sedlex ppx_deriving) (tags ("transcendental syntax" "logic programming" "constraint programming" "resolution logic" "unification" "self-assembly"))) From 0e72ad09d7cd217b058ea7529b6800fb674e91ea Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 19:47:30 +0200 Subject: [PATCH 3/7] Generate new opam file --- stellogen.opam | 1 + 1 file changed, 1 insertion(+) diff --git a/stellogen.opam b/stellogen.opam index c8cd2a4..8c1e23c 100644 --- a/stellogen.opam +++ b/stellogen.opam @@ -23,6 +23,7 @@ depends: [ "menhir" "alcotest" {with-test} "sedlex" + "ppx_deriving" "odoc" {with-doc} ] build: [ From a2bf7e82aba0a9342e8a8a3a2e70ee5bacde89dd Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 20:12:45 +0200 Subject: [PATCH 4/7] Use modules for marked stars and constellations and refactoring --- src/expr.ml | 20 +++++++------- src/lsc_ast.ml | 70 +++++++++++++++++++++++++---------------------- src/lsc_eval.ml | 17 +++++++----- src/lsc_pretty.ml | 1 + src/sgen_ast.ml | 4 +-- src/sgen_eval.ml | 35 ++++++++++++------------ 6 files changed, 77 insertions(+), 70 deletions(-) diff --git a/src/expr.ml b/src/expr.ml index abde414..1082fd2 100644 --- a/src/expr.ml +++ b/src/expr.ml @@ -144,19 +144,19 @@ let rec raylist_of_expr (e : expr) : ray list = ray_of_expr h :: raylist_of_expr t | e -> failwith ("error: unhandled star " ^ to_string e) -let rec star_of_expr : expr -> marked_star = function +let rec star_of_expr : expr -> Marked.star = function | List [ Symbol k; s ] when equal_string k focus_op -> - star_of_expr s |> Lsc_ast.remove_mark |> Lsc_ast.mark + star_of_expr s |> Marked.remove |> Marked.make_state | List [ Symbol k; s; List ps ] when equal_string k params_op -> - Unmarked { content = raylist_of_expr s; bans = bans_of_expr ps } - | e -> Unmarked { content = raylist_of_expr e; bans = [] } + Action { content = raylist_of_expr s; bans = bans_of_expr ps } + | e -> Action { content = raylist_of_expr e; bans = [] } -let rec constellation_of_expr : expr -> marked_constellation = function - | Symbol s -> [ Unmarked { content = [ var (s, None) ]; bans = [] } ] - | Var x -> [ Unmarked { content = [ var (x, None) ]; bans = [] } ] +let rec constellation_of_expr : expr -> Marked.constellation = function + | Symbol s -> [ Action { content = [ var (s, None) ]; bans = [] } ] + | Var x -> [ Action { content = [ var (x, None) ]; bans = [] } ] | List [ Symbol s; h; t ] when equal_string s cons_op -> star_of_expr h :: constellation_of_expr t - | List g -> [ Unmarked { content = [ ray_of_expr (List g) ]; bans = [] } ] + | List g -> [ Action { content = [ ray_of_expr (List g) ]; bans = [] } ] (* --------------------------------------- Stellogen expr of Expr @@ -165,10 +165,10 @@ let rec constellation_of_expr : expr -> marked_constellation = function let rec sgen_expr_of_expr (e : expr) : sgen_expr = match e with | Symbol k when equal_string k nil_op -> - Raw [ Unmarked { content = []; bans = [] } ] + Raw [ Action { content = []; bans = [] } ] (* ray *) | Var _ | Symbol _ -> - Raw [ Unmarked { content = [ ray_of_expr e ]; bans = [] } ] + Raw [ Action { content = [ ray_of_expr e ]; bans = [] } ] (* star *) | List (Symbol s :: _) when equal_string s params_op -> Raw [ star_of_expr e ] | List (Symbol s :: _) when equal_string s cons_op -> Raw [ star_of_expr e ] diff --git a/src/lsc_ast.ml b/src/lsc_ast.ml index 47b1a25..7c3e860 100644 --- a/src/lsc_ast.ml +++ b/src/lsc_ast.ml @@ -48,13 +48,15 @@ type ban = | Incomp of ray * ray [@@deriving eq] -type star = - { content : ray list - ; bans : ban list - } -[@@deriving eq] - -type constellation = star list [@@deriving eq] +module Raw = struct + type star = + { content : ray list + ; bans : ban list + } + [@@deriving eq] + + type constellation = star list [@@deriving eq] +end let to_var x = Var (x, None) @@ -104,25 +106,42 @@ let fresh_var vars = Operation on marked stars --------------------------------------- *) -type marked_star = - | Marked of star - | Unmarked of star -[@@deriving eq] +module Marked = struct + type star = + | State of Raw.star + | Action of Raw.star + [@@deriving eq] + + type constellation = star list [@@deriving eq] -type marked_constellation = marked_star list [@@deriving eq] + let map ~f : star -> star = function + | State s -> State { content = List.map ~f s.content; bans = s.bans } + | Action s -> Action { content = List.map ~f s.content; bans = s.bans } -let map_mstar ~f : marked_star -> marked_star = function - | Marked s -> Marked { content = List.map ~f s.content; bans = s.bans } - | Unmarked s -> Unmarked { content = List.map ~f s.content; bans = s.bans } + let make_action s = Action s + let make_state s = State s -let subst_all_vars sub = List.map ~f:(map_mstar ~f:(subst sub)) + let make_action_all = List.map ~f:make_action + + let make_state_all = List.map ~f:make_state + + let remove : star -> Raw.star = function + | State s -> s + | Action s -> s + + let remove_all = List.map ~f:remove + + let normalize_all x = x |> remove_all |> make_action_all +end + +let subst_all_vars sub = List.map ~f:(Marked.map ~f:(subst sub)) let all_vars mcs : StellarSig.idvar list = - List.map mcs ~f:(function Marked s | Unmarked s -> + List.map mcs ~f:(function Marked.State s | Marked.Action s -> List.map s.content ~f:StellarRays.vars |> List.concat ) |> List.concat -let normalize_vars (mcs : marked_constellation) = +let normalize_vars (mcs : Marked.constellation) = let vars = all_vars mcs in let new_x, new_i = fresh_var vars in let new_vars = @@ -131,18 +150,3 @@ let normalize_vars (mcs : marked_constellation) = in let sub = List.zip_exn vars new_vars in subst_all_vars sub mcs - -let unmark = function s -> Unmarked s - -let mark = function s -> Marked s - -let focus = List.map ~f:(fun r -> mark r) - -let remove_mark : marked_star -> star = function - | Marked s -> s - | Unmarked s -> s - -let unmark_all = List.map ~f:(fun s -> Unmarked s) - -let remove_mark_all : marked_constellation -> constellation = - List.map ~f:remove_mark diff --git a/src/lsc_eval.ml b/src/lsc_eval.ml index aa5881f..e1d0820 100644 --- a/src/lsc_eval.ml +++ b/src/lsc_eval.ml @@ -1,16 +1,19 @@ open Base open Lsc_ast open Lsc_ast.StellarRays +open Lsc_ast.Raw let ( let* ) x f = Result.bind x ~f type configuration = constellation * constellation -let unpolarized_star s = List.for_all ~f:(Fn.compose not is_polarised) s.content +let unpolarized_star s = + let open Raw in + List.for_all ~f:(Fn.compose not is_polarised) s.content -let kill : constellation -> constellation = List.filter ~f:unpolarized_star +let kill = List.filter ~f:unpolarized_star -let clean : constellation -> constellation = +let clean = List.filter ~f:(fun s -> List.is_empty s.content) let fmap_ban ~f = function @@ -53,18 +56,18 @@ let ident_counter = ref 0 let classify = let rec aux (cs, space) = function | [] -> (List.rev cs, List.rev space) - | Marked s :: t -> aux (cs, s :: space) t - | Unmarked s :: t -> aux (s :: cs, space) t + | Marked.State s :: t -> aux (cs, s :: space) t + | Marked.Action s :: t -> aux (s :: cs, space) t in aux ([], []) -let extract_intspace (mcs : 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 repl1 repl2 (selected_action, other_actions) - (selected_ray, other_rays, bans) : star list = + (selected_ray, other_rays, bans) : constellation = match selected_action.content with | [] -> [] | r' :: s' when not (is_polarised r') -> diff --git a/src/lsc_pretty.ml b/src/lsc_pretty.ml index ef6f519..126960b 100644 --- a/src/lsc_pretty.ml +++ b/src/lsc_pretty.ml @@ -1,6 +1,7 @@ open Base open Lsc_ast open Lsc_ast.StellarRays +open Lsc_ast.Raw let string_of_polarity = function Pos -> "+" | Neg -> "-" | Null -> "" diff --git a/src/sgen_ast.ml b/src/sgen_ast.ml index 27442c5..3425d08 100644 --- a/src/sgen_ast.ml +++ b/src/sgen_ast.ml @@ -8,7 +8,7 @@ type idvar = string * int option type idfunc = polarity * string type sgen_expr = - | Raw of marked_constellation + | Raw of Marked.constellation | Id of ident | Exec of bool * sgen_expr | Group of sgen_expr list @@ -19,7 +19,7 @@ type sgen_expr = | Eval of sgen_expr type err = - | ExpectError of marked_constellation * marked_constellation * ident + | ExpectError of Marked.constellation * Marked.constellation * ident | UnknownID of string type env = { objs : (ident * sgen_expr) list } diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index 406fc61..3442ac9 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -58,8 +58,8 @@ let pp_err e : (string, err) Result.t = match e with | ExpectError (x, e, Func ((Null, f), [])) when equal_string f "default" -> sprintf "%s:\n* expected: %s\n* got: %s\n" (red "Expect Error") - (e |> remove_mark_all |> string_of_constellation) - (x |> remove_mark_all |> string_of_constellation) + (e |> Marked.remove_all |> string_of_constellation) + (x |> Marked.remove_all |> string_of_constellation) |> Result.return | ExpectError (_x, _e, Func ((Null, f), [ t ])) when equal_string f "error" -> sprintf "%s: %s\n" (red "Expect Error") (string_of_ray t) |> Result.return @@ -70,7 +70,7 @@ let pp_err e : (string, err) Result.t = |> Result.return let rec eval_sgen_expr (env : env) : - sgen_expr -> (marked_constellation, err) Result.t = function + sgen_expr -> (Marked.constellation, err) Result.t = function | Raw mcs -> Ok mcs | Id x -> begin match get_obj env x with @@ -88,43 +88,43 @@ let rec eval_sgen_expr (env : env) : Ok (List.concat mcs) | Exec (b, e) -> let* eval_e = eval_sgen_expr env e in - Ok (exec ~linear:b eval_e |> unmark_all) + Ok (exec ~linear:b eval_e |> Marked.make_action_all) | Focus e -> let* eval_e = eval_sgen_expr env e in - eval_e |> remove_mark_all |> focus |> Result.return + eval_e |> Marked.remove_all |> Marked.make_state_all |> Result.return | Kill e -> let* eval_e = eval_sgen_expr env e in - eval_e |> remove_mark_all |> kill |> focus |> Result.return + eval_e |> Marked.remove_all |> kill |> Marked.make_state_all |> Result.return | Clean e -> let* eval_e = eval_sgen_expr env e in - eval_e |> remove_mark_all |> clean |> focus |> Result.return + eval_e |> Marked.remove_all |> clean |> Marked.make_state_all |> Result.return | Process [] -> Ok [] | Process (h :: t) -> let* eval_e = eval_sgen_expr env h in - let init = eval_e |> remove_mark_all |> focus in + let init = eval_e |> Marked.remove_all |> Marked.make_state_all in let* res = List.fold_left t ~init:(Ok init) ~f:(fun acc x -> let* acc = acc in match x with | Id (Func ((Null, "&kill"), [])) -> - acc |> remove_mark_all |> kill |> focus |> Result.return + acc |> Marked.remove_all |> kill |> Marked.make_state_all |> Result.return | Id (Func ((Null, "&clean"), [])) -> - acc |> remove_mark_all |> clean |> focus |> Result.return + acc |> Marked.remove_all |> clean |> Marked.make_state_all |> Result.return | _ -> - let origin = acc |> remove_mark_all |> focus in + let origin = acc |> Marked.remove_all |> Marked.make_state_all in eval_sgen_expr env (Focus (Exec (false, Group [ x; Raw origin ]))) ) in res |> Result.return | Eval e -> ( let* eval_e = eval_sgen_expr env e in match eval_e with - | [ Marked { content = [ r ]; bans = _ } ] - | [ Unmarked { content = [ r ]; bans = _ } ] -> + | [ State { content = [ r ]; bans = _ } ] + | [ Action { content = [ r ]; bans = _ } ] -> r |> expr_of_ray |> Expr.sgen_expr_of_expr |> eval_sgen_expr env | e -> failwith ( "eval error: " - ^ string_of_constellation (remove_mark_all e) + ^ string_of_constellation (Marked.remove_all e) ^ " is not a ray." ) ) and expr_of_ray = function @@ -139,13 +139,13 @@ let rec eval_decl env : declaration -> (env, err) Result.t = function let env = { objs = add_obj env x e } in Ok env | Show (Raw mcs) -> - mcs |> remove_mark_all |> string_of_constellation |> Stdlib.print_string; + mcs |> Marked.remove_all |> string_of_constellation |> Stdlib.print_string; Stdlib.print_newline (); Stdlib.flush Stdlib.stdout; Ok env | Show e -> let* eval_e = eval_sgen_expr env e in - List.map eval_e ~f:remove_mark + List.map eval_e ~f:Marked.remove |> string_of_constellation |> Stdlib.print_string; Stdlib.print_newline (); Ok env @@ -155,8 +155,7 @@ let rec eval_decl env : declaration -> (env, err) Result.t = function | Expect (e1, e2, message) -> let* eval_e1 = eval_sgen_expr env e1 in let* eval_e2 = eval_sgen_expr env e2 in - let normalize x = x |> remove_mark_all |> unmark_all in - if not @@ equal_marked_constellation (normalize eval_e1) (normalize eval_e2) + if not @@ Marked.equal_constellation (Marked.normalize_all eval_e1) (Marked.normalize_all eval_e2) then Error (ExpectError (eval_e1, eval_e2, message)) else Ok env | Use path -> From ace5db59c0fc7b98bfdb4201aeef0f87a1555cf8 Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 20:13:20 +0200 Subject: [PATCH 5/7] dune fmt --- src/expr.ml | 2 +- src/lsc_ast.ml | 7 +++---- src/lsc_eval.ml | 3 +-- src/sgen_eval.ml | 18 +++++++++++++----- 4 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/expr.ml b/src/expr.ml index 1082fd2..3884474 100644 --- a/src/expr.ml +++ b/src/expr.ml @@ -23,7 +23,7 @@ type expr = | Symbol of string | Var of ident | List of expr list - [@@derive eq] +[@@derive eq] let primitive = String.append "%" diff --git a/src/lsc_ast.ml b/src/lsc_ast.ml index 7c3e860..6ec0500 100644 --- a/src/lsc_ast.ml +++ b/src/lsc_ast.ml @@ -119,15 +119,14 @@ module Marked = struct | Action s -> Action { content = List.map ~f s.content; bans = s.bans } let make_action s = Action s + let make_state s = State s let make_action_all = List.map ~f:make_action - let make_state_all = List.map ~f:make_state + let make_state_all = List.map ~f:make_state - let remove : star -> Raw.star = function - | State s -> s - | Action s -> s + let remove : star -> Raw.star = function State s -> s | Action s -> s let remove_all = List.map ~f:remove diff --git a/src/lsc_eval.ml b/src/lsc_eval.ml index e1d0820..4240a69 100644 --- a/src/lsc_eval.ml +++ b/src/lsc_eval.ml @@ -13,8 +13,7 @@ let unpolarized_star s = let kill = List.filter ~f:unpolarized_star -let clean = - List.filter ~f:(fun s -> List.is_empty s.content) +let clean = List.filter ~f:(fun s -> List.is_empty s.content) let fmap_ban ~f = function | Ineq (b1, b2) -> Ineq (f b1, f b2) diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index 3442ac9..e907078 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -94,10 +94,12 @@ let rec eval_sgen_expr (env : env) : eval_e |> Marked.remove_all |> Marked.make_state_all |> Result.return | Kill e -> let* eval_e = eval_sgen_expr env e in - eval_e |> Marked.remove_all |> kill |> Marked.make_state_all |> Result.return + eval_e |> Marked.remove_all |> kill |> Marked.make_state_all + |> Result.return | Clean e -> let* eval_e = eval_sgen_expr env e in - eval_e |> Marked.remove_all |> clean |> Marked.make_state_all |> Result.return + eval_e |> Marked.remove_all |> clean |> Marked.make_state_all + |> Result.return | Process [] -> Ok [] | Process (h :: t) -> let* eval_e = eval_sgen_expr env h in @@ -107,9 +109,11 @@ let rec eval_sgen_expr (env : env) : let* acc = acc in match x with | Id (Func ((Null, "&kill"), [])) -> - acc |> Marked.remove_all |> kill |> Marked.make_state_all |> Result.return + acc |> Marked.remove_all |> kill |> Marked.make_state_all + |> Result.return | Id (Func ((Null, "&clean"), [])) -> - acc |> Marked.remove_all |> clean |> Marked.make_state_all |> Result.return + acc |> Marked.remove_all |> clean |> Marked.make_state_all + |> Result.return | _ -> let origin = acc |> Marked.remove_all |> Marked.make_state_all in eval_sgen_expr env (Focus (Exec (false, Group [ x; Raw origin ]))) ) @@ -155,7 +159,11 @@ let rec eval_decl env : declaration -> (env, err) Result.t = function | Expect (e1, e2, message) -> let* eval_e1 = eval_sgen_expr env e1 in let* eval_e2 = eval_sgen_expr env e2 in - if not @@ Marked.equal_constellation (Marked.normalize_all eval_e1) (Marked.normalize_all eval_e2) + if + not + @@ Marked.equal_constellation + (Marked.normalize_all eval_e1) + (Marked.normalize_all eval_e2) then Error (ExpectError (eval_e1, eval_e2, message)) else Ok env | Use path -> From 95edb426139f33b325411ec6214f30067862fb05 Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 22:21:36 +0200 Subject: [PATCH 6/7] Remove kill and clean --- README.md | 10 +++--- examples/automata.sg | 16 +++++---- examples/binary4.sg | 76 +++++++++++++++++---------------------- examples/circuits.sg | 1 - examples/npda.sg | 10 +++--- examples/turing.sg | 16 ++++----- nvim/syntax/stellogen.vim | 2 +- src/expr.ml | 4 --- src/lsc_eval.ml | 9 +---- src/sgen_ast.ml | 2 -- src/sgen_eval.ml | 24 +------------ 11 files changed, 65 insertions(+), 105 deletions(-) diff --git a/README.md b/README.md index d223969..c8d7d8c 100644 --- a/README.md +++ b/README.md @@ -75,10 +75,12 @@ automaton accepting words ending with 00 #(if read 1 on q0 then q0) #(if read 0 on q1 then q2)}) - - - - +(:= kill (-a _ _)) + + + + + ``` More examples can be found in `examples/`. diff --git a/examples/automata.sg b/examples/automata.sg index bced06e..8fb3e76 100644 --- a/examples/automata.sg +++ b/examples/automata.sg @@ -22,13 +22,13 @@ (:= 110 (+i [1 1 0])) (:: 110 binary) -''' -automaton accepting words ending with 00 -''' (:= (initial Q) [(-i W) (+a W Q)]) (:= (accept Q) [(-a [] Q) accept]) (:= (if read C1 on Q1 then Q2) [(-a [C1|W] Q1) (+a W Q2)]) +''' +automaton accepting words ending with 00 +''' (:= a1 { #(initial q0) #(accept q2) @@ -37,7 +37,9 @@ automaton accepting words ending with 00 #(if read 1 on q0 then q0) #(if read 0 on q1 then q2)}) - - - - +(:= kill (-a _ _)) + + + + + diff --git a/examples/binary4.sg b/examples/binary4.sg index ed59e98..6eab180 100644 --- a/examples/binary4.sg +++ b/examples/binary4.sg @@ -1,48 +1,38 @@ -''' -(spec u4 [(-b 1 _) (-b 2 _) (-b 3 _) (-b 4 _) ok]) +(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok]) -(new-declaration (:: tested test) - (:= test @(exec (process #test #test{b=>+b}))) - (== test ok)) +(new-declaration (:: Tested Test) + (== @(exec (process #Test #Tested)) ok)) -(:= b1 [ [(b 1 1)] [(b 2 0)] [(b 3 0)] [(b 4 1)]]) -(:: b1 u4) +(:= (make_bin Name X1 X2 X3 X4) + { [(+b Name 1 X1)] [(+b Name 2 X2)] [(+b Name 3 X3)] [(+b Name 4 X4)] }) -(:= b2 [ [(b 1 0)] [(b 2 0)] [(b 3 1)] [(b 4 1)]]) +(:= b1 #(make_bin b1 0 0 0 1)) (:: b1 u4) -(:= and [ - [(-b1 arg 0) (-b2 arg X) (b arg 0)] - [(-b1 arg 1) (-b2 arg X) (b arg X)]]) - -(:= or [ - [(-b1 arg 0) (-b2 arg X) (b arg X)] - [(-b1 arg 1) (-b2 arg X) (b arg 1)]]) - -(:= xor [ - [(-b1 arg 1) (-b2 arg 0) (b arg 1)] - [(-b1 arg 0) (-b2 arg 1) (b arg 1)] - [(-b1 arg 0) (-b2 arg 0) (b arg 0)] - [(-b1 arg 1) (-b2 arg 1) (b arg 0)]]) - -'logical AND -+b1} - #and{arg=>1} #and{arg=>2} #and{arg=>3} #and{arg=>4} - #b2{b=>+b2} - kill)> - -'logical OR -+b1} - #or{arg=>1} #or{arg=>2} #or{arg=>3} #or{arg=>4} - #b2{b=>+b2} - kill)> - -'logical XOR -+b1} - #xor{arg=>1} #xor{arg=>2} #xor{arg=>3} #xor{arg=>4} - #b2{b=>+b2} - kill)> - ''' +(:= b2 #(make_bin b2 0 0 1 1)) +(:: b2 u4) + +(show #b1) +(show #b2) + +(:= (if A = X and B = Y then R = Z) [(-b A I X) (-b B I Y) (+b R I Z)]) + +''' +'FIXME + +(:= (and AA BB RR) { + #(if AA = 0 and BB = XX then RR = 0) + #(if AA = 1 and BB = XX then RR = XX) }) +(show #(and b1 b2 r1)) +(show (process #b1 #(and b1 b2 r1) #b2)) + +(:= (or A B R) { + [(-b A I 0) (-b B I X) (+b R I X)] + [(-b A I 1) (-b B I X) (+b R I 1)]}) + +(:= (xor A B R) { + [(-b A I 1) (-b B I 0) (+b R I 1)] + [(-b A I 0) (-b B I 1) (+b R I 1)] + [(-b A I 0) (-b B I 0) (+b R I 0)] + [(-b A I 1) (-b B I 1) (+b R I 0)]}) +''' diff --git a/examples/circuits.sg b/examples/circuits.sg index 4aac685..7f7ce7e 100644 --- a/examples/circuits.sg +++ b/examples/circuits.sg @@ -36,4 +36,3 @@ FIXME [(-c4 R) R] 'apply semantics #semantics)> - '&kill diff --git a/examples/npda.sg b/examples/npda.sg index 021736e..c70855b 100644 --- a/examples/npda.sg +++ b/examples/npda.sg @@ -35,7 +35,9 @@ #(if read 0 with 0 on q1 then q1) #(if read 1 with 1 on q1 then q1)}) - - - - +(:= kill (-a _ _ _)) + + + + + diff --git a/examples/turing.sg b/examples/turing.sg index dcdcadd..462085b 100644 --- a/examples/turing.sg +++ b/examples/turing.sg @@ -29,12 +29,12 @@ [(-m q3 L e R) (+m qr L e R)] [(-m qr L C R) reject]}) - - - + + + - - - - - + + + + + diff --git a/nvim/syntax/stellogen.vim b/nvim/syntax/stellogen.vim index 227415c..043cf5a 100644 --- a/nvim/syntax/stellogen.vim +++ b/nvim/syntax/stellogen.vim @@ -1,6 +1,6 @@ syn clear -syn keyword sgKeyword new declaration kill clean eval slice show use exec spec linexec process +syn keyword sgKeyword new declaration eval slice show use exec spec linexec process syn match sgComment "\s*'[^'].*$" syn match sgId "#\%(\l\|\d\)\w*" syn region sgComment start="'''" end="'''" contains=NONE diff --git a/src/expr.ml b/src/expr.ml index 3884474..15e1051 100644 --- a/src/expr.ml +++ b/src/expr.ml @@ -182,10 +182,6 @@ let rec sgen_expr_of_expr (e : expr) : sgen_expr = Group (List.map ~f:sgen_expr_of_expr gs) (* process *) | List (Symbol "process" :: gs) -> Process (List.map ~f:sgen_expr_of_expr gs) - (* kill *) - | List [ Symbol "kill"; g ] -> Kill (sgen_expr_of_expr g) - (* clean *) - | List [ Symbol "clean"; g ] -> Clean (sgen_expr_of_expr g) (* exec *) | List [ Symbol "exec"; g ] -> Exec (false, sgen_expr_of_expr g) (* linear exec *) diff --git a/src/lsc_eval.ml b/src/lsc_eval.ml index 4240a69..5d1b053 100644 --- a/src/lsc_eval.ml +++ b/src/lsc_eval.ml @@ -7,13 +7,6 @@ let ( let* ) x f = Result.bind x ~f type configuration = constellation * constellation -let unpolarized_star s = - let open Raw in - List.for_all ~f:(Fn.compose not is_polarised) s.content - -let kill = List.filter ~f:unpolarized_star - -let clean = List.filter ~f:(fun s -> List.is_empty s.content) let fmap_ban ~f = function | Ineq (b1, b2) -> Ineq (f b1, f b2) @@ -166,4 +159,4 @@ let exec ?(linear = false) mcs : constellation = | Some res, new_actions -> loop (new_actions, res) in let cfg = extract_intspace mcs in - loop cfg + loop cfg |> List.filter ~f:(fun s -> not @@ List.is_empty s.content) diff --git a/src/sgen_ast.ml b/src/sgen_ast.ml index 3425d08..a92c2b1 100644 --- a/src/sgen_ast.ml +++ b/src/sgen_ast.ml @@ -13,8 +13,6 @@ type sgen_expr = | Exec of bool * sgen_expr | Group of sgen_expr list | Focus of sgen_expr - | Clean of sgen_expr - | Kill of sgen_expr | Process of sgen_expr list | Eval of sgen_expr diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index e907078..f680d15 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -29,12 +29,6 @@ let rec map_sgen_expr env ~f : sgen_expr -> (sgen_expr, err) Result.t = function | Exec (b, e) -> let* map_e = map_sgen_expr env ~f e in Exec (b, map_e) |> Result.return - | Kill e -> - let* map_e = map_sgen_expr env ~f e in - Kill map_e |> Result.return - | Clean e -> - let* map_e = map_sgen_expr env ~f e in - Clean map_e |> Result.return | Group es -> let* map_es = List.map ~f:(map_sgen_expr env ~f) es |> Result.all in Group map_es |> Result.return @@ -92,14 +86,6 @@ let rec eval_sgen_expr (env : env) : | Focus e -> let* eval_e = eval_sgen_expr env e in eval_e |> Marked.remove_all |> Marked.make_state_all |> Result.return - | Kill e -> - let* eval_e = eval_sgen_expr env e in - eval_e |> Marked.remove_all |> kill |> Marked.make_state_all - |> Result.return - | Clean e -> - let* eval_e = eval_sgen_expr env e in - eval_e |> Marked.remove_all |> clean |> Marked.make_state_all - |> Result.return | Process [] -> Ok [] | Process (h :: t) -> let* eval_e = eval_sgen_expr env h in @@ -107,15 +93,7 @@ let rec eval_sgen_expr (env : env) : let* res = List.fold_left t ~init:(Ok init) ~f:(fun acc x -> let* acc = acc in - match x with - | Id (Func ((Null, "&kill"), [])) -> - acc |> Marked.remove_all |> kill |> Marked.make_state_all - |> Result.return - | Id (Func ((Null, "&clean"), [])) -> - acc |> Marked.remove_all |> clean |> Marked.make_state_all - |> Result.return - | _ -> - let origin = acc |> Marked.remove_all |> Marked.make_state_all in + let origin = acc |> Marked.remove_all |> Marked.make_state_all in eval_sgen_expr env (Focus (Exec (false, Group [ x; Raw origin ]))) ) in res |> Result.return From 1ee2d46cf7368f21ce9d462c06df3b383c7078f2 Mon Sep 17 00:00:00 2001 From: engboris Date: Fri, 11 Jul 2025 22:36:08 +0200 Subject: [PATCH 7/7] dune fmt --- src/lsc_eval.ml | 1 - src/sgen_eval.ml | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/lsc_eval.ml b/src/lsc_eval.ml index 5d1b053..5aa20e8 100644 --- a/src/lsc_eval.ml +++ b/src/lsc_eval.ml @@ -7,7 +7,6 @@ let ( let* ) x f = Result.bind x ~f 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) diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml index f680d15..c21c300 100644 --- a/src/sgen_eval.ml +++ b/src/sgen_eval.ml @@ -94,7 +94,7 @@ let rec eval_sgen_expr (env : env) : List.fold_left t ~init:(Ok init) ~f:(fun acc x -> let* acc = acc in let origin = acc |> Marked.remove_all |> Marked.make_state_all in - eval_sgen_expr env (Focus (Exec (false, Group [ x; Raw origin ]))) ) + eval_sgen_expr env (Focus (Exec (false, Group [ x; Raw origin ]))) ) in res |> Result.return | Eval e -> (