(* Variables *)
type low_boundary = int
datatype high_boundary = RESTRICTED of int | UNRESTRICTED
type var_spec = {
low: low_boundary,
high: high_boundary,
nesting: bool
}
type var_index = string
type var = var_spec * var_index
fun rigid (({high = UNRESTRICTED,...},_):var) = false
| rigid ({low = lo,high = RESTRICTED hi,...},_) = (lo = hi)
fun flex v = not (rigid v)
fun check_len (({low = lo, high = UNRESTRICTED, ...},_):var, len: int) =
(len >= lo)
| check_len (({low = lo, high = RESTRICTED hi, ...},_), len) =
(len >= lo) andalso (len <= hi)
(* Fractions *)
infix 6 !+! !-!
infix 7 !*! !/!
structure Frac
: sig
type fraction
val frac: int -> fraction
val numerator: fraction -> int
val denominator: fraction -> int
val !+! : fraction * fraction -> fraction
val !-! : fraction * fraction -> fraction
val !*! : fraction * fraction -> fraction
val !/! : fraction * fraction -> fraction
end =
struct
datatype fraction = FR of int * int
fun gcd (x,y) =
let
fun gcd' (a,b) =
let val r = a mod b in
if r = 0 then b else gcd' (b,r)
end
in gcd' (abs x,abs y) end
fun lcm (x,y) = abs(x * y) div gcd(x,y)
fun norm (_,0) = raise Div
| norm (0,_) = FR (0,1)
| norm (n,d) =
if d < 0 then norm(~n,~d)
else let val c = gcd(n,d) in FR (n div c,d div c) end
fun add_op ((n1,d1),(n2,d2)) f =
let
val d = lcm(d1,d2)
val n = f (n1*(d div d1),n2*(d div d2))
in norm (n,d) end
fun frac x = FR (x,1)
fun numerator (FR (n,_)) = n
fun denominator (FR (_,d)) = d
fun ((FR (n1,d1)) !+! (FR (n2,d2))) = add_op ((n1,d1),(n2,d2)) (op +)
fun ((FR (n1,d1)) !-! (FR (n2,d2))) = add_op ((n1,d1),(n2,d2)) (op -)
fun ((FR (n1,d1)) !*! (FR (n2,d2))) = norm (n1*n2,d1*d2)
fun ((FR (n1,d1)) !/! (FR (n2,d2))) = norm (n1*d2,d1*n2)
end
(* Matrices *)
structure Matrix
: sig
datatype column_label
= VAR_LABEL of var_index
| ARG_LABEL of int
| FREE_LABEL
type matrix
val matrix: int * (column_label list) -> matrix
val sub: matrix * int * int -> Frac.fraction
val update: matrix * int * int * Frac.fraction -> unit
val size: matrix -> int * int
val labelIndex: matrix * column_label -> int
val labelArray: matrix -> column_label Array.array
val swapRows: matrix * int * int -> unit
val swapCols: matrix * int * int -> unit
val divRow: matrix * int * Frac.fraction -> unit
val addRow: matrix * int * int * int * Frac.fraction -> unit
val gauss: matrix -> bool
end =
struct
local open Frac in
datatype column_label
= VAR_LABEL of var_index
| ARG_LABEL of int
| FREE_LABEL
datatype matrix = M of (column_label array) * (fraction array array)
fun matrix (m,labels) =
let
val n = List.length labels
val i = ref 1
val rows = Array.array (m,Array.array (n,frac 0))
in
while !i < m do (
Array.update (rows,!i,Array.array (n,frac 0));
i := !i + 1
);
M (Array.fromList labels, rows)
end
fun sub (M (_,rows),i,j) = Array.sub (Array.sub (rows,i),j)
fun update (M (_,rows),i,j,x) = Array.update (Array.sub (rows,i),j,x)
fun size (M (labels,rows)) = (Array.length rows,Array.length labels)
fun labelArray (M (labels,_)) = labels
fun labelIndex (M (labels,_),lab) =
let val j = ref 0 and len = Array.length labels in
while !j < len andalso Array.sub(labels,!j) <> lab do
!j = !j + 1;
if !j < len then !j else ~1
end
fun swap (p,q) ar =
let val vp = Array.sub (ar,p) and vq = Array.sub (ar,q) in
( Array.update(ar,p,vq); Array.update(ar,q,vp) )
end
fun swapRows (M (_,rows),i1,i2) = swap (i1,i2) rows
fun swapCols (M (labels,rows),j1,j2) =
( swap (j1,j2) labels; Array.app (swap (j1,j2)) rows )
fun divRow (M (_,rows),i,c) =
let val row = Array.sub (rows,i) in
Array.modify (fn x => x !/! c) row
end
fun addRow (M (_,rows),start_j,dest_i,src_i,c) =
let
val dest = Array.sub (rows,dest_i) and src = Array.sub (rows,src_i)
fun f (j,x) = x !+! (Array.sub (src,j) !*! c)
in
Array.modifyi f (dest,start_j,NONE)
end
fun gauss matr =
let
val (m',n) = size matr
val m = ref m'
val i = ref 0 and j = ref 0 and k = ref 0
val result = ref true
in
while !i < !m andalso !result do (
j := n-1;
while !j = n-1 andalso !m > !i andalso !result do (
j := !i;
while !j < n-1 andalso sub(matr,!i,!j) = (frac 0) do
j := !j + 1;
if !j = n-1
then if sub(matr,!i,n-1) = (frac 0)
then (
swapRows(matr,!i,!m-1);
m := !m - 1
)
else result := false
else (
swapCols(matr,!i,!j);
divRow(matr,!i,sub(matr,!i,!i))
)
);
k := !i + 1;
while !k < !m do (
addRow(matr,!i,!k,!i,
(frac 0) !-! sub(matr,!k,!i) !/! sub(matr,!i,!i)
);
k := !k + 1
);
i := !i + 1
);
i := !m-1;
while !i > 0 andalso !result do (
k := !i - 1;
while !k >= 0 do (
addRow(matr,0,!k,!i,
(frac 0) !-! sub(matr,!k,!i) !/! sub(matr,!i,!i)
);
k := !k - 1
);
i := !i - 1
);
!result
end
end
end
(* Refal core *)
signature ATOM = sig
type atom
val equal: (atom * atom) -> bool
end
datatype direction = LEFT | RIGHT
datatype attribute
= DIR of direction
| NOATTR
infixr :<:
infixr :>:
functor RefalCore (A: ATOM) = struct
(* Expressions *)
structure Expr
: sig
type expr
datatype term
= EX of expr
| AT of A.atom
| VAR of var
val :<: : expr * term -> expr
val :>: : term * expr -> expr
val empty: attribute -> expr
val length: expr -> int
val attr: expr -> attribute
val hd: direction -> expr -> term
val tl: direction -> expr -> expr
val explode: direction -> expr -> (term * expr)
val equal: (expr * expr) -> bool
val equalTerm: (term * term) -> bool
val check_var: (var * expr) -> bool
val split: direction -> (expr * int) -> (expr * expr)
val shift: direction -> (expr * expr) -> (expr * expr)
end =
struct
exception EmptyExpr
datatype expr = E of attribute * (term list)
and term
= EX of expr
| AT of A.atom
| VAR of var
fun ((E (at,e)) :<: t) = E (at,e @ [t])
fun (t :>: (E (at,e))) = E (at,t::e)
fun empty at = E (at,[])
fun length (E (_,e)) = List.length e
fun attr (E (at,_)) = at
fun hd dir (E (_,[])) = raise EmptyExpr
| hd LEFT (E (_,(t::_))) = t
| hd RIGHT (E (_,ts)) = List.last ts
fun tl dir (E (_,[])) = raise EmptyExpr
| tl LEFT (E (at,(_::ts))) = E (at,ts)
| tl RIGHT (E (at,e)) = E (at,List.take (e,List.length e - 1))
fun explode dir ex = (hd dir ex, tl dir ex)
fun equal (E (at1,e1),E (at2,e2)) =
let
fun eq ([],[]) = true
| eq (t1::e1,t2::e2) =
if equalTerm (t1,t2) then eq(e1,e2) else false
| eq _ = false
in
if at1 = at2 then eq (e1,e2) else false
end
and equalTerm (EX e1,EX e2) = equal (e1,e2)
| equalTerm (AT a1,AT a2) = A.equal (a1,a2)
| equalTerm (VAR v1,VAR v2) = (v1 = v2)
| equalTerm _ = false
fun check_var (({low = lo, high = hi, nesting = ne},_), E (_,e)) =
let
val l = List.length e
fun ck_nesting [] = true
| ck_nesting ((EX x)::xs) = false
| ck_nesting (x::xs) = ck_nesting xs
in
(lo <= l) andalso
(case hi
of RESTRICTED h => (l <= h)
| UNRESTRICTED => true
) andalso (ne orelse ck_nesting e)
end
fun split RIGHT (ex,n) =
let val (e1,e2) = split LEFT (ex,(length ex) - n) in (e2,e1) end
| split LEFT (E (at,e),n) =
(E (at,List.take (e,n)), E (at,List.drop (e,n)))
fun shift LEFT (e1,e2) = (e1 :<: (hd LEFT e2), tl LEFT e2)
| shift RIGHT (e1,e2) = ((hd RIGHT e2) :>: e1, tl RIGHT e2)
end
(* Substitutions *)
structure Sub = struct
exception UnknownIndex;
exception DuplicateIndex;
abstype subst = SUB of (var * Expr.expr) list
with
val empty = SUB []
fun toList (SUB vs) = vs
fun contains (SUB vs) v = List.exists (fn (x,_) => x = v) vs
fun value (SUB []) v = raise UnknownIndex
| value (SUB ((v',expr)::vs)) v =
if v = v' then expr else value (SUB vs) v
fun add (sub as (SUB vs)) (v,expr) =
if contains sub v
then if Expr.equal(value sub v,expr)
then sub else raise DuplicateIndex
else SUB ((v,expr)::vs)
end
end
(* Pattern matching *)
datatype result
= SUCCESS of Sub.subst
| UNDEF
local open Expr in
fun match (G,[]) = SUCCESS G
| match (G,L_M) = search (G,[],L_M)
and search (G,X,(A,B)::Y) =
let
fun matchRigidVar dir (v as (spc,_),A') =
if (#low spc) > (length B) then UNDEF
else
let val (Z,B') = split dir (B,#low spc) in
if Sub.contains G v
then if equal(Z,Sub.value G v)
then match (G, X @ [(A',B')] @ Y)
else UNDEF
else if check_var (v,Z)
then match (Sub.add G (v,Z), X @ [(A',B')] @ Y)
else UNDEF
end
fun matchRepeatedFlexVar dir (V,A') =
if (length V) > (length B) then UNDEF
else let val (V',B') = split dir (B,length V) in
if equal (V,V') then match (G, X @ [(A',B')] @ Y) else UNDEF
end
fun matchHard dir (VAR v,A'') =
if rigid v then matchRigidVar dir (v,A'')
else matchRepeatedFlexVar dir (Sub.value G v,A'')
| matchHard dir (t,A'') =
if (length B = 0) then UNDEF else
case (t, explode dir B)
of (EX A',(EX B',B'')) =>
if dir = LEFT then match (G, X@[(A',B'),(A'',B'')]@Y)
else match (G, X@[(A'',B''),(A',B')]@Y)
| (AT Z,(AT Z',B'')) =>
if A.equal(Z,Z') then match (G, X@[(A'',B'')]@Y)
else UNDEF
| _ => UNDEF
fun matchClosedFlexVar (VAR v) =
if check_var (v,B) then match (Sub.add G (v,B), X@Y) else UNDEF
fun unboundFlex (VAR v) = (flex v) andalso not (Sub.contains G v)
| unboundFlex _ = false
in
if (length A) = 0
then if (length B) = 0 then search (G,X,Y) else UNDEF
else
case (length A, unboundFlex(hd LEFT A), unboundFlex(hd RIGHT A))
of (1,true,true) => matchClosedFlexVar (hd LEFT A)
| (_,true,true) => search (G,X @ [(A,B)],Y)
| (_,_,false) => matchHard RIGHT (explode RIGHT A)
| (_,false,_) => matchHard LEFT (explode LEFT A)
end
| search (G,(p,B)::Y,[]) =
let
val (DIR dir) = attr p
val (VAR (v as (spc,_)), A) = explode dir p
fun iterate (Bk,Ck) =
case match (Sub.add G (v,Bk), [(A,Ck)] @ Y)
of UNDEF => if (length Ck) = 0 then UNDEF
else iterate (shift dir (Bk,Ck))
| Gk => Gk
in
if (#low spc) > (length B) then UNDEF
else iterate (split dir (B,#low spc))
end
end
end
(******************************************************************************)
(* Functor implementations *)
datatype r5atom
= CHAR of char
| WORD of string
| INTEGER of int
structure R5Atom: ATOM =
struct
type atom = r5atom
fun equal (a,b) = (a = b)
end
structure R5Core = RefalCore(R5Atom)
(* Pretty-printers *)
structure RefalPP
: sig
val install: unit -> unit
end =
struct
open Compiler
open PrettyPrint
fun pp_var_spec pps { low = 0, high = UNRESTRICTED, nesting = true } =
add_string pps "e"
| pp_var_spec pps { low = 1, high = UNRESTRICTED, nesting = true } =
add_string pps "v"
| pp_var_spec pps { low = 1, high = RESTRICTED 1, nesting = false } =
add_string pps "s"
| pp_var_spec pps { low = 1, high = RESTRICTED 1, nesting = true } =
add_string pps "t"
| pp_var_spec pps { low = lo, high = hi, nesting = ns } =
let
val hiStr =
case hi
of RESTRICTED h => Int.toString h
| _ => "*"
in
add_string pps ("[" ^ (Int.toString lo) ^ "," ^ hiStr ^ "," ^
(Bool.toString ns) ^ "]")
end
fun pp_var pps (s,i) = (pp_var_spec pps s; add_string pps ("." ^ i))
fun pp_r5atom pps (CHAR c) = add_string pps ("'" ^ (Char.toString c) ^ "'")
| pp_r5atom pps (WORD s) = add_string pps ("\"" ^ s ^ "\"")
| pp_r5atom pps (INTEGER i) = add_string pps (Int.toString i)
fun pp_frac pps x =
let val n = Frac.numerator x and d = Frac.denominator x in (
add_string pps (Int.toString n);
if d = 1 then () else add_string pps ("/" ^ (Int.toString d))
)
end
local open Matrix in
fun pp_matrix pps matr =
let
val (m,n) = size matr
val la = labelArray matr
val i = ref 0 and j = ref 0
in
add_string pps ("Matrix ("^(Int.toString m)^","^(Int.toString n)^")");
add_newline pps;
begin_block pps CONSISTENT 2;
while !j < n do (
case Array.sub(la,!j)
of VAR_LABEL ind => add_string pps ("(" ^ ind ^ ")")
| ARG_LABEL n => add_string pps ("[" ^ (Int.toString n) ^ "]")
| FREE_LABEL => add_string pps "f";
j := !j + 1
);
add_newline pps;
while !i < m do (
j := 0;
while !j < n do (
pp_frac pps (sub (matr,!i,!j));
add_string pps " ";
j := !j + 1
);
if !i < (m-1) then add_newline pps else ();
i := !i + 1
);
end_block pps
end
end
local open R5Core.Expr in
fun pp_r5expr pps expr =
let
fun pp e =
if length e = 0 then ()
else (
pp_r5term pps (hd LEFT e);
if (length (tl LEFT e) = 0) then ()
else (
add_string pps " ";
pp (tl LEFT e)
)
)
in
case attr expr
of (DIR LEFT) => add_string pps "$L "
| (DIR RIGHT) => add_string pps "$R "
| _ => ();
pp expr
end
and pp_r5term pps (EX e) = (
add_string pps "(";
pp_r5expr pps e;
add_string pps ")"
)
| pp_r5term pps (AT a) = pp_r5atom pps a
| pp_r5term pps (VAR v) = pp_var pps v
end
local open R5Core.Sub in
fun pp_r5subst pps sub =
let
fun pp_varexpr (v,e) = (
add_string pps "(";
pp_var pps v;
add_string pps " => ";
pp_r5expr pps e;
add_string pps ")"
)
fun pp [] = ()
| pp (x::[]) = pp_varexpr x
| pp (x::xs) = (pp_varexpr x; add_string pps ", "; pp xs)
in
(add_string pps "["; pp (toList sub); add_string pps "]")
end
end
local open R5Core in
fun pp_result pps (SUCCESS sub) = pp_r5subst pps sub
| pp_result pps UNDEF = add_string pps "UNDEF"
end
fun install () = (
PPTable.install_pp ["r5atom"] pp_r5atom;
PPTable.install_pp ["Frac","fraction"] pp_frac;
PPTable.install_pp ["Matrix","matrix"] pp_matrix;
PPTable.install_pp ["R5Core","Expr","expr"] pp_r5expr;
PPTable.install_pp ["R5Core","Sub","subst"] pp_r5subst;
PPTable.install_pp ["R5Core","result"] pp_result
)
end
(* Debugging pm *)
open R5Core
open Expr
val E = { low = 0, high = UNRESTRICTED, nesting = true }
val V = { low = 1, high = UNRESTRICTED, nesting = true }
val S = { low = 1, high = RESTRICTED 1, nesting = false }
val T = { low = 1, high = RESTRICTED 1, nesting = true }
val e'1 = VAR (E,"1")
val e'2 = VAR (E,"2")
val e'3 = VAR (E,"3")
val e'4 = VAR (E,"4")
val e'w = VAR (E,"w")
val v'1 = VAR (V,"1")
val v'2 = VAR (V,"2")
val s'1 = VAR (S,"1")
val s'2 = VAR (S,"2")
val t'1 = VAR (T,"1")
val t'2 = VAR (T,"2")
fun wrd w = (AT (WORD w))
fun intgr i = (AT (INTEGER i))
val lpat = e'1 :>: (wrd "+") :>: e'2 :>: empty (DIR LEFT)
val rpat = e'1 :>: (wrd "+") :>: e'2 :>: empty (DIR RIGHT)
val expr = (intgr 1) :>: (intgr 2) :>: (wrd "+") :>:
(intgr 3) :>: (intgr 4) :>: (wrd "+") :>: (intgr 5) :>: empty NOATTR
val pat2 = e'1 :>: (wrd "+") :>:
(EX (e'1 :>: e'2 :>: (wrd "|") :>: e'3 :>: empty (DIR RIGHT))) :>:
empty (DIR LEFT)
val expr2 = (intgr 1) :>: (intgr 2) :>: (wrd "+") :>:
(EX ((intgr 1) :>: (intgr 2) :>: (intgr 3) :>: (wrd "|") :>:
(intgr 4) :>: (intgr 5) :>: (wrd "|") :>: (intgr 6) :>: (intgr 7) :>:
(intgr 8) :>: empty NOATTR)) :>: empty NOATTR
fun test (p,e) = match (Sub.empty,[(p,e)])
(* Debugging gauss *)
open Matrix
open Frac
val m = matrix (5, [VAR_LABEL "1", VAR_LABEL "2", VAR_LABEL "3",
VAR_LABEL "4", ARG_LABEL 0, FREE_LABEL])
fun tm () = (
RefalPP.install();
update (m,0,0,frac 1);
update (m,0,1,frac 1);
update (m,0,2,frac 1);
update (m,0,4,(frac 0) !-! (frac 1));
update (m,0,5,frac 2);
update (m,1,0,frac 1);
update (m,1,3,(frac 0) !-! (frac 1));
update (m,1,5,(frac 0) !-! (frac 1));
update (m,2,0,frac 1);
update (m,2,3,(frac 0) !-! (frac 1));
update (m,2,5,(frac 0) !-! (frac 1));
update (m,3,3,frac 1);
update (m,3,5,(frac 0) !-! (frac 2));
update (m,4,0,frac 1);
update (m,4,3,(frac 0) !-! (frac 1));
update (m,4,5,(frac 0) !-! (frac 1))
)