Merge branch 'master' into library-use-case

.github/workflows/ci.yml

@@ -63,10 +63,11 @@ jobs:
 
       # Build and test.
       - name: Build library
-        run: cargo rustc --lib --target ${{ matrix.target }} ${{ matrix.args }} --verbose
+        continue-on-error: ${{ contains(matrix.target,'wasm32') }} # allow wasm builds to fail tests for now
+        run: cargo build --all-targets --target ${{ matrix.target }} ${{ matrix.args }} --verbose
       - name: Test
         continue-on-error: ${{ contains(matrix.target,'wasm32') }} # allow wasm builds to fail tests for now
-        run: cargo test --target ${{ matrix.target }} ${{ matrix.args }} --all --verbose
+        run: cargo test --target ${{ matrix.target }} ${{ matrix.args }} --all
 
       # On stable rust builds, build a binary and publish as a github actions
       # artifact. These binaries could be useful for testing the pipeline but

Cargo.toml

@@ -71,6 +71,7 @@ bytes = "1"
 dashu = "0.4.0"
 num-order = { version = "1.2.0" }
 rand = "0.8.5"
+ring = { version = "0.17.5", features = ["wasm32_unknown_unknown_js"] }
 
 serde_json = "1.0.95"
 serde = "1.0.159"
@@ -83,7 +84,7 @@ ctrlc = { version = "3.2.2", optional = true }
 rustyline = { version = "12.0.0", optional = true }
 native-tls = { version = "0.2.4", optional = true }
 warp = { version = "=0.3.5", features = ["tls"], optional = true }
-reqwest = { version = "0.11.18", features = ["blocking"], optional = true }
+reqwest = { version = "0.11.18", optional = true }
 tokio = { version = "1.28.2", features = ["full"] }
 
 [target.'cfg(target_arch = "wasm32")'.dependencies]
@@ -104,12 +105,6 @@ serde-wasm-bindgen = "0.5"
 web-sys = { version = "0.3", features = ["Document", "Window", "Element", "Performance"] }
 js-sys = "0.3"
 
-[target.'cfg(target_os = "wasi")'.dependencies]
-ring-wasi = { version = "0.16.25" }
-
-[target.'cfg(not(target_os = "wasi"))'.dependencies]
-ring = { version = "0.16.13" }
-
 [dev-dependencies]
 assert_cmd = "1.0.3"
 predicates-core = "1.0.2"
@@ -117,6 +112,7 @@ maplit = "1.0.2"
 serial_test = "2.0.0"
 iai-callgrind = { git = "https://github.com/iai-callgrind/iai-callgrind.git", rev = "c77bc3c83d7f4e976cc42d4597236a8db259e772" }
 criterion = "0.5.1"
+trycmd = "0.14.19"
 
 [target.'cfg(not(target_os = "windows"))'.dev-dependencies]
 pprof = { version = "0.13.0", features = ["criterion", "flamegraph"] }

README.md

