deprime.elpi

kind unit                type.
type unit                unit.

kind spec                type.

kind bool                type.
type btrue               bool.
type bfalse              bool.

kind literal             type.
type unit                literal.
type i                   int -> literal.
type b                   bool -> literal.
type s                   string -> literal.


kind constructor type.

kind tm                  type.

type nom                 tm -> prop.
type abstract_value      tm -> prop.
type pattern_variable    tm -> prop.

type lam                 (tm -> tm) -> tm.
type app                 tm -> tm -> tm.
type let                 tm -> (tm -> tm) -> tm.

type backslash           (tm -> tm) -> tm.
type arobase             tm -> tm -> tm.
type new                 (tm -> tm) -> tm.
type tprint              tm -> tm.
type failwith            tm -> tm.

type lit                 literal -> tm.
type special             spec -> list tm -> tm.

type if_then_else        tm -> tm -> tm -> tm.

type variant             constructor -> list tm -> tm.
type match               tm -> list clause -> tm.

kind pat                 type.

type pany                pat.
type plit                literal -> pat.
type pvar                tm -> pat.
type pnom                tm -> pat.
type pbackslash          (tm -> pat) -> pat.
type parobase            pat -> tm -> pat.
type pvariant            constructor -> list pat -> pat.

kind clause              type.

type arr                 pat -> tm -> clause.
type all                 (tm -> clause) -> clause.
type nab                 (tm -> clause) -> clause.

type val                 tm -> prop.
type eval                tm -> tm -> prop.
type eval_spec           spec -> list tm -> tm -> prop.

kind binding             type.
type bind                tm -> tm -> binding.

type fix                 (tm -> tm) -> tm.

% A "row" <t1; t2; t3> is a piece of program that denotes not a single
% term, but a composite of several terms together.
%
% A row should not be confused with a list literal, such as [t1; t2;
% t3], which is a *single term* containing several subterms. Rows
% belong to a different syntactic category.
%
% (select i row) is a term-former which extracts the i-th term from a row.
%
% Rows are useful to definite mutual fixpoints, as a fixpoint on
% a row.
kind tmrow               type.
type row                 list tm -> tmrow.
type select              int -> tmrow -> tm.
type rowfix              (tmrow -> tmrow) -> tmrow.
type letrow              tmrow -> (tmrow -> tm) -> tm.

val (lam _).
val (lit L) :- val_lit L.

val N :- nom N.
val A :- abstract_value A.

val_lit unit.
val_lit (i _). % TODO: ?
val_lit (s _). % TODO: ?
val_lit (b btrue).
val_lit (b bfalse).

val (variant _C Vs) :- foreach val Vs.
val (backslash R) :- pin x \ val (R x).

pin G :- pi x \ nom x => G x.
piv G :- pi x \ abstract_value x => G x.

% This is merely an optimization, and it makes debug traces easier to read.
eval V V :- val V, !.

eval (lam R) (lam R).
eval (lit L) (lit L) :- val_lit L.

eval N N :- nom N.
eval A A :- abstract_value A.

eval (app T U) V :-
    eval T (lam R),
    eval U VU,
    eval (R VU) V.

eval (let Def Body) V :-
    eval Def VDef,
    eval (Body VDef) V.

eval (new R) V :- sigma W \ pin x \ (sigma U\ eval (R x) U,
    (U = W, !; err_escaped x (new), !, false)), W = V.

eval (backslash R) (backslash VR):-
    pin x \ eval (R x) (VR x).

eval (arobase T N) V :-
    nom N,
    eval T (backslash R),
    eval (R N) V.

eval (special Spec Args) V :- eval_spec Spec Args V.

eval (if_then_else TP TA TB) V :-
    eval TP (lit (b B)),
    if (B = btrue) (eval TA V) (eval TB V).

eval (variant C Ts) (variant C Vs) :- foreach2 eval Ts Vs.

type equal spec.
type add   spec.
type sub   spec.
type mul   spec.
type and   spec.
type or    spec.
type seq    spec.

