Commit 05a23752 authored by sof's avatar sof
Browse files

[project @ 1997-07-26 10:38:02 by sof]

parent e8a827d9
CHAR I/O:
*********
In clausify ...
The unifier would like to propogate use of Char#s all the way to the
readChan and appendChan. However these have explicit [Char] arguments
so we must explicitly coerce the Chars as we extract them.
clause produces [Char#]s
parse reads [Char] and builds Sym Char#
disp takes [Char#]s and produces [Char]
COMMENTS:
* The extent of this unboxification is quite surprising and possibly
unexpected.
* Coersion when constructing or extracting from unboxed structures can
be a pain. Where this occurs defines the extent of the unboxedness.
OVERLOADING CHARS:
Might want to introduce versions of I/O operations which read/write
[Char#]. Use a type class to capture either boxed or unboxed Chars.
class Char a
toChar :: a -> Char
fromChar :: Char -> a
instance Char Char
toChar = id
fromChar = id
instance Char Char#
toChar c# = MkChar c#
fromChar c = case c of MkChar c# -> c#
Now rather than specifying type as
... Char ...
We use
Char c => ... c ...
Now just need a specialised versions I/O operations which deal with [Char#]
The Char class is very similar to the overloading of numeric constants.
TOP = ../../..
include $(TOP)/mk/boilerplate.mk
SUBDIRS = $(wildcard spec* code* clausify*)
include $(TARGET_MK)
HC_OPTS=-v -O -fglasgow-exts \
-keep-hc-files-too -dcore-lint -ftrace-specialisations -ddump-simpl -ddump-stg -odump clausify000.dump
SRCS_HS=Main.hs
OBJS_O= Main.o
NoFibMultiModuleCompileAndRun(clausify000,-i clausify000.stdin -o1 clausify000.stdout)
NoFibHaskellCompile(clausify000,Main,hs)
HaskellDependTarget( $(SRCS_HS) )
-- CLAUSIFY: Reducing Propositions to Clausal Form
-- Colin Runciman, University of York, 10/90
--
-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
--
-- Optimised version: based on Runciman & Wakeling [1993]
-- Patrick Sansom, University of Glasgow, 2/94
module Main ( main ) where
-- the main program: reads stdin and writes stdout
main = _scc_ "CAF:main"
do
input <- getContents
putStr (clausify input)
-- convert lines of propostions input to clausal forms
clausify input = _scc_ "clausify"
concat
(interleave (repeat "prop> ")
(map clausifyline (lines input)))
clausifyline = _scc_ "CAF:clausifyline"
concat . map disp . clauses . parse
-- the main pipeline from propositional formulae to printed clauses
clauses = _scc_ "CAF:clauses" unicl . split . disin . negin . elim
-- clauses = (_scc_ "unicl" unicl) . (_scc_ "split" split) .
-- (_scc_ "disin" disin) . (_scc_ "negin" negin) .
-- (_scc_ "elim" elim)
-- clauses = (\x -> _scc_ "unicl" unicl x) .
-- (\x -> _scc_ "split" split x) .
-- (\x -> _scc_ "disin" disin x) .
-- (\x -> _scc_ "negin" negin x) .
-- (\x -> _scc_ "elim" elim x)
data StackFrame = Ast Formula | Lex Char
data Formula =
Sym Char |
Not Formula |
Dis Formula Formula |
Con Formula Formula |
Imp Formula Formula |
Eqv Formula Formula
-- separate positive and negative literals, eliminating duplicates
clause p = _scc_ "clause"
let
clause' (Dis p q) x = clause' p (clause' q x)
clause' (Sym s) (c,a) = (insert s c , a)
clause' (Not (Sym s)) (c,a) = (c , insert s a)
in
clause' p ([] , [])
conjunct p = _scc_ "conjunct"
case p of
(Con p q) -> True
p -> False
-- shift disjunction within conjunction
disin p = _scc_ "disin"
case p of
(Con p q) -> Con (disin p) (disin q)
(Dis p q) -> disin' (disin p) (disin q)
p -> p
-- auxilary definition encoding (disin . Dis)
disin' p r = _scc_ "disin'"
case p of
(Con p q) -> Con (disin' p r) (disin' q r)
p -> case r of
(Con q r) -> Con (disin' p q) (disin' p r)
q -> Dis p q
-- format pair of lists of propositional symbols as clausal axiom
disp p = _scc_ "disp"
case p of
(l,r) -> interleave l spaces ++ "<="
++ interleave spaces r ++ "\n"
-- eliminate connectives other than not, disjunction and conjunction
elim f = _scc_ "elim"
case f of
(Sym s) -> Sym s
(Not p) -> Not (elim p)
(Dis p q) -> Dis (elim p) (elim q)
(Con p q) -> Con (elim p) (elim q)
(Imp p q) -> Dis (Not (elim p)) (elim q)
(Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f))
-- remove duplicates and any elements satisfying p
filterset p s = _scc_ "filterset"
filterset' [] p s
filterset' res p l = _scc_ "filterset'"
case l of
[] -> []
(x:xs) -> if (notElem x res) && (p x) then
x : filterset' (x:res) p xs
else
filterset' res p xs
-- insertion of an item into an ordered list
insert x l = _scc_ "insert"
case l of
[] -> [x]
(y:ys) -> if x < y then x:(y:ys)
else if x > y then y : insert x ys
else y:ys
interleave xs ys = _scc_ "interleave"
case xs of
(x:xs) -> x : interleave ys xs
[] -> []
-- shift negation to innermost positions
negin f = _scc_ "negin"
case f of
(Not (Not p)) -> negin p
(Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q))
(Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q))
(Dis p q) -> Dis (negin p) (negin q)
(Con p q) -> Con (negin p) (negin q)
p -> p
-- the priorities of symbols during parsing
opri c = _scc_ "opri"
case c of
'(' -> 0
'=' -> 1
'>' -> 2
'|' -> 3
'&' -> 4
'~' -> 5
-- parsing a propositional formula
parse t = _scc_ "parse"
let [Ast f] = parse' t []
in f
parse' cs s = _scc_ "parse'"
case cs of
[] -> redstar s
(' ':t) -> parse' t s
('(':t) -> parse' t (Lex '(' : s)
(')':t) -> let (x : Lex '(' : s') = redstar s
in parse' t (x:s')
(c:t) -> if inRange ('a','z') c then
parse' t (Ast (Sym c) : s)
else if spri s > opri c then parse' (c:t) (red s)
else parse' t (Lex c : s)
-- reduction of the parse stack
red l = _scc_ "red"
case l of
(Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s
(Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s
(Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s
(Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s
(Ast p : Lex '~' : s) -> Ast (Not p) : s
-- iterative reduction of the parse stack
redstar = _scc_ "CAF:redstar"
while ((/=) 0 . spri) red
spaces = _scc_ "CAF:spaces"
repeat ' '
-- split conjunctive proposition into a list of conjuncts
split p = _scc_ "split"
let
split' (Con p q) a = split' p (split' q a)
split' p a = p : a
in
split' p []
-- priority of the parse stack
spri s = _scc_ "spri"
case s of
(Ast x : Lex c : s) -> opri c
s -> 0
-- does any symbol appear in both consequent and antecedant of clause
tautclause p = _scc_ "tautclause"
case p of
(c,a) -> -- [x | x <- c, x `elem` a] /= []
any (\x -> x `elem` a) c
-- form unique clausal axioms excluding tautologies
unicl = _scc_ "CAF:unicl"
filterset (not . tautclause) . map clause
-- functional while loop
while p f x = _scc_ "while"
if p x then while p f (f x) else x
(a = a = a) = (a = a = a) = (a = a = a)
prop> a <=
prop>
\ No newline at end of file
NoFibOneModuleCompileAndRun(clausify001,-i clausify001.stdin -o1 clausify001.stdout)
-- CLAUSIFY: Reducing Propositions to Clausal Form
-- Colin Runciman, University of York, 10/90
--
-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
--
-- Optimised version: based on Runciman & Wakeling [1993]
-- Patrick Sansom, University of Glasgow, 2/94
--
-- Char# specialisation test
-- Patrick Sansom, University of Glasgow, 12/94
module Main ( main ) where
-- the main program: reads stdin and writes stdout
main = _scc_ "CAF:main"
do
input <- getContents
putStr (clausify input)
-- convert lines of propostions input to clausal forms
clausify input = _scc_ "clausify"
concat
(interleave (repeat "prop> ")
(map clausifyline (lines input)))
clausifyline = _scc_ "CAF:clausifyline"
concat . map disp . clauses . parse
-- the main pipeline from propositional formulae to printed clauses
clauses = _scc_ "CAF:clauses" unicl . split . disin . negin . elim
-- clauses = (_scc_ "unicl" unicl) . (_scc_ "split" split) .
-- (_scc_ "disin" disin) . (_scc_ "negin" negin) .
-- (_scc_ "elim" elim)
-- clauses = (\x -> _scc_ "unicl" unicl x) .
-- (\x -> _scc_ "split" split x) .
-- (\x -> _scc_ "disin" disin x) .
-- (\x -> _scc_ "negin" negin x) .
-- (\x -> _scc_ "elim" elim x)
data StackFrame = Ast Formula | Lex Char
data Formula =
Sym Char# | -- ***
Not Formula |
Dis Formula Formula |
Con Formula Formula |
Imp Formula Formula |
Eqv Formula Formula
-- separate positive and negative literals, eliminating duplicates
clause p = _scc_ "clause"
let
clause' (Dis p q) x = clause' p (clause' q x)
clause' (Sym s) (c,a) = (insert s c , a)
clause' (Not (Sym s)) (c,a) = (c , insert s a)
in
clause' p ([] , [])
conjunct p = _scc_ "conjunct"
case p of
(Con p q) -> True
p -> False
-- shift disjunction within conjunction
disin p = _scc_ "disin"
case p of
(Con p q) -> Con (disin p) (disin q)
(Dis p q) -> disin' (disin p) (disin q)
p -> p
-- auxilary definition encoding (disin . Dis)
disin' p r = _scc_ "disin'"
case p of
(Con p q) -> Con (disin' p r) (disin' q r)
p -> case r of
(Con q r) -> Con (disin' p q) (disin' p r)
q -> Dis p q
-- format pair of lists of propositional symbols as clausal axiom
disp p = _scc_ "disp"
case p of
(l,r) -> interleave (foldr ((:) . C#) [] l) spaces ++ "<=" -- ***
++ interleave spaces (foldr ((:) . C#) [] r) ++ "\n" -- ***
-- eliminate connectives other than not, disjunction and conjunction
elim f = _scc_ "elim"
case f of
(Sym s) -> Sym s
(Not p) -> Not (elim p)
(Dis p q) -> Dis (elim p) (elim q)
(Con p q) -> Con (elim p) (elim q)
(Imp p q) -> Dis (Not (elim p)) (elim q)
(Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f))
-- remove duplicates and any elements satisfying p
filterset p s = _scc_ "filterset"
filterset' [] p s
filterset' res p l = _scc_ "filterset'"
case l of
[] -> []
(x:xs) -> if (notElem x res) && (p x) then
x : filterset' (x:res) p xs
else
filterset' res p xs
-- insertion of an item into an ordered list
insert x l = _scc_ "insert"
case l of
[] -> [x]
(y:ys) -> if x < y then x:(y:ys)
else if x > y then y : insert x ys
else y:ys
interleave xs ys = _scc_ "interleave"
case xs of
(x:xs) -> x : interleave ys xs
[] -> []
-- shift negation to innermost positions
negin f = _scc_ "negin"
case f of
(Not (Not p)) -> negin p
(Not (Con p q)) -> Dis (negin (Not p)) (negin (Not q))
(Not (Dis p q)) -> Con (negin (Not p)) (negin (Not q))
(Dis p q) -> Dis (negin p) (negin q)
(Con p q) -> Con (negin p) (negin q)
p -> p
-- the priorities of symbols during parsing
opri c = _scc_ "opri"
case c of
'(' -> 0
'=' -> 1
'>' -> 2
'|' -> 3
'&' -> 4
'~' -> 5
-- parsing a propositional formula
parse t = _scc_ "parse"
let [Ast f] = parse' t []
in f
parse' cs s = _scc_ "parse'"
case cs of
[] -> redstar s
(' ':t) -> parse' t s
('(':t) -> parse' t (Lex '(' : s)
(')':t) -> let (x : Lex '(' : s') = redstar s
in parse' t (x:s')
(c:t) -> if inRange ('a','z') c then
parse' t (Ast (Sym (case c of C# c# -> c#)) : s) -- ***
else if spri s > opri c then parse' (c:t) (red s)
else parse' t (Lex c : s)
-- reduction of the parse stack
red l = _scc_ "red"
case l of
(Ast p : Lex '=' : Ast q : s) -> Ast (Eqv q p) : s
(Ast p : Lex '>' : Ast q : s) -> Ast (Imp q p) : s
(Ast p : Lex '|' : Ast q : s) -> Ast (Dis q p) : s
(Ast p : Lex '&' : Ast q : s) -> Ast (Con q p) : s
(Ast p : Lex '~' : s) -> Ast (Not p) : s
-- iterative reduction of the parse stack
redstar = _scc_ "CAF:redstar"
while ((/=) 0 . spri) red
spaces = _scc_ "CAF:spaces"
repeat ' '
-- split conjunctive proposition into a list of conjuncts
split p = _scc_ "split"
let
split' (Con p q) a = split' p (split' q a)
split' p a = p : a
in
split' p []
-- priority of the parse stack
spri s = _scc_ "spri"
case s of
(Ast x : Lex c : s) -> opri c
s -> 0
-- does any symbol appear in both consequent and antecedant of clause
tautclause p = _scc_ "tautclause"
case p of
(c,a) -> -- [x | x <- c, x `elem` a] /= []
any (\x -> x `elem` a) c
-- form unique clausal axioms excluding tautologies
unicl = _scc_ "CAF:unicl"
filterset (not . tautclause) . map clause
-- functional while loop
while p f x = _scc_ "while"
if p x then while p f (f x) else x
module Main ( main ) where
import PreludeClausify (clausify)
-- the main program: reads stdin and writes stdout
main = scc "CAF:main"
readChan stdin exit ( \input ->
appendChan stdout (clausify input) exit done)
-- CLAUSIFY: Reducing Propositions to Clausal Form
-- Colin Runciman, University of York, 10/90
--
-- An excellent benchmark is: (a = a = a) = (a = a = a) = (a = a = a)
--
-- Optimised version: based on Runciman & Wakeling [1993]
-- Patrick Sansom, University of Glasgow, 2/94
--
-- Char# specialisation test with prelude stuff explicit
-- Patrick Sansom, University of Glasgow, 12/94
module PreludeClausify( clausify, AList(..) ) where
-- convert lines of propostions input to clausal forms
clausify input = scc "clausify"
concat
(interleave (repeat "prop> ")
(map clausifyline (lines input)))
clausifyline = scc "CAF:clausifyline"
concat . map disp . clauses . parse
-- the main pipeline from propositional formulae to printed clauses
clauses = scc "CAF:clauses" unicl . split . disin . negin . elim
-- clauses = (scc "unicl" unicl) . (scc "split" split) .
-- (scc "disin" disin) . (scc "negin" negin) .
-- (scc "elim" elim)
-- clauses = (\x -> scc "unicl" unicl x) .
-- (\x -> scc "split" split x) .
-- (\x -> scc "disin" disin x) .
-- (\x -> scc "negin" negin x) .
-- (\x -> scc "elim" elim x)
data StackFrame = Ast Formula | Lex Char
data Formula =
Sym Char# | -- ***
Not Formula |
Dis Formula Formula |
Con Formula Formula |
Imp Formula Formula |
Eqv Formula Formula
-- separate positive and negative literals, eliminating duplicates
clause p = scc "clause"
let
clause' (Dis p q) x = clause' p (clause' q x)
clause' (Sym s) (c,a) = (insert s c , a)
clause' (Not (Sym s)) (c,a) = (c , insert s a)
in
clause' p (ANil , ANil)
conjunct p = scc "conjunct"
case p of
(Con p q) -> True
p -> False
-- shift disjunction within conjunction
disin p = scc "disin"
case p of
(Con p q) -> Con (disin p) (disin q)
(Dis p q) -> disin' (disin p) (disin q)
p -> p
-- auxilary definition encoding (disin . Dis)
disin' p r = scc "disin'"
case p of
(Con p q) -> Con (disin' p r) (disin' q r)
p -> case r of
(Con q r) -> Con (disin' p q) (disin' p r)
q -> Dis p q
-- format pair of lists of propositional symbols as clausal axiom
disp p = scc "disp"
case p of
(l,r) -> interleave (foldrA ((:) `o` C#) [] l) spaces ++ "<="
++ interleave spaces (foldrA ((:) `o` C#) [] r) ++ "\n"
-- eliminate connectives other than not, disjunction and conjunction
elim f = scc "elim"
case f of
(Sym s) -> Sym s
(Not p) -> Not (elim p)
(Dis p q) -> Dis (elim p) (elim q)
(Con p q) -> Con (elim p) (elim q)
(Imp p q) -> Dis (Not (elim p)) (elim q)
(Eqv f f') -> Con (elim (Imp f f')) (elim (Imp f' f))
-- remove duplicates and any elements satisfying p
filterset p s = scc "filterset"
filterset' [] p s
filterset' res p l = scc "filterset'"
case l of
[] -> []
(x:xs) -> if (notElem x res) && (p x) then
x : filterset' (x:res) p xs
else
filterset' res p xs
-- insertion of an item into an ordered list
insert x l = scc "insert"
case l of
ANil -> x :! ANil
(y:!ys) -> if x < y then x:!(y:!ys)