From 2d8986b80269ee3ccd37060d32131da2437d87eb Mon Sep 17 00:00:00 2001 From: engboris Date: Tue, 13 Aug 2024 23:49:03 +0200 Subject: [PATCH 1/4] Prototype of metaprogramming language for constellations --- bin/dune | 6 +-- bin/ilsc.ml | 9 ++-- bin/{lsc.ml => lscrun.ml} | 7 ++-- bin/sgen.ml | 17 ++++++++ dune-project | 4 +- src/{stellar.ml => lsc/ast.ml} | 11 ++--- src/{ => lsc}/dune | 2 +- src/{ => lsc}/lexer.mll | 0 src/lsc/parser.mly | 56 +++++++++++++++++++++++++ src/{prettyprinter.ml => lsc/pretty.ml} | 0 src/{ => lsc}/unification.ml | 0 src/stellogen/ast.ml | 20 +++++++++ src/stellogen/dune | 9 ++++ src/stellogen/lexer.mll | 29 +++++++++++++ src/stellogen/parser.mly | 27 ++++++++++++ test/dune | 2 +- test/test.ml | 7 ++-- lsc.opam => tsyntax.opam | 0 18 files changed, 184 insertions(+), 22 deletions(-) rename bin/{lsc.ml => lscrun.ml} (91%) create mode 100644 bin/sgen.ml rename src/{stellar.ml => lsc/ast.ml} (93%) rename src/{ => lsc}/dune (91%) rename src/{ => lsc}/lexer.mll (100%) create mode 100644 src/lsc/parser.mly rename src/{prettyprinter.ml => lsc/pretty.ml} (100%) rename src/{ => lsc}/unification.ml (100%) create mode 100644 src/stellogen/ast.ml create mode 100644 src/stellogen/dune create mode 100644 src/stellogen/lexer.mll create mode 100644 src/stellogen/parser.mly rename lsc.opam => tsyntax.opam (100%) diff --git a/bin/dune b/bin/dune index e3b12ba..7f9bab1 100644 --- a/bin/dune +++ b/bin/dune @@ -1,7 +1,7 @@ (executables - (public_names lsc ilsc) - (names lsc ilsc) - (libraries lsclib base)) + (public_names lsc ilsc sgen) + (names lscrun ilsc sgen) + (libraries lsc stellogen base)) (env (dev (flags (:standard -warn-error -A)))) diff --git a/bin/ilsc.ml b/bin/ilsc.ml index dd0cee1..d8ea7e8 100644 --- a/bin/ilsc.ml +++ b/bin/ilsc.ml @@ -1,6 +1,7 @@ open Base -open Lsclib.Stellar -open Lsclib.Parser +open Lsc.Ast +open Lsc.Parser +open Lsc.Lexer let welcome () = Stdlib.print_string "Commands :--------------------------------------\n"; @@ -33,7 +34,7 @@ let rec add cs = let input = prompt "Add stars" in try let lexbuf = Lexing.from_string input in - let mcs = marked_constellation Lsclib.Lexer.read lexbuf in + let mcs = marked_constellation read lexbuf in cs @ (List.map ~f:unmark mcs) with _ -> Stdlib.print_string "Error. Please retry.\n"; @@ -56,7 +57,7 @@ let rec loop (cs : constellation) = let base = List.map ~f:(fun s -> Marked s) cs in let lexbuf = Lexing.from_string input in try - let mcs = marked_constellation Lsclib.Lexer.read lexbuf in + let mcs = marked_constellation read lexbuf in let cs = extract_intspace (base @ mcs) in let result = exec ~unfincomp:true diff --git a/bin/lsc.ml b/bin/lscrun.ml similarity index 91% rename from bin/lsc.ml rename to bin/lscrun.ml index d0e66dd..8fa1520 100644 --- a/bin/lsc.ml +++ b/bin/lscrun.ml @@ -1,6 +1,7 @@ open Base -open Lsclib.Stellar -open Lsclib.Parser +open Lsc.Ast +open Lsc.Parser +open Lsc.Lexer open Out_channel let usage_msg = "exec [-no-trivial-eq] [-allow-unfinished-computation] [-show-steps] [-show-trace] [-allow-self-interaction] " @@ -37,7 +38,7 @@ let speclist = let _ = Stdlib.Arg.parse speclist anon_fun usage_msg; let lexbuf = Lexing.from_channel (Stdlib.open_in !input_file) in - let mcs = marked_constellation Lsclib.Lexer.read lexbuf in + let mcs = marked_constellation read lexbuf in let cs = extract_intspace mcs in (if !showsteps then output_string stdout "Press any key to move to the next step.\n"); diff --git a/bin/sgen.ml b/bin/sgen.ml new file mode 100644 index 0000000..119a3a2 --- /dev/null +++ b/bin/sgen.ml @@ -0,0 +1,17 @@ +open Base +(* open Stellogen.Ast *) +open Stellogen.Parser +open Stellogen.Lexer + +let usage_msg = "sgen " +let input_file = ref "" + +let anon_fun filename = input_file := filename + +let speclist = [] + +let _ = + Stdlib.Arg.parse speclist anon_fun usage_msg; + let lexbuf = Lexing.from_channel (Stdlib.open_in !input_file) in + let prog = program read lexbuf in + () diff --git a/dune-project b/dune-project index e31d429..88b67ac 100644 --- a/dune-project +++ b/dune-project @@ -1,6 +1,6 @@ (lang dune 3.7) -(name lsc) +(name tsyntax) (generate_opam_files true) @@ -16,7 +16,7 @@ (documentation https://github.com/engboris/large-star-collider/blob/main/README.md) (package - (name lsc) + (name tsyntax) (synopsis "Stellar resolution implemented with interactive execution") (description "The Large Star Collider (LSC) is an implementation of stellar resolution which interprets and executes objects called constellations, which are the programs of stellar resolution.") (depends base menhir) diff --git a/src/stellar.ml b/src/lsc/ast.ml similarity index 93% rename from src/stellar.ml rename to src/lsc/ast.ml index 429b1ca..ac11046 100644 --- a/src/stellar.ml +++ b/src/lsc/ast.ml @@ -1,4 +1,5 @@ open Base +open Pretty type polarity = Pos | Neg | Null @@ -87,21 +88,21 @@ let rec string_of_ray = function | Func ((Null, ":"), [r1; r2]) -> (string_of_ray r1) ^ ":" ^ (string_of_ray r2) | Func (pf, ts) -> string_of_polsym pf ^ - Prettyprinter.surround "(" ")" @@ - Prettyprinter.string_of_list string_of_ray " " ts + surround "(" ")" @@ + string_of_list string_of_ray " " ts let string_of_subst sub = List.fold sub ~init:"" ~f:(fun _ (x, r) -> (string_of_var x) ^ "->" ^ (string_of_ray r)) - |> Prettyprinter.surround "{" "}" + |> surround "{" "}" let string_of_star s = if List.is_empty s then "[]" - else Prettyprinter.string_of_list string_of_ray " " s + else string_of_list string_of_ray " " s let string_of_constellation cs = if List.is_empty cs then "{}" - else (Prettyprinter.string_of_list string_of_star ";\n" cs) ^ ";" + else (string_of_list string_of_star ";\n" cs) ^ ";" (* --------------------------------------- Interactive execution diff --git a/src/dune b/src/lsc/dune similarity index 91% rename from src/dune rename to src/lsc/dune index f3db905..5d0e4b4 100644 --- a/src/dune +++ b/src/lsc/dune @@ -1,5 +1,5 @@ (library - (name lsclib) + (name lsc) (libraries base)) (env (dev diff --git a/src/lexer.mll b/src/lsc/lexer.mll similarity index 100% rename from src/lexer.mll rename to src/lsc/lexer.mll diff --git a/src/lsc/parser.mly b/src/lsc/parser.mly new file mode 100644 index 0000000..df46b18 --- /dev/null +++ b/src/lsc/parser.mly @@ -0,0 +1,56 @@ +%{ +open Ast +%} + +%token COMMA +%token LBRACK RBRACK +%token LPAR RPAR +%token VAR +%token SYM +%token PLUS MINUS +%token CONS +%token AT +%token SEMICOLON +%token PLACEHOLDER +%token EMPTY_SYM +%token EOF + +%right CONS + +%start marked_constellation + +%% + +%public marked_constellation: +| EOF { [] } +| cs = nonempty_list(star); EOF { cs } + +star: +| AT; s = star_content; SEMICOLON { Marked s } +| s = star_content; SEMICOLON { Unmarked s } + +star_content: +| LBRACK; RBRACK { [] } +| rs = separated_nonempty_list(COMMA?, ray) { rs } + +symbol: +| PLUS; f = SYM { (Pos, f) } +| MINUS; f = SYM { (Neg, f) } +| f = SYM { (Null, f) } + +ray: +| EMPTY_SYM { to_func ((Null, "$"), []) } +| PLACEHOLDER { to_var ("_"^(fresh_placeholder ())) } +| x = VAR { to_var x } +| e = func_expr { e } + +func_expr: +| e = cons_expr { e } +| pf = symbol; LPAR; ts = separated_nonempty_list(COMMA?, ray); RPAR + { to_func (pf, ts) } +| pf = symbol { to_func (pf, []) } + +cons_expr: +| r1 = ray; CONS; r2 = ray { to_func ((Null, ":"), [r1; r2]) } +| LPAR; e = cons_expr; RPAR; CONS; r = ray + { to_func ((Null, ":"), [e; r]) } diff --git a/src/prettyprinter.ml b/src/lsc/pretty.ml similarity index 100% rename from src/prettyprinter.ml rename to src/lsc/pretty.ml diff --git a/src/unification.ml b/src/lsc/unification.ml similarity index 100% rename from src/unification.ml rename to src/lsc/unification.ml diff --git a/src/stellogen/ast.ml b/src/stellogen/ast.ml new file mode 100644 index 0000000..4a98b9b --- /dev/null +++ b/src/stellogen/ast.ml @@ -0,0 +1,20 @@ +open Base +open Lsc.Ast + +type ident = string + +type stellar_expr = + | Raw of constellation + | Id of ident + | Int of constellation + +type command = + | PrintStellar of stellar_expr + | PrintMessage of string + +type declaration = + | Def of ident * constellation + | Expr of stellar_expr + | Command of command + +type program = declaration list diff --git a/src/stellogen/dune b/src/stellogen/dune new file mode 100644 index 0000000..0ade706 --- /dev/null +++ b/src/stellogen/dune @@ -0,0 +1,9 @@ +(library + (name stellogen) + (libraries base lsc)) +(env + (dev + (flags (:standard -warn-error -A)))) +(menhir (modules parser) + (flags --explain --dump)) +(ocamllex lexer) diff --git a/src/stellogen/lexer.mll b/src/stellogen/lexer.mll new file mode 100644 index 0000000..88af410 --- /dev/null +++ b/src/stellogen/lexer.mll @@ -0,0 +1,29 @@ +{ + open Parser +} + +let ident = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? +let space = [' ' '\t']+ +let newline = '\r' | '\n' | "\r\n" + +rule read = parse + | ident { ID (Lexing.lexeme lexbuf) } + | '\'' { comment lexbuf } + | "'''" { comments lexbuf } + | '{' { LBRACE } + | '}' { RBRACE } + | "print" { PRINT } + | "int" { INT } + | "def" { DEF } + | "end" { END } + | space { read lexbuf } + | newline { read lexbuf } + | eof { EOF } + +and comment = parse + | (newline|eof) { read lexbuf } + | _ { comment lexbuf } + +and comments = parse + | "'''" { read lexbuf } + | _ { comments lexbuf } diff --git a/src/stellogen/parser.mly b/src/stellogen/parser.mly new file mode 100644 index 0000000..e869fe2 --- /dev/null +++ b/src/stellogen/parser.mly @@ -0,0 +1,27 @@ +%{ +open Ast +%} + +%token LBRACE RBRACE +%token ID +%token PRINT +%token INT +%token DEF END +%token EOF + +%start program + +%% + +program: +| EOF { [] } +| ds=nonempty_list(declaration); EOF { ds } + +declaration: +| DEF; x=ID; END { Def (x, []) } +| e=stellar_expr { Expr e } + +stellar_expr: +| LBRACE; RBRACE { Raw [] } +| x=ID { Id x } +| INT { Int [] } diff --git a/test/dune b/test/dune index 90e5a8f..7510f13 100644 --- a/test/dune +++ b/test/dune @@ -7,7 +7,7 @@ ../examples/mll/cut.stellar ../examples/mll/correctness.stellar ) - (libraries alcotest base lsclib)) + (libraries alcotest base lsc)) (env (dev (flags (:standard -warn-error -A)))) diff --git a/test/test.ml b/test/test.ml index 6d4f1b1..e13efd1 100644 --- a/test/test.ml +++ b/test/test.ml @@ -1,11 +1,12 @@ open Alcotest open Base -open Lsclib.Stellar -open Lsclib.Parser +open Lsc.Ast +open Lsc.Parser +open Lsc.Lexer let test filename expected () = let lexbuf = Lexing.from_channel (Stdlib.open_in filename) in - let mcs = marked_constellation Lsclib.Lexer.read lexbuf in + let mcs = marked_constellation read lexbuf in let cs = extract_intspace mcs in let result = exec ~unfincomp:false diff --git a/lsc.opam b/tsyntax.opam similarity index 100% rename from lsc.opam rename to tsyntax.opam From b04334092e0e77458ab76ce19b4ef471dbfae22d Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 15 Aug 2024 00:47:38 +0200 Subject: [PATCH 2/4] Reorganise files and implement sgen interpreter --- bin/ilsc.ml | 10 ++-- bin/lscrun.ml | 8 ++-- bin/sgen.ml | 10 ++-- examples/stellogen/test.sg | 9 ++++ src/common_tokens.mly | 3 ++ src/lsc/common_tokens.mly | 1 + src/lsc/dune | 5 +- src/lsc/{ast.ml => lsc_ast.ml} | 4 ++ src/lsc/{lexer.mll => lsc_lexer.mll} | 2 +- src/lsc/{parser.mly => lsc_parser.mly} | 11 +++-- src/parser.mly | 52 --------------------- src/stellogen/ast.ml | 20 -------- src/stellogen/common_tokens.mly | 1 + src/stellogen/dune | 5 +- src/stellogen/lexer.mll | 29 ------------ src/stellogen/lsc_ast.ml | 1 + src/stellogen/lsc_parser.mly | 1 + src/stellogen/parser.mly | 28 +---------- src/stellogen/pretty.ml | 1 + src/stellogen/sgen_ast.ml | 55 ++++++++++++++++++++++ src/stellogen/sgen_lexer.mll | 65 ++++++++++++++++++++++++++ src/stellogen/sgen_parser.mly | 39 ++++++++++++++++ src/stellogen/unification.ml | 1 + test/test.ml | 8 ++-- 24 files changed, 212 insertions(+), 157 deletions(-) create mode 100644 examples/stellogen/test.sg create mode 100644 src/common_tokens.mly create mode 120000 src/lsc/common_tokens.mly rename src/lsc/{ast.ml => lsc_ast.ml} (96%) rename src/lsc/{lexer.mll => lsc_lexer.mll} (94%) rename src/lsc/{parser.mly => lsc_parser.mly} (81%) delete mode 100644 src/parser.mly delete mode 100644 src/stellogen/ast.ml create mode 120000 src/stellogen/common_tokens.mly delete mode 100644 src/stellogen/lexer.mll create mode 120000 src/stellogen/lsc_ast.ml create mode 120000 src/stellogen/lsc_parser.mly mode change 100644 => 120000 src/stellogen/parser.mly create mode 120000 src/stellogen/pretty.ml create mode 100644 src/stellogen/sgen_ast.ml create mode 100644 src/stellogen/sgen_lexer.mll create mode 100644 src/stellogen/sgen_parser.mly create mode 120000 src/stellogen/unification.ml diff --git a/bin/ilsc.ml b/bin/ilsc.ml index d8ea7e8..a86149a 100644 --- a/bin/ilsc.ml +++ b/bin/ilsc.ml @@ -1,7 +1,7 @@ open Base -open Lsc.Ast -open Lsc.Parser -open Lsc.Lexer +open Lsc.Lsc_ast +open Lsc.Lsc_parser +open Lsc.Lsc_lexer let welcome () = Stdlib.print_string "Commands :--------------------------------------\n"; @@ -26,10 +26,6 @@ let rec delete cs = Stdlib.print_string "This is not a positive integer. Please retry.\n"; delete cs -let unmark = function - | Marked s -> s - | Unmarked s -> s - let rec add cs = let input = prompt "Add stars" in try diff --git a/bin/lscrun.ml b/bin/lscrun.ml index 8fa1520..0ea6045 100644 --- a/bin/lscrun.ml +++ b/bin/lscrun.ml @@ -1,7 +1,7 @@ open Base -open Lsc.Ast -open Lsc.Parser -open Lsc.Lexer +open Lsc.Lsc_ast +open Lsc.Lsc_parser +open Lsc.Lsc_lexer open Out_channel let usage_msg = "exec [-no-trivial-eq] [-allow-unfinished-computation] [-show-steps] [-show-trace] [-allow-self-interaction] " @@ -38,7 +38,7 @@ let speclist = let _ = Stdlib.Arg.parse speclist anon_fun usage_msg; let lexbuf = Lexing.from_channel (Stdlib.open_in !input_file) in - let mcs = marked_constellation read lexbuf in + let mcs = constellation_file read lexbuf in let cs = extract_intspace mcs in (if !showsteps then output_string stdout "Press any key to move to the next step.\n"); diff --git a/bin/sgen.ml b/bin/sgen.ml index 119a3a2..b8f1585 100644 --- a/bin/sgen.ml +++ b/bin/sgen.ml @@ -1,7 +1,7 @@ open Base -(* open Stellogen.Ast *) -open Stellogen.Parser -open Stellogen.Lexer +open Stellogen.Sgen_ast +open Stellogen.Sgen_parser +open Stellogen.Sgen_lexer let usage_msg = "sgen " let input_file = ref "" @@ -13,5 +13,5 @@ let speclist = [] let _ = Stdlib.Arg.parse speclist anon_fun usage_msg; let lexbuf = Lexing.from_channel (Stdlib.open_in !input_file) in - let prog = program read lexbuf in - () + let p = program read lexbuf in + eval_program p diff --git a/examples/stellogen/test.sg b/examples/stellogen/test.sg new file mode 100644 index 0000000..68ebe53 --- /dev/null +++ b/examples/stellogen/test.sg @@ -0,0 +1,9 @@ +'''' +Example of Stellogen program +'''' + +print "Welcome" +print { []; } +print + a; b; c; +end diff --git a/src/common_tokens.mly b/src/common_tokens.mly new file mode 100644 index 0000000..d5aef5b --- /dev/null +++ b/src/common_tokens.mly @@ -0,0 +1,3 @@ +%token EOF + +%% diff --git a/src/lsc/common_tokens.mly b/src/lsc/common_tokens.mly new file mode 120000 index 0000000..038bfc2 --- /dev/null +++ b/src/lsc/common_tokens.mly @@ -0,0 +1 @@ +../common_tokens.mly \ No newline at end of file diff --git a/src/lsc/dune b/src/lsc/dune index 5d0e4b4..6b61386 100644 --- a/src/lsc/dune +++ b/src/lsc/dune @@ -4,6 +4,7 @@ (env (dev (flags (:standard -warn-error -A)))) -(menhir (modules parser) +(menhir (modules common_tokens lsc_parser) + (merge_into lsc_parser) (flags --explain --dump)) -(ocamllex lexer) +(ocamllex lsc_lexer) diff --git a/src/lsc/ast.ml b/src/lsc/lsc_ast.ml similarity index 96% rename from src/lsc/ast.ml rename to src/lsc/lsc_ast.ml index ac11046..5c9d2ef 100644 --- a/src/lsc/ast.ml +++ b/src/lsc/lsc_ast.ml @@ -111,6 +111,10 @@ let string_of_constellation cs = type marked_star = Marked of star | Unmarked of star type marked_constellation = marked_star list +let unmark = function + | Marked s -> s + | Unmarked s -> s + let extract_intspace (mcs : marked_constellation) = let rec aux (cs, space) = function | [] -> (List.rev cs, List.rev space) diff --git a/src/lsc/lexer.mll b/src/lsc/lsc_lexer.mll similarity index 94% rename from src/lsc/lexer.mll rename to src/lsc/lsc_lexer.mll index 2a41900..6ae8cbc 100644 --- a/src/lsc/lexer.mll +++ b/src/lsc/lsc_lexer.mll @@ -1,5 +1,5 @@ { - open Parser + open Lsc_parser } let var_id = ['A'-'Z'] ['A'-'Z' '0'-'9' '_' '-']* '\''* diff --git a/src/lsc/parser.mly b/src/lsc/lsc_parser.mly similarity index 81% rename from src/lsc/parser.mly rename to src/lsc/lsc_parser.mly index df46b18..98bd895 100644 --- a/src/lsc/parser.mly +++ b/src/lsc/lsc_parser.mly @@ -1,5 +1,5 @@ %{ -open Ast +open Lsc_ast %} %token COMMA @@ -13,17 +13,20 @@ open Ast %token SEMICOLON %token PLACEHOLDER %token EMPTY_SYM -%token EOF %right CONS +%start constellation_file %start marked_constellation %% -%public marked_constellation: +constellation_file: | EOF { [] } -| cs = nonempty_list(star); EOF { cs } +| cs = marked_constellation; EOF { cs } + +marked_constellation: +| cs = nonempty_list(star) { cs } star: | AT; s = star_content; SEMICOLON { Marked s } diff --git a/src/parser.mly b/src/parser.mly deleted file mode 100644 index 2c2702c..0000000 --- a/src/parser.mly +++ /dev/null @@ -1,52 +0,0 @@ -%token COMMA -%token LBRACK RBRACK -%token LPAR RPAR -%token VAR -%token SYM -%token PLUS MINUS -%token CONS -%token AT -%token SEMICOLON -%token PLACEHOLDER -%token EMPTY_SYM -%token EOF - -%right CONS - -%start marked_constellation - -%% - -marked_constellation: -| EOF { [] } -| cs = nonempty_list(star); EOF { cs } - -star: -| AT; s = star_content; SEMICOLON { Stellar.Marked s } -| s = star_content; SEMICOLON { Stellar.Unmarked s } - -star_content: -| LBRACK; RBRACK { [] } -| rs = separated_nonempty_list(COMMA?, ray) { rs } - -symbol: -| PLUS; f = SYM { (Pos, f) } -| MINUS; f = SYM { (Neg, f) } -| f = SYM { (Stellar.Null, f) } - -ray: -| EMPTY_SYM { Stellar.to_func ((Stellar.Null, "$"), []) } -| PLACEHOLDER { Stellar.to_var ("_"^(Stellar.fresh_placeholder ())) } -| x = VAR { Stellar.to_var x } -| e = func_expr { e } - -func_expr: -| e = cons_expr { e } -| pf = symbol; LPAR; ts = separated_nonempty_list(COMMA?, ray); RPAR - { Stellar.to_func (pf, ts) } -| pf = symbol { Stellar.to_func (pf, []) } - -cons_expr: -| r1 = ray; CONS; r2 = ray { Stellar.to_func ((Stellar.Null, ":"), [r1; r2]) } -| LPAR; e = cons_expr; RPAR; CONS; r = ray - { Stellar.to_func ((Stellar.Null, ":"), [e; r]) } diff --git a/src/stellogen/ast.ml b/src/stellogen/ast.ml deleted file mode 100644 index 4a98b9b..0000000 --- a/src/stellogen/ast.ml +++ /dev/null @@ -1,20 +0,0 @@ -open Base -open Lsc.Ast - -type ident = string - -type stellar_expr = - | Raw of constellation - | Id of ident - | Int of constellation - -type command = - | PrintStellar of stellar_expr - | PrintMessage of string - -type declaration = - | Def of ident * constellation - | Expr of stellar_expr - | Command of command - -type program = declaration list diff --git a/src/stellogen/common_tokens.mly b/src/stellogen/common_tokens.mly new file mode 120000 index 0000000..038bfc2 --- /dev/null +++ b/src/stellogen/common_tokens.mly @@ -0,0 +1 @@ +../common_tokens.mly \ No newline at end of file diff --git a/src/stellogen/dune b/src/stellogen/dune index 0ade706..736bd82 100644 --- a/src/stellogen/dune +++ b/src/stellogen/dune @@ -4,6 +4,7 @@ (env (dev (flags (:standard -warn-error -A)))) -(menhir (modules parser) +(menhir (modules common_tokens lsc_parser sgen_parser) + (merge_into sgen_parser) (flags --explain --dump)) -(ocamllex lexer) +(ocamllex sgen_lexer) diff --git a/src/stellogen/lexer.mll b/src/stellogen/lexer.mll deleted file mode 100644 index 88af410..0000000 --- a/src/stellogen/lexer.mll +++ /dev/null @@ -1,29 +0,0 @@ -{ - open Parser -} - -let ident = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? -let space = [' ' '\t']+ -let newline = '\r' | '\n' | "\r\n" - -rule read = parse - | ident { ID (Lexing.lexeme lexbuf) } - | '\'' { comment lexbuf } - | "'''" { comments lexbuf } - | '{' { LBRACE } - | '}' { RBRACE } - | "print" { PRINT } - | "int" { INT } - | "def" { DEF } - | "end" { END } - | space { read lexbuf } - | newline { read lexbuf } - | eof { EOF } - -and comment = parse - | (newline|eof) { read lexbuf } - | _ { comment lexbuf } - -and comments = parse - | "'''" { read lexbuf } - | _ { comments lexbuf } diff --git a/src/stellogen/lsc_ast.ml b/src/stellogen/lsc_ast.ml new file mode 120000 index 0000000..6c30619 --- /dev/null +++ b/src/stellogen/lsc_ast.ml @@ -0,0 +1 @@ +../lsc/lsc_ast.ml \ No newline at end of file diff --git a/src/stellogen/lsc_parser.mly b/src/stellogen/lsc_parser.mly new file mode 120000 index 0000000..ea060e8 --- /dev/null +++ b/src/stellogen/lsc_parser.mly @@ -0,0 +1 @@ +../lsc/lsc_parser.mly \ No newline at end of file diff --git a/src/stellogen/parser.mly b/src/stellogen/parser.mly deleted file mode 100644 index e869fe2..0000000 --- a/src/stellogen/parser.mly +++ /dev/null @@ -1,27 +0,0 @@ -%{ -open Ast -%} - -%token LBRACE RBRACE -%token ID -%token PRINT -%token INT -%token DEF END -%token EOF - -%start program - -%% - -program: -| EOF { [] } -| ds=nonempty_list(declaration); EOF { ds } - -declaration: -| DEF; x=ID; END { Def (x, []) } -| e=stellar_expr { Expr e } - -stellar_expr: -| LBRACE; RBRACE { Raw [] } -| x=ID { Id x } -| INT { Int [] } diff --git a/src/stellogen/parser.mly b/src/stellogen/parser.mly new file mode 120000 index 0000000..4d85639 --- /dev/null +++ b/src/stellogen/parser.mly @@ -0,0 +1 @@ +../lsc/parser.mly \ No newline at end of file diff --git a/src/stellogen/pretty.ml b/src/stellogen/pretty.ml new file mode 120000 index 0000000..80937fc --- /dev/null +++ b/src/stellogen/pretty.ml @@ -0,0 +1 @@ +../lsc/pretty.ml \ No newline at end of file diff --git a/src/stellogen/sgen_ast.ml b/src/stellogen/sgen_ast.ml new file mode 100644 index 0000000..c60f4fd --- /dev/null +++ b/src/stellogen/sgen_ast.ml @@ -0,0 +1,55 @@ +open Base +open Lsc_ast + +type ident = string + +type stellar_expr = + | Raw of marked_constellation + | Id of ident + | Int of stellar_expr * stellar_expr + +type env = (ident * stellar_expr) list + +type command = + | PrintStellar of stellar_expr + | PrintMessage of string + +type declaration = + | Def of ident * stellar_expr + | Command of command + +type program = declaration list + +let rec eval_stellar_expr (env : env) + : stellar_expr -> marked_constellation = function + | Raw mcs -> mcs + | Id x -> + List.Assoc.find_exn ~equal:equal_string env x + |> eval_stellar_expr env + | Int (e, e') -> + let mcs = eval_stellar_expr env e in + let mcs' = eval_stellar_expr env e' in + let cs = extract_intspace (mcs@mcs') in + exec ~unfincomp:false ~withloops:false ~showtrace:false + ~selfint:false ~showsteps:false cs + |> List.map ~f:(fun x -> Unmarked x) + +let eval_command env = function + | PrintStellar e -> + eval_stellar_expr env e + |> List.map ~f:unmark + |> string_of_constellation + |> Stdlib.print_string; + Stdlib.print_newline (); + env + | PrintMessage m -> + Stdlib.print_string m; + Stdlib.print_newline (); + env + +let eval_decl env : declaration -> env = function + | Def (x, e) -> List.Assoc.add ~equal:equal_string env x e + | Command c -> eval_command env c + +let eval_program p = + List.fold_left ~f:(fun acc x -> eval_decl acc x) ~init:[] p diff --git a/src/stellogen/sgen_lexer.mll b/src/stellogen/sgen_lexer.mll new file mode 100644 index 0000000..7068bdf --- /dev/null +++ b/src/stellogen/sgen_lexer.mll @@ -0,0 +1,65 @@ +{ + open Sgen_parser + exception SyntaxError of string +} + +let func_id = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? +let ident = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? +let space = [' ' '\t']+ +let newline = '\r' | '\n' | "\r\n" + +rule read = parse + (* Stellogen *) + | '{' { LBRACE } + | '}' { RBRACE } + | "def" { DEF } + | "end" { END } + | "int" { INT } + | "print" { PRINT } + | '"' { read_string (Buffer.create 255) lexbuf } + (* Stellar resolution *) + | '_' { PLACEHOLDER } + | '[' { LBRACK } + | ']' { RBRACK } + | '(' { LPAR } + | ')' { RPAR } + | ',' { COMMA } + | '@' { AT } + | '+' { PLUS } + | '-' { MINUS } + | '$' { EMPTY_SYM } + | ':' { CONS } + | ';' { SEMICOLON } + | func_id { SYM (Lexing.lexeme lexbuf) } + (* Common *) + | '\'' { comment lexbuf } + | "'''" { comments lexbuf } + | ident { ID (Lexing.lexeme lexbuf) } + | space { read lexbuf } + | newline { read lexbuf } + | eof { EOF } + +and read_string buf = + parse + | '"' { STRING (Buffer.contents buf) } + | '\\' '/' { Buffer.add_char buf '/'; read_string buf lexbuf } + | '\\' '\\' { Buffer.add_char buf '\\'; read_string buf lexbuf } + | '\\' 'b' { Buffer.add_char buf '\b'; read_string buf lexbuf } + | '\\' 'f' { Buffer.add_char buf '\012'; read_string buf lexbuf } + | '\\' 'n' { Buffer.add_char buf '\n'; read_string buf lexbuf } + | '\\' 'r' { Buffer.add_char buf '\r'; read_string buf lexbuf } + | '\\' 't' { Buffer.add_char buf '\t'; read_string buf lexbuf } + | [^ '"' '\\']+ + { Buffer.add_string buf (Lexing.lexeme lexbuf); + read_string buf lexbuf + } + | _ { raise (SyntaxError ("Illegal string character: " ^ Lexing.lexeme lexbuf)) } + | eof { raise (SyntaxError ("String is not terminated")) } + +and comment = parse + | (newline|eof) { read lexbuf } + | _ { comment lexbuf } + +and comments = parse + | "'''" { read lexbuf } + | _ { comments lexbuf } diff --git a/src/stellogen/sgen_parser.mly b/src/stellogen/sgen_parser.mly new file mode 100644 index 0000000..f6225b6 --- /dev/null +++ b/src/stellogen/sgen_parser.mly @@ -0,0 +1,39 @@ +%{ +open Sgen_ast +%} + +%token LBRACE RBRACE +%token ID +%token STRING +%token PRINT +%token INT +%token DEF END + +%start program + +%% + +program: +| EOF { [] } +| ds=nonempty_list(declaration); EOF { ds } + +declaration: +| DEF; x=ID; e=stellar_expr; END { Def (x, e) } +| DEF; x=ID; cs=marked_constellation; END { Def (x, Raw cs) } +| c=command { Command c } + +command: +| PRINT; e=stellar_expr { PrintStellar e } +| PRINT; cs=marked_constellation; END { PrintStellar (Raw cs) } +| PRINT; s=STRING { PrintMessage s } + +stellar_expr: +| LBRACE; RBRACE + { Raw [] } +| LBRACE; cs=marked_constellation; RBRACE + { Raw cs } +| x=ID + { Id x } +| INT; e1=stellar_expr; e2=stellar_expr + { Int (e1, e2) } + diff --git a/src/stellogen/unification.ml b/src/stellogen/unification.ml new file mode 120000 index 0000000..1d705c1 --- /dev/null +++ b/src/stellogen/unification.ml @@ -0,0 +1 @@ +../lsc/unification.ml \ No newline at end of file diff --git a/test/test.ml b/test/test.ml index e13efd1..4af505e 100644 --- a/test/test.ml +++ b/test/test.ml @@ -1,12 +1,12 @@ open Alcotest open Base -open Lsc.Ast -open Lsc.Parser -open Lsc.Lexer +open Lsc.Lsc_ast +open Lsc.Lsc_parser +open Lsc.Lsc_lexer let test filename expected () = let lexbuf = Lexing.from_channel (Stdlib.open_in filename) in - let mcs = marked_constellation read lexbuf in + let mcs = constellation_file read lexbuf in let cs = extract_intspace mcs in let result = exec ~unfincomp:false From 810388248c1b232dc7d6ed9ab4fa0e99c2dc17f0 Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 15 Aug 2024 17:00:58 +0200 Subject: [PATCH 3/4] Implement union and execution with stellogen program example --- examples/stellogen/syntax.sg | 28 ++++++++++++++++++++++++++++ examples/stellogen/test.sg | 9 --------- src/lsc/lsc_parser.mly | 2 +- src/stellogen/sgen_ast.ml | 18 +++++++++++++----- src/stellogen/sgen_lexer.mll | 17 ++++++++++++----- src/stellogen/sgen_parser.mly | 27 ++++++++++++++++----------- 6 files changed, 70 insertions(+), 31 deletions(-) create mode 100644 examples/stellogen/syntax.sg delete mode 100644 examples/stellogen/test.sg diff --git a/examples/stellogen/syntax.sg b/examples/stellogen/syntax.sg new file mode 100644 index 0000000..77ef4cb --- /dev/null +++ b/examples/stellogen/syntax.sg @@ -0,0 +1,28 @@ +'''' +Syntax of Stellogen programs +'''' + +'print text +print "Welcome" + +'definition of constellation +def x + +a; -a b; +end +def y x + +'union +def union_x_y + x@y +end + +'execution +def exec_x + exec x +end + +'print contellations +print { a; b; c; } +print a; b; c; end +print (x @ x) +print (exec x) diff --git a/examples/stellogen/test.sg b/examples/stellogen/test.sg deleted file mode 100644 index 68ebe53..0000000 --- a/examples/stellogen/test.sg +++ /dev/null @@ -1,9 +0,0 @@ -'''' -Example of Stellogen program -'''' - -print "Welcome" -print { []; } -print - a; b; c; -end diff --git a/src/lsc/lsc_parser.mly b/src/lsc/lsc_parser.mly index 98bd895..d64bb3d 100644 --- a/src/lsc/lsc_parser.mly +++ b/src/lsc/lsc_parser.mly @@ -26,7 +26,7 @@ constellation_file: | cs = marked_constellation; EOF { cs } marked_constellation: -| cs = nonempty_list(star) { cs } +| cs = star+ { cs } star: | AT; s = star_content; SEMICOLON { Marked s } diff --git a/src/stellogen/sgen_ast.ml b/src/stellogen/sgen_ast.ml index c60f4fd..363efc6 100644 --- a/src/stellogen/sgen_ast.ml +++ b/src/stellogen/sgen_ast.ml @@ -6,7 +6,8 @@ type ident = string type stellar_expr = | Raw of marked_constellation | Id of ident - | Int of stellar_expr * stellar_expr + | Exec of stellar_expr + | Union of stellar_expr * stellar_expr type env = (ident * stellar_expr) list @@ -24,12 +25,19 @@ let rec eval_stellar_expr (env : env) : stellar_expr -> marked_constellation = function | Raw mcs -> mcs | Id x -> - List.Assoc.find_exn ~equal:equal_string env x - |> eval_stellar_expr env - | Int (e, e') -> + begin try + List.Assoc.find_exn ~equal:equal_string env x + |> eval_stellar_expr env + with Sexplib0__Sexp.Not_found_s _ -> + failwith ("Error: undefined identifier " ^ x ^ "."); + end + | Union (e, e') -> let mcs = eval_stellar_expr env e in let mcs' = eval_stellar_expr env e' in - let cs = extract_intspace (mcs@mcs') in + mcs@mcs' + | Exec e -> + let mcs = eval_stellar_expr env e in + let cs = extract_intspace mcs in exec ~unfincomp:false ~withloops:false ~showtrace:false ~selfint:false ~showsteps:false cs |> List.map ~f:(fun x -> Unmarked x) diff --git a/src/stellogen/sgen_lexer.mll b/src/stellogen/sgen_lexer.mll index 7068bdf..2402b99 100644 --- a/src/stellogen/sgen_lexer.mll +++ b/src/stellogen/sgen_lexer.mll @@ -3,7 +3,6 @@ exception SyntaxError of string } -let func_id = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? let ident = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? let space = [' ' '\t']+ let newline = '\r' | '\n' | "\r\n" @@ -14,7 +13,7 @@ rule read = parse | '}' { RBRACE } | "def" { DEF } | "end" { END } - | "int" { INT } + | "exec" { EXEC } | "print" { PRINT } | '"' { read_string (Buffer.create 255) lexbuf } (* Stellar resolution *) @@ -30,14 +29,19 @@ rule read = parse | '$' { EMPTY_SYM } | ':' { CONS } | ';' { SEMICOLON } - | func_id { SYM (Lexing.lexeme lexbuf) } + | ident { SYM (Lexing.lexeme lexbuf) } (* Common *) | '\'' { comment lexbuf } | "'''" { comments lexbuf } - | ident { ID (Lexing.lexeme lexbuf) } | space { read lexbuf } | newline { read lexbuf } | eof { EOF } + | _ { + raise (SyntaxError + ("Unexpected character '" ^ + (Lexing.lexeme lexbuf) ^ + "' during lexing")) + } and read_string buf = parse @@ -53,7 +57,10 @@ and read_string buf = { Buffer.add_string buf (Lexing.lexeme lexbuf); read_string buf lexbuf } - | _ { raise (SyntaxError ("Illegal string character: " ^ Lexing.lexeme lexbuf)) } + | _ { + raise (SyntaxError + ("Illegal string character: " ^ Lexing.lexeme lexbuf)) + } | eof { raise (SyntaxError ("String is not terminated")) } and comment = parse diff --git a/src/stellogen/sgen_parser.mly b/src/stellogen/sgen_parser.mly index f6225b6..ddefcf9 100644 --- a/src/stellogen/sgen_parser.mly +++ b/src/stellogen/sgen_parser.mly @@ -3,37 +3,42 @@ open Sgen_ast %} %token LBRACE RBRACE -%token ID -%token STRING +%token STRING %token PRINT -%token INT +%token EXEC %token DEF END +%right PLUS + %start program %% program: | EOF { [] } -| ds=nonempty_list(declaration); EOF { ds } +| ds=declaration+; EOF { ds } declaration: -| DEF; x=ID; e=stellar_expr; END { Def (x, e) } -| DEF; x=ID; cs=marked_constellation; END { Def (x, Raw cs) } +| DEF; x=SYM; e=stellar_expr; END? { Def (x, e) } +| DEF; x=SYM; cs=marked_constellation; END { Def (x, Raw cs) } | c=command { Command c } command: -| PRINT; e=stellar_expr { PrintStellar e } +| PRINT; e=stellar_expr; END? { PrintStellar e } | PRINT; cs=marked_constellation; END { PrintStellar (Raw cs) } -| PRINT; s=STRING { PrintMessage s } +| PRINT; s=STRING; END? { PrintMessage s } stellar_expr: +| LPAR; e=stellar_expr; RPAR + { e } | LBRACE; RBRACE { Raw [] } | LBRACE; cs=marked_constellation; RBRACE { Raw cs } -| x=ID +| x=SYM { Id x } -| INT; e1=stellar_expr; e2=stellar_expr - { Int (e1, e2) } +| EXEC; e=stellar_expr + { Exec e } +| e1=stellar_expr; AT; e2=stellar_expr + { Union (e1, e2) } From f8c22383beaca782504fdf4a49779de848c5c888 Mon Sep 17 00:00:00 2001 From: engboris Date: Thu, 15 Aug 2024 17:26:23 +0200 Subject: [PATCH 4/4] Update README --- README.md | 50 +++++++++++++++++++++++++++++++++++++++++--------- dune-project | 8 ++++---- tsyntax.opam | 12 ++++++------ 3 files changed, 51 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 7edf239..779a027 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,18 @@ -# Context: stellar resolution +# Transcendental Syntax + +The transcendental syntax is a method of constructing logical abstractions from +a low-level elementary and "logic-agnostic" language. + +This elementary language we use to build abstractions is called +"stellar resolution" and its elementary objects corresponding to programs are +called "constellations". + +Those constellations are used in a higher-level language called "Stellogen" in +which notions such as proofs and formulas are defined (this is basically a +metaprogramming language for constellations). By the proof-as-program +correspondence, this can be extended to programs and types. + +## Stellar resolution The stellar resolution (RS) is a model of computation introduced by Jean-Yves Girard [1] in his transcendental syntax project as a basis for the study of the @@ -20,14 +34,13 @@ tiles used in DNA computing; Stellar resolution is very elementary and an interpreter for it can be written in a very concise way since it mostly relies on a unification algorithm. -# Large Star Collider +## Learn -The Large Star Collider (LSC) is an implementation of stellar resolution that -interprets and executes objects called *constellations*, which are the programs -of stellar resolution. +This project is still in development, hence the syntax and features are still +changing. Go to https://tsguide.refl.fr/ (guide currently in French only) to learn more -about how to write programs. +about how to play with the current implementation of transcendental syntax. # Use @@ -57,7 +70,11 @@ Executables are in `_build/default/bin/`. ## Commands -### Constellation collider +The project provides three programs. + +### Large Star Collider (LSC) + +This program is an interpreter for stellar resolution. Assume the executable is named `lsc.exe`. Execute the program with: @@ -89,11 +106,26 @@ dune exec ilsc The instructions are provided in the program. +### Stellogen interpreter + +Assume the executable is named `sgen.exe`. Interpreter Stellogen programs with: + +``` +./sgen.exe +``` + +or if you use Dune: + +``` +dune exec sgen -- +``` + # Examples Some example files with the `.stellar` extension in `/examples` are ready to be -executed. In Eng's thesis, ways to work with other models of computation are described -(Turing machines, pushdown automata, transducers, alternating automata etc). +executed. In Eng's thesis, ways to work with other models of computation are +described (Turing machines, pushdown automata, transducers, alternating +automata etc). # References diff --git a/dune-project b/dune-project index 88b67ac..fe2a7d8 100644 --- a/dune-project +++ b/dune-project @@ -5,7 +5,7 @@ (generate_opam_files true) (source - (github engboris/large-star-collider)) + (github engboris/transcendental-syntax)) (authors "Boris Eng") @@ -13,12 +13,12 @@ (license GPL-3.0-only) -(documentation https://github.com/engboris/large-star-collider/blob/main/README.md) +(documentation https://github.com/engboris/transcendental-syntax/blob/main/README.md) (package (name tsyntax) - (synopsis "Stellar resolution implemented with interactive execution") - (description "The Large Star Collider (LSC) is an implementation of stellar resolution which interprets and executes objects called constellations, which are the programs of stellar resolution.") + (synopsis "Technical interpretation of Girard's transcendental syntax") + (description "The transcendental syntax provides a low-level language called stellar resolution used to build higher-level abstractions defining types, formulas, proofs and any other logical concepts.") (depends base menhir) (tags ("transcendental syntax" "logic programming" "constraint programming" "resolution logic" "unification" "self-assembly"))) diff --git a/tsyntax.opam b/tsyntax.opam index b11c599..c3cdec9 100644 --- a/tsyntax.opam +++ b/tsyntax.opam @@ -1,8 +1,8 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -synopsis: "Stellar resolution implemented with interactive execution" +synopsis: "Technical interpretation of Girard's transcendental syntax" description: - "The Large Star Collider (LSC) is an implementation of stellar resolution which interprets and executes objects called constellations, which are the programs of stellar resolution." + "The transcendental syntax provides a low-level language called stellar resolution used to build higher-level abstractions defining types, formulas, proofs and any other logical concepts." maintainer: ["Pablo Donato"] authors: ["Boris Eng"] license: "GPL-3.0-only" @@ -14,9 +14,9 @@ tags: [ "unification" "self-assembly" ] -homepage: "https://github.com/engboris/large-star-collider" -doc: "https://github.com/engboris/large-star-collider/blob/main/README.md" -bug-reports: "https://github.com/engboris/large-star-collider/issues" +homepage: "https://github.com/engboris/transcendental-syntax" +doc: "https://github.com/engboris/transcendental-syntax/blob/main/README.md" +bug-reports: "https://github.com/engboris/transcendental-syntax/issues" depends: [ "dune" {>= "3.7"} "base" @@ -37,4 +37,4 @@ build: [ "@doc" {with-doc} ] ] -dev-repo: "git+https://github.com/engboris/large-star-collider.git" +dev-repo: "git+https://github.com/engboris/transcendental-syntax.git"