Checkpoint (possibly broken)

TcTypeNats.hs

@@ -67,8 +67,7 @@ insertFact g props =
   case addFact g (facts props) of
     Inconsistent  -> mzero
     AlreadyKnown  -> return (noChanges props)
-    Improved fs   -> return (noChanges props)
-                            { newFacts = Props.fromList fs }
+    Improved f    -> return (noChanges props) { newFacts = Props.singleton f }
     Added new newProps -> return
       InsertInert { newGoals     = Props.toList (goals props)
                   , newFacts     = new
@@ -90,9 +89,11 @@ new work.
 -}
 
 addFact :: Fact -> Facts -> AddFact
-addFact f fs =
+addFact f fs
+  | gTrace (text "adding fact:" <+> pp f) = undefined
+  | otherwise =
   case improveFact (getEqFacts fs) f of
-    Just f1 -> Improved [f1]
+    Just f1 -> Improved f1
     Nothing ->
       case factProp f of
         _ | impossible (factProp f) -> Inconsistent
@@ -133,7 +134,7 @@ addFactTrans facts0  fact =
   case addFact fact facts0 of
     Inconsistent    -> mzero
     AlreadyKnown    -> return facts0
-    Improved fs     -> addFactsTrans' facts0 fs
+    Improved f      -> addFactTrans facts0 f
     Added fs facts1 -> addFactsTrans  facts1 fs
 
 

TcTypeNatsBase.hs

@@ -172,7 +172,7 @@ data Theorem  = EqRefl      -- forall a.                        a = a
               | AddAssocFL | AddAssocFR | AddAssocBL | AddAssocBR
               | MulAssocFL | MulAssocFR | MulAssocBL | MulAssocBR
 
-              | MulTo0L
+              | MulTo0L | MulTo0R
                 deriving Show
 
 

TcTypeNatsFacts.hs

@@ -105,7 +105,7 @@ data AddFact
   | AlreadyKnown
   -- ^ The fact was not added because it was already known.
 
-  | Improved [Fact]
+  | Improved Fact
   -- ^ The fact was not added because we found a better set of equivalent facts.
 
   | Added (Props Fact) Facts
@@ -154,7 +154,7 @@ addLeqFact :: Proof -> Term -> Term -> Facts -> AddFact
 addLeqFact ev t1 t2 fs =
   case Leq.addFact ev t1 t2 (factsLeq fs) of
     Leq.AlreadyKnown -> AlreadyKnown
-    Leq.Improved f   -> Improved [f]
+    Leq.Improved f   -> Improved f
     Leq.Added ls     -> Added (facts fs) fs { factsLeq = ls
                                             , facts = Props.empty
                                             }

genRule.lhs

@@ -5,8 +5,8 @@
 > import Data.Char(toUpper)
 
 > main :: IO ()
-> main = print $ genRules $ allRules ++ otherRules ++ concatMap specAx allRules
->   where allRules = funRules ++ assocRules
+> main = print $ genRules allRules
+>   where allRules = funRules ++ anihRules ++ otherRules ++ assocRules
 
 > names :: [String]
 > names = concatMap block [ 0 :: Integer .. ]
@@ -33,6 +33,8 @@
 
 
 
+
+
 Terms, Propositions, and Rules
 ==============================
 
@@ -104,8 +106,14 @@ Syntactic Sugar
 Concrete Rules
 ==============
 
+Instantiate Fun* with basic axioms:
+  0 + a = a
+  1 * a = a
+  0 * a = 0
+
+
 > funRules :: [Rule]
-> funRules =
+> funRules = concatMap spec1 $
 >   [ rule "AddFun"  [ a :+ b === c, a :+ b === d ] (c === d)
 >   , rule "SubFunR" [ a :+ b === c, d :+ b === c ] (a === d)
 >   , rule "SubFunL" [ a :+ b === c, a :+ d === c ] (b === d)
@@ -122,18 +130,31 @@ Concrete Rules
 >   ]
 >
 >   where a : b : c : d : _ = map Var names
+>         spec1 r = r : take 1 (specAx r)
+
+
+
+> anihRules :: [Rule]
+> anihRules =
+>   [ rule "MulTo0L"  [ Num 2 <== a, a :* b === b ] (b === Num 0)
+>   , rule "MulTo0R"  [ Num 2 <== b, a :* b === a ] (a === Num 0)
+>   ]
+>   where a : b : c : d : _ = map Var names
+
 
 > otherRules :: [Rule]
 > otherRules =
->   [ rule "MulTo0L"  [ Num 1 <== a, a :* b === b ] (b === Num 0) ]
+>   [ rule "AddComm"  [ a :+ b === c ] (b :+ a === c)
+>   , rule "MulComm"  [ a :* b === c ] (b :* a === c)
+>   ]
 >
 >   where a : b : c : d : _ = map Var names
 
 
 
 
 > assocRules :: [Rule]
-> assocRules =
+> assocRules = concatMap specAx $
 >   [ rule "AddAssocFL"
 >       [ a :+ b === x, b :+ c === y, a :+ y === z ]
 >       (x :+ c === z)
@@ -171,6 +192,38 @@ Concrete Rules
 >   where a : b : c : x : y : z : _ = map Var names
 
 
+
+> baseRules :: [Rule]
+> baseRules =
+>   [ rule "Add0_L" [] (a :+ Num 0 === a)
+>   ]
+>   where a : b : c : x : y : z : _ = map Var names
+
+> {-
+> cut1gt
+
+> specAx :: Rule -> [Rule]
+> specAx r =
+>   do (n, Prop op [ Var x, Var y, Var z ]) <- rAsmps r
+>      let upd (Var a) | a `elem` [ x, y, z ] = Con a
+>          upd a                              = a
+>          updP (Prop o ts)                   = Prop o (map upd ts)
+>      return Rule
+>        { rForall = rForall r \\ [ x, y, z ]
+>        , rAsmps  = [ (m,updP p) | (m,p) <- rAsmps r, m /= n ]
+>        , rConc   = updP $ rConc r
+>        , rSides  = nub $ Prop op [ Con x, Con y, Con z ] : rSides r
+>        , rProof  = \ts ps -> rProof r (map conVar [x,y,z] ++ ts)
+>                       ((n, DefAx op (Con x) (Con y)) : ps)
+>        }
+>   where conVar x                         = (x, Con x)
+> -}
+
+
+
+
+
+
 Generating Haskell
 ==================