Skip to content

Commit

Permalink
* Changed behaviour of the "Check Proof" button.
Browse files Browse the repository at this point in the history
  Proofs are only checked when proofing is On, otherwise a dummy proof stating
  "Incomplete" is  used.

  This is a work around
  • Loading branch information
spockz committed Jan 19, 2012
1 parent d613e66 commit f07155f
Show file tree
Hide file tree
Showing 5 changed files with 44 additions and 10 deletions.
10 changes: 10 additions & 0 deletions resources/static/brunch/src/vendor/jquery-ui-1.8.16.custom.min.js

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions resources/static/hjs/Data/Tree.hs
@@ -1,4 +1,6 @@
module Data.Tree where

import UHC.Generics

data Tree a = Node {
rootLabel :: a, -- ^ label value
Expand Down
4 changes: 4 additions & 0 deletions resources/static/hjs/Prolog.hs
Expand Up @@ -17,6 +17,10 @@ data Status = Correct
| Incomplete
| Invalid
deriving Show

dummyProof :: Proof -> PCheck
-- dummyProof = fmap (const Incomplete)
dummyProof (Node _ xs) = Node Incomplete (map dummyProof xs)

-- | Check if the proof provided by the client is correct, incomplete or
-- incorrect. It returns a @PCheck@: a @Tree Status@. Each node is assigned
Expand Down
2 changes: 1 addition & 1 deletion resources/static/hjs/Templates.hs
Expand Up @@ -2,7 +2,7 @@ module Templates where

import Prolog (Status(..))

home = "<div class=\"yui3-g\"> <div class=\"yui3-u-1-2\"> <div class=\"content\"> <h2>Proof Tree</h2> <div id=\"proof-tree-div\" class=\"noClue\"><!-- TREE GOES HERE --></div> <div id=\"subst\">Substitute <input type=\"text\" id=\"txtSubstSub\" style=\"width: 50px\" /> for <input type=\"text\" id=\"txtSubstFor\" style=\"width: 50px\" /> <input type=\"button\" id=\"btnSubst\" value=\"Substitute\" /> (e.g. substitute bea for X0) </div> <input type=\"button\" id=\"btnCheck\" value=\"Check Proof\" /> <input type=\"button\" id=\"btnReset\" value=\"Reset Tree\" /> <!-- <h3>Note</h3> <p class=\"lhsText\">Due to limitations in the current version of the software, you might see variables with the same name in different text fields in the tree. However, these are not necessarily the same variable! Double-check to see which rules you can apply and which variables those rules have.</p> --> <h3>Color coding help</h3> <ul id=\"color-coding-list\"> <li><div class=\"box redField\"></div> Incorrect rule application</li> <li><div class=\"box yellowField\"></div> Incomplete proof</li> <li><div class=\"box greenField\"></div> Correct rule</li> <li><div class=\"box blueField\"></div> Syntax error</li> </ul> <h3>Example data</h3> <p class=\"lhsText\"> Example data containing the Dutch royal family, the list structure and lookup, and the natural numbers (as discussed in the JCU lecture notes) can be loaded by <a href=\"/load-example\">clicking this link</a>. Beware that this will replace all your existing rules! </p> </div> </div> <div class=\"yui3-u-1-2\"> <div class=\"content\"> <h2>Stored Rules</h2> <p>Drag a rule form the list below to a field containing a term in the tree on the left.</p> <div id=\"rules-list-div\"><!-- LIST GOES HERE --></div> <div id=\"divListAdd\"> <input type=\"text\" id=\"txtAddRule\" /> <input type=\"button\" value=\"Add\" id=\"btnAddRule\" /> </div> </div> </div></div>"
home = "<div class=\"yui3-g\"> <div class=\"yui3-u-1-2\"> <div class=\"content\"> <h2>Proof Tree</h2> <div id=\"proof-tree-div\" class=\"noClue\"><!-- TREE GOES HERE --></div> <div id=\"subst\">Substitute <input type=\"text\" id=\"txtSubstSub\" style=\"width: 50px\" /> for <input type=\"text\" id=\"txtSubstFor\" style=\"width: 50px\" /> <input type=\"button\" id=\"btnSubst\" value=\"Substitute\" /> (e.g. substitute bea for X0) </div><input type=\"hidden\" id=\"storeDoChecking\" value=\"False\"/> <input type=\"button\" id=\"btnCheck\" value=\"Check Proof\" /> <input type=\"button\" id=\"btnReset\" value=\"Reset Tree\" /> <!-- <h3>Note</h3> <p class=\"lhsText\">Due to limitations in the current version of the software, you might see variables with the same name in different text fields in the tree. However, these are not necessarily the same variable! Double-check to see which rules you can apply and which variables those rules have.</p> --> <h3>Color coding help</h3> <ul id=\"color-coding-list\"> <li><div class=\"box redField\"></div> Incorrect rule application</li> <li><div class=\"box yellowField\"></div> Incomplete proof</li> <li><div class=\"box greenField\"></div> Correct rule</li> <li><div class=\"box blueField\"></div> Syntax error</li> </ul> <h3>Example data</h3> <p class=\"lhsText\"> Example data containing the Dutch royal family, the list structure and lookup, and the natural numbers (as discussed in the JCU lecture notes) can be loaded by <a href=\"/load-example\">clicking this link</a>. Beware that this will replace all your existing rules! </p> </div> </div> <div class=\"yui3-u-1-2\"> <div class=\"content\"> <h2>Stored Rules</h2> <p>Drag a rule form the list below to a field containing a term in the tree on the left.</p> <div id=\"rules-list-div\"><!-- LIST GOES HERE --></div> <div id=\"divListAdd\"> <input type=\"text\" id=\"txtAddRule\" /> <input type=\"button\" value=\"Add\" id=\"btnAddRule\" /> </div> </div> </div></div>"

proof_tree_item term treeLbl disabled status =
"<div class=\"tree_item dropzone\"> " ++ treeLbl ++
Expand Down
36 changes: 27 additions & 9 deletions resources/static/hjs/jcu.hs
Expand Up @@ -59,13 +59,15 @@ ajaxQ rt url =

registerEvents :: [(String, JEventType, EventHandler)] -> IO ()
registerEvents = mapM_ (\ (e, event, eh) -> do elem <- jQuery e
unbind elem event
bind elem event eh)

main :: IO ()
main = do init <- wrapIO initialize
onDocumentReady init

ruleTreeId = "ul#proof-tree-view.tree"
storeDoCheckId = "#storeDoChecking"

initialize :: IO ()
initialize = do -- Rendering
Expand All @@ -80,17 +82,14 @@ initialize = do -- Rendering

addRuleTree

registerEvents [("#btnCheck" , "click" , toggleClue)
registerEvents [("#btnCheck" , "click" , toggleClue emptyProof)
,("#btnAddRule", "click" , addRuleEvent)
,("#btnReset" , "click" , resetTree)
,("#txtAddRule", "keypress", noevent)
,("#txtAddRule", "blur" , checkTermSyntax)
]
where noevent :: EventHandler
noevent x = return False
toggleClue :: EventHandler
toggleClue _ = do toggleClassString "#proof-tree-div" "noClue"
return True
checkTermSyntax _ = do inp <- jQuery "#txtAddRule"
input <- valString inp
case tryParseRule input of
Expand All @@ -99,7 +98,14 @@ initialize = do -- Rendering
return True
resetTree _ = do replaceRuleTree emptyProof
return True


toggleClue :: Proof -> EventHandler
toggleClue p _ = do toggleClassString "#proof-tree-div" "noClue"
store <- jQuery storeDoCheckId
val <- fmap (read :: String -> Bool) (valString store)
setValString store (show $ not val)
replaceRuleTree p
return True


emptyProof :: Proof
Expand Down Expand Up @@ -174,7 +180,9 @@ replaceRuleTree p = do
newUL <- buildRuleUl p status

-- Store new proof in the subst funct
registerEvents [("#btnSubst", "click", doSubst p)]
registerEvents [("#btnCheck", "click", toggleClue p)
,("#btnSubst", "click", doSubst p)
]
-- Draw the new ruleTree
replaceWith oldUL newUL

Expand Down Expand Up @@ -223,9 +231,16 @@ createRuleLi rule id = do item <- jQuery $ "<li>" ++ rules_list_item rule ++ "</
return item

checkProof :: Proof -> IO PCheck
checkProof p = do rules <- jQuery ".rule-list-item" >>= jQueryToArray
checkProof p = do alert (show p)
rules <- jQuery ".rule-list-item" >>= jQueryToArray
rules' <- (mapM f . elems . jsArrayToArray) rules
return $ Prolog.checkProof rules' p
-- t <- deepE (rules', p)
-- alert (show t)
doCheck <- fmap (read :: String -> Bool) (jQuery storeDoCheckId >>= valString)
if doCheck then
return $ Prolog.checkProof rules' p
else
return $ Prolog.dummyProof p
where f x = getAttr "innerText" x
>>= return . fromJust . tryParseRule . (fromJS :: JSString -> String)

Expand All @@ -245,8 +260,11 @@ checkProof p = do rules <- jQuery ".rule-list-item" >>= jQueryToArray
-- setAttr "proof" p' msg
-- setAttr "rules" rules' msg
-- postMessage proofWorker msg

-- where f x = getAttr "innerText" x
-- >>= return . fromJust . tryParseRule . (fromJS :: JSString -> String)

foreign import jscript "_deepe_"
deepE :: a -> IO a

doSubst :: Proof -> EventHandler
doSubst p _ = do sub <- jQuery "#txtSubstSub" >>= valString
Expand Down

0 comments on commit f07155f

Please sign in to comment.