is_int (lit (i N)) N.
is_bool (lit (b B)) B.

int_op E1 E2 V3 Op :-
    eval E1 V1,
    eval E2 V2,
    is_int V1 N1,
    is_int V2 N2,
    Op N1 N2 N3,
    is_int V3 N3.

eval_spec add [E1, E2] V3 :-
    int_op E1 E2 V3
     (N1 \ N2 \ N3 \
      N3 is N1 + N2).

eval_spec mul [E1, E2] V3 :-
    int_op E1 E2 V3
     (N1 \ N2 \ N3 \
      N3 is N1 * N2).

eval_spec sub [E1, E2] V3 :-
    int_op E1 E2 V3
     (N1 \ N2 \ N3 \
      N3 is N1 - N2).


eval_spec or [E1, E2] V3 :-
    eval E1 V1,
    if (V1 = (lit (b btrue)))
       (V3 is lit (b btrue))
       (eval E2 V3).

eval_spec and [E1, E2] V3 :-
    eval E1 V1,
    if (V1 = (lit (b btrue)))
       (eval E2 V3)
       (V3 is lit (b bfalse)).


eval_spec seq [E1, E2] V3 :-
    eval E1 _V1,
    eval E2 V3.

if P Q _R :- P, !, Q.
if _P _Q R :- R.

eval_spec equal [E1, E2] V3 :-
    eval E1 V1,
    eval E2 V2,
    %is_int V1 N1,
    %is_int V2 N2,
    if (V1 = V2) (B = btrue) (B = bfalse),
    is_bool V3 B.

eval_row (row Ts) (row Vs) :-
    foreach2 eval Ts Vs.

eval (select N Row) V :-
    eval_row Row (row Vs),
    eval_select N Vs V.

eval_select 0 (V::_) V.
eval_select N (_::Vs) V :-
    Nm1 is N - 1,
    eval_select Nm1 Vs V.

eval (letrow RowDef Body) V :-
    eval_row RowDef VR,
    eval (Body VR) V.

eval (tprint T) (lit unit) :- print T.
eval (failwith T) _V :- print T, fail.

eval (match T Cls) V :-
    eval T VT,
    eval_clauses VT Cls V.

type eval_clauses tm -> list clause -> tm -> prop.
eval_clauses _VL [] _VR :- false.
eval_clauses VL (Cl::Cls) VR :-
    if (eval_clause VL Cl [] R)
      (eval R VR)
      (!, eval_clauses VL Cls VR).

type eval_clause tm -> clause -> list binding -> tm -> prop.
eval_clause L (all RCl) Sigma (R Vx) :-
  pi x \ pattern_variable x =>
  eval_clause L (RCl x) (Sigma_in x) (R x),
  extract (Sigma_in x) x Vx Sigma.

eval_clause L (nab RCl) Sigma (R Y) :-
  pin x \
  locate_rigid_clause x Y L (RCl x), !,
  subst copy [bind Y x] L (Lx x),
  eval_clause (Lx x) (RCl x) Sigma (R x).

eval_clause L (arr P R) Sigma R :-
  matches L P Sigma.

type extract   list binding -> tm -> tm -> list binding -> prop.
extract (bind X Y :: Sigma) X Y Sigma :- !.
extract (bind X1 Y1 :: Sigma1) X2 Y2 (bind X1 Y1 :: Sigma2) :-
    not (X1 = X2), !,
    extract Sigma1 X2 Y2 Sigma2.

type concat_bindings  list binding -> list binding -> list binding -> prop.
concat_bindings [] Subst2 Subst2.
concat_bindings (bind X Y :: Subst1) Subst2 (bind X Y :: Subst3) :-
    concat_bindings Subst1 Subst2 Subst3.

type subst   (A -> A -> prop) -> list binding -> A -> A -> prop.
subst Copy Subst Tin Tout :-
    if (current_subst _)
      (print "assert failure in subst", !, false)
      (current_subst Subst => Copy Tin Tout).

copy_nom N1 N2 :-
    nom N1,
    current_subst Subst,
    binds Subst N1 N2.

