Merge pull request #212 from LPCIC/cleanup

Cleanup
LPCIC · Dec 1, 2023 · 3ebfce2 · 3ebfce2
2 parents 263e4e5 + c58068e
commit 3ebfce2
Show file tree

Hide file tree

Showing 20 changed files with 160 additions and 1,130 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -21,17 +21,10 @@ jobs:
           - 4.08.x
         profile:
           - dev
-        parser:
-          - menhir
         include:
           - os: ubuntu-latest
             ocaml-compiler: 5.1.x
             profile: fatalwarnings
-            parser: menhir
-          - os: ubuntu-latest
-            ocaml-compiler: 4.11.x
-            profile: dev
-            parser: menhir-camlp5
 
     runs-on: ${{ matrix.os }}
 
@@ -98,66 +91,57 @@ jobs:
         run: |
           opam install ./elpi.opam --deps-only --with-doc --with-test
 
-      - name: Install optional dependencies for menhir-camlp5 parser
-        if: matrix.parser == 'menhir-camlp5'
-        run: |
-          opam depext camlp5 || true # no depext on opam 2.1
-          sudo apt-get install libstring-shellquote-perl
-          sudo apt-get install libipc-system-simple-perl
-          opam install ./elpi-option-legacy-parser.opam
-          opam exec -- make config LEGACY_PARSER=1
-
       - name: Build elpi with dune profile ${{ matrix.profile }}
         run: |
           opam exec -- dune subst
           opam exec -- make build DUNE_OPTS='--profile ${{ matrix.profile }}'
-          opam exec -- cp _build/install/default/bin/elpi elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- cp _build/install/default/bin/elpi-trace-elaborator elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
+          opam exec -- cp _build/install/default/bin/elpi elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- cp _build/install/default/bin/elpi-trace-elaborator elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
 
       - name: Strip binary
         run: |
-          opam exec -- chmod u+w ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- chmod u+w ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- strip ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
-          opam exec -- strip ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
+          opam exec -- chmod u+w ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- chmod u+w ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- strip ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
+          opam exec -- strip ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
 
 # Artifacts 1 ################################################################
 
       - name: Save binary
         uses: actions/upload-artifact@v2
         with:
-          name: elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}
-          path: elpi*-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe
+          name: elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}
+          path: elpi*-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe
 
 # Test ######################################################################
 #
 # We run the test suite which also produces data.csf containing benchmarks
 
       - name: Test elpi on Unix
         if: runner.os != 'Windows'
