Merge pull request #3 from engboris/engboris-metaprog

[WIP] Prototype of metaprogramming language for constellations

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 -- <inputfile>
+```
+
 # 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
 

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))))

bin/ilsc.ml

@@ -1,6 +1,7 @@
 open Base
-open Lsclib.Stellar
-open Lsclib.Parser
+open Lsc.Lsc_ast
+open Lsc.Lsc_parser
+open Lsc.Lsc_lexer
 
 let welcome () =
   Stdlib.print_string "Commands :--------------------------------------\n";
@@ -25,15 +26,11 @@ 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
     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 +53,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

bin/lsc.ml → bin/lscrun.ml

@@ -1,6 +1,7 @@
 open Base
-open Lsclib.Stellar
-open Lsclib.Parser
+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] <filename>"
@@ -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 = 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");

bin/sgen.ml

@@ -0,0 +1,17 @@
+open Base
+open Stellogen.Sgen_ast
+open Stellogen.Sgen_parser
+open Stellogen.Sgen_lexer
+
+let usage_msg = "sgen <filename>"
+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 p = program read lexbuf in
+  eval_program p

dune-project

@@ -1,24 +1,24 @@
 (lang dune 3.7)
 
-(name lsc)
+(name tsyntax)
 
 (generate_opam_files true)
 
 (source
- (github engboris/large-star-collider))
+ (github engboris/transcendental-syntax))
 
 (authors "Boris Eng")
 
 (maintainers "Pablo Donato")
 
 (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 lsc)
- (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.")
+ (name tsyntax)
+ (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")))

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)

src/common_tokens.mly

@@ -0,0 +1,3 @@
+%token EOF
+
+%%

src/lsc/common_tokens.mly

@@ -0,0 +1 @@
+../common_tokens.mly

src/dune → src/lsc/dune

@@ -1,9 +1,10 @@
 (library
- (name lsclib)
+ (name lsc)
  (libraries base))
 (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)

src/stellar.ml → src/lsc/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
@@ -110,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)

src/lexer.mll → src/lsc/lsc_lexer.mll

@@ -1,5 +1,5 @@
 {
-  open Parser
+  open Lsc_parser
 }
 
 let var_id   = ['A'-'Z'] ['A'-'Z' '0'-'9' '_' '-']* '\''*

src/lsc/lsc_parser.mly

@@ -0,0 +1,59 @@
+%{
+open Lsc_ast
+%}
+
+%token COMMA
+%token LBRACK RBRACK
+%token LPAR RPAR
+%token <string> VAR
+%token <string> SYM
+%token PLUS MINUS
+%token CONS
+%token AT
+%token SEMICOLON
+%token PLACEHOLDER
+%token EMPTY_SYM
+
+%right CONS
+
+%start <marked_constellation> constellation_file
+%start <marked_constellation> marked_constellation
+
+%%
+
+constellation_file:
+| EOF { [] }
+| cs = marked_constellation; EOF { cs }
+
+marked_constellation:
+| cs = star+ { 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]) }