Permalink
Browse files

Major cleanup/reordening. Also start on verification algorithm

  • Loading branch information...
1 parent d4074a0 commit 4ecb2318bcc28ee1d86324177c348b14cf8ad0d5 @norm2782 norm2782 committed May 10, 2011
View
@@ -3,6 +3,8 @@
:set -XDeriveDataTypeable
:set -XMultiParamTypeClasses
:set -XFunctionalDependencies
+:set -XFlexibleInstances
+:set -XTypeSynonymInstances
:set -Wall
:set -isrc
:set -itest/suite
View
@@ -42,6 +42,7 @@ Executable jcu
transformers >= 0.2,
attoparsec >= 0.8.5 && < 0.9,
ListLike >= 3.1 && < 3.2,
+ containers >= 0.4 && < 0.5,
-- For Snap stuff, until it hits Hackage
cereal >= 0.3 && < 0.4,
@@ -88,5 +89,4 @@ Library
Build-Depends: base >= 4.0 && < 5.0
Hs-Source-Dirs: src
- Exposed-modules: JCU.Prolog.Types, JCU.Prolog.Parser, JCU.Prolog.Prolog,
- JCU.Web.Handlers, JCU.Web.Types
+ Exposed-modules: JCU.Types, JCU.Parser, JCU.Prolog, JCU.Handlers
View
@@ -17,3 +17,12 @@ run:
debug:
DEBUG=1 jcu
+
+deps:
+ git clone https://github.com/snapframework/snap-auth.git
+ cd snap-auth
+ cabal install
+ git clone https://github.com/ozataman/snap-extension-mongodb.git
+ cd snap-extension-mongodb
+ cabal install
+ cd ..
@@ -11069,11 +11069,36 @@ d.data(g[0],"droppable");e.greedyChild=c=="isover"?1:0}}if(e&&c=="isover"){e.iso
ProofTree.prototype.url = function() {
return '/rules/inuse';
};
- ProofTree.prototype.initialize = function() {
- this.set({
- root: new ProofTreeNode()
+ ProofTree.prototype.mkTree = function(raw, t) {
+ var cs, ct, node, _i, _len, _ref;
+ node = new ProofTreeNode();
+ node.set({
+ term: raw.term
+ });
+ cs = new Backbone.Collection(cs);
+ _ref = raw.childTerms;
+ for (_i = 0, _len = _ref.length; _i < _len; _i++) {
+ ct = _ref[_i];
+ cs.add(t.mkTree(ct, t));
+ }
+ node.set({
+ childTerms: cs
});
- return this.fetch();
+ return node;
+ };
+ ProofTree.prototype.initialize = function() {
+ var model, options;
+ model = this;
+ options = {};
+ options.success = function(resp, status, xhr) {
+ var r;
+ r = model.mkTree(resp, model);
+ console.log(r);
+ return model.set({
+ root: r
+ });
+ };
+ return Backbone.sync.call(this, 'read', this, options);
};
ProofTree.prototype.allValid = function() {
return this.get('root').isValid();
@@ -11095,7 +11120,7 @@ d.data(g[0],"droppable");e.greedyChild=c=="isover"?1:0}}if(e&&c=="isover"){e.iso
ProofTreeNode.__super__.constructor.apply(this, arguments);
}
__extends(ProofTreeNode, Backbone.Model);
- ProofTreeNode.prototype.initialize = function(attrs) {
+ ProofTreeNode.prototype.initialize = function() {
return this.set({
childTerms: new Backbone.Collection()
});
@@ -11205,7 +11230,7 @@ d.data(g[0],"droppable");e.greedyChild=c=="isover"?1:0}}if(e&&c=="isover"){e.iso
return _safe(result);
};
(function() {
- _print(_safe('<div class="yui3-g">\n <div class="yui3-u-2-3">\n <div class="content">\n <h2>Derivation Tree</h2>\n <div id="proof-tree-div"><!-- TREE GOES HERE --></div>\n <input type="button" id="btnCheck" value="Check" />\n </div>\n </div>\n\n <div class="yui3-u-1-3">\n <div class="content">\n <h2>Stored Rules</h2>\n <div id="rules-list-div"><!-- LIST GOES HERE --></div>\n <div id="divListAdd">\n <input type="text" id="txtAddRule" />\n <input type="button" value="Add" id="btnAddRule" />\n </div>\n </div>\n </div>\n</div>\n'));
+ _print(_safe('<div class="yui3-g">\n <div class="yui3-u-2-3">\n <div class="content">\n <h2>Proof Tree</h2>\n <div id="proof-tree-div"><!-- TREE GOES HERE --></div>\n <input type="button" id="btnCheck" value="Check" />\n </div>\n </div>\n\n <div class="yui3-u-1-3">\n <div class="content">\n <h2>Stored Rules</h2>\n <div id="rules-list-div"><!-- LIST GOES HERE --></div>\n <div id="divListAdd">\n <input type="text" id="txtAddRule" />\n <input type="button" value="Add" id="btnAddRule" />\n </div>\n </div>\n </div>\n</div>\n'));
}).call(this);
return __out.join('');
@@ -5,9 +5,22 @@ class exports.ProofTree extends Backbone.Model
# root :: RuleTreeNode
url: -> '/rules/inuse'
+ mkTree: (raw, t) ->
+ node = new ProofTreeNode()
+ node.set({term: raw.term})
+ cs = new Backbone.Collection(cs)
+ cs.add(t.mkTree ct, t) for ct in raw.childTerms
+ node.set({childTerms: cs})
+ node
+
initialize: ->
- @set {root: new ProofTreeNode()}
- @fetch()
+ model = @
+ options = {}
+ options.success = (resp, status, xhr) ->
+ r = model.mkTree resp, model
+ console.log r
+ model.set({root: r})
+ Backbone.sync.call(this, 'read', this, options)
allValid: ->
@get('root').isValid()
@@ -3,7 +3,8 @@ class exports.ProofTreeNode extends Backbone.Model
# term :: Term
# childTerms :: BackBone.Collection
- initialize: (attrs) ->
+ initialize: ->
+ # console.log attrs
@set {childTerms: new Backbone.Collection()}
hasTerm: ->
@@ -1,7 +1,7 @@
<div class="yui3-g">
<div class="yui3-u-2-3">
<div class="content">
- <h2>Derivation Tree</h2>
+ <h2>Proof Tree</h2>
<div id="proof-tree-div"><!-- TREE GOES HERE --></div>
<input type="button" id="btnCheck" value="Check" />
</div>
@@ -1,6 +1,6 @@
{-# LANGUAGE OverloadedStrings #-}
-module JCU.Web.Handlers where
+module JCU.Handlers where
import Application (Application)
import Data.Aeson (encode, fromJSON, json)
@@ -12,9 +12,9 @@ import qualified Data.ByteString.Lazy.Char8 as L (ByteString)
import Data.List as DL (length)
import Data.Map (Map, member, (!))
import Debug.Trace (trace) -- TODO: Remove
-import JCU.Prolog.Types
-import JCU.Prolog.Prolog (solve, unify)
-import JCU.Web.Types
+import JCU.Parser
+import JCU.Prolog
+import JCU.Types
import Snap.Auth
import Snap.Auth.Handlers
import Snap.Extension.DB.MongoDB ((=:), Document, MonadMongoDB)
@@ -176,27 +176,27 @@ mkRules raw =
r <- getResponse
finishWith r
-
-checkRules :: [Rule] -> [EnvTrace] -> [Bool]
-checkRules rules = foldr (comp . checkRules') []
- where checkRules' (env, trcs) = [ any (cmpRuleTrace env r) trcs
- | r <- rules ]
-
-comp :: [Bool] -> [Bool] -> [Bool]
-comp lst highest | l lst > l highest = lst
- | otherwise = highest
- where l = DL.length . takeWhile (== True)
-
--- TODO: Is this right? Also, do we need r == u?
--- TODO: Take the conclusion into account
--- TODO: Send data from client from text fields, not from collection...
-cmpRuleTrace :: Env -> Rule -> Trace -> Bool
-cmpRuleTrace env r@(t :<-: _) (Trace g u _ _) =
- trace ("env: " ++ show env ++ "\n" ++
- "rterm: " ++ show r ++ "\n" ++
- "traceg: " ++ show g ++ "\n" ++
- "traceu: " ++ show u ++ "\n")
- unify (t, g) (Just env) /= Nothing || r == u
+-- TODO: Still needed?
+{- checkRules :: [Rule] -> [Env] -> [Bool]-}
+{- checkRules rules = foldr (comp . checkRules') []-}
+{- where checkRules' (env, trcs) = [ any (cmpRuleTrace env r) trcs-}
+{- | r <- rules ]-}
+
+{- comp :: [Bool] -> [Bool] -> [Bool]-}
+{- comp lst highest | l lst > l highest = lst-}
+{- | otherwise = highest-}
+{- where l = DL.length . takeWhile (== True)-}
+
+{- -- TODO: Is this right? Also, do we need r == u?-}
+{- -- TODO: Take the conclusion into account-}
+{- -- TODO: Send data from client from text fields, not from collection...-}
+{- cmpRuleTrace :: Env -> Rule -> Trace -> Bool-}
+{- cmpRuleTrace env r@(t :<-: _) (Trace g u _ _) =-}
+{- trace ("env: " ++ show env ++ "\n" ++-}
+{- "rterm: " ++ show r ++ "\n" ++-}
+{- "traceg: " ++ show g ++ "\n" ++-}
+{- "traceu: " ++ show u ++ "\n")-}
+{- unify (t, g) (Just env) /= Nothing || r == u-}
readInUseRulesH :: Application ()
readInUseRulesH = do-- TODO restrict forbiddenH $ do
@@ -211,45 +211,6 @@ updateInUseRulesH = do-- TODO restrict forbiddenH $ do
trace ("updateInUseRulesH: " ++ show dmods) (return ())
return ()
-cnst s = Fun s []
-testStoredRules :: [Rule]
-testStoredRules = [ Fun "ma" [cnst "mien", cnst "juul"] :<-: []
- , Fun "ma" [cnst "juul", cnst "bea"] :<-: []
- , Fun "ma" [cnst "bea" , cnst "alex"] :<-: []
- , Fun "ma" [cnst "bea" , cnst "cons"] :<-: []
- , Fun "ma" [cnst "max" , cnst "ale"] :<-: []
- , Fun "ma" [cnst "max" , cnst "ama"] :<-: []
- , Fun "ma" [cnst "max" , cnst "ari"] :<-: []
- , Fun "oma" [Var "X" , Var "Z"] :<-: [ Fun "ma" [Var "X", Var "Y"]
- , Fun "ouder" [Var "Y", Var "Z"] ]
- , Fun "pa" [cnst "alex", cnst "ale"] :<-: []
- , Fun "pa" [cnst "alex", cnst "ama"] :<-: []
- , Fun "pa" [cnst "alex", cnst "ari"] :<-: []
- , Fun "ouder" [Var "X", Var "Y"] :<-: [ Fun "pa" [Var "X", Var "Y"] ]
- , Fun "ouder" [Var "X", Var "Y"] :<-: [ Fun "ma" [Var "X", Var "Y"] ]
- , Fun "voor" [Var "X", Var "Y"] :<-: [ Fun "ouder" [Var "X", Var "Y"] ]
- , Fun "voor" [Var "X", Var "Y"] :<-: [ Fun "ouder" [Var "X", Var "Z"]
- , Fun "voor" [Var "Z", Var "Y"] ] ]
-
-testInUseRules :: [Rule]
-testInUseRules = [ Fun "voor" [cnst "bea", cnst "ama"] :<-: []
- , Fun "" [] :<-: [ Fun "pa" [Var "X", Var "Y"] ]
- , Fun "pa" [Var "X" , cnst "ama"] :<-: []
- , Fun "pa" [cnst "alex", cnst "ama"] :<-: []
- {- , Fun "alex" [] :<-: []-}
- ]
-
-voorBeaAmaProof :: Proof
-voorBeaAmaProof = Proof (Fun "voor" [cnst "bea", cnst "ama"])
- [ Proof (Fun "ouder" [cnst "bea", cnst "alex"]) [
- Proof (Fun "ma" [cnst "bea", cnst "alex"]) []
- ]
- , Proof (Fun "voor" [cnst "alex", cnst "ama"]) [
- Proof (Fun "ouder" [cnst "alex", cnst "ama"]) [
- Proof (Fun "pa" [cnst "alex", cnst "ama"]) []
- ]
- ]
- ]
{-
alex
View
@@ -0,0 +1,58 @@
+{-# LANGUAGE Rank2Types, FlexibleContexts #-}
+
+module JCU.Parser where
+
+import Data.Aeson
+import Data.ListLike.Base (ListLike)
+import Data.Tree (Tree(..))
+import JCU.Types
+import Text.ParserCombinators.UU
+import Text.ParserCombinators.UU.BasicInstances
+import Text.ParserCombinators.UU.Utils
+
+pRules :: Parser [Rule]
+pRules = pList pRule
+
+-- TODO: Add support for rules with more pFuns before the :-
+pRule :: Parser Rule
+pRule = (:<-:) <$> pFun <*> (pSymbol ":-" *> pTerms `opt` []) <* pDot
+
+pTerm, pCon, pVar, pFun :: Parser Term
+pTerm = pCon <|> pVar <|> pFun
+pCon = Con <$> pNatural
+pVar = Var <$> lexeme (pList1 pUpper)
+pFun = Fun <$> pIdentifier <*> (pParens pTerms `opt` [])
+
+pTerms :: Parser [Term]
+pTerms = pListSep pComma pTerm
+
+startParse :: (ListLike s b, Show b) => P (Str b s LineColPos) a -> s
+ -> (a, [Error LineColPos])
+startParse p inp = parse ((,) <$> p <*> pEnd)
+ $ createStr (LineColPos 0 0 0) inp
+
+pIdentifier :: Parser String
+pIdentifier = (:) <$> pLower <*> lexeme (pList (pLower <|> pUpper <|> pDigit))
+
+
+instance ToJSON Rule where
+ toJSON t = object [ "rule" .= show t ]
+
+instance FromJSON Proof where
+ parseJSON (Object o) = mkProofTree <$> o .: "term" <*> o .: "childTerms"
+
+instance ToJSON Proof where
+ toJSON (Node t ps) = object [ "term" .= show t
+ , "childTerms" .= toJSON ps ]
+
+mkProofTree :: String -> Value -> Proof
+mkProofTree r rts = Node (mkTerm r) mkProofTrees
+ where mkProofTrees = case fromJSON rts :: Result [Proof] of
+ (Success a) -> a
+ _ -> error "failed!"
+
+-- TODO: Something with errors
+mkTerm :: String -> Term
+mkTerm r = a
+ where (a, e) = startParse pTerm r
+
Oops, something went wrong.

0 comments on commit 4ecb231

Please sign in to comment.