-        run: opam exec -- make tests RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe'
+        run: opam exec -- make tests RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe'
 
       - name: Test elpi on Windows
         if: runner.os == 'Windows'
         run: |
           opam exec -- ls -l tests/sources/*.elpi
-          opam exec -- make tests PWD=${{ env.workspace }} RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}.exe' TIME=--time=${{ env.cygwin_root }}/bin/time.exe
+          opam exec -- make tests PWD=${{ env.workspace }} RUNNERS='dune ${{ env.workspace }}/elpi-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe ${{ env.workspace }}/elpi-trace-elaborator-${{ matrix.ocaml-compiler }}-${{ runner.os }}.exe' TIME=--time=${{ env.cygwin_root }}/bin/time.exe
 
 # Artifacts 2 ################################################################
 
       - name: Save logs
         uses: actions/upload-artifact@v2
         if: always()
         with:
-          name: .logs-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}
+          name: .logs-${{ matrix.ocaml-compiler }}-${{ runner.os }}
           path: _log
           retention-days: 1
 
       - name: Save benchmarking data
         uses: actions/upload-artifact@v2
         if: always()
         with:
-          name: .benchmark-${{ matrix.ocaml-compiler }}-${{ matrix.parser }}-${{ runner.os }}
+          name: .benchmark-${{ matrix.ocaml-compiler }}-${{ runner.os }}
           path: data.csv
           retention-days: 1
 

diff --git a/CHANGES.md b/CHANGES.md
@@ -1,13 +1,15 @@
-# v1.18.1 (November 2023)
+# v1.18.1 (December 2023)
 
 Requires Menhir 20211230 and OCaml 4.08 or above.
-Camlp5 8.0 or above is optional.
+
+Parser:
+  - Remove legacy parsing engine based on Camlp5
 
 API:
   - New `RawQuery.compile_ast`, lets one set up the initial state in which the
     query is run, even if the query is given as an ast.
-  - New `Utils.relocate_closed_term` to move a term from one runtime to another
-    (experimental)
+  - New `solution.relocate_assignment_to_runtime` to pass a query result
+    to another query
   - New `BuiltInPredicate.FullHO` for higher order external predicates
   - New `BuiltInPredicate.HOAdaptors` for `map` and `filter` like HO predicates
   - New `Calc.register` to register operators for `calc` (aka infix `is`)

diff --git a/Makefile b/Makefile
@@ -40,12 +40,6 @@ DUNE_OPTS=
 build:
 	dune build $(DUNE_OPTS) @all
 
-config:
-	@(if [ -z $$LEGACY_PARSER ]; \
-	then echo '(dirs :standard \ legacy_parser)'; \
-	else echo '(dirs :standard )'; \
-	fi ) > src/dune.config
-
 install:
 	dune install $(DUNE_OPTS)
 

diff --git a/elpi-option-legacy-parser.opam b/elpi-option-legacy-parser.opam
diff --git a/elpi.opam b/elpi.opam
@@ -9,7 +9,6 @@ bug-reports: "https://github.com/LPCIC/elpi/issues"
 
 build: [
   ["dune" "subst"] {dev}
-  [make "config" "LEGACY_PARSER=1"] {elpi-option-legacy-parser:installed}
   ["dune" "build" "-p" name "-j" jobs]
   [make "tests" "DUNE_OPTS=-p %{name}%" "SKIP=performance_HO" "SKIP+=performance_FO" "SKIP+=elpi_api_performance"] {with-test & os != "macos" & os-distribution != "alpine" & os-distribution != "freebsd"}
 ]
@@ -29,12 +28,6 @@ depends: [
   "atdts" {>= "2.10.0"}
   "odoc" {with-doc}
 ]
-depopts: [
-  "elpi-option-legacy-parser"
-]
-conflicts: [
-  "elpi-option-legacy-parser" {!= "1"}
-]
 synopsis: "ELPI - Embeddable λProlog Interpreter"
 description: """
 ELPI implements a variant of λProlog enriched with Constraint Handling Rules,

diff --git a/src/API.ml b/src/API.ml
@@ -73,9 +73,10 @@ let init ?(flags=Compiler.default_flags) ?(state=default_state_descriptor) ?(quo
         List.iteri (fun i s ->
           Printf.eprintf "%4d: %s\n" (i+1) s)
           (Re.Str.(split_delim (regexp_string "\n") text));
-        Printf.eprintf "Excerpt of %s:\n%s\n" fname
+        begin try Printf.eprintf "Excerpt of %s:\n%s\n" fname
           (String.sub text loc.Util.Loc.line_starts_at
-            Util.Loc.(loc.source_stop - loc.line_starts_at));
+            Util.Loc.(loc.source_stop - loc.line_starts_at))
+        with _ -> (* loc could be bogus *) (); end;
         Util.anomaly ~loc msg) in
   let header =
     try Compiler.header_of_ast ~flags ~parser state !quotations !hoas !calc builtins (List.concat header_src)
@@ -193,14 +194,26 @@ module Execute = struct
   type 'a outcome =
     Success of 'a Data.solution | Failure | NoMoreSteps
 
+  let rec uvar2discard ~depth t =
+    let open ED in
+    let module R = (val !r) in
+    match R.deref_head ~depth t with
+    | App(c,x,xs) -> mkApp c (uvar2discard ~depth x) (List.map (uvar2discard ~depth) xs)
+    | Cons(x,xs) -> mkCons (uvar2discard ~depth x) (uvar2discard ~depth xs)
+    | Lam x -> mkLam (uvar2discard ~depth:(depth+1) x)
+    | Builtin(c,xs) -> mkBuiltin c (List.map (uvar2discard ~depth) xs)
+    | UVar _ | AppUVar _ -> mkDiscard
+    | Arg _ | AppArg _ -> assert false
+    | Const _ | Nil | CData _ | Discard -> t
+
   let map_outcome full_deref hmove = function
     | ED.Failure -> Failure
     | ED.NoMoreSteps -> NoMoreSteps
     | ED.Success { ED.assignments; constraints; state; output; pp_ctx; state_for_relocation = (idepth,from); } -> 
       Success { assignments; constraints; state; output; pp_ctx;
         relocate_assignment_to_runtime = (fun ~target ~depth s ->
           Compiler.relocate_closed_term ~from
-            (Util.StrMap.find s assignments |> full_deref ~depth:idepth) ~to_:target
+            (Util.StrMap.find s assignments |> full_deref ~depth:idepth |> uvar2discard ~depth:idepth) ~to_:target
           |> Stdlib.Result.map (hmove ?avoid:None ~from:depth ~to_:depth)
         );
         }
@@ -448,7 +461,7 @@ module BuiltInData = struct
     { Conversion.embed; readback; ty;
       pp = (fun fmt (t,d) ->
         let module R = (val !r) in let open R in
-        Pp.uppterm d [] d ED.empty_env fmt t);
+        Pp.uppterm d [] ~argsdepth:d ED.empty_env fmt t);
       pp_doc = (fun fmt () -> ()) }
 
   let map_acc f s l =
@@ -506,7 +519,7 @@ module Elpi = struct
         Format.fprintf fmt "%s" str
     | Ref ub ->
         let module R = (val !r) in let open R in
-        Pp.uppterm 0 [] 0 [||] fmt (ED.mkUVar ub 0 0)
+        Pp.uppterm 0 [] ~argsdepth:0 [||] fmt (ED.mkUVar ub 0 0)
 
   let show m = Format.asprintf "%a" pp m
 
@@ -1339,9 +1352,6 @@ module Utils = struct
       body = aux depth Util.IntMap.empty term;
     }]
 
-  let relocate_closed_term (state,t) new_state =
-    Compiler.relocate_closed_term ~from:state t ~to_:new_state
-
   let map_acc = BuiltInData.map_acc
 
   module type Show = Util.Show
@@ -1356,7 +1366,7 @@ end
 module RawPp = struct
   let term depth fmt t =
     let module R = (val !r) in let open R in
-    Pp.uppterm depth [] 0 ED.empty_env fmt t
+    Pp.uppterm depth [] ~argsdepth:0 ED.empty_env fmt t
 
   let constraints f c = 
     let module R = (val !r) in let open R in
@@ -1367,7 +1377,7 @@ module RawPp = struct
   module Debug = struct
     let term depth fmt t =
       let module R = (val !r) in let open R in
-       Pp.ppterm depth [] 0 ED.empty_env fmt t
+       Pp.ppterm depth [] ~argsdepth:0 ED.empty_env fmt t
     let show_term = ED.show_term
   end
 end
diff --git a/src/API.mli b/src/API.mli
@@ -161,7 +161,7 @@ module Data : sig
     state : state;
     output : 'a;
     pp_ctx : pretty_printer_context;
-    relocate_assignment_to_runtime : target:state -> depth:int -> string -> (term, string) Stdlib.Result.t
+    relocate_assignment_to_runtime : target:state -> depth:int -> string -> (term, string) Stdlib.Result.t (* uvars are turned into discard *)
   }
 
   (* Hypothetical context *)
@@ -1224,11 +1224,6 @@ module Utils : sig
     ?name:string -> ?graft:([`After | `Before] * string) ->
     depth:int -> Ast.Loc.t -> Data.term -> Ast.program
 
-  (** Hackish API. Move a term from one runtime (after execution) to another
-      one which has all the needed symbols *)
-  val relocate_closed_term :
-    State.t * Data.term -> State.t -> (Data.term,string) Stdlib.Result.t
-
   (** Lifting/restriction/beta (LOW LEVEL, don't use) *)
   val move : from:int -> to_:int -> Data.term -> Data.term
   val beta : depth:int -> Data.term -> Data.term list -> Data.term

diff --git a/src/compiler.ml b/src/compiler.ml
@@ -2100,7 +2100,7 @@ let unit_or_header_of_ast { print_passes } s ?(toplevel_macros=F.Map.empty) p =
   s, {
     version = "%%VERSION_NUM%%";
     code = p;
-    symbol_table = Symbols.prune (State.get Symbols.table s) p.Flat.symbols
+    symbol_table = Symbols.prune (State.get Symbols.table s) ~alive:p.Flat.symbols
   }
 ;;
 
@@ -2121,22 +2121,19 @@ let header_of_ast ~flags ~parser:p state_descriptor quotation_descriptor hoas_de
     | Some x ->
         D.State.set D.Conversion.extra_goals_postprocessing state x
     | None -> state in          
+  let { D.QuotationHooks.default_quotation;
+        named_quotations;
+        singlequote_compilation;
+        backtick_compilation } = quotation_descriptor in
+
+  let state = D.State.set CustomFunctorCompilation.backtick state (Option.map snd backtick_compilation) in
+  let state = D.State.set CustomFunctorCompilation.singlequote state (Option.map snd singlequote_compilation) in
+  let state = D.State.set Quotation.default_quotation state default_quotation in
+  let state = D.State.set Quotation.named_quotations state named_quotations in
   let state =
-    let { D.QuotationHooks.default_quotation;
-          named_quotations;
-          singlequote_compilation;
-          backtick_compilation } = quotation_descriptor in
-
-    let state = D.State.set CustomFunctorCompilation.backtick state (Option.map snd backtick_compilation) in
-    let state = D.State.set CustomFunctorCompilation.singlequote state (Option.map snd singlequote_compilation) in
-    let state = D.State.set Quotation.default_quotation state default_quotation in
-    let state = D.State.set Quotation.named_quotations state named_quotations in
-    let state =
-      let eval_map = List.fold_left (fun m (c,{ CalcHooks.code }) -> Constants.Map.add c code m) Constants.Map.empty (List.rev calc_descriptor) in
-      D.State.set CalcHooks.eval state eval_map in
-    state
-  in
-
+    let eval_map = List.fold_left (fun m (c,{ CalcHooks.code }) -> Constants.Map.add c code m) Constants.Map.empty (List.rev calc_descriptor) in
+    D.State.set CalcHooks.eval state eval_map in
+  let state = D.State.set parser state (Some p) in
   let state = D.State.set D.while_compiling state true in
   let state = State.set Symbols.table state (Symbols.global_table ()) in
   let state =
@@ -2147,7 +2144,6 @@ let header_of_ast ~flags ~parser:p state_descriptor quotation_descriptor hoas_de
       | Data.BuiltInPredicate.MLDataC _ -> state
       | Data.BuiltInPredicate.LPCode _ -> state
       | Data.BuiltInPredicate.LPDoc _ -> state) state decls) state builtins in
-  let state = D.State.set parser state (Some p) in
   let state, u = unit_or_header_of_ast flags state ast in
   print_unit flags u;
   state, u

diff --git a/src/data.ml b/src/data.ml
@@ -286,8 +286,8 @@ module State : sig
      - end_compilation (just once before running)
      - end_execution (just once after running)
   *)
+
   val init : descriptor -> t
-  val descriptor : t -> descriptor
   val end_clause_compilation : t -> t
   val begin_goal_compilation : t -> t
   val end_goal_compilation : uvar_body StrMap.t -> t -> t
@@ -301,9 +301,12 @@ module State : sig
   val update_return : 'a component -> t -> ('a -> 'a * 'b) -> t * 'b
   val pp : Format.formatter -> t -> unit
 
+  val dummy : t
+
 end = struct
 
   type stage =
+    | Dummy
     | Compile_prog
     | Compile_goal
     | Link
@@ -323,6 +326,7 @@ end = struct
   type descriptor = extension StrMap.t ref
 
   type t = { data : Obj.t StrMap.t; stage : stage; extensions : descriptor }
+  let dummy : t = { data = StrMap.empty; stage = Dummy; extensions = ref StrMap.empty }
   let descriptor { extensions = x } = x
 
   let new_descriptor () : descriptor = ref StrMap.empty
@@ -366,13 +370,15 @@ end = struct
     name
 
   let init extensions : t =
-    { data =
-       StrMap.fold (fun name { init } acc ->
-        let o = init () in
-        StrMap.add name o acc)
-        !extensions StrMap.empty;
+    let data = StrMap.fold (fun name { init } acc ->
+      let o = init () in
+      StrMap.add name o acc)
+      !extensions StrMap.empty in
+    {
+      data;
       stage = Compile_prog;
-      extensions }
+      extensions;
+    }
 
   let end_clause_compilation { data = m; stage = s; extensions } : t =
     assert(s = Compile_prog);

diff --git a/src/dune b/src/dune
@@ -82,5 +82,3 @@
 (rule
   (targets trace.ts)
   (action (run atdts %{dep:trace.atd})))
-
-(include dune.config)
diff --git a/src/legacy_parser/dune b/src/legacy_parser/dune