Merge pull request #269 from LPCIC/scoped-term

New backend (elpi 2.0)

Author: gares

.github/workflows/users.yml

@@ -26,10 +26,10 @@ jobs:
           env:
             OPAMWITHTEST: false
 
-        - run: opam pin add coq-elpi https://github.com/LPCIC/coq-elpi.git#master
-        - run: opam pin add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#fix-elpi-loc
-        - run: opam pin add coq-mathcomp-ssreflect https://github.com/math-comp/math-comp.git#master
-        - run: opam pin add coq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master
-        - run: opam pin add coq-mathcomp-algebra https://github.com/math-comp/math-comp.git#master
-        - run: opam pin add coq-mathcomp-solvable https://github.com/math-comp/math-comp.git#master
-        - run: opam pin add coq-mathcomp-field https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-elpi https://github.com/LPCIC/coq-elpi.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-mathcomp-ssreflect https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-mathcomp-algebra https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-mathcomp-solvable https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi add coq-mathcomp-field https://github.com/math-comp/math-comp.git#master

CHANGES.md

@@ -3,24 +3,78 @@
 Requires Menhir 20211230 and OCaml 4.08 or above.
 
 - Compiler:
-  - New syntax: anonymous predicates can be passed to type signatures in order
-    to have more information about modes and attributes of higher-order
-    arguments, eg: `pred p i:(pred i:A, o:B)` tells that the first argument of
-    `p` is a predicate whose first argument is in input and the second in
-    output.
-  - Separated terms from types; the parser generates 
-    - `TypeExpression.t` objects for `pred` and `type` objects
-    - `TypeAbbreviation.closedTypeexpression` objects for `typeabbrev`, that is
-       the `TypeExpression.t` type decorated with the `TLam` constructor
-  - The attribute `:functional` can be passed to predicates (not types),
-    for example, `:functional pred q i:int, o:int` tells the interpreter that `q` is
-    a predicate meant to be functional. Note that, due to anonymous predicates,
-    the `:functional` attributes can be passed to higher-order arguments
-  - The piece of information likes modes and functionality is transmitted to the
-    checker (currently this information is not taken into account) 
+  - Change the pipeline completely to make unit relocation unnecessary. Current
+    phases are (roughly):
+    1. `Ast.program` —[`RecoverStructure`]—> `Ast.Structured.program`
+    2. `Ast.Structured.program` —[`Scope`,`Quotation`,`Macro`]—> `Scoped.program` (aka `API.Compile.scoped_program`)
+    3. `Scoped.program` —[`Flatten`]—> `Flat.program`
+    4. `Flat.program` —[`Check`]—> `CheckedFlat.program` (aka `API.Compile.compilation_unit`)
+    5. `CheckedFlat.program` —[`Spill`,`ToDbl`]—> `Assembled.program`
+
+    Steps 4 and 5 operate on a base, that is an `Assembled.program` being
+    extended. `ToDbl` is in charge of allocating constants (numbers) for global
+    names and takes place when the unit is assembled on the base. These
+    constants don't need to be relocated as in the previous backend that
+    would allocate these constants much earlier.
+  - Change compilation units can declare new builtin predicates
+  - Fix macros are hygienic
+  - New type checker written in OCaml. The new type checker is faster,
+    reports error messages with a precise location and performs checking
+    incrementally when the API for separate compilation is used.
+    The new type checker is a bit less permissive since the old one would
+    merged together all types declaration before type checking the entire
+    program, while the new one type checks each unit using the types declared
+    inside the unit or declared in the base it extends, but not the types
+    declared in units that (will) follow it.
+  - Remove the need of `typeabbrv string (ctype "string")` and similar
+  - New type check types and kinds (used to be ignored).
+
+- API:
+  - Change quotations generate `Ast.Term.t` and not `RawData.t`. The data
+    type `Ast.Term.t` contains locations (for locating type errors) and
+    has named (bound) variables and type annotations in `Ast.Type.t`.
+  - New `Compile.extend_signature` and `Compile.signature` to extend a
+    program with the signature (the types, not the code) of a unit
+  - New `Ast.Loc.t` carries a opaque payload defined by the host application
+  - Remove `Query`, only `RawQuery` is available (or `Compile.query`)
+
+- Parser:
+  - Remove legacy parser
+  - New `% elpi:if version op A.B.C` and `% elpi:endif` lexing directives
+  - New warning for `A => B, C` to be disabled by putting parentheses
+    around `A => B`.
+
+- Language:
+  - New infix `==>` standing for application but with "the right precedence™",
+    i.e. `A ==> B, C` means `A => (B, C)`.
+  - New `pred` is allowed in anonymous predicates, eg:
+    `pred map i:list A, i:(pred i:A, o:B), o:list B` declares that the first
+    argument of `map` is a predicate whose first argument is in input and
+    the second in output. Currently the mode checker is still in development,
+    annotations for higher order arguments are ignored.
+  - New attribute `:functional` can be passed to predicates (but not types).
+    For example, `:functional pred map i:list A, i:(:functional pred i:A, o:B), o:list B`
+    declares `map` to be a functional predicate iff its higher order argument is
+    functional. Currently the determinacy checker is still in development, these
+    annotations are ignored.
+  - New `func` keyword standing for `:functional pred`. The declaration above
+    can be shortened to `func map i:list A, i:(func i:A, o:B), o:list B`.
+  - New type annotations on variables quantified by `pi` as in `pi x : term \ ...`
+  - New type casts on terms, as in `f (x : term)`
+  - New attribute `:untyped` to skip the type checking of a rule.
+
+- Stdlib:
+  - New `std.list.init N E L` builds a list `L = [E, ..., E]` with length `N`
+  - New `std.list.make N F L` builds the list `L = [F 0, F 1, ..., F (N-1)]`
+  - New `triple` data type with constructor `triple` and projections `triple_1`...
+
 - Builtins:
