Enable λProlog builtins

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.
+
 
 
 

src/coq_elpi_programs.ml

@@ -264,6 +264,7 @@ let elpi_builtins =
       elpi_set @
       io_builtins @
       ocaml_runtime @
+      lp_builtins @
       []
     )
 

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.