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.