binds [] X1 Y1 :- X1 = Y1.
binds (bind X1 Y1 :: Subst) X2 Y2 :-
    if (X1 = X2)
       (Y1 = Y2)
       (binds Subst X2 Y2).

kind list_path type.
type now       list_path.
type next      list_path -> list_path.

type in_list  A -> list_path -> list A -> prop.
in_list X now      (Y :: _Ys) :- X = Y.
in_list X (next P) (_Y :: Ys) :- in_list X P Ys.

kind value_path         type.
type here               value_path.
type under_cons         constructor -> list_path -> value_path -> value_path.
type under_backslash    (tm -> value_path) -> value_path.
type under_arobase      value_path -> tm -> value_path.

type rigid_in_clause    tm -> value_path -> clause -> prop.
rigid_in_clause X Path (all Cl) :-
    piv x \ rigid_in_clause X Path (Cl x).
rigid_in_clause X Path (nab Cl) :-
    pin x \ rigid_in_clause X Path (Cl x).
rigid_in_clause X Path (arr P _) :-
    rigid_in_pat X Path P.

type rigid_in_pat       tm -> value_path -> pat -> prop.
rigid_in_pat X here (pnom X).
rigid_in_pat X here (pvar X).
rigid_in_pat X (under_cons C N Path) (pvariant C Ps) :-
    in_list P N Ps,
    rigid_in_pat X Path P.
rigid_in_pat X (under_backslash Pathx) (pbackslash Px) :-
    pin x \ (rigid_in_pat X) (Pathx x) (Px x).
rigid_in_pat X (under_arobase Path Y) (parobase P Y) :-
    not (X = Y),
    rigid_in_pat X Path P.

type rigid_in_val      tm -> value_path -> tm -> prop.
rigid_in_val X here X.
rigid_in_val X (under_cons C N Path) (variant C Vs) :-
    in_list V N Vs,
    rigid_in_val X Path V.
rigid_in_val X (under_backslash Pathx) (backslash R) :-
    pin x \ rigid_in_val X (Pathx x) (R x).
rigid_in_val X (under_arobase Path Y) (Vx Y) :-
    rigid_in_val X Path (backslash (x \ Vx x)).

type locate_rigid_clause   tm -> tm -> tm -> clause -> prop.
type locate_rigid   tm -> tm -> tm -> pat -> prop.

type silence-rigid-occurrence-constraint prop.
locate_rigid_clause Xin Xout V Cl :-
    (rigid_in_clause Xin Path Cl, !;
     not silence-rigid-occurrence-constraint, !,
     term_to_string Xin XinStr,
     term_to_string Cl PStr,
     ErrMsg is "Nominal " ^ XinStr ^ " has no rigid occurrence in " ^ PStr,
     eval_error ErrMsg,
     false),
    rigid_in_val Xout Path V.

type current_subst list binding -> prop.
type copy         tm -> tm -> prop.
type copy_nom     tm -> tm -> prop.
type copy_clause  clause -> clause -> prop.
type copy_pat     pat -> pat -> prop.
type copy_row     tmrow -> tmrow -> prop.


type underv    (A -> B -> prop) -> ((tm -> A) -> (tm -> B) -> prop).
type undern    (A -> B -> prop) -> ((tm -> A) -> (tm -> B) -> prop).
type under_row (A -> B -> prop) -> ((tmrow -> A) -> (tmrow -> B) -> prop).

copy (lit L1) (lit L2) :- L1 = L2.
copy V V :- abstract_value V.
copy N1 N2 :-
    nom N1,
    copy_nom N1 N2.
copy V T :-
    pattern_variable V,
    current_subst Subst,
    binds Subst V T.

underv Copy R1 R2 :- piv x \ Copy (R1 x) (R2 x).
undern Copy R1 R2 :- pin x \ copy_nom x x => Copy (R1 x) (R2 x).



