From 6b463fca6b244a8bf52d567f59dfdac8a374dd39 Mon Sep 17 00:00:00 2001
From: Philip Kaludercic <philipk@posteo.net>
Date: Thu, 28 Sep 2023 11:17:22 +0200
Subject: [PATCH] =?UTF-8?q?Enable=20=CE=BBProlog=20builtins?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* elpi-builtin.elpi: Update auto-generated file.
* src/coq_elpi_programs.ml (elpi_builtins): Add 'lp_builtins' to
'elpi_builtins'.
* tests/test_link_order_import3.ref: Update expected test results.

As discussed in the "Elpi users & devs" Zulip chatroom:
https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/ELPI.20Hacks/near/393206572
---
 elpi-builtin.elpi                 | 26 ++++++++++++++++++++++++++
 src/coq_elpi_programs.ml          |  1 +
 tests/test_link_order_import3.ref |  2 ++
 3 files changed, 29 insertions(+)

diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi
index c3dc18f8f..b45cc0b0e 100644
--- a/elpi-builtin.elpi
+++ b/elpi-builtin.elpi
@@ -1222,6 +1222,32 @@ external pred gc.stat o:float, o:float, o:float, o:int, o:int, o:int,
 external pred gc.quick-stat o:float, o:float, o:float, o:int, o:int, 
                             o:int, o:int, o:int, o:int, o:int.
 
+% == Lambda Prolog builtins =====================================
+
+%  -- Extra I/O --
+
+% [open_string DataIn InStream] opens DataIn as an input stream
+external pred open_string i:string, o:in_stream.
+
+% [lookahead InStream NextChar] peeks one byte from InStream
+external pred lookahead i:in_stream, o:string.
+
+%  -- Hacks --
+
+% [string_to_term S T] parses a term T from S
+external pred string_to_term i:string, o:any.
+
+% [readterm InStream T] reads T from InStream, ends with \n
+external pred readterm i:in_stream, o:any.
+
+pred printterm i:out_stream, i:A.
+
+printterm S T :- term_to_string T T1, output S T1.
+
+pred read o:A.
+
+read S :- flush std_out, input_line std_in X, string_to_term X S.
+
 
 
 
diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml
index 9ce389a97..e5476157e 100644
--- a/src/coq_elpi_programs.ml
+++ b/src/coq_elpi_programs.ml
@@ -264,6 +264,7 @@ let elpi_builtins =
       elpi_set @
       io_builtins @
       ocaml_runtime @
+      lp_builtins @
       []
     )
 
diff --git a/tests/test_link_order_import3.ref b/tests/test_link_order_import3.ref
index 56bc640d3..a96138e45 100644
--- a/tests/test_link_order_import3.ref
+++ b/tests/test_link_order_import3.ref
@@ -396,6 +396,8 @@ std.set.private.cardinal (std.set.private.node A0 _ A1 _) A2 :-
 std.set.private.elements std.set.private.empty A0 A0.
 std.set.private.elements (std.set.private.node A0 A1 A2 _) A3 A4 :-
  std.set.private.elements A2 A3 A5 , std.set.private.elements A0 [A1 | A5] A4.
+printterm A0 A1 :- term_to_string A1 A2 , output A0 A2.
+read A0 :- , (flush std_out) (input_line std_in A1) (string_to_term A1 A0).
 p before 2.
 p before 22.
 p before 1.