module Axioms where import PrelSequent import Sequent import PrSequent import PSequent -- non-logical rules formed from axioms. AR 15/4/1999 -- 24/3/2000 type Axiom = ([Atom],[Atom]) data Atom = Atom Ident [ATerm] deriving (Eq,Read,Show) data ATerm = Par Ident | Appl Ident [ATerm] deriving (Eq,Read,Show) axioms2calculus :: [(Ident,Axiom)] -> AbsCalculus axioms2calculus axx = [(i,axiom2rule a) | (i,a) <- axx] axiom2rule :: Axiom -> AbsRule axiom2rule (prems,concl) = \ (ant,suc) -> case findInstanceOfAtoms concl ant of Just insts -> Just (map (Left . (mkPrem insts)) prems ++ map Right params) where mkPrem i p = (substFormula s substTerm i (atom2formula params p) : ant, suc) where s = foldl (++) [] (map (freeVariablesOfTerm . snd) i) params = nub [c | Atom _ args <- prems, c <- foldl (++) [] (map parOf args), not (c elem [d | Atom _ xx <- concl, d <- foldl (++) [] (map parOf xx)])] parOf t = case t of Par x -> [x] Appl _ y -> foldl (++) [] (map parOf y) _ -> Nothing findInstanceOfAtoms :: [Atom] -> [Formula] -> Maybe [(Ident,Term)] findInstanceOfAtoms atoms formulae = case (atoms,formulae) of ([],_) -> Just [] (_, []) -> Nothing (_, f:fs) -> findOne [f:fs' | fs' <- subsets (length atoms - 1) fs] where findOne [] = Nothing findOne (s:ss) = case instanceOfAtoms atoms s of Just i -> Just i _ -> findOne ss instanceOfAtoms :: [Atom] -> [Formula] -> Maybe [(Ident,Term)] instanceOfAtoms atoms formulae = if length atoms == length formulae && all matchForm (zip atoms formulae) && complete insts && consistent insts then Just [(a,f) | (a,Just f) <- insts] else Nothing where matchForm ((Atom pred args),formula) = case formula of Predic f xx | f == pred && length xx == length args -> True _ -> False insts = foldl (++) [] (map tryInst (zip args1 args2)) tryInst (a1,a2) = case (a1,a2) of (Par a,f) -> [(a,Just f)] (Appl c a, Apply c' a') | c==c' -> foldl (++) [] (map tryInst (zip a a')) _ -> [("x",Nothing)] args1 = (foldl (++) [] [xx | Atom _ xx <- atoms]) args2 = (foldl (++) [] [xx | Predic _ xx <- formulae]) consistent t = all (lookupIsUnique t) (map fst t) complete t = case t of (_,Nothing):_ -> False (_,Just _):t' -> complete t' [] -> True atom2formula params (Atom f xx) = Predic f (map aterm2term xx) where aterm2term t = case t of Par x -> if x elem params then NewMeta x else Meta x Appl f yy -> Apply f (map aterm2term yy) ----------------- prAxiom :: Axiom -> String prAxiom (prems,concl) = case prems of [] -> prOneInAxiom concl _ -> prems' ++++ replicate (max (length prems') (length concl')) '-' ++++ concl' where concl' = prOneInAxiom concl prems' = foldr1 (+++) [prOneInAxiom (p:concl) | p <- prems] prOneInAxiom atoms = case atoms of [] -> "Gamma => Delta" _ -> prTList ", " (map prAtom atoms) ++ "," +++ "Gamma => Delta" where prAtom (Atom p [x,y]) | infixPredicate p = prATerm x +++ p +++ prATerm y prAtom (Atom p xx) = p ++ prArgList (map prATerm xx) prATerm (Par c) = c prATerm (Appl f [x,y]) | infixFunction f = prATerm x +++ f +++ prATerm y prATerm (Appl f xx) = f ++ prArgList (map prATerm xx) prLatexAxioms (ns,axx) = "\\documentstyle[proof]{article}" ++++ "\\begin{document}" ++++ ns ++++ -- new commands foldr (++++) "" ["\$" ++++ prLatexAxiom ax ++++ "\$" | ax <- axx] ++++ "\\end{document}" prLatexAxiom (name,([],concl)) = makeLatex (prOneInAxiom concl) ++ "^{" ++ makeLatex name ++"}" prLatexAxiom (name,(prems,concl)) = "\\infer[{\\scriptsize" +++ makeLatex name ++ "}]{" ++++ makeLatex (prOneInAxiom concl) ++++ "}{" ++++ prTList "\n & \n" [makeLatex (prOneInAxiom (p:concl)) | p <- prems] ++++ "}" ----------------- pAxiom :: Parser Char Axiom pAxiom = ((pConclusion ..+ jL "->" ||| succeed []) ... pPremises *** (\ (x,y) -> (y,x)) ||| jL "~" +.. (pConclusion ||| pParenth pConclusion) *** (\x -> ([],x))) pPremises = pTList "v" pAtom ||| lits "_|_" <<< [] pConclusion = pTList "&" pAtom pAtom = pATerm .... pPrInfix .... pATerm *** (\ (x,(p,y)) -> Atom p [x,y]) ||| pPred ... pArgList pATerm *** (\ (p,x) -> Atom p x) pATerm = pATerm2 .... (pInfix .... pATerm2 *** (\ (f,y) -> \x -> Appl f [x,y]) ||| succeed (\x -> x)) *** (\ (x,y) -> y x) pATerm2 = pConst ... pArgList pATerm *** (\ (p,x) -> Appl p x) ||| pVar *** Par ||| pParenth pATerm pAxioms :: Parser Char [(Ident,Axiom)] pAxioms = longestOfMany (pJ pRuleIdent ... pJ pAxiom) ----------------- -- get LaTeX newcommand prelude and the axioms, separated by a comment line -- starting with --. readAxioms :: String -> ((String,[(Ident,Axiom)]),String) readAxioms s = case pAxioms (remComm s') of (a,""):_ -> ((news,a), "all axioms accepted\n") (a, _):_ -> ((news,a), show (length a) +++ "axioms accepted\n") _ -> ((news,[]), "no axioms accepted\n") where (news,s') = let ss = lines s ; (ss1,ss2) = span (\l -> take 2 l /= "--") ss in (unlines ss1, unlines ss2) remComm s = case s of [] -> [] '-':'-':t -> remComm t2 where t2 = dropWhile (/='\n') t c :t -> c : remComm t ----------------- subsets int list = case int of 0 -> [[]] n -> [h:t | h <- list, t <- subsets (n-1) (del h list)] where del x [] = [] del x (y:ys) = if x==y then ys else y : del x ys lookupIsUnique x t = length (nub [y | (z,y) <- t, z==x]) < 2