copy (lam R1) (lam R2) :- underv copy R1 R2.
copy (app M1 N1) (app M2 N2) :- copy M1 M2, copy N1 N2.
copy (let M1 R1) (let M2 R2) :- copy M1 M2, underv copy R1 R2.
copy (backslash R1) (backslash R2) :- undern copy R1 R2.
copy (arobase M1 X1) (arobase M2 X2) :- copy M1 M2, copy_nom X1 X2.

copy (tprint X1) (tprint X2) :- copy X1 X2.
copy (failwith X1) (failwith X2) :- copy X1 X2.

copy (new R1) (new R2) :- undern copy R1 R2.
copy (special Sp T1s) (special Sp T2s) :- foreach2 copy T1s T2s.
copy (if_then_else P1 T1 E1) (if_then_else P2 T2 E2) :-
    copy P1 P2, copy T1 T2, copy E1 E2.

copy (variant C T1s) (variant C T2s) :- foreach2 copy T1s T2s.
copy (match M1 Cl1s) (match M2 Cl2s) :-
    copy M1 M2, foreach2 copy_clause Cl1s Cl2s.

copy_clause (arr P1 T1) (arr P2 T2) :- copy_pat P1 P2, copy T1 T2.
copy_clause (all C1) (all C2) :- underv copy_clause C1 C2.
copy_clause (nab C1) (nab C2) :- undern copy_clause C1 C2.

copy_pat pany pany.
copy_pat (plit L1) (plit L2) :- L1 = L2.
copy_pat (pvar X1) (pvar X2) :- copy X1 X2.
copy_pat (pnom N1) (pnom N2) :- copy_nom N1 N2.
copy_pat (pbackslash R1) (pbackslash R2) :- undern copy_pat R1 R2.
copy_pat (parobase P1 X1) (parobase P2 X2) :- copy_pat P1 P2, copy_nom X1 X2.
copy_pat (pvariant C P1s) (pvariant C P2s) :- foreach2 copy_pat P1s P2s.

copy (fix F1) (fix F2) :- underv copy F1 F2.

under_row Copy R1 R2 :- pi x \ copy_row x x => Copy (R1 x) (R2 x).

copy_row (row R1) (row R2) :- foreach2 copy R1 R2.
copy (select N R1) (select N R2) :- copy_row R1 R2.
copy_row (rowfix F1) (rowfix F2) :- under_row copy_row F1 F2.
copy (letrow R1 B1) (letrow R2 B2) :-
    copy_row R1 R2, under_row copy B1 B2.

% on paper: (v matches p as σ)
type matches    tm -> pat -> list binding -> prop.

matches _ pany [].

matches (lit L) (plit L) [].

matches X (pvar Y) [bind Y X] :-
    pattern_variable Y.

matches X (pnom X) [].

matches (variant C Vs) (pvariant C Ps) TmSubst :-
    matches_all Vs Ps TmSubst.

matches_all [] [] [].
matches_all (V :: Vs) (P :: Ps) TmSubst_all :-
    matches V P TmSubst,
    matches_all Vs Ps TmSubst_rest,
    concat_bindings TmSubst TmSubst_rest TmSubst_all.

matches (backslash V) (pbackslash P) TmSubst :-
    pin x \ matches (V x) (P x) TmSubst.

matches V (parobase P X) TmSubst :-
    nom X,
    sigma Vx \
    pin x \
    subst copy [bind X x] V (Vx x),
    matches (backslash (x \ Vx x)) P TmSubst.

eval (fix F) V :- eval (F (fix F)) V.
eval_row (rowfix F) VR :- eval_row (F (rowfix F)) VR.

type foreach (A -> prop) -> list A -> prop.
foreach _P [].
foreach P (X::Xs) :- P X, foreach P Xs.

type foreach2 (A -> B -> prop) -> list A -> list B -> prop.
foreach2 _P [] [].
foreach2 P (X::Xs) (Y::Ys) :-
    P X Y, foreach2 P Xs Ys.

type any2 (A -> B -> prop) -> list A -> list B -> prop.
any2 P (X::Xs) (Y::Ys) :-
    P X Y; any2 P Xs Ys.