-  - `std.list.init N E L` builds a list `L = [E, ..., E]` with length `N`
-  - `std.list.make N F L` builds the list `L = [F 0, F 1, ..., F (N-1)]`
+  - Remove `string_to_term`, `read`, `readterm`, `quote_syntax`
+
+- REPL:
+  - Remove `-no-tc`, `-legacy-parser`, `-legacy-parser-available`
+  - New `-document-infix-syntax`
+
 
 # v1.20.0 (September 2024)
 

ELPI.md

@@ -298,6 +298,30 @@ to `elpi`.
 
 The attribute `:if` can also be used on CHR rules.
 
+### Compatibility ifdefs
+
+It is also possible ask the lexer to discard text before it reaches the parser.
+
+```prolog
+% elpi:if version < 2.0.0
+This text is ignored if the version of Elpi old
+% elpi:endif
+```
+
+Currently the only variable available is `version` and it must be placed
+on the left of the operator (either `<` or `>` or `=`) and ifdefs cannot
+be nested. If not available (e.g. `dune subst` did not run) the version
+defaults to `99.99.99`.
+
+One can also ask the lexer to always skip some text. That can be useful if one
+wants to keep around code that is not meant for Elpi (but for example for Teyjus).
+
+```prolog
+% elpi:skip 2
+infixr ==> 120. % directive not supported by Elpi
+infixr || 120. % last line being skipped
+```
+
 ## Configurable argument indexing
 
 By default the clauses for a predicate are indexed by looking
@@ -939,8 +963,7 @@ A macro is declared with the following syntax
 ```prolog
 macro @name Args :- Body.
 ```
-It is expanded everywhere (even in type declarations)
-at compilation time. 
+It is expanded at compilation time. 
 
 #### Example: literlas
 
