diff --git a/src/Cryptol/Eval/Reference.hs b/src/Cryptol/Eval/Reference.hs index 1b2b0c84..79af905e 100644 --- a/src/Cryptol/Eval/Reference.hs +++ b/src/Cryptol/Eval/Reference.hs @@ -1,5 +1,6 @@ -- | -- Module : $Header$ +-- Description : The reference implementation of the Cryptol evaluation semantics. -- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com @@ -8,8 +9,6 @@ {-# LANGUAGE PatternGuards #-} --- | The reference implementation of the Cryptol evaluation semantics. - module Cryptol.Eval.Reference where import Control.Applicative (liftA2) diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index d9a40301..0e58ab63 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -109,11 +109,11 @@ quickSolverIO ctxt gs = , d ])) -- -} -quickSolver :: Ctxt -> {- ^ Facts we can know -} - [Goal] -> {- ^ Need to solve these -} - Either Goal (Subst,[Goal]) - -- ^ Left: contradiciting goals, - -- Right: inferred types, unsolved goals. +quickSolver :: Ctxt -- ^ Facts we can know + -> [Goal] -- ^ Need to solve these + -> Either Goal (Subst,[Goal]) + -- ^ Left: contradicting goals, + -- Right: inferred types, unsolved goals. quickSolver ctxt gs0 = go emptySubst [] gs0 where go su [] [] = Right (su,[]) @@ -364,10 +364,9 @@ computeImprovements s gs = , (x,t) : _ <- mapMaybe (improveByDefn ints) gs -> do let su' = singleSubst x t debugLog s ("Improve by definition: " ++ show (pp su')) - return (Right su') -} - - -- | otherwise -> return (Right su) - + return (Right su') + | otherwise -> return (Right su) + -} Nothing -> do bad <- Num.minimizeContradictionSimpDef s (map Num.knownDefined nums)