Fix some bugs and refactor some common code.

Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
ezyang · Dec 20, 2012 · 35fc5ac · 35fc5ac
1 parent ae36125
commit 35fc5ac
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 57 deletions.
diff --git a/Linear.hs b/Linear.hs
@@ -25,12 +25,12 @@ errorModule s = error ("Linear." ++ s)
 data S = S { persistent :: [L], ephemeral :: [L], goal :: L }
     deriving (Show, Eq, Data, Typeable)
 
+-- All of these are *linear* variants (this is reflected syntactically)
 data L = Prop String
        | Conj L L
        | Disj L L
        | Imp L L
-       | Iff L L
-       | Not L
+       | Bang L
        | Top
        | Bot
     deriving (Show, Eq, Data, Typeable)
@@ -54,14 +54,18 @@ linearStyle = emptyDef
                 , P.opStart         = P.opLetter linearStyle
                 , P.opLetter        = oneOf ":!#$%&*+./<=>?@\\^|-~,"
                 , P.reservedOpNames =
-                    ["(",")",".",",",";",
-                    "->", "→",
+                    ["(", ")", ",", ";",
                     "-o", "⊸",
-                    "<->", "↔", "<=>",
-                    "/\\","∧",
-                    "\\/","∨",
-                    "|-","⊢",
-                    "~","¬"]
+                    "!",
+                    "&",
+                    "?&", "⅋", -- what is conventional?
+                    "+", "⊕",
+                    "*", "⊗",
+                    -- "/\\","∧",
+                    -- "\\/","∨",
+                    "|-","⊢"
+                    -- "~","¬"
+                    ]
                 , P.reservedNames   =
                     [
                     "True","False","⊤","⊥",
@@ -117,10 +121,9 @@ sequent = try (S <$> commaSep expr <* choice [reservedOp ";"] <*> commaSep expr
        <?> "sequent"
 
 table :: [[Operator String u Identity L]]
-table   = [ [prefix "~" Not, prefix "¬" Not ]
-          , [binary "/\\" Conj AssocLeft, binary "∧" Conj AssocLeft ]
+table   = [ [binary "/\\" Conj AssocLeft, binary "∧" Conj AssocLeft ]
           , [binary "\\/" Disj AssocLeft, binary "∨" Disj AssocLeft ]
-          , [binary "->" Imp AssocRight, binary "→" Imp AssocRight, binary "<->" Iff AssocRight, binary "↔" Iff AssocRight, binary "<=>" Iff AssocRight ]
+          , [binary "->" Imp AssocRight, binary "→" Imp AssocRight ]
           ]
 
 binary :: String -> (a -> a -> a) -> Assoc -> Operator String u Identity a

diff --git a/build.sh b/build.sh
@@ -12,7 +12,7 @@ do
     pkill -f $NAME.exe
     (
         ghc -Wall -Werror --make -c ClassicalFOLFFI.hs && \
-        ghc -Wall -Werror --make -c LinearFFI.hs && \
+        #ghc -Wall -Werror --make -c LinearFFI.hs && \
         ghc -Wall -Werror --make -c IntuitionisticFFI.hs && \
         ghc -Wall -Werror --make -c haskell.c && \
         urweb $URWEB_FLAGS $NAME && \

diff --git a/common.ur b/common.ur
@@ -4,7 +4,7 @@ val typeCase = @@Variant.typeCase
 fun activeCode m = <xml><active code={m; return <xml/>} /></xml>
 fun activate x m = <xml>{x}{activeCode m}</xml>
 
-val head = <xml>
+val headTemplate = <xml>
     <link rel="stylesheet" type="text/css" href="http://localhost/logitext/style.css" />
     <link rel="stylesheet" type="text/css" href="http://localhost/logitext/tipsy.css" />
     </xml>

diff --git a/intuitionistic.ur b/intuitionistic.ur
@@ -379,7 +379,7 @@ fun proving goal =
   return <xml>
         <head>
           <title>Proving {[goal]}</title>
-          {head}
+          {headTemplate}
         </head>
         <body>
         <div class={page}>
@@ -397,7 +397,7 @@ and main () : transaction page =
   return <xml>
       <head>
         <title>Logitext/Intuitionistic</title>
-          {head}
+          {headTemplate}
       </head>
       <body>
       <div class={page}>

diff --git a/linear.ur b/linear.ur
@@ -1,30 +1,7 @@
-style proof
-style proofIsDone
-style proofIsIncomplete
-style proofIsPending
-style rules
-style inference
-style tagBox
-style tag
-style sibling
-style junct
-style viewport
-style commaList
-style relMark
-style offsetBox
-style working
-style page
-style errorStyle
-style turnstile
-style centerTable
-style offsetInner
-style green
-style primaryConnective
-style primaryExpr
-
 open Json
 open List
 open Common
+open Style
 
 task initialize = Haskell.initVanilla
 
@@ -218,7 +195,7 @@ fun renderSequent (showError : xbody -> transaction unit) (h : proof -> transact
                     }>{renderLogic True 0 x}</span></li></xml>
               in return bod
               end
-            ) s.Persistent;
+            ) s.Ephemeral;
     let val right =
       case s.Goal of
         Disj (x,y) => <xml><span class={junct}>

diff --git a/logitext.ur b/logitext.ur
@@ -1,14 +1,9 @@
 open Json
 open Style
-
-val declareCase = @@Variant.declareCase
-val typeCase = @@Variant.typeCase
+open Common
 
 task initialize = Haskell.initClassicalFOL
 
-fun activeCode m = <xml><active code={m; return <xml/>} /></xml>
-fun activate x m = <xml>{x}{activeCode m}</xml>
-
 fun renderName (f : string) : xbody =
   let val i = strcspn f "0123456789"
   in <xml>{[substring f 0 i]}<sub>{[substring f i (strlen f - i)]}</sub></xml>
@@ -207,8 +202,6 @@ structure Proof = Json.Recursive(struct
 end)
 type proof = Proof.r
 
-fun andB a b = if a then b else False
-
 fun proofComplete (Proof.Rec p) : bool =
     match p {Goal = fn _ => False,
              Pending = fn _ => False,
@@ -344,11 +337,6 @@ fun renderProof showError (h : proof -> transaction unit) ((Proof.Rec r) : proof
 
 fun zapRefine (x : proof) : transaction string  = return (Haskell.refineClassicalFOL (toJson x))
 
-val head = <xml>
-    <link rel="stylesheet" type="text/css" href="http://localhost/logitext/style.css" />
-    <link rel="stylesheet" type="text/css" href="http://localhost/logitext/tipsy.css" />
-    </xml>
-
 val wSequent : xbody =
     <xml><span title="A statement of provability.  Γ ⊢ Δ states that given the
     hypotheses Γ, one of the conclusions Δ is provable.">sequent</span></xml>
@@ -463,7 +451,7 @@ fun tutorial () =
   return <xml>
   <head>
     <title>Interactive Tutorial of the Sequent Calculus</title>
-    {head}
+    {headTemplate}
   </head>
   <body>
     <div class={page}>
@@ -804,7 +792,7 @@ and proving goal =
   return <xml>
         <head>
           <title>Proving {[goal]}</title>
-          {head}
+          {headTemplate}
         </head>
         <body>
         <div class={page}>
@@ -832,7 +820,7 @@ and main () =
   return <xml>
       <head>
         <title>Logitext</title>
-          {head}
+          {headTemplate}
       </head>
       <body>
       <div class={page}>