@@ -316,6 +316,35 @@ To quit Scryer Prolog, use the standard predicate `halt/0`:
 ?- halt.
 ```
 
+### Starting Scryer Prolog
+
+Scryer Prolog can be started from the command line by specifying
+options, files and additional arguments. All components are optional:
+
+<pre>
+scryer-prolog [OPTIONS] [FILES] [-- ARGUMENTS]
+</pre>
+
+The supported options are:
+
+```
+   -h, --help             Display help message
+   -v, --version          Print version information and exit
+   -g, --goal GOAL        Run the query GOAL after consulting files
+   -f                     Fast startup. Do not load initialization file (~/.scryerrc)
+   --no-add-history       Prevent adding input to history file (~/.scryer_history)
+```
+
+All specified Prolog files are consulted.
+
+After Prolog files, application-specific arguments can be specified on
+the command line. These arguments can be accessed from within Prolog
+applications with the predicate&nbsp;`argv/1`, which yields the list
+of arguments represented as strings.
+
+Prolog files can also be turned into *shell&nbsp;scripts* as explained in
+https://github.com/mthom/scryer-prolog/issues/2170#issuecomment-1821713993.
+
 ### Dynamic operators
 
 Scryer supports dynamic operators. Using the built-in

build/instructions_template.rs

@@ -511,18 +511,12 @@ enum SystemClauseType {
     #[cfg(feature = "crypto-full")]
     #[strum_discriminants(strum(props(Arity = "6", Name = "$crypto_data_decrypt")))]
     CryptoDataDecrypt,
-    #[cfg(feature = "crypto-full")]
+    #[strum_discriminants(strum(props(Arity = "4", Name = "$ed25519_sign_raw")))]
-    #[strum_discriminants(strum(props(Arity = "4", Name = "$ed25519_sign")))]
+    Ed25519SignRaw,
-    Ed25519Sign,
+    #[strum_discriminants(strum(props(Arity = "4", Name = "$ed25519_verify_raw")))]
-    #[cfg(feature = "crypto-full")]
+    Ed25519VerifyRaw,
-    #[strum_discriminants(strum(props(Arity = "4", Name = "$ed25519_verify")))]
+    #[strum_discriminants(strum(props(Arity = "2", Name = "$ed25519_seed_to_public_key")))]
-    Ed25519Verify,
+    Ed25519SeedToPublicKey,
-    #[cfg(feature = "crypto-full")]
-    #[strum_discriminants(strum(props(Arity = "1", Name = "$ed25519_new_keypair")))]
-    Ed25519NewKeyPair,
-    #[cfg(feature = "crypto-full")]
-    #[strum_discriminants(strum(props(Arity = "2", Name = "$ed25519_keypair_public_key")))]
-    Ed25519KeyPairPublicKey,
     #[strum_discriminants(strum(props(Arity = "2", Name = "$first_non_octet")))]
     FirstNonOctet,
     #[strum_discriminants(strum(props(Arity = "3", Name = "$load_html")))]
@@ -610,6 +604,8 @@ enum SystemClauseType {
     KeySortWithConstantVarOrdering,
     #[strum_discriminants(strum(props(Arity = "0", Name = "$inference_limit_exceeded")))]
     InferenceLimitExceeded,
+    #[strum_discriminants(strum(props(Arity = "1", Name = "$argv")))]
+    Argv,
     REPL(REPLCodePtr),
 }
 
@@ -796,8 +792,8 @@ enum InstructionTemplate {
     #[strum_discriminants(strum(props(Arity = "0", Name = "install_verify_attr")))]
     InstallVerifyAttr,
     // call verify_attrs.
-    #[strum_discriminants(strum(props(Arity = "0", Name = "verify_attr_interrupt")))]
+    #[strum_discriminants(strum(props(Arity = "1", Name = "verify_attr_interrupt")))]
-    VerifyAttrInterrupt,
+    VerifyAttrInterrupt(usize),
     // procedures
     CallClause(ClauseType, usize, usize, bool, bool), // ClauseType,
                                                       // arity,
@@ -1157,6 +1153,33 @@ fn generate_instruction_preface() -> TokenStream {
         pub type CodeDeque = VecDeque<Instruction>;
 
         impl Instruction {
+            #[inline]
+            pub fn registers(&self) -> Vec<RegType> {
+                match self {
+                    &Instruction::GetConstant(_, _, r) => vec![r],
+                    &Instruction::GetList(_, r) => vec![r],
+                    &Instruction::GetPartialString(_, _, r, _) => vec![r],
+                    &Instruction::GetStructure(_, _, _, r) => vec![r],
+                    &Instruction::GetVariable(r, t) => vec![r, temp_v!(t)],
+                    &Instruction::GetValue(r, t) => vec![r, temp_v!(t)],
+                    &Instruction::UnifyLocalValue(r) => vec![r],
+                    &Instruction::UnifyVariable(r) => vec![r],
+                    &Instruction::PutConstant(_, _, r) => vec![r],
+                    &Instruction::PutList(_, r) => vec![r],
+                    &Instruction::PutPartialString(_, _, r, _) => vec![r],
+                    &Instruction::PutStructure(_, _, r) => vec![r],
+                    &Instruction::PutValue(r, t) => vec![r, temp_v!(t)],
+                    &Instruction::PutVariable(r, t) => vec![r, temp_v!(t)],
+                    &Instruction::SetLocalValue(r) => vec![r],
+                    &Instruction::SetVariable(r) => vec![r],
+                    &Instruction::SetValue(r) => vec![r],
+                    &Instruction::GetLevel(r) => vec![r],
+                    &Instruction::GetPrevLevel(r) => vec![r],
+                    &Instruction::GetCutPoint(r) => vec![r],
+                    _ => vec![],
+                }
+            }
+
             #[inline]
             pub fn to_indexing_line_mut(&mut self) -> Option<&mut Vec<IndexingLine>> {
                 match self {
@@ -1199,7 +1222,10 @@ fn generate_instruction_preface() -> TokenStream {
                     Instruction::SetLocalValue(..) |
                     Instruction::SetVariable(..) |
                     Instruction::SetValue(..) |
-                    Instruction::SetVoid(..))
+                    Instruction::SetVoid(..) |
+                    Instruction::GetLevel(..) |
+                    Instruction::GetPrevLevel(..) |
+                    Instruction::GetCutPoint(..))
             }
 
             pub fn enqueue_functors(
@@ -1244,8 +1270,8 @@ fn generate_instruction_preface() -> TokenStream {
                     &Instruction::InstallVerifyAttr => {
                         functor!(atom!("install_verify_attr"))
                     }
-                    &Instruction::VerifyAttrInterrupt => {
+                    &Instruction::VerifyAttrInterrupt(arity) => {
-                        functor!(atom!("verify_attr_interrupt"))
+                        functor!(atom!("verify_attr_interrupt"), [fixnum(arity)])
                     }
                     &Instruction::DynamicElse(birth, death, next_or_fail) => {
                         match (death, next_or_fail) {
@@ -1874,18 +1900,18 @@ fn generate_instruction_preface() -> TokenStream {
                     &Instruction::CallFlushTermQueue |
                     &Instruction::CallRemoveModuleExports |
                     &Instruction::CallAddNonCountedBacktracking |
-                    &Instruction::CallPopCount => {
+                    &Instruction::CallPopCount |
+                    &Instruction::CallArgv |
+                    &Instruction::CallEd25519SignRaw |
+                    &Instruction::CallEd25519VerifyRaw |
+                    &Instruction::CallEd25519SeedToPublicKey => {
                         let (name, arity) = self.to_name_and_arity();
                         functor!(atom!("call"), [atom(name), fixnum(arity)])
                     }
                     //
                     #[cfg(feature = "crypto-full")]
                     &Instruction::CallCryptoDataEncrypt |
-                    &Instruction::CallCryptoDataDecrypt |
+                    &Instruction::CallCryptoDataDecrypt => {
-                    &Instruction::CallEd25519Sign |
-                    &Instruction::CallEd25519Verify |
-                    &Instruction::CallEd25519NewKeyPair |
-                    &Instruction::CallEd25519KeyPairPublicKey => {
                         let (name, arity) = self.to_name_and_arity();
                         functor!(atom!("call"), [atom(name), fixnum(arity)])
                     }
@@ -2110,18 +2136,18 @@ fn generate_instruction_preface() -> TokenStream {
                     &Instruction::ExecuteFlushTermQueue |
                     &Instruction::ExecuteRemoveModuleExports |
                     &Instruction::ExecuteAddNonCountedBacktracking |
-                    &Instruction::ExecutePopCount => {
+                    &Instruction::ExecutePopCount |
+                    &Instruction::ExecuteArgv |
+                    &Instruction::ExecuteEd25519SignRaw |
+                    &Instruction::ExecuteEd25519VerifyRaw |
+                    &Instruction::ExecuteEd25519SeedToPublicKey => {
                         let (name, arity) = self.to_name_and_arity();
                         functor!(atom!("execute"), [atom(name), fixnum(arity)])
                     }
                     //
                     #[cfg(feature = "crypto-full")]
                     &Instruction::ExecuteCryptoDataEncrypt |
-                    &Instruction::ExecuteCryptoDataDecrypt |
+                    &Instruction::ExecuteCryptoDataDecrypt => {
-                    &Instruction::ExecuteEd25519Sign |
-                    &Instruction::ExecuteEd25519Verify |
-                    &Instruction::ExecuteEd25519NewKeyPair |
-                    &Instruction::ExecuteEd25519KeyPairPublicKey => {
                         let (name, arity) = self.to_name_and_arity();
                         functor!(atom!("execute"), [atom(name), fixnum(arity)])
                     }

src/allocator.rs

@@ -53,40 +53,5 @@ pub(crate) trait Allocator {
     fn reset_contents(&mut self);
 
     fn advance_arg(&mut self);
-
-    /*
-    fn bindings(&self) -> &AllocVarDict;
-    fn bindings_mut(&mut self) -> &mut AllocVarDict;
-    fn take_bindings(self) -> AllocVarDict;
-    */
-
     fn max_reg_allocated(&self) -> usize;
-
-    // TODO: wha.. why?? grrr. it drains the VarStatus data from vs (which it owns!)
-    // into self.bindings and perm_vs after all is computed (i.e. vs.populate_restricting_sets()
-    // and vs.set_perm_vals(has_deep_cut) have both been called).
-    /*
-    fn drain_var_data<'a>(
-        &mut self,
-        vs: VariableFixtures,
-        num_of_chunks: usize,
-    ) -> VariableFixtures {
-        let mut perm_vs = VariableFixtures::new();
-
-        for (var, var_status) in vs.into_iter() {
-            match var_status {
-                VarStatus::Temp(chunk_num, tvd) => {
-                    self.bindings_mut()
-                        .insert(var.clone(), VarAlloc::Temp(chunk_num, 0, tvd));
-                }
-                VarStatus::Perm(_) => {
-                    self.bindings_mut().insert(var.clone(), VarAlloc::Perm(0));
-                    perm_vs.insert(var, var_status);
-                }
-            };
-        }
-
-        perm_vs
-    }
-    */
 }

src/arena.rs

@@ -821,9 +821,9 @@ impl AllocSlab {
     }
 
     fn payload_offset<T>(&self) -> *mut T {
-        let mut ptr = (self as *const AllocSlab) as usize;
+        // This looks really scary, should this method be marked as unsafe?
-        ptr += mem::size_of::<AllocSlab>();
+        // Also, this seems to cause UB.
-        ptr as *mut T
+        unsafe { (self as *const AllocSlab).add(1) as *mut T }
     }
 }
 
@@ -864,6 +864,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn heap_cell_value_const_cast() {
         let mut wam = MockWAM::new();
         #[cfg(target_pointer_width = "32")]
@@ -907,6 +908,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on arena.rs UB")]
     fn heap_put_literal_tests() {
         let mut wam = MockWAM::new();
 

src/atom_table.rs

@@ -239,6 +239,7 @@ impl Atom {
         } else if let Some(ptr) = self.as_ptr() {
             AtomString::Dynamic(AtomTableRef::map(ptr, |ptr| {
                 let header =
+                    // Miri seems to hit this line a lot
                     unsafe { ptr::read::<AtomHeader>(ptr as *const u8 as *const AtomHeader) };
                 let len = header.len() as usize;
                 let buf = unsafe { (ptr as *const u8).add(mem::size_of::<AtomHeader>()) };
@@ -265,7 +266,7 @@ impl Atom {
 
 unsafe fn write_to_ptr(string: &str, ptr: *mut u8) {
     ptr::write(ptr as *mut _, AtomHeader::build_with(string.len() as u64));
-    let str_ptr = (ptr as usize + mem::size_of::<AtomHeader>()) as *mut u8;
+    let str_ptr = ptr.add(mem::size_of::<AtomHeader>());
     ptr::copy_nonoverlapping(string.as_ptr(), str_ptr, string.len());
 }
 

src/bin/scryer-prolog.rs

@@ -23,6 +23,6 @@ fn main() -> std::process::ExitCode {
 
     runtime.block_on(async move {
         let mut wam = machine::Machine::new(Default::default());
-        wam.run_top_level(atom!("$toplevel"), (atom!("$repl"), 1))
+        wam.run_module_predicate(atom!("$toplevel"), (atom!("$repl"), 0))
     })
 }

src/codegen.rs

@@ -860,6 +860,9 @@ impl<'b> CodeGenerator<'b> {
                     self.marker.mark_safe_var_unconditionally(var_num);
                     compile_expr!(self, &terms[1], term_loc, code)
                 } else {
+                    self.marker
+                        .mark_anon_var::<QueryInstruction>(Level::Shallow, term_loc, code);
+
                     if let Term::Var(ref vr, ref var) = &terms[1] {
                         let var_num = var.to_var_num().unwrap();
 

src/debray_allocator.rs

@@ -604,16 +604,9 @@ impl DebrayAllocator {
                     Target::unsafe_argument_to_value(r, arg_c)
                 }
             }
-            VarAlloc::Temp { ref mut safety, .. } => {
+            VarAlloc::Temp { .. } => {
-                if self
+                debug_assert!(matches!(r, RegType::Temp(_)));
-                    .branch_stack
-                    .safety_unneeded_in_branch(safety, &branch_designator)
-                {
                 Target::argument_to_value(r, arg_c)
-                } else {
-                    *safety = VarSafetyStatus::GloballyUnneeded;
-                    Target::unsafe_argument_to_value(r, arg_c)
-                }
             }
             _ => {
                 unreachable!()

src/heap_iter.rs

@@ -108,7 +108,7 @@ impl<'a> EagerStackfulPreOrderHeapIter<'a> {
                     let var_value = self.heap[h];
                     self.heap[h].set_mark_bit(self.mark_phase);
 
-                    if !(self.heap[h].is_var() && self.heap[h].get_value() as usize == h) {
+                    if var_value.get_mark_bit() || !(self.heap[h].is_var() && self.heap[h].get_value() as usize == h) {
                         self.iter_stack.push(var_value);
                         continue;
                     }
@@ -125,13 +125,14 @@ impl<'a> EagerStackfulPreOrderHeapIter<'a> {
                         continue;
                     }
 
-                    let value = self.heap[h+1];
-
                     self.heap[h].set_mark_bit(self.mark_phase);
-                    self.heap[h+1].set_mark_bit(self.mark_phase);
 
+                    if self.heap[h].get_tag() == HeapCellValueTag::PStr {
+                        let value = self.heap[h+1];
+                        self.heap[h+1].set_mark_bit(self.mark_phase);
                         self.iter_stack.push(value);
                     }
+                }
                 _ => {
                 }
             );
@@ -685,6 +686,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "it takes too long to run")]
     fn heap_stackless_iter_tests() {
         let mut wam = MockWAM::new();
 
@@ -1756,6 +1758,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on atom_table.rs UB")]
     fn heap_stackful_iter_tests() {
         let mut wam = MockWAM::new();
 
@@ -2348,6 +2351,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on atom_table.rs UB")]
     fn heap_stackful_post_order_iter() {
         let mut wam = MockWAM::new();
 
@@ -2831,6 +2835,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on atom_table.rs UB")]
     fn heap_stackless_post_order_iter() {
         let mut wam = MockWAM::new();
 

src/heap_print.rs

@@ -1444,7 +1444,6 @@ impl<'a, Outputter: HCValueOutputter> HCPrinter<'a, Outputter> {
         }
     }
 
-    #[allow(dead_code)]
     fn print_tcp_listener(&mut self, tcp_listener: &TcpListener, max_depth: usize) {
         let (ip, port) = if let Ok(addr) = tcp_listener.local_addr() {
             (addr.ip(), addr.port())
@@ -1727,6 +1726,9 @@ impl<'a, Outputter: HCValueOutputter> HCPrinter<'a, Outputter> {
                    (ArenaHeaderTag::Stream, stream) => {
                        self.print_stream(stream, max_depth);
                    }
+                   (ArenaHeaderTag::TcpListener, listener) => {
+                       self.print_tcp_listener(&*listener, max_depth);
+                   }
                    (ArenaHeaderTag::Dropped, _value) => {
                        self.print_impromptu_atom(atom!("$dropped_value"));
                    }
@@ -1833,6 +1835,7 @@ mod tests {
     use crate::machine::mock_wam::*;
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn term_printing_tests() {
         let mut wam = MockWAM::new();
 

src/lib/atts.pl

@@ -1,8 +1,8 @@
 :- module(atts, [op(1199, fx, attribute),
-                 call_residue_vars/2,
                  term_attributed_variables/2]).
 
 :- use_module(library(dcgs)).
+:- use_module(library(error)).
 :- use_module(library(terms)).
 
 /* represent the list of attributes belonging to a variable,
@@ -110,12 +110,5 @@ user:goal_expansion(Term, M:get_atts(Var, Attr)) :-
     nonvar(Term),
     Term = get_atts(Var, M, Attr).
 
-:- meta_predicate call_residue_vars(0, ?).
-
-call_residue_vars(Goal, Vars) :-
-    '$get_attr_var_queue_delim'(B),
-    call(Goal),
-    '$get_attr_var_queue_beyond'(B, Vars).
-
 term_attributed_variables(Term, Vars) :-
     '$term_attributed_variables'(Term, Vars).

src/lib/builtins.pl

@@ -1239,7 +1239,10 @@ call_retract_helper(Head, Body, P, Module) :-
     ;  ClauseQualifier = Module
     ),
     ClauseQualifier:'$clause'(Head, Body),
-    '$get_clause_p'(Head, P, Module).
+    % ensure '$get_clause_p'/3 is not the last clause so it can
+    % recover the choice point of '$clause' if necessary.
+    '$get_clause_p'(Head, P, Module),
+    true.
 
 call_retract(Head, Body, Name, Arity, Module) :-
     findall(P, builtins:call_retract_helper(Head, Body, P, Module), Ps),

src/lib/clpb.pl

@@ -189,18 +189,18 @@ A _Boolean expression_ is one of:
 | `1`                | true                                 |
 | _variable_         | unknown truth value                  |
 | _atom_             | universally quantified variable      |
-| ~ _Expr_           | logical NOT                          |
+| `~` _Expr_           | logical NOT                          |
-| _Expr_ + _Expr_    | logical OR                           |
+| _Expr_ `+` _Expr_    | logical OR                           |
-| _Expr_ * _Expr_    | logical AND                          |
+| _Expr_ `*` _Expr_    | logical AND                          |
-| _Expr_ # _Expr_    | exclusive OR                         |
+| _Expr_ `#` _Expr_    | exclusive OR                         |
-| _Var_ ^ _Expr_     | existential quantification           |
+| _Var_ `^` _Expr_     | existential quantification           |
-| _Expr_ =:= _Expr_  | equality                             |
+| _Expr_ `=:=` _Expr_  | equality                             |
-| _Expr_ =\= _Expr_  | disequality (same as #)              |
+| _Expr_ `=\=` _Expr_  | disequality (same as #)              |
-| _Expr_ =< _Expr_   | less or equal (implication)          |
+| _Expr_ `=<` _Expr_   | less or equal (implication)          |
-| _Expr_ >= _Expr_   | greater or equal                     |
+| _Expr_ `>=` _Expr_   | greater or equal                     |
-| _Expr_ < _Expr_    | less than                            |
+| _Expr_ `<` _Expr_    | less than                            |
-| _Expr_ > _Expr_    | greater than                         |
+| _Expr_ `>` _Expr_    | greater than                         |
-| card(Is,Exprs)     | cardinality constraint (_see below_) |
+| `card(Is,Exprs)`     | cardinality constraint (_see below_) |
 | `+(Exprs)`         | n-fold disjunction (_see below_)     |
 | `*(Exprs)`         | n-fold conjunction (_see below_)     |
 
@@ -1251,7 +1251,7 @@ bdd_restriction_(Node, VI, Value, Res) -->
                   node_id(Node, ID) },
                 (   { I0 =:= VI } ->
                     (   { Value =:= 0 } -> { Res = Low }
-                    ;   { Value =:= 1 } -> { Res = High }
+                    ;   { Res = High }
                     )
                 ;   { I0 > VI } -> { Res = Node }
                 ;   state(G0), { get_assoc(ID, G0, Res) } -> []

src/lib/clpz.pl

@@ -3,7 +3,7 @@
     Author:        Markus Triska
     E-mail:        triska@metalevel.at
     WWW:           https://www.metalevel.at
-    Copyright (C): 2016-2023 Markus Triska
+    Copyright (C): 2016-2024 Markus Triska
 
     This library provides CLP(ℤ):
 
@@ -1015,6 +1015,9 @@ X in inf..sup.
    needed to schedule the propagators!
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
+:- meta_predicate(duophrase(4, ?, ?)).
+:- meta_predicate(duophrase(4, ?, ?, ?, ?)).
+
 duophrase(NT, As, Bs) :-
         duophrase(NT, As, [], Bs, []).
 
@@ -1735,7 +1738,7 @@ intervals_to_domain(Is, D) :-
 %           _Lower_ must be an integer or the atom *inf*, which
 %           denotes negative infinity. _Upper_ must be an integer or
 %           the atom *sup*, which denotes positive infinity.
-%         * Domain1 \/ Domain2
+%         * Domain1 `\/` Domain2
 %           The union of Domain1 and Domain2.
 
 Var in Dom :- clpz_in(Var, Dom).
@@ -2409,22 +2412,22 @@ sum_finite_domains([C|Cs], [V|Vs], Inf0, Sup0, Inf, Sup) ++>
         ),
         sum_finite_domains(Cs, Vs, Inf2, Sup2, Inf, Sup).
 
-remove_dist_upper_lower([], _, _, _).
+remove_dist_upper_lower([], _, _, _) --> [].
-remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) :-
+remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) -->
-        (   fd_get(V, VD, VPs) ->
+        (   { fd_get(V, VD, VPs) } ->
             (   C < 0 ->
-                domain_supremum(VD, n(Sup)),
+                { domain_supremum(VD, n(Sup)),
                   L is Sup + D1//C,
                   domain_remove_smaller_than(VD, L, VD1),
                   domain_infimum(VD1, n(Inf)),
                   G is Inf - D2//C,
-                domain_remove_greater_than(VD1, G, VD2)
+                  domain_remove_greater_than(VD1, G, VD2) }
-            ;   domain_infimum(VD, n(Inf)),
+            ;   { domain_infimum(VD, n(Inf)),
                   G is Inf + D1//C,
                   domain_remove_greater_than(VD, G, VD1),
                   domain_supremum(VD1, n(Sup)),
                   L is Sup - D2//C,
-                domain_remove_smaller_than(VD1, L, VD2)
+                  domain_remove_smaller_than(VD1, L, VD2) }
             ),
             fd_put(V, VD2, VPs)
         ;   true
@@ -2432,16 +2435,16 @@ remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) :-
         remove_dist_upper_lower(Cs, Vs, D1, D2).
 
 
-remove_dist_upper_leq([], _, _).
+remove_dist_upper_leq([], _, _) --> [].
-remove_dist_upper_leq([C|Cs], [V|Vs], D1) :-
+remove_dist_upper_leq([C|Cs], [V|Vs], D1) -->
-        (   fd_get(V, VD, VPs) ->
+        (   { fd_get(V, VD, VPs) } ->
             (   C < 0 ->
-                domain_supremum(VD, n(Sup)),
+                { domain_supremum(VD, n(Sup)),
                   L is Sup + D1//C,
-                domain_remove_smaller_than(VD, L, VD1)
+                  domain_remove_smaller_than(VD, L, VD1) }
-            ;   domain_infimum(VD, n(Inf)),
+            ;   { domain_infimum(VD, n(Inf)),
                   G is Inf + D1//C,
-                domain_remove_greater_than(VD, G, VD1)
+                  domain_remove_greater_than(VD, G, VD1) }
             ),
             fd_put(V, VD1, VPs)
         ;   true
@@ -2449,18 +2452,18 @@ remove_dist_upper_leq([C|Cs], [V|Vs], D1) :-
         remove_dist_upper_leq(Cs, Vs, D1).
 
 
-remove_dist_upper([], _).
+remove_dist_upper([], _) --> [].
-remove_dist_upper([C*V|CVs], D) :-
+remove_dist_upper([C*V|CVs], D) -->
-        (   fd_get(V, VD, VPs) ->
+        (   { fd_get(V, VD, VPs) } ->
             (   C < 0 ->
-                (   domain_supremum(VD, n(Sup)) ->
+                (   { domain_supremum(VD, n(Sup)) } ->
-                    L is Sup + D//C,
+                    { L is Sup + D//C,
-                    domain_remove_smaller_than(VD, L, VD1)
+                      domain_remove_smaller_than(VD, L, VD1) }
                 ;   VD1 = VD
                 )
-            ;   (   domain_infimum(VD, n(Inf)) ->
+            ;   (   { domain_infimum(VD, n(Inf)) } ->
-                    G is Inf + D//C,
+                    { G is Inf + D//C,
-                    domain_remove_greater_than(VD, G, VD1)
+                      domain_remove_greater_than(VD, G, VD1) }
                 ;   VD1 = VD
                 )
             ),
@@ -2469,18 +2472,18 @@ remove_dist_upper([C*V|CVs], D) :-
         ),
         remove_dist_upper(CVs, D).
 
-remove_dist_lower([], _).
+remove_dist_lower([], _) --> [].
-remove_dist_lower([C*V|CVs], D) :-
+remove_dist_lower([C*V|CVs], D) -->
-        (   fd_get(V, VD, VPs) ->
+        (   { fd_get(V, VD, VPs) } ->
             (   C < 0 ->
-                (   domain_infimum(VD, n(Inf)) ->
+                (   { domain_infimum(VD, n(Inf)) } ->
-                    G is Inf - D//C,
+                    { G is Inf - D//C,
-                    domain_remove_greater_than(VD, G, VD1)
+                      domain_remove_greater_than(VD, G, VD1) }
                 ;   VD1 = VD
                 )
-            ;   (   domain_supremum(VD, n(Sup)) ->
+            ;   (   { domain_supremum(VD, n(Sup)) } ->
-                    L is Sup - D//C,
+                    { L is Sup - D//C,
-                    domain_remove_smaller_than(VD, L, VD1)
+                      domain_remove_smaller_than(VD, L, VD1) }
                 ;   VD1 = VD
                 )
             ),
@@ -2489,26 +2492,26 @@ remove_dist_lower([C*V|CVs], D) :-
         ),
         remove_dist_lower(CVs, D).
 
-remove_upper([], _).
+remove_upper([], _) --> [].
-remove_upper([C*X|CXs], Max) :-
+remove_upper([C*X|CXs], Max) -->
-        (   fd_get(X, XD, XPs) ->
+        (   { fd_get(X, XD, XPs) } ->
             D is Max//C,
             (   C < 0 ->
-                domain_remove_smaller_than(XD, D, XD1)
+                { domain_remove_smaller_than(XD, D, XD1) }
-            ;   domain_remove_greater_than(XD, D, XD1)
+            ;   { domain_remove_greater_than(XD, D, XD1) }
             ),
             fd_put(X, XD1, XPs)
         ;   true
         ),
         remove_upper(CXs, Max).
 
-remove_lower([], _).
+remove_lower([], _) --> [].
-remove_lower([C*X|CXs], Min) :-
+remove_lower([C*X|CXs], Min) -->
-        (   fd_get(X, XD, XPs) ->
+        (   { fd_get(X, XD, XPs) } ->
             D is -Min//C,
             (   C < 0 ->
-                domain_remove_greater_than(XD, D, XD1)
+                { domain_remove_greater_than(XD, D, XD1) }
-            ;   domain_remove_smaller_than(XD, D, XD1)
+            ;   { domain_remove_smaller_than(XD, D, XD1) }
             ),
             fd_put(X, XD1, XPs)
         ;   true
@@ -2747,20 +2750,24 @@ propagator_init_trigger(Vs, P) :-
 prop_init(Prop, V) :- init_propagator(V, Prop).
 
 geq(A, B) :-
-        (   fd_get(A, AD, APs) ->
+        new_queue(Q),
-            domain_infimum(AD, AI),
+        phrase((geq(A, B),do_queue), [Q], _).
-            (   fd_get(B, BD, _) ->
+
-                domain_supremum(BD, BS),
+geq(A, B) -->
-                (   AI cis_geq BS -> true
+        (   { fd_get(A, AD, APs) } ->
-                ;   propagator_init_trigger(pgeq(A,B))
+            { domain_infimum(AD, AI) },
+            (   { fd_get(B, BD, _) } ->
+                { domain_supremum(BD, BS) },
+                (   { AI cis_geq BS } -> true
+                ;   { propagator_init_trigger(pgeq(A,B)) }
                 )
-            ;   (   AI cis_geq n(B) -> true
+            ;   (   { AI cis_geq n(B) } -> true
-                ;   domain_remove_smaller_than(AD, B, AD1),
+                ;   { domain_remove_smaller_than(AD, B, AD1) },
                     fd_put(A, AD1, APs)
                 )
             )
-        ;   fd_get(B, BD, BPs) ->
+        ;   { fd_get(B, BD, BPs) } ->
-            domain_remove_greater_than(BD, A, BD1),
+            { domain_remove_greater_than(BD, A, BD1) },
             fd_put(B, BD1, BPs)
         ;   A >= B
         ).
@@ -4164,6 +4171,7 @@ var(V) --> { var(V) }.
 ground(T) --> { ground(T) }.
 
 true --> [].
+false --> { false }.
 
 X >= Y	--> { X >= Y }.
 X =< Y  --> { X =< Y }.
@@ -4221,10 +4229,7 @@ activate_propagator(propagator(P,State)) -->
             )
         ).
 
-enable_queue  :- true. % NOP
+%do_queue --> print_queue, false.
-disable_queue :- true. % NOP
-
-%do_queue --> print_queue, { false }.
 do_queue -->
         (   queue_enabled ->
             (   queue_get_goal(Goal) -> { call(Goal) }, do_queue
@@ -4507,13 +4512,13 @@ run_propagator(pelement(N, Is, V), MState) -->
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-run_propagator(pgcc_single(Vs, Pairs), _) --> { gcc_global(Vs, Pairs) }.
+run_propagator(pgcc_single(Vs, Pairs), _) --> gcc_global(Vs, Pairs).
 
-run_propagator(pgcc_check_single(Pairs), _) --> { gcc_check(Pairs) }.
+run_propagator(pgcc_check_single(Pairs), _) --> gcc_check(Pairs).
 
-run_propagator(pgcc_check(Pairs), _) --> { gcc_check(Pairs) }.
+run_propagator(pgcc_check(Pairs), _) --> gcc_check(Pairs).
 
-run_propagator(pgcc(Vs, _, Pairs), _) --> { gcc_global(Vs, Pairs) }.
+run_propagator(pgcc(Vs, _, Pairs), _) --> gcc_global(Vs, Pairs).
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -4588,7 +4593,7 @@ run_propagator(pserialized(S_I, D_I, S_J, D_J, _), MState) -->
             kill(MState),
             (   S_I + D_I =< S_J -> []
             ;   S_J + D_J =< S_I -> []
-            ;   { false }
+            ;   false
             )
         ;   serialize_lower_upper(S_I, D_I, S_J, D_J, MState),
             serialize_lower_upper(S_J, D_J, S_I, D_I, MState)
@@ -4661,7 +4666,7 @@ run_propagator(x_eq_abs_plus_v(X,V), MState) -->
         (   nonvar(V) ->
             (   V =:= 0 -> kill(MState), { X in 0..sup }
             ;   V < 0 -> kill(MState), { X #= V / 2 }
-            ;   V > 0 -> { false }
+            ;   false % V > 0
             )
         ;   nonvar(X) ->
             kill(MState),
@@ -4753,10 +4758,10 @@ run_propagator(scalar_product_neq(Cs0,Vs0,P0), MState) -->
           ) }.
 
 run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) -->
-        { coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
+        { coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I) },
         P is P0 - I,
         (   Vs = [] -> kill(MState), P >= 0
-          ;   duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups),
+        ;   { duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups) },
             D1 is P - Inf,
             disable_queue,
             (   Infs == [], Sups == [] ->
@@ -4769,27 +4774,27 @@ run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) -->
             ;   true
             ),
             enable_queue
-          ) }.
+        ).
 
 run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) -->
-        { coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I),
+        { coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I) },
         P is P0 - I,
         (   Vs = [] -> kill(MState), P =:= 0
         ;   Vs = [V], Cs = [C] -> kill(MState), P mod C =:= 0, V is P // C
-          ;   Cs == [1,1] -> kill(MState), Vs = [A,B], A + B #= P
+        ;   Cs == [1,1] -> kill(MState), Vs = [A,B], { A + B #= P }
-          ;   Cs == [1,-1] -> kill(MState), Vs = [A,B], A #= P + B
+        ;   Cs == [1,-1] -> kill(MState), Vs = [A,B], { A #= P + B }
-          ;   Cs == [-1,1] -> kill(MState), Vs = [A,B], B #= P + A
+        ;   Cs == [-1,1] -> kill(MState), Vs = [A,B], { B #= P + A }
-          ;   Cs == [-1,-1] -> kill(MState), Vs = [A,B], P1 is -P, A + B #= P1
+        ;   Cs == [-1,-1] -> kill(MState), Vs = [A,B], P1 is -P, { A + B #= P1 }
-          ;   P =:= 0, Cs == [1,1,-1] -> kill(MState), Vs = [A,B,C], A + B #= C
+        ;   P =:= 0, Cs == [1,1,-1] -> kill(MState), Vs = [A,B,C], { A + B #= C }
-          ;   P =:= 0, Cs == [1,-1,1] -> kill(MState), Vs = [A,B,C], A + C #= B
+        ;   P =:= 0, Cs == [1,-1,1] -> kill(MState), Vs = [A,B,C], { A + C #= B }
-          ;   P =:= 0, Cs == [-1,1,1] -> kill(MState), Vs = [A,B,C], B + C #= A
+        ;   P =:= 0, Cs == [-1,1,1] -> kill(MState), Vs = [A,B,C], { B + C #= A }
-          ;   duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups),
+        ;   { duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups) },
-              % nl, writeln(Infs-Sups-Inf-Sup),
+            % { nl, writeln(Infs-Sups-Inf-Sup) },
             D1 is P - Inf,
             D2 is Sup - P,
             disable_queue,
             (   Infs == [], Sups == [] ->
-                  between(Inf, Sup, P),
+                { between(Inf, Sup, P) },
                 remove_dist_upper_lower(Cs, Vs, D1, D2)
             ;   Sups = [] -> P =< Sup, remove_dist_lower(Infs, D2)
             ;   Infs = [] -> Inf =< P, remove_dist_upper(Sups, D1)
@@ -4801,7 +4806,7 @@ run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) -->
             ;   true
             ),
             enable_queue
-          ) }.
+        ).
 
 % X + Y = Z
 run_propagator(pplus(X,Y,Z,Morph), MState) -->
@@ -5048,8 +5053,8 @@ run_propagator(ptzdiv(X,Y,Z,Morph), MState) -->
 %% % Z = X mod Y
 
 run_propagator(pmod(X,Y,Z), MState) -->
-        (   Y == 0 -> { false }
+        (   Y == 0 -> false
-        ;   Y == Z -> { false }
+        ;   Y == Z -> false
         ;   X == Y -> kill(MState), queue_goal(Z = 0)
         ;   true
         ),
@@ -5058,7 +5063,7 @@ run_propagator(pmod(X,Y,Z), MState) -->
             Z is X mod Y
         ;   nonvar(Y), nonvar(Z) ->
             (   Y > 0 -> Z >= 0, Z < Y
-            ;   Y < 0 -> Z =< 0, Z > Y
+            ;   Z =< 0, Z > Y    % Y < 0
             ),
             (   { fd_get(X, _, n(XL), _, _) } ->
                 (   (XL - Z) mod Y =\= 0 ->
@@ -5127,7 +5132,7 @@ run_propagator(pmodz(X,Y,Z), MState) -->
                         fd_put(Z, ZD2, ZPs)
                         % queue_goal(Z #=< X)
                     )
-                ;   X < 0 ->
+                ;   X < 0,
                     (   { fd_get(Y, _, _, n(YU), _), YU < X } ->
                         kill(MState),
                         queue_goal(Z = X)
@@ -5167,7 +5172,7 @@ run_propagator(pmodz(X,Y,Z), MState) -->
                     fd_put(Z, ZD5, ZPs)
                     % queue_goal(Z in ZMin..0)
                 )
-            ;   Y > 0 ->
+            ;   Y > 0,
                 (   { fd_get(X, _, n(XL), n(XU), _), XL >= 0, Y > XU } ->
                     kill(MState),
                     queue_goal(Z = X)
@@ -5378,8 +5383,9 @@ run_propagator(pmax(X,Y,Z), MState) -->
             ;   nonvar(Z) ->
                 (   Z =:= X -> kill(MState), queue_goal(X #>= Y)
                 ;   Z > X -> queue_goal(Z = Y)
-                ;   { false } % Z < X
+                ;   false % Z < X
                 )
+            ;   Y == Z -> kill(MState), queue_goal(Y #>= X)
             ;   { fd_get(Y, _, YInf, YSup, _) },
                 (   { YInf cis_gt n(X) } -> queue_goal(Z = Y)
                 ;   { YSup cis_lt n(X) } -> queue_goal(Z = X)
@@ -5394,7 +5400,7 @@ run_propagator(pmax(X,Y,Z), MState) -->
         ;   { fd_get(Z, ZD, ZPs) } ->
             { fd_get(X, _, XInf, XSup, _),
               fd_get(Y, _, YInf, YSup, _) },
-            (   { YInf cis_gt YSup } -> kill(MState), queue_goal(Z = Y)
+            (   { YInf cis_gt XSup } -> kill(MState), queue_goal(Z = Y)
             ;   { YSup cis_lt XInf } -> kill(MState), queue_goal(Z = X)
             ;   { n(M) cis max(XSup, YSup) } ->
                 { domain_remove_greater_than(ZD, M, ZD1) },
@@ -5413,8 +5419,9 @@ run_propagator(pmin(X,Y,Z), MState) -->
             ;   nonvar(Z) ->
                 (   Z =:= X -> kill(MState), { X #=< Y }
                 ;   Z < X -> Z = Y
-                ;   { false } % Z > X
+                ;   false % Z > X
                 )
+            ;   Y == Z -> kill(MState), queue_goal(Y #=< X)
             ;   { fd_get(Y, _, YInf, YSup, _) },
                 (   { YSup cis_lt n(X) } -> Z = Y
                 ;   { YInf cis_gt n(X) } -> Z = X
@@ -5429,7 +5436,7 @@ run_propagator(pmin(X,Y,Z), MState) -->
         ;   { fd_get(Z, ZD, ZPs) } ->
             { fd_get(X, _, XInf, XSup, _),
               fd_get(Y, _, YInf, YSup, _) },
-            (   { YSup cis_lt YInf } -> kill(MState), Z = Y
+            (   { YSup cis_lt XInf } -> kill(MState), Z = Y
             ;   { YInf cis_gt XSup } -> kill(MState), Z = X
             ;   { n(M) cis min(XInf, YInf) } ->
                 { domain_remove_smaller_than(ZD, M, ZD1) },
@@ -5448,6 +5455,7 @@ run_propagator(pexp(X,Y,Z,Morph), MState) -->
             morph_into_propagator(MState, [Y,Z], reified_eq(1,Y,1,0,[],Z), Morph)
         ;   Y == 0 -> kill(MState), Z = 1
         ;   Y == 1 -> kill(MState), Z = X
+        ;   Y == Z -> kill(MState), X = Y, queue_goal(X in -1\/1)
         ;   nonvar(X) ->
             (   nonvar(Y) ->
                 (   Y >= 0 -> true ; X =:= -1 ),
@@ -5536,7 +5544,7 @@ run_propagator(pexp(X,Y,Z,Morph), MState) -->
                 fd_put(Z, ZD2, ZPs),
                 { (   even(Y), ZU = n(Num) ->
                     integer_kth_root_leq(Num, Y, RU),
-                    (   XL cis_geq n(0), ZL = n(Num1) ->
+                    (   XL cis_geq n(0), ZL = n(Num1), Num1 >= 0 ->
                         integer_kth_root_leq(Num1, Y, RL0),
                         (   RL0^Y < Num1 -> RL is RL0 + 1
                         ;   RL = RL0
@@ -5726,8 +5734,7 @@ run_propagator(reified_fd(V,B), MState) -->
             B = 1
         ;   { B == 0 } ->
             (   { fd_inf(V, inf) } -> []
-            ;   { fd_sup(V, sup) } -> []
+            ;   { fd_sup(V, sup) }
-            ;   { false }
             )
         ;   []
         ).
@@ -6788,13 +6795,20 @@ gcc_pairs([Key-Num0|KNs], Vs, [Key-Num|Rest]) :-
     Constraint", AAAI-96 Portland, OR, USA, pp 209--215, 1996
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
-gcc_global(Vs, KNs) :-
+gcc_global(Vs, KNs) -->
-        gcc_check(KNs),
+        % at this point, all elements of clpz_gcc_vs must be
-        % previously: call do_queue/0 (now a NOP) here to reach a
+        % variables, which a previously scheduled and called
-        % fix-point: all elements of clpz_gcc_vs must be variables. We
+        % gcc_check//1 ensures. Note that gcc_check//1 disables the
-        % must ensure this holds if gcc_check/1 is later rewritten to
+        % queue and accumulates constraints in the queue. Do we need
-        % actually disable the queue.
+        % to insert a call of do_queue//0 here to reach a fixpoint?  I
-        with_local_attributes(Vs,
+        % think not, because verify_attributes/3 gives each variable
+        % that is involved in a unification an opportunity to schedule
+        % its propagators, even if the unifications happen
+        % simultaneously (such as [A,B] = [0,1], which can happen in
+        % the propagator of tuples_in/2). Hence: We need this only if
+        % an example shows it, ideally found by a systematic search
+        % that can be used to test the implementation.
+        { with_local_attributes(Vs,
               (gcc_arcs(KNs, S, Vals),
                variables_with_num_occurrences(Vs, VNs),
                maplist(target_to_v(T), VNs),
@@ -6805,9 +6819,9 @@ gcc_global(Vs, KNs) :-
                    gcc_consistent(T),
                    scc(Vals, gcc_successors),
                    phrase(gcc_goals(Vals), Gs)
-               ;   Gs = [] )), Gs),
+               ;   Gs = [] )), Gs) },
         disable_queue,
-        maplist(call, Gs),
+        neq_nums(Gs),
         enable_queue.
 
 gcc_consistent(T) :-
@@ -6834,7 +6848,7 @@ gcc_edge_goal(arc_to(_,_,V,F), Val) -->
               get_attr(Val, lowlink, L2),
               L1 =\= L2,
               get_attr(Val, value, Value) } ->
-            [clpz:neq_num(V, Value)]
+            [neq_num(V, Value)]
         ;   []
         ).
 
@@ -7004,7 +7018,7 @@ gcc_succ_edge(arc_from(_,_,V,F)) -->
    consistency.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
-gcc_check(Pairs) :-
+gcc_check(Pairs) -->
         disable_queue,
         gcc_check_(Pairs),
         enable_queue.
@@ -7014,36 +7028,36 @@ gcc_done(Num) :-
         del_attr(Num, clpz_gcc_num),
         del_attr(Num, clpz_gcc_occurred).
 
-gcc_check_([]).
+gcc_check_([]) --> [].
-gcc_check_([Key-Num0|KNs]) :-
+gcc_check_([Key-Num0|KNs]) -->
-        (   get_attr(Num0, clpz_gcc_vs, Vs) ->
+        (   { get_attr(Num0, clpz_gcc_vs, Vs) } ->
-            get_attr(Num0, clpz_gcc_num, Num),
+            { get_attr(Num0, clpz_gcc_num, Num),
               get_attr(Num0, clpz_gcc_occurred, Occ0),
               vs_key_min_others(Vs, Key, 0, Min, Os),
               put_attr(Num0, clpz_gcc_vs, Os),
               put_attr(Num0, clpz_gcc_occurred, Occ1),
-            Occ1 is Occ0 + Min,
+              Occ1 is Occ0 + Min },
             geq(Num, Occ1),
             % The queue is disabled for efficiency here in any case.
             % If it were enabled, make sure to retain the invariant
             % that gcc_global is never triggered during an
             % inconsistent state (after gcc_done/1 but before all
             % relevant constraints are posted).
-            (   Occ1 == Num -> all_neq(Os, Key), gcc_done(Num0)
+            (   Occ1 == Num -> all_neq(Os, Key), { gcc_done(Num0) }
-            ;   Os == [] -> gcc_done(Num0), Num = Occ1
+            ;   Os == [] -> { gcc_done(Num0) }, Num = Occ1
-            ;   length(Os, L),
+            ;   { length(Os, L),
-                Max is Occ1 + L,
+                  Max is Occ1 + L },
                 geq(Max, Num),
-                (   nonvar(Num) -> Diff is Num - Occ1
+                (   { nonvar(Num) } -> Diff is Num - Occ1
-                ;   fd_get(Num, ND, _),
+                ;   { fd_get(Num, ND, _),
-                    domain_infimum(ND, n(NInf)),
+                      domain_infimum(ND, n(NInf)) },
                     Diff is NInf - Occ1
                 ),
                 L >= Diff,
                 (   L =:= Diff ->
                     Num is Occ1 + Diff,
-                    maplist(=(Key), Os),
+                    { maplist(=(Key), Os),
-                    gcc_done(Num0)
+                      gcc_done(Num0) }
                 ;   true
                 )
             )

src/lib/crypto.pl

@@ -25,6 +25,7 @@
            crypto_password_hash/3,       % +Password, -Hash, +Options
            crypto_data_encrypt/6,        % +PlainText, +Algorithm, +Key, +IV, -CipherText, +Options
            crypto_data_decrypt/6,        % +CipherText, +Algorithm, +Key, +IV, -PlainText, +Options
+           ed25519_seed_keypair/2,       % +Seed, -KeyPair
            ed25519_new_keypair/1,        % -KeyPair
            ed25519_keypair_public_key/2, % +KeyPair, +PublicKey
            ed25519_sign/4,               % +KeyPair, +Data, -Signature, +Options
@@ -612,6 +613,50 @@ encoding_chars(utf8, Cs, Cs) :-
    ===============================
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
+%% ed25519_seed_keypair(+Seed, -Pair)
+%
+% Use Seed to deterministically generate an Ed25519 key pair Pair, a
+% list of characters. Seed must be a list of 32 bytes.  It can be
+% chosen at random (using for example `crypto_n_random_bytes/2`) or
+% derived from input keying material (IKM) using for example
+% `crypto_data_hkdf/4`.  The pair contains the private key and must be
+% kept absolutely secret.  Pair can be used for signing. Its public
+% key can be obtained with `ed25519_keypair_public_key/2`.
+
+ed25519_seed_keypair(Seed, Pair) :-
+        must_be_bytes(Seed, ed25519_keypair_from_seed/2),
+        length(Seed, 32),
+        '$ed25519_seed_to_public_key'(Seed, Public),
+        maplist(char_code, Public, PublicBytes),
+        phrase(ed25519_PKCS8v2(Seed,PublicBytes), DERs),
+        maplist(char_code, Pair, DERs).
+
+% DER (and hence BER) encoding of an Ed25519 private key and
+% corresponding public key in PKCS#8v2 format (RFC 5958) as specified
+% in RFC 8410.
+
+ed25519_PKCS8v2(Seed, PublicBytes) -->
+        [0x30,81],    % a SEQUENCE of 81 bytes follows
+
+        % the publicKey is present, hence we set version to v2
+        [2,1,1],      % the integer 1 denoting version 2 (awesome design!)
+
+        % privateKeyAlgorithm: SEQUENCE
+        [0x30,5],     % a SEQUENCE of 5 bytes follows
+        [6,3],        % an OBJECT IDENTIFIER of 3 bytes follows
+        [43,101,112], % OID of Ed25519
+
+        % privateKey: OCTET STRING
+        [4,34],       % an OCTET STRING of 34 bytes follows
+        [4,32],       % an OCTET STRING of 32 bytes follows
+        seq(Seed),    % the seed is the private key
+
+        % publicKey: [1] IMPLICIT BIT STRING; context-specific, hence bit 7 set
+        [0b10000001], % the public key follows
+        [33],         % a BIT STRING of length 33 follows
+        [0],          % 32 bytes is divisible by 8, hence 0 unused bits
+        seq(PublicBytes).
+
 %% ed25519_new_keypair(-Pair)
 %
 %  Yields a new Ed25519 key pair Pair, a list of characters. The
@@ -620,7 +665,8 @@ encoding_chars(utf8, Cs, Cs) :-
 %  with `ed25519_keypair_public_key/2`.
 
 ed25519_new_keypair(Pair) :-
-        '$ed25519_new_keypair'(Pair).
+        crypto_n_random_bytes(32, Bytes),
+        ed25519_seed_keypair(Bytes, Pair).
 
 %% ed25519_keypair_public_key(+Pair, -PublicKey)
 %
@@ -629,8 +675,11 @@ ed25519_new_keypair(Pair) :-
 %  The public key is represented as a list of characters.
 
 ed25519_keypair_public_key(Pair, PublicKey) :-
-        must_be_octet_chars(Pair, ed25519_keypair_public_key),
+        must_be_octet_chars(Pair, ed25519_keypair_public_key/2),
-        '$ed25519_keypair_public_key'(Pair, PublicKey).
+        reverse(Pair, RPs),
+        length(RPublicKey, 32),
+        phrase((seq(RPublicKey),...), RPs),
+        reverse(RPublicKey, PublicKey).
 
 %% ed25519_sign(+Key, +Data, -Signature, +Options)
 %
@@ -638,10 +687,14 @@ ed25519_keypair_public_key(Pair, PublicKey) :-
 %  PKCS#8 v2 format as generated by `ed25519_new_keypair/1`. Sign Data
 %  with Key, yielding Signature as a list of hexadecimal characters.
 
-ed25519_sign(Key, Data0, Signature, Options) :-
+ed25519_sign(KeyPair, Data0, Signature, Options) :-
-        must_be_octet_chars(Key, ed25519_sign),
+        must_be_octet_chars(KeyPair, ed25519_sign/4),
+        length(Prefix, 16),
+        length(PrivateKeyChars, 32),
+        phrase((seq(Prefix),seq(PrivateKeyChars),...), KeyPair),
+        maplist(char_code, PrivateKeyChars, PrivateKey),
         options_data_chars(Options, Data0, Data, Encoding),
-        '$ed25519_sign'(Key, Data, Encoding, Signature0),
+        '$ed25519_sign_raw'(PrivateKey, Data, Encoding, Signature0),
         hex_bytes(Signature, Signature0).
 
 %% ed25519_verify(+Key, +Data, +Signature, +Options)
@@ -658,10 +711,10 @@ ed25519_sign(Key, Data0, Signature, Options) :-
 %    which treats Data as a list of raw bytes.
 
 ed25519_verify(Key, Data0, Signature0, Options) :-
-        must_be_octet_chars(Key, ed25519_verify),
+        must_be_octet_chars(Key, ed25519_verify/4),
         options_data_chars(Options, Data0, Data, Encoding),
         hex_bytes(Signature0, Signature),
-        '$ed25519_verify'(Key, Data, Encoding, Signature).
+        '$ed25519_verify_raw'(Key, Data, Encoding, Signature).
 
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    X25519: ECDH key exchange over Curve25519

src/lib/dcgs.pl

@@ -12,9 +12,12 @@ to learn more about them.
           [op(1105, xfy, '|'),
            phrase/2,
            phrase/3,
+           phrase/4,
+           phrase/5,
            seq//1,
            seqq//1,
-           ... //0
+           ... //0,
+           (-->)/2
           ]).
 
 :- use_module(library(error)).
@@ -26,6 +29,10 @@ to learn more about them.
 
 :- meta_predicate phrase(2, ?, ?).
 
+:- meta_predicate phrase(2, ?, ?, ?).
+
+:- meta_predicate phrase(2, ?, ?, ?, ?).
+
 %% phrase(+Body, ?Ls).
 %
 % True iff Body describes the list Ls. Body must be a DCG body.
@@ -75,6 +82,34 @@ phrase(GRBody, S0, S) :-
     ;  call(M:GRBody1, S0, S)
     ).
 
+phrase(GRBody, Arg, S0, S) :-
+    strip_module(GRBody, M, GRBody1),
+    (  var(GRBody) ->
+       instantiation_error(phrase/4)
+    ;  nonvar(GRBody1),
+       GRBody1 =.. GRBodys1,
+       append(GRBodys1, [Arg], GRBodys2),
+       GRBody2 =.. GRBodys2,
+       dcg_constr(GRBody2),
+       dcg_body(GRBody2, S0, S, GRBody3) ->
+       call(M:GRBody3)
+    ;  call(M:GRBody1, Arg, S0, S)
+    ).
+
+phrase(GRBody, Arg1, Arg2, S0, S) :-
+    strip_module(GRBody, M, GRBody1),
+    (  var(GRBody) ->
+       instantiation_error(phrase/5)
+    ;  nonvar(GRBody1),
+       GRBody1 =.. GRBodys1,
+       append(GRBodys1, [Arg1,Arg2], GRBodys2),
+       GRBody2 =.. GRBodys2,
+       dcg_constr(GRBody2),
+       dcg_body(GRBody2, S0, S, GRBody3) ->
+       call(M:GRBody3)
+    ;  call(M:GRBody1, Arg1, Arg2, S0, S)
+    ).
+
 % The same version of the below two dcg_rule clauses, but with module scoping.
 dcg_rule(( M:NonTerminal, Terminals --> GRBody ), ( M:Head :- Body )) :-
     dcg_non_terminal(NonTerminal, S0, S, Head),
@@ -101,7 +136,10 @@ dcg_rule(( NonTerminal --> GRBody ), ( Head :- Body )) :-
 dcg_non_terminal(NonTerminal, S0, S, Goal) :-
     NonTerminal =.. NonTerminalUniv,
     append(NonTerminalUniv, [S0, S], GoalUniv),
-    Goal =.. GoalUniv.
+    (  callable(NonTerminal) ->
+       Goal =.. GoalUniv
+    ;  Goal = NonTerminal % let call/N throw an error instead of throwing one here.
+    ).
 
 dcg_terminals(Terminals, S0, S, S0 = List) :-
     append(Terminals, S, List).
@@ -116,8 +154,6 @@ dcg_body(GRBody, S0, S, Body) :-
 dcg_body(NonTerminal, S0, S, Goal1) :-
     nonvar(NonTerminal),
     \+ dcg_constr(NonTerminal),
-    NonTerminal \= ( _ -> _ ),
-    NonTerminal \= ( \+ _ ),
     loader:strip_module(NonTerminal, M, NonTerminal0),
     dcg_non_terminal(NonTerminal0, S0, S, Goal0),
     (  functor(NonTerminal, (:), 2) ->
@@ -135,9 +171,13 @@ dcg_constr(( _'|'_ )). % 7.14.6 - alternative
 dcg_constr({_}). % 7.14.7
 dcg_constr(call(_)). % 7.14.8
 dcg_constr(phrase(_)). % 7.14.9
+dcg_constr(phrase(_,_)). % extension of 7.14.9
+dcg_constr(phrase(_,_,_)). % extension of 7.14.9
 dcg_constr(!). % 7.14.10
-%% dcg_constr(\+ _). % 7.14.11 - not (existence implementation dep.)
+dcg_constr(\+ G_0) :- % 7.14.11 - not (existence implementation def.)
-dcg_constr((_->_)). % 7.14.12 - if-then (existence implementation dep.)
+    throw(error(representation_error(dcg_body), [culprit- (\+ G_0)])).
+dcg_constr((If->Then)) :- % 7.14.12 - if-then (existence implementation def.)
+    throw(error(representation_error(dcg_body), [culprit- (If->Then)])).
 
 % The principal functor of the first argument indicates
 % the construct to be expanded.
@@ -162,8 +202,10 @@ dcg_cbody(( GREither '|' GROr ), S0, S, ( Either ; Or )) :-
 dcg_cbody({Goal}, S0, S, ( Goal, S0 = S )).
 dcg_cbody(call(Cont), S0, S, call(Cont, S0, S)).
 dcg_cbody(phrase(Body), S0, S, phrase(Body, S0, S)).
+dcg_cbody(phrase(Body, Arg), S0, S, phrase(Body, Arg, S0, S)).
+dcg_cbody(phrase(Body, Arg1, Arg2), S0, S, phrase(Body, Arg1, Arg2, S0, S)).
 dcg_cbody(!, S0, S, ( !, S0 = S )).
-dcg_cbody(\+ GRBody, S0, S, ( \+ phrase(GRBody,S0,_), S0 = S )).
+% dcg_cbody(\+ GRBody, S0, S, ( \+ phrase(GRBody,S0,_), S0 = S )).
 dcg_cbody(( GRIf -> GRThen ), S0, S, ( If -> Then )) :-
     dcg_body(GRIf, S0, S1, If),
     dcg_body(GRThen, S1, S, Then).
@@ -202,6 +244,8 @@ seqq([Es|Ess]) --> seq(Es), seqq(Ess).
 
 error_goal(error(E, must_be/2), error(E, must_be/2)).
 error_goal(error(E, (=..)/2), error(E, (=..)/2)).
+error_goal(error(representation_error(dcg_body), Context),
+           error(representation_error(dcg_body), Context)).
 error_goal(E, _) :- throw(E).
 
 user:goal_expansion(phrase(GRBody, S, S0), GRBody2) :-
@@ -217,3 +261,10 @@ user:goal_expansion(phrase(GRBody, S, S0), GRBody2) :-
     ).
 
 user:goal_expansion(phrase(GRBody, S), phrase(GRBody, S, [])).
+
+
+% (-->)/2 behaves as if it didn't exist. We export (and define) it
+% only so that clauses for (-->)/2 cannot be asserted when
+% library(dcgs) is loaded.
+
+(_-->_) :- throw(error(existence_error(procedure,(-->)/2),(-->)/2)).

src/lib/files.pl

@@ -178,7 +178,7 @@ directory_must_exist(Directory, Context) :-
         ;   throw(error(existence_error(directory, Directory), Context))
         ).
 
-%% workind_directory(Dir0, Dir).
+%% working_directory(Dir0, Dir).
 %
 % Dir0 is the current working directory, and the working directory
 % is changed to Dir.

src/lib/format.pl

@@ -1,5 +1,5 @@
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-   Written 2020-2023 by Markus Triska (triska@metalevel.at)
+   Written 2020-2024 by Markus Triska (triska@metalevel.at)
    Part of Scryer Prolog.
    I place this code in the public domain. Use it in any way you want.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
@@ -302,14 +302,14 @@ format_number_chars(N0, Chars) :-
         N is N0, % evaluate compound expression
         number_chars(N, Chars).
 
-n_newlines(0) --> !.
 n_newlines(N0) --> { N0 > 0, N is N0 - 1 }, [newline], n_newlines(N).
+n_newlines(0)  --> [].
 
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-?- phrase(upto_what(Cs, ~), "abc~test", Rest).
+?- phrase(format:upto_what(Cs, ~), "abc~test", Rest).
-Cs = [a,b,c], Rest = [~,t,e,s,t].
+   Cs = "abc", Rest = "~test".
-?- phrase(upto_what(Cs, ~), "abc", Rest).
+?- phrase(format:upto_what(Cs, ~), "abc", Rest).
-Cs = [a,b,c], Rest = [].
+   Cs = "abc", Rest = [].
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
 separate_digits_fractional(Arg, Sep, Num, Cs) :-
@@ -444,9 +444,9 @@ format(Stream, Fs, Args) :-
 ?- phrase(format:cells("~`at~50|", [], 0, [], []), Cs),
    phrase(format:format_cells(Cs), Ls).
 ?- phrase(format:cells("~ta~t~tb~tc~21|", [], 0, [], []), Cs).
-Cs = [cell(0,21,[glue(' ',_A),chars("a"),glue(' ',_B),glue(' ',_C),chars("b"),glue(' ',_D),chars("c ...")])]
+   Cs = [cell(0,21,[glue(' ',_A),chars("a"),glue(' ',_B),glue(' ',_C),chars("b"),glue(' ',_D),chars("c")])].
 ?- phrase(format:cells("~ta~t~4|", [], 0, [], []), Cs).
-Cs = [cell(0,4,[glue(' ',_A),chars("a"),glue(' ',_B)])]
+   Cs = [cell(0,4,[glue(' ',_A),chars("a"),glue(' ',_B)])].
 
 ?- phrase(format:format_cell(cell(0,1,[glue(a,_94)])), Ls).
 

src/lib/iso_ext.pl

@@ -9,6 +9,7 @@ but they're not part of the ISO Prolog standard at the moment.
                     bb_put/2,
                     call_cleanup/2,
                     call_with_inference_limit/3,
+                    call_residue_vars/2,
                     forall/2,
                     partial_string/1,
                     partial_string/3,
@@ -17,7 +18,8 @@ but they're not part of the ISO Prolog standard at the moment.
                     succ/2,
                     call_nth/2,
                     countall/2,
-                    copy_term_nat/2]).
+                    copy_term_nat/2,
+		    copy_term/3]).
 
 :- use_module(library(error), [can_be/2,
                                domain_error/3,
@@ -26,6 +28,8 @@ but they're not part of the ISO Prolog standard at the moment.
 
 :- use_module(library(lists), [maplist/3]).
 
+:- use_module(library('$project_atts')).
+
 :- meta_predicate(forall(0, 0)).
 
 %% forall(Generate, Test).
@@ -382,3 +386,23 @@ countall(Goal, N) :-
 copy_term_nat(Source, Dest) :-
     '$copy_term_without_attr_vars'(Source, Dest).
 
+%% copy_term(+Term, -Copy, -Gs).
+%
+% Produce a deep copy of Term and unify it to Copy, without attributes.
+% Unify Gs with a list of goals that represent the attributes of Term.
+% Similar to `copy_term/2` but splitting the attributes.
+copy_term(Term, Copy, Gs) :-
+   can_be(list, Gs),
+   findall(Term-Rs, '$project_atts':term_residual_goals(Term,Rs), [Copy-Gs]),
+   (  var(Gs) ->
+      Gs = []
+   ;  true
+   ).
+
+:- meta_predicate call_residue_vars(0, ?).
+
+call_residue_vars(Goal, Vars) :-
+    can_be(list, Vars),
+    '$get_attr_var_queue_delim'(B),
+    call(Goal),
+    '$get_attr_var_queue_beyond'(B, Vars).

src/lib/os.pl

@@ -23,7 +23,9 @@ finding out the PID of the running system.
                unsetenv/1,
                shell/1,
                shell/2,
-               pid/1]).
+               pid/1,
+	       raw_argv/1,
+	       argv/1]).
 
 :- use_module(library(error)).
 :- use_module(library(charsio)).
@@ -110,3 +112,34 @@ permitted('_').
 must_be_chars(Cs) :-
         must_be(list, Cs),
         maplist(must_be(character), Cs).
+
+%% raw_argv(-Argv)
+%
+% True iff Argv is the list of arguments that this program was started with (usually passed via command line).
+% In contrast to `argv/1`, this version includes every argument, without any postprocessing, just as the operating
+% system reports it to the system. This includes-flags of Scryer itself, which are not needed in general.
+raw_argv(Argv) :-
+    can_be(list, Argv),
+    '$argv'(Argv).
+
+%% argv(-Argv)
+%
+% True if Argv is the list of arguments that this program was started with (usually passed via command line).
+% In this version, only arguments specific to the program are passed. To differentiate between the system
+% arguments and the program arguments, we use `--` as a separator.
+%
+% Example:
+%
+% ```
+% % Call with scryer-prolog -f -- -t hello
+% ?- argv(X).
+%     X = ["-t", "hello"].
+% ```
+argv(Argv) :-
+    can_be(list, Argv),
+    '$argv'(Argv0),
+    ( append(_, ["--"|Argv1], Argv0) ->
+        Argv = Argv1
+    ;
+        Argv = []
+    ).

src/lib/si.pl

@@ -39,7 +39,8 @@
                character_si/1,
                term_si/1,
                chars_si/1,
-               dif_si/2]).
+               dif_si/2,
+               when_si/2]).
 
 :- use_module(library(lists)).
 
@@ -98,3 +99,31 @@ dif_si(X, Y) :-
    ( X \= Y -> true
    ; throw(error(instantiation_error,dif_si/2))
    ).
+
+:- meta_predicate(when_si(+, 0)).
+
+%% when_si(Condition, Goal).
+%
+% Executes Goal when Condition becomes true. Throws an instantiation error if
+% it can't decide.
+when_si(Condition, Goal) :-
+    % Taken from https://stackoverflow.com/a/40449516
+    (   when_condition_si(Condition) ->
+        (   Condition ->
+            Goal
+        ;   throw(error(instantiation_error,when_si/2))
+        )
+    ;   throw(error(domain_error(when_condition_si, Condition),_))
+    ).
+
+when_condition_si(Cond) :-
+    var(Cond), !, throw(error(instantiation_error,when_condition_si/2)).
+when_condition_si(ground(_)).
+when_condition_si(nonvar(_)).
+when_condition_si((A, B)) :-
+    when_condition_si(A),
+    when_condition_si(B).
+when_condition_si((A ; B)) :-
+    when_condition_si(A),
+    when_condition_si(B).
+

src/lib/when.pl

@@ -0,0 +1,106 @@
+/**
+Provides the predicate `when/2`.
+*/
+
+:- module(when, [when/2]).
+
+:- use_module(library(atts)).
+:- use_module(library(dcgs)).
+:- use_module(library(lists)).
+:- use_module(library(lambda)).
+
+:- use_module(library(format)).
+:- use_module(library(debug)).
+
+:- attribute when_list/1.
+
+:- meta_predicate(when(+, 0)).
+
+%% when(Condition, Goal).
+%
+% Executes Goal when Condition becomes true.
+when(Condition, Goal) :-
+    (   when_condition(Condition) ->
+        (   Condition ->
+            Goal
+        ;   term_variables(Condition, Vars),
+            maplist(
+                [Goal, Condition]+\Var^(
+                    get_atts(Var, when_list(Whens0)) ->
+                    Whens = [when(Condition, Goal) | Whens0],
+                    put_atts(Var, when_list(Whens))
+                ;   put_atts(Var, when_list([when(Condition, Goal)]))
+                ),
+                Vars
+            )
+        )
+    ;   throw(error(domain_error(when_condition, Condition),_))
+    ).
+
+when_condition(Cond) :-
+    % Should this be delayed?
+    var(Cond), !, throw(error(instantiation_error,when_condition/1)).
+when_condition(ground(_)).
+when_condition(nonvar(_)).
+when_condition((A, B)) :-
+    when_condition(A),
+    when_condition(B).
+when_condition((A ; B)) :-
+    when_condition(A),
+    when_condition(B).
+
+remove_goal([], _, []).
+remove_goal([G0|G0s], Goal, Goals) :-
+    (   G0 == Goal ->
+        remove_goal(G0s, Goal, Goals)
+    ;   Goals = [G0|Goals1],
+        remove_goal(G0s, Goal, Goals1)
+    ).
+
+vars_remove_goal(Vars, Goal) :-
+    maplist(
+        Goal+\Var^(
+            get_atts(Var, when_list(Whens0)) ->
+            remove_goal(Whens0, Goal, Whens),
+            (   Whens = [] ->
+                put_atts(Var, -when_list(_))
+            ;   put_atts(Var, when_list(Whens))
+            )
+        ;   true
+        ),
+        Vars
+    ).
+
+reinforce_goal(Goal0, Goal) :-
+    Goal = (
+        term_variables(Goal0, Vars),
+        when:vars_remove_goal(Vars, Goal0),
+        Goal0
+    ).
+
+verify_attributes(Var, Value, Goals) :-
+    (   get_atts(Var, when_list(Whens)) ->
+        (   var(Value) ->
+            (   get_atts(Value, when_list(WhensValue)) ->
+                append(Whens, WhensValue, WhensNew),
+                put_atts(Value, when_list(WhensNew))
+            ;   put_atts(Value, when_list(Whens))
+            ),
+            Goals = []
+        ;   maplist(reinforce_goal, Whens, Goals)
+        )
+    ;   Goals = []
+    ).
+
+gather_when_goals([], _) --> [].
+gather_when_goals([When|Whens], Var) -->
+    ( { term_variables(When, [V0|_]), Var == V0 } ->
+        [when:When]
+    ;   []
+    ),
+    gather_when_goals(Whens, Var).
+
+attribute_goals(Var) -->
+    { get_atts(Var, when_list(Whens)) },
+    gather_when_goals(Whens, Var),
+    { put_atts(Var, -when_list(_)) }.

src/loader.pl

@@ -112,7 +112,7 @@ success_or_warning(Goal) :-
     (   call(Goal) ->
         true
     ;   %% initialization goals can fail without thwarting the load.
-        write('Warning: initialization/1 failed for: '),
+        write('% Warning: initialization/1 failed for: '),
         writeq(Goal),
         nl
     ).
@@ -138,7 +138,7 @@ file_load_cleanup(Evacuable, Error) :-
     load_context(Module),
     abolish(Module:'$initialization_goals'/1),
     unload_evacuable(Evacuable),
-    (  clause('$toplevel':argv(_), _) ->
+    (  clause('$toplevel':started, _) ->
        % let the toplevel call loader:write_error/1
        throw(Error)
     ;  '$print_message_and_fail'(Error)
@@ -188,7 +188,7 @@ warn_about_singletons([], _).
 warn_about_singletons([Singleton|Singletons], LinesRead) :-
     (  filter_anonymous_vars([Singleton|Singletons], VarEqs),
        VarEqs \== [] ->
-       write('Warning: singleton variables '),
+       write('% Warning: singleton variables '),
        print_comma_separated_list(VarEqs),
        write(' at line '),
        write(LinesRead),
@@ -231,6 +231,7 @@ complete_partial_goal(N, HeadArg, InnerHeadArgs, SuppArgs, CompleteHeadArg) :-
     integer(N),
     N >= 0,
     HeadArg =.. [Functor | InnerHeadArgs],
+    (  callable(Functor) ->
        % the next two lines are equivalent to length(SuppArgs, N) but
        % avoid length/2 so that copy_term/3 (which is invoked by
        % length/2) can be bootstrapped without self-reference.
@@ -238,7 +239,9 @@ complete_partial_goal(N, HeadArg, InnerHeadArgs, SuppArgs, CompleteHeadArg) :-
        SuppArgsFunctor =.. [_ | SuppArgs],
        % length(SuppArgs, N),
        append(InnerHeadArgs, SuppArgs, InnerHeadArgs0),
-    CompleteHeadArg =.. [Functor | InnerHeadArgs0].
+       CompleteHeadArg =.. [Functor | InnerHeadArgs0]
+    ;  type_error(callable, Functor, _)
+    ).
 
 inner_meta_specs(0, HeadArg, InnerHeadArgs, InnerMetaSpecs) :-
     !,
@@ -283,7 +286,7 @@ module_expanded_head_variables(Head, HeadVars) :-
 
 print_goal_expansion_warning(Pred) :-
     nl,
-    write('Warning: clause body goal expansion failed because '),
+    write('% Warning: clause body goal expansion failed because '),
     writeq(Pred),
     write(' is not callable.'),
     nl.
@@ -296,7 +299,7 @@ expand_term_goals(Terms0, Terms) :-
           (  atom(Module) ->
              prolog_load_context(module, Target),
              module_expanded_head_variables(Head2, HeadVars),
-             catch(expand_goal(Body0, Target, Body1, HeadVars),
+             catch(expand_goal(Body0, Target, Body1, HeadVars, []),
                    error(type_error(callable, Pred), _),
                    (  loader:print_goal_expansion_warning(Pred),
                       builtins:(Body1 = Body0)
@@ -306,7 +309,7 @@ expand_term_goals(Terms0, Terms) :-
           )
        ;  module_expanded_head_variables(Head1, HeadVars),
           prolog_load_context(module, Target),
-          catch(expand_goal(Body0, Target, Body1, HeadVars),
+          catch(expand_goal(Body0, Target, Body1, HeadVars, []),
                 error(type_error(callable, Pred), _),
                 (  loader:print_goal_expansion_warning(Pred),
                    builtins:(Body1 = Body0)
@@ -726,9 +729,9 @@ subgoal_expansion(Goal, Module, ExpandedGoal) :-
     ).
 
 
-:- non_counted_backtracking expand_subgoal/5.
+:- non_counted_backtracking expand_subgoal/6.
 
-expand_subgoal(UnexpandedGoals, MS, M, ExpandedGoals, HeadVars) :-
+expand_subgoal(UnexpandedGoals, MS, M, ExpandedGoals, HeadVars, TGs) :-
     strip_subst_module(UnexpandedGoals, M, Module, UnexpandedGoals0),
     nonvar(UnexpandedGoals0),
     complete_partial_goal(MS, UnexpandedGoals0, _, SuppArgs, UnexpandedGoals1),
@@ -740,7 +743,7 @@ expand_subgoal(UnexpandedGoals, MS, M, ExpandedGoals, HeadVars) :-
     ),
     strip_subst_module(UnexpandedGoals3, Module, Module1, UnexpandedGoals4),
     (  inner_meta_specs(0, UnexpandedGoals4, _, MetaSpecs) ->
-       expand_module_names(UnexpandedGoals4, MetaSpecs, Module1, ExpandedGoals0, HeadVars)
+       expand_module_names(UnexpandedGoals4, MetaSpecs, Module1, ExpandedGoals0, HeadVars, TGs)
     ;  ExpandedGoals0 = UnexpandedGoals4
     ),
     '$compile_inline_or_expanded_goal'(ExpandedGoals0, SuppArgs, ExpandedGoals1, Module1, UnexpandedGoals0),
@@ -769,10 +772,10 @@ expand_module_name(ESG0, MS, M, ESG) :-
 
 :- non_counted_backtracking eq_member/2.
 
-eq_member(V, [L-_|Ls]) :-
+eq_member(V-M, [L-M|Ls]) :-
     V == L.
-eq_member(V, [_|Ls]) :-
+eq_member(V-M, [_|Ls]) :-
-    eq_member(V, Ls).
+    eq_member(V-M, Ls).
 
 :- non_counted_backtracking qualified_spec/1.
 
@@ -782,11 +785,19 @@ qualified_spec(MS) :- integer(MS), MS >= 0.
 
 :- non_counted_backtracking expand_meta_predicate_subgoals/5.
 
-expand_meta_predicate_subgoals([SG | SGs], [MS | MSs], M, [ESG | ESGs], HeadVars) :-
+expand_meta_predicate_subgoals([SG | SGs], [MS | MSs], M, [ESG | ESGs], HeadVars, TGs) :-
     (  var(SG) ->
        (  qualified_spec(MS) ->
-          (  eq_member(SG, HeadVars) ->
+          (  eq_member(SG-_, HeadVars) ->
              ESG = SG
+          ;  eq_member(SG-TG, TGs),
+             % transitive goals come about from previous equalities:
+             % if SG was bound by (=)/2 to a potential goal TG earlier
+             % in the goal sequence, expand TG and substitute SG with it
+             % in this subgoal context. the binding to SG must not be
+             % changed.
+             expand_subgoal(TG, MS, M, ESG, HeadVars, TGs) ->
+             true
           ;  expand_module_name(SG, MS, M, ESG)
           )
        ;  ESG = SG
@@ -795,26 +806,26 @@ expand_meta_predicate_subgoals([SG | SGs], [MS | MSs], M, [ESG | ESGs], HeadVars
        expand_module_name(SG, MS, M, ESG)
     ;  '$is_expanded_or_inlined'(SG) ->
        ESG = SG
-    ;  expand_subgoal(SG, MS, M, ESG, HeadVars) ->
+    ;  expand_subgoal(SG, MS, M, ESG, HeadVars, TGs) ->
        true
     ;  integer(MS),
        MS >= 0 ->
        expand_module_name(SG, MS, M, ESG)
     ;  SG = ESG
     ),
-    expand_meta_predicate_subgoals(SGs, MSs, M, ESGs, HeadVars).
+    expand_meta_predicate_subgoals(SGs, MSs, M, ESGs, HeadVars, TGs).
 
-expand_meta_predicate_subgoals([], _, _, [], _).
+expand_meta_predicate_subgoals([], _, _, [], _, _).
 
-:- non_counted_backtracking expand_module_names/5.
+:- non_counted_backtracking expand_module_names/6.
 
-expand_module_names(Goals, MetaSpecs, Module, ExpandedGoals, HeadVars) :-
+expand_module_names(Goals, MetaSpecs, Module, ExpandedGoals, HeadVars, TGs) :-
     Goals =.. [GoalFunctor | SubGoals],
     (  GoalFunctor == (:),
        SubGoals = [M, SubGoal] ->
-       expand_module_names(SubGoal, MetaSpecs, M, ExpandedSubGoal, HeadVars),
+       expand_module_names(SubGoal, MetaSpecs, M, ExpandedSubGoal, HeadVars, TGs),
        expand_module_name(ExpandedSubGoal, 0, M, ExpandedGoals)
-    ;  expand_meta_predicate_subgoals(SubGoals, MetaSpecs, Module, ExpandedGoalList, HeadVars),
+    ;  expand_meta_predicate_subgoals(SubGoals, MetaSpecs, Module, ExpandedGoalList, HeadVars, TGs),
        ExpandedGoals =.. [GoalFunctor | ExpandedGoalList]
     ).
 
@@ -822,26 +833,26 @@ expand_module_names(Goals, MetaSpecs, Module, ExpandedGoals, HeadVars) :-
 :- non_counted_backtracking expand_goal/3.
 
 expand_goal(UnexpandedGoals, Module, ExpandedGoals) :-
-    catch(loader:expand_goal(UnexpandedGoals, Module, ExpandedGoals, []),
+    catch(loader:expand_goal(UnexpandedGoals, Module, ExpandedGoals, [], []),
           error(type_error(callable, _), _),
           UnexpandedGoals = ExpandedGoals),
     !.
 
-:- non_counted_backtracking expand_goal/4.
+:- non_counted_backtracking expand_goal/5.
 
-expand_goal(UnexpandedGoals, Module, ExpandedGoals, HeadVars) :-
+expand_goal(UnexpandedGoals, Module, ExpandedGoals, HeadVars, TGs) :-
     (  var(UnexpandedGoals) ->
-       expand_module_names(call(UnexpandedGoals), [0], Module, ExpandedGoals, HeadVars)
+       expand_module_names(call(UnexpandedGoals), [0], Module, ExpandedGoals, HeadVars, TGs)
     ;  goal_expansion(UnexpandedGoals, Module, UnexpandedGoals1),
        (  Module \== user ->
           goal_expansion(UnexpandedGoals1, user, Goals)
        ;  Goals = UnexpandedGoals1
        ),
-       (  expand_goal_cases(Goals, Module, ExpandedGoals, HeadVars) ->
+       (  expand_goal_cases(Goals, Module, ExpandedGoals, HeadVars, TGs) ->
           true
        ;  predicate_property(Module:Goals, meta_predicate(MetaSpecs0)),
           MetaSpecs0 =.. [_ | MetaSpecs] ->
-          expand_module_names(Goals, MetaSpecs, Module, ExpandedGoals, HeadVars)
+          expand_module_names(Goals, MetaSpecs, Module, ExpandedGoals, HeadVars, TGs)
        ;  thread_goals(Goals, ExpandedGoals, (','))
        ;  Goals = ExpandedGoals
        )
@@ -874,28 +885,40 @@ expand_call_goal_(UnexpandedGoals, Module, ExpandedGoals) :-
        )
     ).
 
-:- non_counted_backtracking expand_goal_cases/4.
+:- non_counted_backtracking transitive_goal/3.
 
-expand_goal_cases((Goal0, Goals0), Module, ExpandedGoals, HeadVars) :-
+transitive_goal(G, TGs0, TGs1) :-
-    (  expand_goal(Goal0, Module, Goal1, HeadVars) ->
+    (  G = (G1 = PotentialGoal),
-       expand_goal(Goals0, Module, Goals1, HeadVars),
+       callable(PotentialGoal),
+       subsumes_term(G1, PotentialGoal) ->
+       TGs1 = [G1-PotentialGoal|TGs0]
+    ;  TGs1 = TGs0
+    ).
+
+:- non_counted_backtracking expand_goal_cases/5.
+
+expand_goal_cases((Goal0, Goals0), Module, ExpandedGoals, HeadVars, TGs) :-
+    (  expand_goal(Goal0, Module, Goal1, HeadVars, TGs) ->
+       transitive_goal(Goal0, TGs, TGs1),
+       expand_goal(Goals0, Module, Goals1, HeadVars, TGs1),
        thread_goals(Goal1, ExpandedGoals, Goals1, (','))
-    ;  expand_goal(Goals0, Module, Goals1, HeadVars),
+    ;  expand_goal(Goals0, Module, Goals1, HeadVars, TGs),
        ExpandedGoals = (Goal0, Goals1)
     ).
-expand_goal_cases((Goals0 -> Goals1), Module, ExpandedGoals, HeadVars) :-
+expand_goal_cases((Goals0 -> Goals1), Module, ExpandedGoals, HeadVars, TGs) :-
-    expand_goal(Goals0, Module, ExpandedGoals0, HeadVars),
+    expand_goal(Goals0, Module, ExpandedGoals0, HeadVars, TGs),
-    expand_goal(Goals1, Module, ExpandedGoals1, HeadVars),
+    transitive_goal(ExpandedGoals0, TGs, TGs1),
+    expand_goal(Goals1, Module, ExpandedGoals1, HeadVars, TGs1),
     ExpandedGoals = (ExpandedGoals0 -> ExpandedGoals1).
-expand_goal_cases((Goals0 ; Goals1), Module, ExpandedGoals, HeadVars) :-
+expand_goal_cases((Goals0 ; Goals1), Module, ExpandedGoals, HeadVars, TGs) :-
-    expand_goal(Goals0, Module, ExpandedGoals0, HeadVars),
+    expand_goal(Goals0, Module, ExpandedGoals0, HeadVars, TGs),
-    expand_goal(Goals1, Module, ExpandedGoals1, HeadVars),
+    expand_goal(Goals1, Module, ExpandedGoals1, HeadVars, TGs),
     ExpandedGoals = (ExpandedGoals0 ; ExpandedGoals1).
-expand_goal_cases((\+ Goals0), Module, ExpandedGoals, HeadVars) :-
+expand_goal_cases((\+ Goals0), Module, ExpandedGoals, HeadVars, TGs) :-
-    expand_goal(Goals0, Module, Goals1, HeadVars),
+    expand_goal(Goals0, Module, Goals1, HeadVars, TGs),
     ExpandedGoals = (\+ Goals1).
-expand_goal_cases((Module:Goals0), _, ExpandedGoals, HeadVars) :-
+expand_goal_cases((Module:Goals0), _, ExpandedGoals, HeadVars, TGs) :-
-    expand_goal(Goals0, Module, Goals1, HeadVars),
+    expand_goal(Goals0, Module, Goals1, HeadVars, TGs),
     ExpandedGoals = (Module:Goals1).
 
 :- non_counted_backtracking thread_goals/3.

src/machine/arithmetic_ops.rs

@@ -1423,6 +1423,7 @@ mod tests {
     use crate::machine::mock_wam::*;
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn arith_eval_by_metacall_tests() {
         let mut wam = MachineState::new();
         let mut op_dir = default_op_dir();

src/machine/compile.rs

@@ -42,42 +42,35 @@ pub(super) fn bootstrapping_compile(
     Ok(())
 }
 
-fn lower_bound_of_target_clause(skeleton: &PredicateSkeleton, target_pos: usize) -> usize {
+fn lower_bound_of_target_clause(skeleton: &mut PredicateSkeleton, target_pos: usize) -> usize {
     if target_pos == 0 {
         return 0;
     }
 
-    let arg_num = skeleton.clauses[target_pos - 1].opt_arg_index_key.arg_num();
+    debug_assert!(skeleton.clauses.len() >= 2);
 
-    if arg_num == 0 {
+    let index = target_pos - 1;
-        return target_pos - 1;
-    }
 
-    let mut index_loc_opt = None;
+    let index = if let Some(index_loc) = skeleton.clauses[index]
-
-    for index in (0..target_pos).rev() {
-        let current_arg_num = skeleton.clauses[index].opt_arg_index_key.arg_num();
-
-        if current_arg_num == 0 || current_arg_num != arg_num {
-            return index + 1;
-        }
-
-        if let Some(index_loc) = index_loc_opt {
-            let current_index_loc = skeleton.clauses[index]
         .opt_arg_index_key
-                .switch_on_term_loc();
+        .switch_on_term_loc()
+    {
+        let search_result = skeleton.clauses.make_contiguous()
+            [0..skeleton.core.clause_assert_margin]
+            .partition_point(|clause_index_info| clause_index_info.clause_start > index_loc);
 
-            if Some(index_loc) != current_index_loc {
+        if search_result < skeleton.core.clause_assert_margin {
-                return index + 1;
+            search_result
+        } else {
+            skeleton.clauses.make_contiguous()[skeleton.core.clause_assert_margin..]
+                .partition_point(|clause_index_info| clause_index_info.clause_start < index_loc)
+                + skeleton.core.clause_assert_margin
         }
     } else {
-            index_loc_opt = skeleton.clauses[index]
+        index
-                .opt_arg_index_key
+    };
-                .switch_on_term_loc();
-        }
-    }
 
-    0
+    index.clamp(0, skeleton.clauses.len() - 2)
 }
 
 fn derelictize_try_me_else(
@@ -1215,7 +1208,7 @@ fn print_overwrite_warning(
     }
 
     println!(
-        "Warning: overwriting {}/{} because the clauses are discontiguous",
+        "% Warning: overwriting {}/{} because the clauses are discontiguous",
         key.0.as_str(),
         key.1
     );
@@ -1327,7 +1320,8 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
                         .clause_clause_locs
                         .extend(&clause_clause_locs.make_contiguous()[0..]);
 
-                    let skeleton = cg.skeleton;
+                    let mut skeleton = cg.skeleton;
+                    skeleton.core.is_dynamic = settings.is_dynamic();
 
                     self.add_extensible_predicate(key, skeleton, predicates.compilation_target);
                 }
@@ -1527,6 +1521,8 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
 
         let code_len = self.wam_prelude.code.len();
 
+        standalone_skeleton.clauses[0].clause_start += code_len;
+
         let skeleton = match self
             .wam_prelude
             .indices
@@ -1539,8 +1535,8 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
         match append_or_prepend {
             AppendOrPrepend::Append => {
                 let clause_index_info = standalone_skeleton.clauses.pop_back().unwrap();
-                skeleton.clauses.push_back(clause_index_info);
 
+                skeleton.clauses.push_back(clause_index_info);
                 skeleton.core.clause_clause_locs.push_back(code_len);
 
                 self.payload
@@ -2148,7 +2144,7 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
             .map(|skeleton| skeleton.predicate_info())
             .unwrap_or_default();
 
-        let mut predicate_info = self
+        let predicate_info = self
             .wam_prelude
             .indices
             .get_predicate_skeleton(&self.payload.predicates.compilation_target, &key)
@@ -2183,7 +2179,7 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
             if is_cross_module_clause && !local_predicate_info.is_extensible {
                 if predicate_info.is_multifile {
                     println!(
-                        "Warning: overwriting multifile predicate {}:{}/{} because \
+                        "% Warning: overwriting multifile predicate {}:{}/{} because \
                               it was not locally declared multifile.",
                         self.payload.predicates.compilation_target,
                         key.0.as_str(),
@@ -2210,8 +2206,6 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
                             (0..skeleton.clauses.len()).map(Some).collect(),
                             false, // the builtin M:'$clause'/2 is never dynamic.
                         );
-
-                        predicate_info.is_dynamic = false;
                     }
 
                     self.payload

src/machine/copier.rs

@@ -398,6 +398,7 @@ mod tests {
     use crate::machine::mock_wam::*;
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on atom_table.rs UB")]
     fn copier_tests() {
         let mut wam = MockWAM::new();
 

src/machine/dispatch.rs

@@ -557,20 +557,29 @@ impl Machine {
                         }
 
                         let mut p = self.machine_st.p;
+                        let mut arity = 0;
 
                         while self.code[p].is_head_instr() {
+                            for r in self.code[p].registers() {
+                                if let RegType::Temp(t) = r {
+                                    arity = std::cmp::max(arity, t);
+                                }
+                            }
+
                             p += 1;
                         }
 
-                        let instr =
+                        let instr = std::mem::replace(
-                            std::mem::replace(&mut self.code[p], Instruction::VerifyAttrInterrupt);
+                            &mut self.code[p],
+                            Instruction::VerifyAttrInterrupt(arity),
+                        );
 
                         self.code[VERIFY_ATTR_INTERRUPT_LOC] = instr;
                         self.machine_st.attr_var_init.cp = p;
                     }
-                    &Instruction::VerifyAttrInterrupt => {
+                    &Instruction::VerifyAttrInterrupt(arity) => {
-                        let (_, arity) = self.code[VERIFY_ATTR_INTERRUPT_LOC].to_name_and_arity();
+                        // let (_, arity) = self.code[VERIFY_ATTR_INTERRUPT_LOC].to_name_and_arity();
-                        let arity = std::cmp::max(arity, self.machine_st.num_of_args);
+                        // let arity = std::cmp::max(arity, self.machine_st.num_of_args);
                         self.run_verify_attr_interrupt(arity);
                     }
                     &Instruction::Add(ref a1, ref a2, t) => {
@@ -4147,6 +4156,14 @@ impl Machine {
                         try_or_throw!(self.machine_st, self.js_eval());
                         step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
                     }
+                    &Instruction::CallArgv => {
+                        try_or_throw!(self.machine_st, self.argv());
+                        step_or_fail!(self, self.machine_st.p += 1);
+                    }
+                    &Instruction::ExecuteArgv => {
+                        try_or_throw!(self.machine_st, self.argv());
+                        step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
+                    }
                     &Instruction::CallCurrentTime => {
                         self.current_time();
                         step_or_fail!(self, self.machine_st.p += 1);
@@ -4491,44 +4508,28 @@ impl Machine {
                         self.crypto_curve_scalar_mult();
                         step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
                     }
-                    #[cfg(feature = "crypto-full")]
+                    &Instruction::CallEd25519SignRaw => {
-                    &Instruction::CallEd25519Sign => {
+                        self.ed25519_sign_raw();
-                        self.ed25519_sign();
                         step_or_fail!(self, self.machine_st.p += 1);
                     }
-                    #[cfg(feature = "crypto-full")]
+                    &Instruction::ExecuteEd25519SignRaw => {
-                    &Instruction::ExecuteEd25519Sign => {
+                        self.ed25519_sign_raw();
-                        self.ed25519_sign();
                         step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
                     }
-                    #[cfg(feature = "crypto-full")]
+                    &Instruction::CallEd25519VerifyRaw => {
-                    &Instruction::CallEd25519Verify => {
+                        self.ed25519_verify_raw();
-                        self.ed25519_verify();
                         step_or_fail!(self, self.machine_st.p += 1);
                     }
-                    #[cfg(feature = "crypto-full")]
+                    &Instruction::ExecuteEd25519VerifyRaw => {
-                    &Instruction::ExecuteEd25519Verify => {
+                        self.ed25519_verify_raw();
-                        self.ed25519_verify();
                         step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
                     }
-                    #[cfg(feature = "crypto-full")]
+                    &Instruction::CallEd25519SeedToPublicKey => {
-                    &Instruction::CallEd25519NewKeyPair => {
+                        self.ed25519_seed_to_public_key();
-                        self.ed25519_new_key_pair();
                         step_or_fail!(self, self.machine_st.p += 1);
                     }
-                    #[cfg(feature = "crypto-full")]
+                    &Instruction::ExecuteEd25519SeedToPublicKey => {
-                    &Instruction::ExecuteEd25519NewKeyPair => {
+                        self.ed25519_seed_to_public_key();
-                        self.ed25519_new_key_pair();
-                        step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
-                    }
-                    #[cfg(feature = "crypto-full")]
-                    &Instruction::CallEd25519KeyPairPublicKey => {
-                        self.ed25519_key_pair_public_key();
-                        step_or_fail!(self, self.machine_st.p += 1);
-                    }
-                    #[cfg(feature = "crypto-full")]
-                    &Instruction::ExecuteEd25519KeyPairPublicKey => {
-                        self.ed25519_key_pair_public_key();
                         step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
                     }
                     &Instruction::CallCurve25519ScalarMult => {

src/machine/gc.rs

@@ -369,6 +369,7 @@ mod tests {
     use crate::machine::mock_wam::*;
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn heap_marking_tests() {
         let mut wam = MockWAM::new();
 

src/machine/lib_machine.rs

@@ -236,6 +236,7 @@ mod tests {
     use crate::machine::{QueryMatch, QueryResolution, Value};
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn programatic_query() {
         let mut machine = Machine::new_lib();
 
@@ -275,6 +276,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn failing_query() {
         let mut machine = Machine::new_lib();
         let query = String::from(r#"triple("a",P,"b")."#);
@@ -288,6 +290,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore)]
     fn complex_results() {
         let mut machine = Machine::new_lib();
         machine.load_module_string(
@@ -344,6 +347,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn empty_predicate() {
         let mut machine = Machine::new_lib();
         machine.load_module_string(
@@ -359,6 +363,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn list_results() {
         let mut machine = Machine::new_lib();
         machine.load_module_string(
@@ -387,6 +392,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn consult() {
         let mut machine = Machine::new_lib();
 
@@ -445,6 +451,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn integration_test() {
         let mut machine = Machine::new_lib();
 
@@ -495,6 +502,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn findall() {
         let mut machine = Machine::new_lib();
 

src/machine/load_state.rs

@@ -466,24 +466,48 @@ impl<'a, LS: LoadState<'a>> Loader<'a, LS> {
             None => return,
         };
 
-        for (key, code_index) in removed_module.code_dir.iter_mut() {
+        let mut skipped_local_predicates = IndexSet::with_hasher(FxBuildHasher::default());
-            match removed_module
+
-                .local_extensible_predicates
+        for ((local_compilation_target, key), skeleton) in
-                .get(&(CompilationTarget::User, *key))
+            removed_module.local_extensible_predicates.iter()
         {
-                Some(skeleton) if skeleton.is_multifile => continue,
+            skipped_local_predicates.insert(key);
-                _ => {}
+
+            if skeleton.is_multifile {
+                continue;
             }
 
+            if let Some(code_index) = removed_module.code_dir.get_mut(key) {
+                if let Some(global_skeleton) = self
+                    .wam_prelude
+                    .indices
+                    .get_predicate_skeleton(local_compilation_target, key)
+                {
+                    let old_index_ptr = code_index.replace(if global_skeleton.core.is_dynamic {
+                        IndexPtr::dynamic_undefined()
+                    } else {
+                        IndexPtr::undefined()
+                    });
+
+                    self.payload.retraction_info.push_record(
+                        RetractionRecord::ReplacedModulePredicate(module_name, *key, old_index_ptr),
+                    );
+                }
+            }
+        }
+
+        for (key, code_index) in removed_module.code_dir.iter_mut() {
+            if skipped_local_predicates.contains(key) {
+                continue;
+            }
+
+            if !code_index.is_undefined() && !code_index.is_dynamic_undefined() {
                 let old_index_ptr = code_index.replace(IndexPtr::undefined());
 
-            self.payload
+                self.payload.retraction_info.push_record(
-                .retraction_info
+                    RetractionRecord::ReplacedModulePredicate(module_name, *key, old_index_ptr),
-                .push_record(RetractionRecord::ReplacedModulePredicate(
+                );
-                    module_name,
+            }
-                    *key,
-                    old_index_ptr,
-                ));
         }
 
         for (key, skeleton) in removed_module.extensible_predicates.drain(..) {

src/machine/loader.rs

@@ -1833,9 +1833,33 @@ impl Machine {
     }
 
     pub(crate) fn scoped_clause_to_evacuable(&mut self) -> CallResult {
-        let module_name = cell_as_atom!(self
+        let target = self.deref_register(1);
-            .machine_st
+
-            .store(self.machine_st.deref(self.machine_st.registers[1])));
+        let mut permission_error = || {
+            let err = self.machine_st.permission_error(
+                Permission::Modify,
+                atom!("static_procedure"),
+                functor_stub(atom!(":"), 2)
+                    .into_iter()
+                    .collect::<MachineStub>(),
+            );
+
+            self.machine_st
+                .error_form(err, functor_stub(atom!("load"), 1))
+        };
+
+        let module_name = read_heap_cell!(target,
+            (HeapCellValueTag::Atom, (name, arity)) => {
+                if arity == 0 {
+                    name
+                } else {
+                    return Err(permission_error());
+                }
+            }
+            _ => {
+                return Err(permission_error());
+            }
+        );
 
         let loader = self.loader_from_heap_evacuable(temp_v!(3));
 
@@ -1948,11 +1972,13 @@ impl Machine {
             _ => CompilationTarget::Module(module_name),
         };
 
-        let stub_gen = || match append_or_prepend {
+        let key = match append_or_prepend {
-            AppendOrPrepend::Append => functor_stub(atom!("assertz"), 1),
+            AppendOrPrepend::Append => (atom!("assertz"), 1),
-            AppendOrPrepend::Prepend => functor_stub(atom!("asserta"), 1),
+            AppendOrPrepend::Prepend => (atom!("asserta"), 1),
         };
 
+        let stub_gen = || functor_stub(key.0, key.1);
+
         let head = self.deref_register(2);
 
         if head.is_var() {
@@ -1991,7 +2017,11 @@ impl Machine {
                     .map(|code_idx| code_idx.get_tag())
                     .unwrap_or(IndexPtrTag::DynamicUndefined);
 
-                idx_tag == IndexPtrTag::DynamicUndefined || idx_tag == IndexPtrTag::Undefined
+                if idx_tag == IndexPtrTag::Index {
+                    return Err(SessionError::CannotOverwriteStaticProcedure((name, arity)));
+                } else {
+                    idx_tag == IndexPtrTag::Undefined || idx_tag == IndexPtrTag::DynamicUndefined
+                }
             } else if is_builtin {
                 return Err(SessionError::CannotOverwriteBuiltIn((name, arity)));
             } else {

src/machine/machine_errors.rs

@@ -488,6 +488,13 @@ impl MachineState {
                     .into_iter()
                     .collect::<MachineStub>(),
             ),
+            SessionError::CannotOverwriteStaticProcedure(key) => self.permission_error(
+                Permission::Modify,
+                atom!("static_procedure"),
+                functor_stub(key.0, key.1)
+                    .into_iter()
+                    .collect::<MachineStub>(),
+            ),
             SessionError::CannotOverwriteBuiltInModule(module) => {
                 self.permission_error(Permission::Modify, atom!("static_module"), module)
             }
@@ -1005,6 +1012,7 @@ pub enum SessionError {
     CompilationError(CompilationError),
     CannotOverwriteBuiltIn(PredicateKey),
     CannotOverwriteBuiltInModule(Atom),
+    CannotOverwriteStaticProcedure(PredicateKey),
     ExistenceError(ExistenceError),
     ModuleDoesNotContainExport(Atom, PredicateKey),
     ModuleCannotImportSelf(Atom),

src/machine/machine_state_impl.rs

@@ -1450,10 +1450,15 @@ impl MachineState {
                             a1.as_var().unwrap(),
                         );
                     }
+                    (HeapCellValueTag::Cons | HeapCellValueTag::Fixnum |
+                     HeapCellValueTag::F64) if arity != 0 => {
+                        let err = self.type_error(ValidType::Atom, store_name);
+                        return Err(self.error_form(err, stub_gen())); // 8.5.1.3 e)
+                    }
                     _ => {
                         let err = self.type_error(ValidType::Atomic, store_name);
-                        return Err(self.error_form(err, stub_gen()));
+                        return Err(self.error_form(err, stub_gen())); // 8.5.1.3 c)
-                    } // 8.5.1.3 c)
+                    }
                 );
             }
             _ => {

src/machine/mock_wam.rs

@@ -260,6 +260,7 @@ mod tests {
     use super::*;
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn unify_tests() {
         let mut wam = MachineState::new();
         let mut op_dir = default_op_dir();
@@ -481,6 +482,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn test_unify_with_occurs_check() {
         let mut wam = MachineState::new();
         let mut op_dir = default_op_dir();

src/machine/mod.rs

@@ -228,7 +228,7 @@ impl Machine {
         self.machine_st.throw_exception(err);
     }
 
-    fn run_module_predicate(
+    pub fn run_module_predicate(
         &mut self,
         module_name: Atom,
         key: PredicateKey,
@@ -307,29 +307,6 @@ impl Machine {
         }
     }
 
-    pub fn run_top_level(
-        &mut self,
-        module_name: Atom,
-        key: PredicateKey,
-    ) -> std::process::ExitCode {
-        let mut arg_pstrs = vec![];
-
-        for arg in env::args() {
-            arg_pstrs.push(put_complete_string(
-                &mut self.machine_st.heap,
-                &arg,
-                &self.machine_st.atom_tbl,
-            ));
-        }
-
-        self.machine_st.registers[1] = heap_loc_as_cell!(iter_to_heap_list(
-            &mut self.machine_st.heap,
-            arg_pstrs.into_iter()
-        ));
-
-        self.run_module_predicate(module_name, key)
-    }
-
     pub fn set_user_input(&mut self, input: String) {
         self.user_input = Stream::from_owned_string(input, &mut self.machine_st.arena);
     }
@@ -414,7 +391,7 @@ impl Machine {
         self.code.extend(vec![
             Instruction::BreakFromDispatchLoop,
             Instruction::InstallVerifyAttr,
-            Instruction::VerifyAttrInterrupt,
+            Instruction::VerifyAttrInterrupt(0),
             Instruction::BreakFromDispatchLoop, // the location of LIB_QUERY_SUCCESS
             Instruction::ExecuteTermGreaterThan,
             Instruction::ExecuteTermLessThan,
@@ -925,8 +902,8 @@ impl Machine {
 
             self.machine_st.hb = self.machine_st.heap.len();
 
-            self.machine_st.oip = 0;
+            // self.machine_st.oip = 0;
-            self.machine_st.iip = 0;
+            // self.machine_st.iip = 0;
         }
 
         self.machine_st.p += offset;
@@ -1010,8 +987,22 @@ impl Machine {
 
             self.machine_st.heap.truncate(target_h);
 
-            self.machine_st.oip = 0;
+            // these registers don't need to be reset here and MUST
-            self.machine_st.iip = 0;
+            // NOT be (nor in indexed_try! trust_epilogue is an
+            // exception, see next paragraph)! oip could be reset
+            // without any adverse effects but iip is needed by
+            // get_clause_p to find the last executed clause/2 clause.
+
+            // trust_epilogue must reset these for the sake of
+            // subsequent predicates beginning with
+            // switch_to_term. get_clause_p copes by checking
+            // self.machine_st.b > self.machine.e: if true, it is safe
+            // to use self.machine_st.iip; if false, use the choice
+            // point left at the top of the stack by '$clause'
+            // (specifically its biip value).
+
+            // self.machine_st.oip = 0;
+            // self.machine_st.iip = 0;
         } else {
             self.trust_epilogue(offset);
         }
@@ -1116,7 +1107,7 @@ impl Machine {
             }
             Unknown::Warn => {
                 println!(
-                    "warning: predicate {}/{} is undefined",
+                    "% Warning: predicate {}/{} is undefined",
                     name.as_str(),
                     arity
                 );

src/machine/partial_string.rs

@@ -764,13 +764,29 @@ pub fn compare_pstr_prefixes<'a>(
         if i1.focus == empty_list_as_cell!() {
             PStrCmpResult::Ordered(Ordering::Less)
         } else {
-            PStrCmpResult::SecondIterContinuable(r2.unwrap().iteratee)
+            let r2_step = r2.unwrap();
+
+            // advance i2 to the next character so the same character
+            // isn't repeated
+            if matches!(r2_step.iteratee, PStrIteratee::Char(..)) {
+                cycle_detection_step(i2, i1, &r2_step);
+            }
+
+            PStrCmpResult::SecondIterContinuable(r2_step.iteratee)
         }
     } else if r2_at_end {
         if i2.focus == empty_list_as_cell!() {
             PStrCmpResult::Ordered(Ordering::Greater)
         } else {
-            PStrCmpResult::FirstIterContinuable(r1.unwrap().iteratee)
+            let r1_step = r1.unwrap();
+
+            // advance i1 to the next character so the same character
+            // isn't repeated
+            if matches!(r1_step.iteratee, PStrIteratee::Char(..)) {
+                cycle_detection_step(i1, i2, &r1_step);
+            }
+
+            PStrCmpResult::FirstIterContinuable(r1_step.iteratee)
         }
     } else if i1.is_continuable() && i2.is_continuable() {
         PStrCmpResult::Ordered(Ordering::Equal)
@@ -785,6 +801,7 @@ mod test {
     use crate::machine::mock_wam::*;
 
     #[test]
+    #[cfg_attr(miri, ignore = "blocked on streams.rs UB")]
     fn pstr_iter_tests() {
         let mut wam = MockWAM::new();
 
@@ -1089,9 +1106,119 @@ mod test {
                 Some(PStrIteratee::PStrSegment(2, atom!("abc"), 1))
             );
 
-            // assert!(iter.next().is_none());
-
             for _ in iter {}
         }
+
+        // #2293, test1.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!("a ")));
+        wam.machine_st.heap.push(heap_loc_as_cell!(1));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(empty_list_as_cell!());
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
+
+        // #2293, test2.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!(" a")));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(heap_loc_as_cell!(3));
+        wam.machine_st.heap.push(empty_list_as_cell!());
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
+
+        // #2293, test3.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!("a b")));
+        wam.machine_st.heap.push(heap_loc_as_cell!(1));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(list_loc_as_cell!(5));
+        wam.machine_st.heap.push(heap_loc_as_cell!(5));
+        wam.machine_st.heap.push(empty_list_as_cell!());
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
+
+        // #2293, test4.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!(" a ")));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(heap_loc_as_cell!(3));
+        wam.machine_st.heap.push(list_loc_as_cell!(5));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(empty_list_as_cell!());
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
+
+        // #2293, test5.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!(" a bc")));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(heap_loc_as_cell!(3));
+        wam.machine_st.heap.push(list_loc_as_cell!(5));
+        wam.machine_st.heap.push(char_as_cell!(' '));
+        wam.machine_st.heap.push(heap_loc_as_cell!(6));
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
+
+        // #2293, test6.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!("abc")));
+        wam.machine_st.heap.push(heap_loc_as_cell!(1));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(char_as_cell!('b'));
+        wam.machine_st.heap.push(list_loc_as_cell!(5));
+        wam.machine_st.heap.push(heap_loc_as_cell!(5));
+        wam.machine_st.heap.push(empty_list_as_cell!());
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
+
+        // #2293, test7.
+
+        wam.machine_st.heap.clear();
+
+        wam.machine_st.heap.push(atom_as_cstr_cell!(atom!("abcde")));
+        wam.machine_st.heap.push(char_as_cell!('a'));
+        wam.machine_st.heap.push(list_loc_as_cell!(3));
+        wam.machine_st.heap.push(heap_loc_as_cell!(3));
+        wam.machine_st.heap.push(list_loc_as_cell!(5));
+        wam.machine_st.heap.push(char_as_cell!('c'));
+        wam.machine_st.heap.push(list_loc_as_cell!(7));
+        wam.machine_st.heap.push(heap_loc_as_cell!(7));
+        wam.machine_st.heap.push(list_loc_as_cell!(9));
+        wam.machine_st.heap.push(char_as_cell!('e'));
+        wam.machine_st.heap.push(empty_list_as_cell!());
+
+        unify!(wam.machine_st, list_loc_as_cell!(1), heap_loc_as_cell!(0));
+
+        assert!(!wam.machine_st.fail);
     }
 }

src/machine/preprocessor.rs

@@ -565,21 +565,6 @@ impl Preprocessor {
         }
     }
 
-    /*
-    fn try_term_to_query<'a, LS: LoadState<'a>>(
-        &mut self,
-        loader: &mut Loader<'a, LS>,
-        terms: Vec<Term>,
-        cut_context: CutContext,
-    ) -> Result<TopLevel, CompilationError> {
-        Ok(TopLevel::Query(self.setup_query(
-            loader,
-            terms,
-            cut_context,
-        )?))
-    }
-    */
-
     pub(super) fn try_term_to_tl<'a, LS: LoadState<'a>>(
         &mut self,
         loader: &mut Loader<'a, LS>,
@@ -607,20 +592,4 @@ impl Preprocessor {
             }
         }
     }
-
-    /*
-    fn try_terms_to_tls<'a, I: IntoIterator<Item = Term>, LS: LoadState<'a>>(
-        &mut self,
-        loader: &mut Loader<'a, LS>,
-        terms: I,
-    ) -> Result<VecDeque<TopLevel>, CompilationError> {
-        let mut results = VecDeque::new();
-
-        for term in terms.into_iter() {
-            results.push_back(self.try_term_to_tl(loader, term)?);
-        }
-
-        Ok(results)
-    }
-    */
 }

src/machine/project_attributes.pl

@@ -1,4 +1,4 @@
-:- module('$project_atts', [copy_term/3]).
+:- module('$project_atts', []).
 
 :- use_module(library(dcgs)).
 :- use_module(library(error), [can_be/2]).
@@ -100,14 +100,6 @@ gather_residual_goals([V|Vs]) -->
 
 delete_all_attributes_from_var(V) :- '$delete_all_attributes_from_var'(V).
 
-copy_term(Term, Copy, Gs) :-
-   can_be(list, Gs),
-   findall(Term-Rs, term_residual_goals(Term,Rs), [Copy-Gs]),
-   (  var(Gs) ->
-      Gs = []
-   ;  true
-   ).
-
 term_residual_goals(Term,Rs) :-
     '$term_attributed_variables'(Term, Vs),
     phrase(gather_residual_goals(Vs), Rs),

src/machine/stack.rs

@@ -189,7 +189,7 @@ impl Stack {
 
             for idx in 0..num_cells {
                 ptr::write(
-                    (new_ptr as usize + offset) as *mut HeapCellValue,
+                    new_ptr.add(offset) as *mut HeapCellValue,
                     stack_loc_as_cell!(AndFrame, e, idx + 1),
                 );
 
@@ -203,6 +203,10 @@ impl Stack {
         }
     }
 
+    pub(crate) fn top(&self) -> usize {
+        unsafe { (*self.buf.ptr.get()) as usize - self.buf.base as usize }
+    }
+
     pub(crate) fn allocate_or_frame(&mut self, num_cells: usize) -> usize {
         let frame_size = OrFrame::size_of(num_cells);
 
@@ -238,7 +242,8 @@ impl Stack {
     #[inline(always)]
     pub(crate) fn index_and_frame_mut(&mut self, e: usize) -> &mut AndFrame {
         unsafe {
-            let ptr = self.buf.base as usize + e;
+            // This is doing alignment wrong
+            let ptr = self.buf.base.add(e);
             &mut *(ptr as *mut AndFrame)
         }
     }
@@ -276,6 +281,7 @@ mod tests {
     use crate::machine::mock_wam::*;
 
     #[test]
+    #[cfg_attr(miri, ignore)]
     fn stack_tests() {
         let mut wam = MockWAM::new();
 

src/machine/streams.rs

@@ -469,6 +469,7 @@ macro_rules! arena_allocated_impl_for_stream {
             #[inline]
             fn copy_to_arena(self, dst: *mut Self) -> Self::PtrToAllocated {
                 unsafe {
+                    // Miri seems to hit this a lot
                     ptr::write(dst, self);
                     TypedArenaPtr::new(dst as *mut Self)
                 }

src/machine/system_calls.rs

@@ -81,14 +81,11 @@ use ring::rand::{SecureRandom, SystemRandom};
 use ring::{digest, hkdf, pbkdf2};
 
 #[cfg(feature = "crypto-full")]
-use ring::{
+use ring::aead;
-    aead,
-    signature::{self, KeyPair},
-};
 use ripemd160::{Digest, Ripemd160};
 use sha3::{Sha3_224, Sha3_256, Sha3_384, Sha3_512};
 
-use crrl::{secp256k1, x25519};
+use crrl::{ed25519, secp256k1, x25519};
 
 #[cfg(feature = "tls")]
 use native_tls::{Identity, TlsAcceptor, TlsConnector};
@@ -1171,43 +1168,12 @@ impl Machine {
             .get_predicate_skeleton(&compilation_target, &key)
             .unwrap();
 
-        if self.machine_st.b > self.machine_st.e {
-            let or_frame = self.machine_st.stack.index_or_frame(self.machine_st.b);
-            let bp = or_frame.prelude.bp;
-
-            match &self.code[bp] {
-                Instruction::IndexingCode(ref indexing_code) => {
-                    match &indexing_code[or_frame.prelude.boip as usize] {
-                        IndexingLine::IndexedChoice(ref indexed_choice) => {
-                            let p = or_frame.prelude.biip as usize - 1;
-
-                            match &indexed_choice[p] {
-                                &IndexedChoiceInstruction::Try(offset)
-                                | &IndexedChoiceInstruction::Retry(offset)
-                                | &IndexedChoiceInstruction::DefaultRetry(offset) => {
-                                    let clause_clause_loc = skeleton.core.clause_clause_locs[p];
-                                    (clause_clause_loc, bp + offset)
-                                }
-                                &IndexedChoiceInstruction::Trust(_)
-                                | &IndexedChoiceInstruction::DefaultTrust(_) => {
-                                    unreachable!()
-                                }
-                            }
-                        }
-                        _ => {
-                            unreachable!()
-                        }
-                    }
-                }
-                _ => unreachable!(),
-            }
-        } else {
         let module_name = match compilation_target {
             CompilationTarget::User => atom!("builtins"),
             CompilationTarget::Module(target) => target,
         };
 
-            let bp = self
+        let mut bp = self
             .indices
             .get_predicate_code_index(atom!("$clause"), 2, module_name)
             .and_then(|idx| idx.local())
@@ -1228,6 +1194,7 @@ impl Machine {
             };
         }
 
+        loop {
             match &self.code[bp] {
                 Instruction::IndexingCode(ref indexing_code) => {
                     let indexing_code_ptr = match &indexing_code[0] {
@@ -1263,14 +1230,38 @@ impl Machine {
 
                     match &indexing_code[boip] {
                         IndexingLine::IndexedChoice(indexed_choice) => {
+                            let p = if self.machine_st.b > self.machine_st.e {
+                                // this means the last
+                                // self.machine_st.iip value has yet
+                                // to be overwritten by the Trust
+                                // instruction. In this case, return
+                                // it.
+                                self.machine_st.iip as usize
+                            } else {
+                                // otherwise, read the '$clause'
+                                // choicepoint from the top of the
+                                // stack. this is very volatile in
+                                // that it depends on '$clause'
+                                // immediately preceding
+                                // '$get_clause_p', which cannot be
+                                // the last clause of the retract
+                                // helper to delay deallocation of its
+                                // environment frame.
+                                let clause_b = self.machine_st.stack.top();
+                                self.machine_st.stack.index_or_frame(clause_b).prelude.biip as usize
+                            };
+
                             return (
-                                skeleton.core.clause_clause_locs.back().cloned().unwrap(),
+                                skeleton.core.clause_clause_locs[p],
-                                bp + indexed_choice.back().unwrap().offset(),
+                                bp + indexed_choice[p].offset(),
                             );
                         }
                         _ => unreachable!(),
                     }
                 }
+                &Instruction::RevJmpBy(offset) => {
+                    bp -= offset;
+                }
                 _ => {
                     return (
                         skeleton.core.clause_clause_locs.back().cloned().unwrap(),
@@ -3501,6 +3492,12 @@ impl Machine {
                     Some(Ok(c)) => {
                         string.push(c);
                     }
+                    Some(Err(e)) => {
+                        let stub = functor_stub(atom!("$get_n_chars"), 3);
+                        let err = self.machine_st.session_error(SessionError::from(e));
+
+                        return Err(self.machine_st.error_form(err, stub));
+                    }
                     _ => {
                         break;
                     }
@@ -4291,18 +4288,18 @@ impl Machine {
             let address_string = address_sink.as_str(); //to_string();
             let address: Url = address_string.parse().unwrap();
 
-            let client = reqwest::blocking::Client::builder().build().unwrap();
+            let client = reqwest::Client::builder().build().unwrap();
 
             // request
-            let mut req = reqwest::blocking::Request::new(method, address);
+            let mut req = reqwest::Request::new(method, address);
 
             *req.headers_mut() = headers;
             if !bytes.is_empty() {
-                *req.body_mut() = Some(reqwest::blocking::Body::from(bytes));
+                *req.body_mut() = Some(reqwest::Body::from(bytes));
             }
 
             // do it!
-            match client.execute(req) {
+            match futures::executor::block_on(client.execute(req)) {
                 Ok(resp) => {
                     // status code
                     let status = resp.status().as_u16();
@@ -4339,7 +4336,7 @@ impl Machine {
                         self.machine_st.registers[6]
                     );
                     // body
-                    let reader = resp.bytes().unwrap().reader();
+                    let reader = futures::executor::block_on(resp.bytes()).unwrap().reader();
 
                     let mut stream = Stream::from_http_stream(
                         AtomTable::build_with(&self.machine_st.atom_tbl, &address_string),
@@ -4953,6 +4950,27 @@ impl Machine {
         }
     }
 
+    #[inline(always)]
+    pub(crate) fn argv(&mut self) -> CallResult {
+        let args = self.deref_register(1);
+
+        let mut args_pstrs = vec![];
+        for arg in env::args() {
+            args_pstrs.push(put_complete_string(
+                &mut self.machine_st.heap,
+                &arg,
+                &self.machine_st.atom_tbl,
+            ));
+        }
+        let cell = heap_loc_as_cell!(iter_to_heap_list(
+            &mut self.machine_st.heap,
+            args_pstrs.into_iter()
+        ));
+
+        unify!(self.machine_st, args, cell);
+        Ok(())
+    }
+
     #[inline(always)]
     pub(crate) fn current_time(&mut self) {
         let timestamp = self.systemtime_to_timestamp(SystemTime::now());
@@ -5721,11 +5739,11 @@ impl Machine {
     #[inline(always)]
     pub(super) fn restore_instr_at_verify_attr_interrupt(&mut self) {
         match &self.code[VERIFY_ATTR_INTERRUPT_LOC] {
-            &Instruction::VerifyAttrInterrupt => {}
+            &Instruction::VerifyAttrInterrupt(_) => {}
             _ => {
                 let instr = mem::replace(
                     &mut self.code[VERIFY_ATTR_INTERRUPT_LOC],
-                    Instruction::VerifyAttrInterrupt,
+                    Instruction::VerifyAttrInterrupt(0),
                 );
 
                 self.code[self.machine_st.attr_var_init.cp] = instr;
@@ -6520,10 +6538,8 @@ impl Machine {
         );
 
         if had_zero_port {
-            self.machine_st.unify_fixnum(
+            self.machine_st
-                Fixnum::build_with(port as i64),
+                .unify_fixnum(Fixnum::build_with(port as i64), self.deref_register(2));
-                self.machine_st.registers[2],
-            );
         }
 
         Ok(())
@@ -7625,33 +7641,16 @@ impl Machine {
         unify!(self.machine_st, self.machine_st.registers[4], uncompressed);
     }
 
-    #[cfg(feature = "crypto-full")]
     #[inline(always)]
-    pub(crate) fn ed25519_new_key_pair(&mut self) {
+    pub(crate) fn ed25519_seed_to_public_key(&mut self) {
-        let pkcs8_bytes = signature::Ed25519KeyPair::generate_pkcs8(rng()).unwrap();
+        let stub_gen = || functor_stub(atom!("ed25519_seed_keypair"), 2);
-        let complete_string = self.u8s_to_string(pkcs8_bytes.as_ref());
+        let seed_bytes = self
+            .machine_st
+            .integers_to_bytevec(self.machine_st.registers[1], stub_gen);
 
-        unify!(
+        let skey = ed25519::PrivateKey::from_seed(&seed_bytes);
-            self.machine_st,
-            self.machine_st.registers[1],
-            complete_string
-        )
-    }
 
-    #[cfg(feature = "crypto-full")]
+        let complete_string = self.u8s_to_string(skey.public_key.encoded.as_ref());
-    #[inline(always)]
-    pub(crate) fn ed25519_key_pair_public_key(&mut self) {
-        let bytes = self.string_encoding_bytes(self.machine_st.registers[1], atom!("octet"));
-
-        let key_pair = match signature::Ed25519KeyPair::from_pkcs8(&bytes) {
-            Ok(kp) => kp,
-            _ => {
-                self.machine_st.fail = true;
-                return;
-            }
-        };
-
-        let complete_string = self.u8s_to_string(key_pair.public_key().as_ref());
 
         unify!(
             self.machine_st,
@@ -7660,22 +7659,19 @@ impl Machine {
         );
     }
 
-    #[cfg(feature = "crypto-full")]
     #[inline(always)]
-    pub(crate) fn ed25519_sign(&mut self) {
+    pub(crate) fn ed25519_sign_raw(&mut self) {
-        let key = self.string_encoding_bytes(self.machine_st.registers[1], atom!("octet"));
+        let stub_gen = || functor_stub(atom!("ed25519_sign"), 4);
+        let seed_bytes = self
+            .machine_st
+            .integers_to_bytevec(self.machine_st.registers[1], stub_gen);
+
+        let skey = ed25519::PrivateKey::from_seed(&seed_bytes);
+
         let encoding = cell_as_atom!(self.deref_register(3));
         let data = self.string_encoding_bytes(self.machine_st.registers[2], encoding);
 
-        let key_pair = match signature::Ed25519KeyPair::from_pkcs8(&key) {
+        let sig = skey.sign_raw(&data);
-            Ok(kp) => kp,
-            _ => {
-                self.machine_st.fail = true;
-                return;
-            }
-        };
-
-        let sig = key_pair.sign(&data);
 
         let sig_list = heap_loc_as_cell!(iter_to_heap_list(
             &mut self.machine_st.heap,
@@ -7687,25 +7683,21 @@ impl Machine {
         unify!(self.machine_st, self.machine_st.registers[4], sig_list);
     }
 
-    #[cfg(feature = "crypto-full")]
     #[inline(always)]
-    pub(crate) fn ed25519_verify(&mut self) {
+    pub(crate) fn ed25519_verify_raw(&mut self) {
-        let key = self.string_encoding_bytes(self.machine_st.registers[1], atom!("octet"));
+        let key_bytes = self.string_encoding_bytes(self.machine_st.registers[1], atom!("octet"));
+        let pkey = ed25519::PublicKey::decode(&key_bytes).unwrap();
+
         let encoding = cell_as_atom!(self.deref_register(3));
         let data = self.string_encoding_bytes(self.machine_st.registers[2], encoding);
-        let stub_gen = || functor_stub(atom!("ed25519_verify"), 5);
+
+        let stub_gen = || functor_stub(atom!("ed25519_verify"), 4);
+
         let signature = self
             .machine_st
             .integers_to_bytevec(self.machine_st.registers[4], stub_gen);
 
-        let peer_public_key = signature::UnparsedPublicKey::new(&signature::ED25519, &key);
+        self.machine_st.fail = !pkey.verify_raw(&signature, &data);
-
-        match peer_public_key.verify(&data, &signature) {
-            Ok(_) => {}
-            _ => {
-                self.machine_st.fail = true;
-            }
-        }
     }
 
     #[inline(always)]

src/machine/unify.rs

@@ -173,6 +173,98 @@ pub(crate) trait Unifier: DerefMut<Target = MachineState> {
         let mut pstr_iter1 = HeapPStrIter::new(&machine_st.heap, s1);
         let mut pstr_iter2 = HeapPStrIter::new(&machine_st.heap, s1 + 1);
 
+        fn unify_sequence(
+            machine_st: &mut MachineState,
+            iter: PStrIteratee,
+            source_cell: HeapCellValue,
+        ) -> bool {
+            match iter {
+                PStrIteratee::Char(focus, _) => {
+                    machine_st.pdl.push(machine_st.heap[focus]);
+                    machine_st.pdl.push(source_cell);
+                }
+                PStrIteratee::PStrSegment(focus, _, n) => {
+                    read_heap_cell!(machine_st.heap[focus],
+                        (HeapCellValueTag::CStr | HeapCellValueTag::PStr, pstr_atom) => {
+                            if focus < machine_st.heap.len() - 2 {
+                                machine_st.heap.pop();
+                                machine_st.heap.pop();
+                            }
+
+                            if n == 0 {
+                                let target_cell = match machine_st.heap[focus].get_tag() {
+                                    HeapCellValueTag::CStr => {
+                                        atom_as_cstr_cell!(pstr_atom)
+                                    }
+                                    HeapCellValueTag::PStr => {
+                                        pstr_loc_as_cell!(focus)
+                                    }
+                                    _ => {
+                                        unreachable!()
+                                    }
+                                };
+
+                                machine_st.pdl.push(target_cell);
+                                machine_st.pdl.push(source_cell);
+                            } else {
+                                let h_len = machine_st.heap.len();
+
+                                machine_st.heap.push(pstr_offset_as_cell!(focus));
+                                machine_st.heap.push(fixnum_as_cell!(
+                                    Fixnum::build_with(n as i64)
+                                ));
+
+                                machine_st.pdl.push(pstr_loc_as_cell!(h_len));
+                                machine_st.pdl.push(source_cell);
+                            }
+
+                            return true;
+                        }
+                        (HeapCellValueTag::PStrOffset, pstr_loc) => {
+                            let n0 = cell_as_fixnum!(machine_st.heap[focus+1])
+                                .get_num() as usize;
+
+                            if pstr_loc < machine_st.heap.len() - 2 {
+                                machine_st.heap.pop();
+                                machine_st.heap.pop();
+                            }
+
+                            if n == n0 {
+                                machine_st.pdl.push(pstr_loc_as_cell!(focus));
+                                machine_st.pdl.push(source_cell);
+                            } else {
+                                let h_len = machine_st.heap.len();
+
+                                machine_st.heap.push(pstr_offset_as_cell!(pstr_loc));
+                                machine_st.heap.push(fixnum_as_cell!(
+                                    Fixnum::build_with(n as i64)
+                                ));
+
+                                machine_st.pdl.push(pstr_loc_as_cell!(h_len));
+                                machine_st.pdl.push(source_cell);
+                            }
+
+                            return true;
+                        }
+                        _ => {
+                        }
+                    );
+
+                    if focus < machine_st.heap.len() - 2 {
+                        machine_st.heap.pop();
+                        machine_st.heap.pop();
+                    }
+
+                    machine_st.pdl.push(machine_st.heap[focus]);
+                    machine_st.pdl.push(source_cell);
+
+                    return true;
+                }
+            }
+
+            false
+        }
+
         match compare_pstr_prefixes(&mut pstr_iter1, &mut pstr_iter2) {
             PStrCmpResult::Ordered(Ordering::Equal) => {}
             PStrCmpResult::Ordered(Ordering::Less) => {
@@ -229,90 +321,14 @@ pub(crate) trait Unifier: DerefMut<Target = MachineState> {
                                     break 'outer;
                                 }
                             }
+                            (HeapCellValueTag::CStr | HeapCellValueTag::PStrLoc) => {
+                                unify_sequence(machine_st, chars_iter.item.unwrap(), focus);
+                                return;
+                            }
                             (HeapCellValueTag::AttrVar | HeapCellValueTag::Var, h) => {
-                                match chars_iter.item.unwrap() {
+                                if unify_sequence(machine_st, chars_iter.item.unwrap(), heap_loc_as_cell!(h)) {
-                                    PStrIteratee::Char(focus, _) => {
-                                        machine_st.pdl.push(machine_st.heap[focus]);
-                                        machine_st.pdl.push(heap_loc_as_cell!(h));
-                                    }
-                                    PStrIteratee::PStrSegment(focus, _, n) => {
-                                        read_heap_cell!(machine_st.heap[focus],
-                                            (HeapCellValueTag::CStr | HeapCellValueTag::PStr, pstr_atom) => {
-                                                if focus < machine_st.heap.len() - 2 {
-                                                    machine_st.heap.pop();
-                                                    machine_st.heap.pop();
-                                                }
-
-                                                if n == 0 {
-                                                    let target_cell = match machine_st.heap[focus].get_tag() {
-                                                        HeapCellValueTag::CStr => {
-                                                            atom_as_cstr_cell!(pstr_atom)
-                                                        }
-                                                        HeapCellValueTag::PStr => {
-                                                            pstr_loc_as_cell!(focus)
-                                                        }
-                                                        _ => {
-                                                            unreachable!()
-                                                        }
-                                                    };
-
-                                                    machine_st.pdl.push(target_cell);
-                                                    machine_st.pdl.push(heap_loc_as_cell!(h));
-                                                } else {
-                                                    let h_len = machine_st.heap.len();
-
-                                                    machine_st.heap.push(pstr_offset_as_cell!(focus));
-                                                    machine_st.heap.push(fixnum_as_cell!(
-                                                        Fixnum::build_with(n as i64)
-                                                    ));
-
-                                                    machine_st.pdl.push(pstr_loc_as_cell!(h_len));
-                                                    machine_st.pdl.push(heap_loc_as_cell!(h));
-                                                }
-
                                     return;
                                 }
-                                            (HeapCellValueTag::PStrOffset, pstr_loc) => {
-                                                let n0 = cell_as_fixnum!(machine_st.heap[focus+1])
-                                                    .get_num() as usize;
-
-                                                if pstr_loc < machine_st.heap.len() - 2 {
-                                                    machine_st.heap.pop();
-                                                    machine_st.heap.pop();
-                                                }
-
-                                                if n == n0 {
-                                                    machine_st.pdl.push(pstr_loc_as_cell!(focus));
-                                                    machine_st.pdl.push(heap_loc_as_cell!(h));
-                                                } else {
-                                                    let h_len = machine_st.heap.len();
-
-                                                    machine_st.heap.push(pstr_offset_as_cell!(pstr_loc));
-                                                    machine_st.heap.push(fixnum_as_cell!(
-                                                        Fixnum::build_with(n as i64)
-                                                    ));
-
-                                                    machine_st.pdl.push(pstr_loc_as_cell!(h_len));
-                                                    machine_st.pdl.push(heap_loc_as_cell!(h));
-                                                }
-
-                                                return;
-                                            }
-                                            _ => {
-                                            }
-                                        );
-
-                                        if focus < machine_st.heap.len() - 2 {
-                                            machine_st.heap.pop();
-                                            machine_st.heap.pop();
-                                        }
-
-                                        machine_st.pdl.push(machine_st.heap[focus]);
-                                        machine_st.pdl.push(heap_loc_as_cell!(h));
-
-                                        return;
-                                    }
-                                }
 
                                 break 'outer;
                             }

src/parser/ast.rs

@@ -417,6 +417,9 @@ impl ParserError {
             ParserError::IO(e) if e.kind() == ErrorKind::UnexpectedEof => {
                 atom!("unexpected_end_of_file")
             }
+            ParserError::IO(e) if e.kind() == ErrorKind::InvalidData => {
+                atom!("invalid_data")
+            }
             ParserError::IO(_) => atom!("input_output_error"),
             ParserError::LexicalError(_) => atom!("lexical_error"),
             ParserError::MissingQuote(..) => atom!("missing_quote"),

src/parser/char_reader.rs

@@ -144,21 +144,7 @@ impl<R: Read> CharRead for CharReader<R> {
             Err(e) => return Some(Err(e)),
         }
 
-        loop {
+        let bad_bytes_error = |buf: &[u8]| {
-            let buf = &self.buf[self.pos..];
-
-            if !buf.is_empty() {
-                let e = match str::from_utf8(buf) {
-                    Ok(s) => {
-                        let mut chars = s.chars();
-                        let c = chars.next().unwrap();
-
-                        return Some(Ok(c));
-                    }
-                    Err(e) => e,
-                };
-
-                if buf.len() - e.valid_up_to() >= 4 {
             // If we have 4 bytes that still don't make up
             // a valid code point, then we have garbage.
 
@@ -184,13 +170,28 @@ impl<R: Read> CharRead for CharReader<R> {
             // the buffer, it will be returned on the next
             // loop.
 
-                    return Some(Err(io::Error::new(
+            io::Error::new(io::ErrorKind::InvalidData, BadUtf8Error { bytes: badbytes })
-                        io::ErrorKind::InvalidData,
+        };
-                        BadUtf8Error { bytes: badbytes },
+
-                    )));
+        loop {
+            let buf = &self.buf[self.pos..];
+
+            if !buf.is_empty() {
+                let e = match str::from_utf8(buf) {
+                    Ok(s) => {
+                        let mut chars = s.chars();
+                        let c = chars.next().unwrap();
+
+                        return Some(Ok(c));
+                    }
+                    Err(e) => e,
+                };
+
+                if buf.len() - e.valid_up_to() >= 4 {
+                    return Some(Err(bad_bytes_error(buf)));
                 } else if self.pos >= self.buf.len() {
                     return None;
-                } else if self.buf.len() - self.pos >= 4 {
+                } else if self.buf.len() - self.pos >= 4 && self.pos < e.valid_up_to() {
                     return match str::from_utf8(&self.buf[self.pos..e.valid_up_to()]) {
                         Ok(s) => {
                             let mut chars = s.chars();
@@ -217,18 +218,22 @@ impl<R: Read> CharRead for CharReader<R> {
                     self.buf.truncate(buf_len - self.pos);
 
                     let buf_len = self.buf.len();
+                    self.pos = 0;
+
+                    if buf_len >= 4 {
+                        continue;
+                    }
 
                     let mut word = [0u8; 4];
                     let word_slice = &mut word[buf_len..4];
 
                     match self.inner.read(word_slice) {
                         Err(e) => return Some(Err(e)),
+                        Ok(nread) if nread == 0 => return Some(Err(bad_bytes_error(&self.buf))),
                         Ok(nread) => {
                             self.buf.extend_from_slice(&word_slice[0..nread]);
                         }
                     }
-
-                    self.pos = 0;
                 }
             } else {
                 return None;
@@ -375,6 +380,7 @@ mod tests {
     use std::io::Cursor;
 
     #[test]
+    #[cfg_attr(miri, ignore = "slow and not very relevant")]
     fn plain_string() {
         let mut read_string = CharReader::new(Cursor::new("a string"));
 
@@ -387,6 +393,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "slow and not very relevant")]
     fn greek_string() {
         let mut read_string = CharReader::new(Cursor::new("λέξη"));
 
@@ -399,6 +406,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "slow and not very relevant")]
     fn russian_string() {
         let mut read_string = CharReader::new(Cursor::new("слово"));
 
@@ -411,6 +419,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "slow and not very relevant")]
     fn greek_lorem_ipsum() {
         let lorem_ipsum = "Λορεμ ιπσθμ δολορ σιτ αμετ, οφφενδιτ
     εφφιcιενδι σιτ ει, ηαρθμ λεγερε qθαερενδθμ ιθσ νε. Ηασ νο εροσ
@@ -482,6 +491,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "slow and not very relevant")]
     fn armenian_lorem_ipsum() {
         let lorem_ipsum = "լոռեմ իպսում դոլոռ սիթ ամեթ, նովում գռաեծո
         սեա եա, աբհոռռեանթ դիսպութանդո եի քուի. իդ քուոդ ինդոծթում
@@ -555,6 +565,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(miri, ignore = "slow and not very relevant")]
     fn russian_lorem_ipsum() {
         let lorem_ipsum = "Лорем ипсум долор сит амет, атяуи дицам еи
         сит, ид сеа фацилис елаборарет. Меа еу яуас алияуид, те яуи

src/parser/parser.rs

@@ -97,7 +97,12 @@ pub(crate) fn as_partial_string(
                         string.push(*c);
                     }
                     _ => {
-                        return Err(Term::Cons(Cell::default(), Box::new(head), orig_tail));
+                        tail = Term::Cons(
+                            Cell::default(),
+                            Box::new((**prev).clone()),
+                            Box::new((**succ).clone()),
+                        );
+                        break;
                     }
                 }
 
@@ -880,11 +885,7 @@ impl<'a, R: CharRead> Parser<'a, R> {
                         .push(Term::Literal(Cell::default(), Literal::Atom(atom)));
                 }
 
-                self.stack[idx].spec = if self.stack[idx].priority > 0 {
+                self.stack[idx].spec = BTERM;
-                    TERM
-                } else {
-                    BTERM
-                };
                 self.stack[idx].tt = TokenType::Term;
                 self.stack[idx].priority = 0;
 

src/raw_block.rs

@@ -43,7 +43,7 @@ impl<T: RawBlockTraits> RawBlock<T> {
         let layout = alloc::Layout::from_size_align_unchecked(cap, T::align());
 
         self.base = alloc::alloc(layout) as *const _;
-        self.top = (self.base as usize + cap) as *const _;
+        self.top = self.base.add(cap);
         *self.ptr.get_mut() = self.base as *mut _;
     }
 
@@ -98,7 +98,7 @@ impl<T: RawBlockTraits> RawBlock<T> {
     pub unsafe fn alloc(&self, size: usize) -> *mut u8 {
         if self.free_space() >= size {
             let ptr = *self.ptr.get();
-            *self.ptr.get() = (ptr as usize + size) as *mut _;
+            *self.ptr.get() = ptr.add(size) as *mut _;
             ptr
         } else {
             ptr::null_mut()

src/read.rs

@@ -130,7 +130,7 @@ impl ReadlineStream {
             if let Some(mut path) = dirs_next::home_dir() {
                 path.push(HISTORY_FILE);
                 if path.exists() && rl.load_history(&path).is_err() {
-                    println!("Warning: loading history failed");
+                    println!("% Warning: loading history failed");
                 }
             }
 
@@ -213,10 +213,10 @@ impl ReadlineStream {
             path.push(HISTORY_FILE);
             if path.exists() {
                 if self.rl.append_history(&path).is_err() {
-                    println!("Warning: couldn't append history (existing file)");
+                    println!("% Warning: couldn't append history (existing file)");
                 }
             } else if self.rl.save_history(&path).is_err() {
-                println!("Warning: couldn't save history (new file)");
+                println!("% Warning: couldn't save history (new file)");
             }
         }
     }

src/tests/dif.pl

@@ -1,10 +1,10 @@
 /**/
 
-:- use_module(library(format)).
 :- use_module(library(dcgs)).
+:- use_module(library(format)).
 :- use_module(library(lists)).
 :- use_module(library(debug)).
-:- use_module(library(atts)).
+:- use_module(library(iso_ext)).
 :- use_module(library(dif)).
 
 % Tests from https://www.complang.tuwien.ac.at/ulrich/iso-prolog/dif

src/tests/when.pl

@@ -0,0 +1,145 @@
+/**/
+
+:- use_module(library(iso_ext)).
+:- use_module(library(format)).
+:- use_module(library(dcgs)).
+:- use_module(library(lists)).
+:- use_module(library(debug)).
+
+:- use_module(library(when)).
+
+test("condition true before ground/1",(
+    A = 1,
+    when(ground(A), Run = true),
+    Run == true
+)).
+
+test("condition true before nonvar/1",(
+    A = a(_),
+    when(nonvar(A), Run = true),
+    Run == true
+)).
+
+test("condition true before ','/2",(
+    A = 1,
+    B = a(_),
+    when((ground(A), nonvar(B)), Run = true),
+    Run == true
+)).
+
+test("condition true before (;)/2",(
+    A = 1,
+    when((ground(A) ; nonvar(_)), Run1 = true),
+    Run1 == true,
+
+    B = a(_),
+    when((ground(_) ; nonvar(B)), Run2 = true),
+    Run2 == true
+)).
+
+test("condition true after ground/1",(
+    when(ground(A), Run = true),
+    var(Run),
+    A = 1,
+    Run == true
+)).
+
+test("condition true after nonvar/1",(
+    when(nonvar(A), Run = true),
+    var(Run),
+    A = a(_),
+    Run == true
+)).
+
+test("condition true after ','/2",(
+    when((ground(A), nonvar(B)), Run = true),
+    var(Run),
+    A = 1,
+    var(Run),
+    B = a(_),
+    Run == true
+)).
+
+test("condition true after (;)/2",(
+    when((ground(A) ; nonvar(_)), Run1 = true),
+    var(Run1),
+    A = 1,
+    Run1 == true,
+
+    when((ground(_) ; nonvar(B)), Run2 = true),
+    var(Run2),
+    B = a(_),
+    Run2 == true
+)).
+
+test("multiple when/2 on same variable",(
+    when(nonvar(A), Run1 = true),
+    when(ground(A), Run2 = true),
+    var(Run1), var(Run2),
+    A = a(B),
+    Run1 == true, var(Run2),
+    B = 1,
+    Run2 == true
+)).
+
+main :-
+    findall(test(Name, Goal), test(Name, Goal), Tests),
+    run_tests(Tests, Failed),
+    show_failed(Failed),
+    halt.
+
+main_quiet :-
+    findall(test(Name, Goal), test(Name, Goal), Tests),
+    run_tests_quiet(Tests, Failed),
+    (   Failed = [] ->
+        format("All tests passed", [])
+    ;   format("Some tests failed", [])
+    ),
+    halt.
+
+portray_failed_([]) --> [].
+portray_failed_([F|Fs]) -->
+    "\"", F, "\"",  "\n", portray_failed_(Fs).
+
+portray_failed([]) --> [].
+portray_failed([F|Fs]) -->
+    "\n", "Failed tests:", "\n", portray_failed_([F|Fs]).
+
+show_failed(Failed) :-
+    phrase(portray_failed(Failed), F),
+    format("~s", [F]).
+
+run_tests([], []).
+run_tests([test(Name, Goal)|Tests], Failed) :-
+    format("Running test \"~s\"~n", [Name]),
+    (   call(Goal) ->
+        Failed = Failed1
+    ;   format("Failed test \"~s\"~n", [Name]),
+        Failed = [Name|Failed1]
+    ),
+    run_tests(Tests, Failed1).
+
+run_tests_quiet([], []).
+run_tests_quiet([test(Name, Goal)|Tests], Failed) :-
+    (   call(Goal) ->
+        Failed = Failed1
+    ;   Failed = [Name|Failed1]
+    ),
+    run_tests_quiet(Tests, Failed1).
+
+assert_p(A, B) :-
+    phrase(portray_clause_(A), Portrayed),
+    phrase((B, ".\n"), Portrayed).
+
+call_residual_goals(Goal, ResidualGoals) :-
+    call_residue_vars(Goal, Vars),
+    variables_residual_goals(Vars, ResidualGoals).
+
+variables_residual_goals(Vars, Goals) :-
+    phrase(variables_residual_goals(Vars), Goals).
+
+variables_residual_goals([]) --> [].
+variables_residual_goals([Var|Vars]) -->
+    dif_:attribute_goals(Var),
+    variables_residual_goals(Vars).
+

src/toplevel.pl

@@ -1,7 +1,5 @@
-:- module('$toplevel', [argv/1,
+:- module('$toplevel', []).
-                        copy_term/3]).
 
-:- use_module(library(atts), [call_residue_vars/2]).
 :- use_module(library(charsio)).
 :- use_module(library(error)).
 :- use_module(library(files)).
@@ -9,11 +7,13 @@
 :- use_module(library(lambda)).
 :- use_module(library(lists)).
 :- use_module(library(si)).
+:- use_module(library(os)).
 
 :- use_module(library('$project_atts')).
 :- use_module(library('$atts')).
 
 :- dynamic(disabled_init_file/0).
+:- dynamic(started/0).
 
 load_scryerrc :-
     (  '$home_directory'(HomeDir) ->
@@ -26,24 +26,18 @@ load_scryerrc :-
     ;  true
     ).
 
-:- dynamic(argv/1).
+'$repl' :-
-
+    asserta('$toplevel':started),
-'$repl'([_|Args0]) :-
+    raw_argv(Args0),
-    \+ argv(_),
+    (   append(Args1, ["--"|_], Args0) ->
-    (   append(Args1, ["--"|Args2], Args0) ->
-        asserta('$toplevel':argv(Args2)),
         Args = Args1
-    ;   asserta('$toplevel':argv([])),
+    ;   Args = Args0
-        Args = Args0
     ),
-    delegate_task(Args, []),
+    (   Args = [_|TaskArgs] ->
-    (\+ disabled_init_file -> load_scryerrc ; true),
+	delegate_task(TaskArgs, [])
-    repl.
-'$repl'(_) :-
-    (   \+ argv(_) -> asserta('$toplevel':argv([]))
     ;   true
     ),
-    load_scryerrc,
+    (\+ disabled_init_file -> load_scryerrc ; true),
     repl.
 
 delegate_task([], []).
@@ -134,7 +128,7 @@ run_goals([g(Gs0)|Goals]) :- !,
                   write_term(Exception, [double_quotes(DQ)]), nl % halt?
               )
         ) -> true
-    ;   write('Warning: initialization failed for: '),
+    ;   write('% Warning: initialization failed for: '),
         write_term(Goal, [variable_names(VNs),double_quotes(DQ)]), nl
     ),
     run_goals(Goals).
@@ -191,7 +185,7 @@ submit_query_and_print_results_(Term, VarList) :-
     bb_put('$report_all', false),
     bb_put('$report_n_more', 0),
     expand_goal(Term, user, Term0),
-    atts:call_residue_vars(user:Term0, AttrVars),
+    call_residue_vars(user:Term0, AttrVars),
     write_eqs_and_read_input(B, VarList, AttrVars),
     !.
 submit_query_and_print_results_(_, _) :-
@@ -314,7 +308,11 @@ write_eqs_and_read_input(B, VarList, AttrVars) :-
     % one layer of depth added for (=/2) functor
     '$term_variables_under_max_depth'(OrigVars, 22, Vars0),
     '$project_atts':project_attributes(Vars0, AttrVars),
-    copy_term(AttrVars, AttrVars, AttrGoals),
+    % Need to copy all the visible Vars here so that they appear
+    % properly in AttrGoals, even the non-attributed. Need to also
+    % copy all the attributed variables here so that anonymous
+    % attributed variables also appear properly in AttrGoals.
+    copy_term([Vars0, AttrVars], [Vars0, AttrVars], AttrGoals),
     term_variables(AttrGoals, AttrGoalVars),
     append([Vars0, AttrGoalVars, AttrVars], Vars),
     charsio:extend_var_list(Vars, VarList, NewVarList, fabricated),
@@ -452,4 +450,3 @@ print_exception_with_check(E) :-
     % is expected to be printed instead.
     ;  print_exception(E)
     ).
-

tests-pl/iso-conformity-tests.pl

@@ -1005,6 +1005,18 @@ test_311 :- test_syntax_error("Finis ().", syntax_error(incomplete_reduction)).
 test_318 :- writeq_term_to_chars(+((1*2)^3), C),
             C == "+ (1*2)^3".
 
+test_320 :- writeq_term_to_chars([a|\+2], C),
+            C == "[a|\\+2]".
+
+test_321 :- test_syntax_error("writeq((a)(b)).", syntax_error(incomplete_reduction)).
+
+test_324 :- writeq_term_to_chars('%', C),
+            C == "'%'".
+
+test_325 :- test_syntax_error("writeq({[y}]).", syntax_error(incomplete_reduction)).
+
+test_326 :- test_syntax_error("(>)(1,2).", syntax_error(incomplete_reduction)).
+
 run_tests([Test|Tests]) -->
     (  { call(Test) } ->
        []

tests/scryer/cli/issues/display_constraints.stdin

@@ -0,0 +1,5 @@
+X = 1.
+use_module(library(dif)).
+X = 1.
+dif(X,1).
+halt.

tests/scryer/cli/issues/display_constraints.stdout

@@ -0,0 +1,4 @@
+   X = 1.
+   true.
+   X = 1.
+   dif:dif(X,1).

tests/scryer/cli/issues/display_constraints.toml

@@ -0,0 +1,2 @@
+# issue 857
+args = ["-f", "--no-add-history"]

tests/scryer/cli/issues/do_not_duplicate_path_components.stdin

@@ -0,0 +1,3 @@
+['throw_e.pl'].
+['throw_e.pl'].
+halt.

tests/scryer/cli/issues/do_not_duplicate_path_components.stdout

@@ -0,0 +1,2 @@
+   throw(e).
+   throw(e).

tests/scryer/cli/issues/do_not_duplicate_path_components.toml

@@ -0,0 +1,2 @@
+# issue 852
+args = ["-f", "--no-add-history"]

tests/scryer/cli/issues/goals_compound_goal.stdout

@@ -0,0 +1 @@
+helloworld

tests/scryer/cli/issues/goals_compound_goal.toml

@@ -0,0 +1,2 @@
+# issue 820
+args = ["-f", "--no-add-history", "-g", "test,halt", "goals.pl"]

tests/scryer/cli/issues/goals_multiple_goals.in/goals.pl

@@ -0,0 +1,3 @@
+test :- write(world), nl.
+
+:- initialization(write(hello)).

tests/scryer/cli/issues/goals_multiple_goals.stdout

@@ -0,0 +1 @@
+helloworld

tests/scryer/cli/issues/goals_multiple_goals.toml

@@ -0,0 +1,2 @@
+# issue 820
+args = ["-f", "--no-add-history", "-g", "test", "-g", "halt", "goals.pl"]

tests/scryer/cli/issues/handle_residual_goal.stdin

@@ -0,0 +1,11 @@
+use_module(library(dif)).
+use_module(library(iso_ext)).
+-X\=X.
+-X=X.
+dif(-X,X).
+dif(-X,X), -X=X.
+call_residue_vars(dif(-X,X), Vars).
+set_prolog_flag(occurs_check, true).
+-X\=X.
+dif(-X,X).
+halt.

tests/scryer/cli/issues/handle_residual_goal.stdout

@@ -0,0 +1,10 @@
+   true.
+   true.
+   false.
+   X = -X.
+   dif:dif(-X,X).
+   false.
+   Vars = [X], dif:dif(-X,X).
+   true.
+   true.
+   true.

tests/scryer/cli/issues/handle_residual_goal.toml

@@ -0,0 +1,2 @@
+# issue 844
+args = ["-f", "--no-add-history"]

tests/scryer/cli/issues/ignored_constraint.stdin

@@ -0,0 +1,2 @@
+use_module(library(freeze)), freeze(X,false), X \=a.
+halt.

tests/scryer/cli/issues/ignored_constraint.stdout

@@ -0,0 +1 @@
+   freeze:freeze(X,false).

tests/scryer/cli/issues/ignored_constraint.toml

@@ -0,0 +1,2 @@
+# issue 807
+args = ["-f", "--no-add-history"]

tests/scryer/cli/issues/no_stutter.stdin

@@ -0,0 +1,2 @@
+write(a), write(b), false.
+halt.

tests/scryer/cli/issues/no_stutter.stdout

@@ -0,0 +1 @@
+ab   false.

tests/scryer/cli/issues/no_stutter.toml

@@ -0,0 +1,2 @@
+# issue 815
+args = ["-f", "--no-add-history"]

tests/scryer/cli/issues/occurs_check_flag.stdin

@@ -0,0 +1,2 @@
+f(X, X).
+halt.

tests/scryer/cli/issues/occurs_check_flag.stdout

@@ -0,0 +1 @@
+   false.

tests/scryer/cli/issues/occurs_check_flag.toml

@@ -0,0 +1,2 @@
+# issue 841
+args = ["-f", "--no-add-history", "occurs_check_example.pl"]

tests/scryer/cli/issues/occurs_check_flag2.stdin

@@ -0,0 +1,6 @@
+set_prolog_flag(occurs_check, true).
+X = -X.
+asserta(f(X,g(X))).
+f(X,X).
+X-X = X-g(X).
+halt.

tests/scryer/cli/issues/occurs_check_flag2.stdout

@@ -0,0 +1,5 @@
+   true.
+   false.
+   true.
+   false.
+   false.

tests/scryer/cli/issues/occurs_check_flag2.toml

@@ -0,0 +1,2 @@
+# issue 841
+args = ["-f", "--no-add-history"]

tests/scryer/cli/issues/op3.toml

@@ -0,0 +1,2 @@
+# issue 839
+args = ["-f", "--no-add-history", "op3.pl", "-g", "halt"]

tests/scryer/cli/issues/os_argv-no-final--.stdin

@@ -0,0 +1,6 @@
+os:argv(V).
+os:argv(["test1"|_]).
+os:argv(["--"|_]).
+os:argv([V, "--"|_]).
+os:argv(["test2"|_]).
+os:argv([]).

tests/scryer/cli/issues/os_argv-no-final--.stdout

@@ -0,0 +1,6 @@
+   V = ["test1","--","test2"].
+   true.
+   false.
+   V = "test1".
+   false.
+   false.

tests/scryer/cli/issues/os_argv-no-final--.toml

@@ -0,0 +1,2 @@
+# https://github.com/mthom/scryer-prolog/pull/2263#issuecomment-1874400820
+args = ["-f", "--no-add-history", "--", "test1", "--", "test2"]