@@ -956,39 +979,3 @@ macro @of X N T :- (of X T, pp X N).
 of (lambda Name   F) (arr A B) :-         pi x\ @of x Name A =>            of (F x) B.
 of (let-in Name V F) R         :- of V T, pi x\ @of x Name T => val x V => of (F x) R.
 ```
-
-#### Example: optional cut.
-```prolog
-macro @neck-cut-if P Hd Hyps :- (
-  (Hd :- P,      !, Hyps),
-  (Hd :- not P,     Hyps)
-).
-
-@neck-cut-if greedy 
-(f X)  (X = 1).
- f X :- X = 2.
-```
-
-```
-goal> greedy => f X.
-Success:
-  X = 1
-goal> f X.
-Success:
-  X = 1
-More? (Y/n)
-Success:
-  X = 2 
-```
-
-### Caveat
-Currently macros are not truly "hygienic",
-that is the body of the macro is not lexically analyzed before
-expansion and its free names (of constants) may be captured.
-
-```prolog
-macro @m A :- x = A.
-main :- pi x\ @m x. % works, but should not!
-```
-
-Use with care.

Makefile

@@ -12,6 +12,8 @@ help:
 	@echo '  tests ONLY=rex         runs only tests matching rex'
 	@echo '  tests PROMOTE=true     runs and promote tests if different'
 	@echo '                           (can be combined with ONLY)'
+	@echo '  tests LN_NB=nb         sets max number of lines to print of failing tests'
+	@echo '                           (negave numbers means print all file)'
 	@echo '  tests STOP_ON_FST_ERROR=true stops the test suite after first error'
 	@echo
 	@echo '  git/treeish            checkout treeish and build elpi.git.treeish'
@@ -29,6 +31,7 @@ BUILD=_build/default
 SHELL:=/usr/bin/env bash
 TIMEOUT=90.0
 PROMOTE=false
+LN_NB=-1
 STOP_ON_FST_ERROR=false
 PWD=$(shell pwd)
 RUNNERS=\
@@ -84,6 +87,7 @@ tests:
 		tests/test.exe \
 		--seed $$RANDOM \
 		--promote $(PROMOTE) \
+		--ln_nb=$(LN_NB) \
 		--timeout $(TIMEOUT) \
 		--stop-on-first-error=$(STOP_ON_FST_ERROR) \
 		$(TIME) \

dune

@@ -1,13 +1,14 @@
 (executable
   (name elpi_REPL)
   (public_name elpi)
-  (libraries elpi)
+  (libraries elpi elpi.parser ;memtrace
+  )
   (modules elpi_REPL)
   (package elpi)
 )
 
 (env
   (dev
-    (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A)))
+    (flags (:standard -w -9 -w -32 -w -27 -warn-error -A)))
   (fatalwarnings
-    (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error +A))))
+    (flags (:standard -w -9 -w -32 -w -27 -warn-error +A))))

elpi_REPL.ml

@@ -58,60 +58,54 @@ let usage =
   "\t-exec pred  runs the query \"pred ARGS\"\n" ^ 
   "\t-D var  Define variable (conditional compilation)\n" ^ 
   "\t-document-builtins Print documentation for built-in predicates\n" ^
-  "\t-no-tc don't typecheck the program\n" ^ 
+  "\t-document-infix-syntax Print the documentation for infix operators\n" ^
   "\t-I PATH  search for accumulated files in PATH\n" ^
   "\t-delay-problems-outside-pattern-fragment (deprecated, for Teyjus\n" ^
   "\t                                          compatibility)\n" ^
-  "\t-legacy-parser enable the legacy parser (deprecated)\n"^
-  "\t-legacy-parser-available exists with 0 if it is the case\n"^
   "\t--version prints the version of Elpi (also -v or -version)\n" ^ 
   "\t--help prints this help (also -h or -help)\n" ^ 
  API.Setup.usage ^
   "\nDebug options (for debugging Elpi, not your program):\n" ^ 
   "\t-parse-term parses a term from standard input and prints it\n" ^ 
   "\t-print-ast prints files as parsed, then exit\n" ^ 
   "\t-print prints files after most compilation passes, then exit\n" ^ 
-  "\t-print-passes prints intermediate data during compilation, then exit\n" ^
   "\t-print-units prints compilation units data, then exit\n"
 ;;
 
 (* For testing purposes we declare an identity quotation *)
 let quotations = API.Quotation.new_quotations_descriptor ()
 let _ =
   API.Quotation.register_named_quotation ~descriptor:quotations ~name:"elpi"
-    API.Quotation.lp
+    API.Quotation.elpi
 
 let _ =
+  (* Memtrace.trace_if_requested (); <-- new line *)
+  (* Hashtbl.randomize (); *)
   let test = ref false in
   let exec = ref "" in
   let print_lprolog = ref false in
   let print_ast = ref false in
-  let typecheck = ref true in
   let batch = ref false in
   let doc_builtins = ref false in
+  let doc_infix = ref false in
   let delay_outside_fragment = ref false in 
   let print_passes = ref false in
   let print_units = ref false in
   let extra_paths = ref [] in
-  let legacy_parser = ref false in
   let parse_term = ref false in
   let vars =
     ref API.Compile.(default_flags.defined_variables) in
   let rec eat_options = function
     | [] -> []
     | "-delay-problems-outside-pattern-fragment" :: rest -> delay_outside_fragment := true; eat_options rest
-    | "-legacy-parser" :: rest -> legacy_parser := true; eat_options rest
-    | "-legacy-parser-available" :: _ ->
-          if API.Setup.legacy_parser_available then exit 0 else exit 1
     | "-test" :: rest -> batch := true; test := true; eat_options rest
     | "-exec" :: goal :: rest ->  batch := true; exec := goal; eat_options rest
     | "-print" :: rest -> print_lprolog := true; eat_options rest
     | "-print-ast" :: rest -> print_ast := true; eat_options rest
-    | "-print-passes" :: rest -> print_passes := true; eat_options rest
     | "-print-units" :: rest -> print_units := true; eat_options rest
     | "-parse-term" :: rest -> parse_term := true; eat_options rest
-    | "-no-tc" :: rest -> typecheck := false; eat_options rest
     | "-document-builtins" :: rest -> doc_builtins := true; eat_options rest
+    | "-document-infix-syntax" :: rest -> doc_infix := true; eat_options rest
     | "-D" :: var :: rest -> vars := API.Compile.StrSet.add var !vars; eat_options rest
     | "-I" :: p :: rest -> extra_paths := !extra_paths @ [p]; eat_options rest
     | ("-h" | "--help" | "-help") :: _ -> Printf.eprintf "%s" usage; exit 0
@@ -133,12 +127,14 @@ let _ =
   let paths = tjpath @ installpath @ [execpath] @ !extra_paths in
   let flags = {
       API.Compile.defined_variables = !vars;
-      API.Compile.print_passes = !print_passes;
       API.Compile.print_units = !print_units;
   } in
+  if !doc_infix then begin
+    Printf.eprintf "%s" Elpi_parser.Parser_config.legacy_parser_compat_error;
+    exit 0
+  end;
   let elpi =
     API.Setup.init
-      ~legacy_parser:!legacy_parser
       ~quotations
       ~flags:(API.Compile.to_setup_flags flags)
       ~builtins:[Builtin.std_builtins]
@@ -199,29 +195,22 @@ let _ =
   end;
 
   Format.eprintf "@\nParsing time: %5.3f@\n%!" (Unix.gettimeofday () -. t0_parsing);
-  let query, exec =
+  let query, prog, exec, type_checking_time =
     let t0_compilation = Unix.gettimeofday () in
     try
       let prog = API.Compile.program ~flags ~elpi [p] in
       let query = API.Compile.query prog g in
+      let type_checking_time = API.Compile.total_type_checking_time query in
       let exec = API.Compile.optimize query in
       Format.eprintf "@\nCompilation time: %5.3f@\n%!" (Unix.gettimeofday () -. t0_compilation);
-      query, exec
+      query, prog, exec, type_checking_time
     with API.Compile.CompileError(loc,msg) ->
       API.Utils.error ?loc msg
   in
-  if !typecheck then begin
-    let t0 = Unix.gettimeofday () in
-    let b = API.Compile.static_check ~checker:(Builtin.default_checker ()) query in
-    Format.eprintf "@\nTypechecking time: %5.3f@\n%!" (Unix.gettimeofday () -. t0);
-    if not b then begin
-       Format.eprintf "Type error. To ignore it, pass -no-tc.\n";
-       exit 1
-    end;
-  end;
+  Format.eprintf "@\nTypechecking time: %5.3f@\n%!" type_checking_time;
   if !print_lprolog then begin
-    API.Pp.program Format.std_formatter query;
-    Format.printf "?- ";
+    API.Pp.program Format.std_formatter prog;
+    Format.printf "\n\n%% query\n?- ";
     API.Pp.goal Format.std_formatter query;
     exit 0;
   end;