GeoffChurch

"""
Provides speculative_if(cond, branch1, branch2), which runs branch1 followed by
branch2 while cond is running.
"""

from dataclasses import dataclass
import itertools
import multiprocessing as mp
import time

GeoffChurch

:- op(700, xfx, .=).

A:AFs .= B:BFs =>
    gets(AFs, A, Val),
    gets(BFs, B, Val).
X:Fs .= Val  => gets(Fs, X, Val).
Val  .= X:Fs => gets(Fs, X, Val).
A    .= B    => A = B.

colon_list(X:Xs0, Out) => colon_list(Xs0, Xs), Out = [X|Xs].

GeoffChurch

% The following is a 3-line meta-interpreter for pure Prolog (no
% cuts/negation). It reifies conjunction and dispatch, leaving
% unification and backtracking implicit. It is written for brevity,
% leveraging DCG notation and using lists to denote conjunctions of
% goals. It implements the semantics of a program (in the sense of a
% set of rules or "immediate consequence operator") as the program's
% least fixed point, obtained by "reflexive transitive closure" /
% exponential / "Kleene iteration".

%%%%%

GeoffChurch

from os import get_terminal_size
from time import sleep

terminal_size = get_terminal_size()
num_cells = terminal_size.columns # We'll have as many cells as can fit in the terminal's width
sleep_time = 4.0 / terminal_size.lines # Animation speed will be proportional to the terminal's height

# Lookup table for Wolfram's "rule 30" cellular automaton
RULE_30 = {
  (0,0,0) : 0,

GeoffChurch

unescape(\X, X). % Subterms, and in particular logic variables, can be marked as pre-evaluated.

cata(Alg) --> unescape *-> {} ; mapargs(cata(Alg)), call(Alg).

% Example:

alg( 0 +  0,  0).
alg( 0 +  1,  1).
alg( 1 +  0,  1).
alg( 1 + 12, 13).

GeoffChurch

foldargs(Goal, A, B) -->
    { maplist(functor_arity_term_args(_, _), [A, B], [As, Bs]) },
    foldl(Goal, As, Bs).

functor_arity_term_args(Functor, Arity, Term, Args) :-
    functor(Term, Functor, Arity),
    Term =.. [_|Args].

GeoffChurch

%!  unifier(@Term1, @Term2, ?Unifier) is semidet.
%
%   Like SWI Prolog's unifiable/3, but maintains the left-right order of the terms in the unifier, rather than placing variables on the left.
unifier(A, B, Unifier) :-
    rb_empty(Seen),
    unifier_(Seen, A, B, [], Unifier0),
    exclude(unifier_is_reflexive, Unifier0, Unifier1),
    sort(Unifier1, Unifier).

unifier_(Seen0, A, B, Unifier0, Unifier) :-

GeoffChurch

copy_term(VarsIn, In, VarsOut, Out) :-
  term_variables(In, AllVarsIn),
  maplist(list_to_ord_set, [AllVarsIn, VarsIn], [AllVarsInOrdSet, VarsInOrdSet]),
  ord_subtract(AllVarsInOrdSet, VarsInOrdSet, PreservedVars),
  copy_term(PreservedVars-VarsIn-In, PreservedVars-VarsOut-Out).

GeoffChurch

:- use_module(library(reif)).

phrase_t(P, I, O, T) :- phrase(call(P, T), I, O).

if_(If, Then, Else, I, O) :-
    if_(phrase_t(If, I, M),
	phrase(Then, M, O),
	phrase(Else, M, O)).

% Example:

GeoffChurch

import Data.Void ( Void )

dneFalse :: ((Void -> Void) -> Void) -> Void
dneFalse f = f id

dneTrue :: ((() -> Void) -> Void) -> ()
dneTrue _ = ()