mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
More debug info and comments only
This commit is contained in:
parent
c9bbf02a71
commit
aa4bd9c9b0
@ -247,6 +247,11 @@ simpGoals s gs0 =
|
|||||||
panic "simpGoals" ( "Unable to import required well-definedness constraints:"
|
panic "simpGoals" ( "Unable to import required well-definedness constraints:"
|
||||||
: map (show . Num.ppProp) invalid )
|
: map (show . Num.ppProp) invalid )
|
||||||
|
|
||||||
|
if null nonDef
|
||||||
|
then debugLog s "(all constraints are well-defined)"
|
||||||
|
else debugBlock s "Non-well defined constratins:" $
|
||||||
|
debugLog s (map fst nonDef)
|
||||||
|
|
||||||
def2 <- Num.simplifyProps s def1
|
def2 <- Num.simplifyProps s def1
|
||||||
let allCts = apSubst su $ map toGoal extraProps ++
|
let allCts = apSubst su $ map toGoal extraProps ++
|
||||||
map fst nonDef ++
|
map fst nonDef ++
|
||||||
|
@ -455,7 +455,9 @@ cryIsFin expr =
|
|||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
-- An alternative representation
|
-- An alternative representation
|
||||||
|
|
||||||
data Atom = AFin Name | AGt Expr Expr | AEq Expr Expr
|
data Atom = AFin Name
|
||||||
|
| AGt Expr Expr -- on naturals
|
||||||
|
| AEq Expr Expr -- on naturals
|
||||||
deriving Eq
|
deriving Eq
|
||||||
|
|
||||||
type Prop' = IfExpr' Atom Bool
|
type Prop' = IfExpr' Atom Bool
|
||||||
@ -477,6 +479,8 @@ propToProp' prop =
|
|||||||
PTrue -> pTrue
|
PTrue -> pTrue
|
||||||
|
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Pretty print
|
||||||
|
|
||||||
ppAtom :: Atom -> Doc
|
ppAtom :: Atom -> Doc
|
||||||
ppAtom atom =
|
ppAtom atom =
|
||||||
@ -488,6 +492,10 @@ ppAtom atom =
|
|||||||
ppProp' :: Prop' -> Doc
|
ppProp' :: Prop' -> Doc
|
||||||
ppProp' = ppIf ppAtom (text . show)
|
ppProp' = ppIf ppAtom (text . show)
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
|
-- | Implementation of `==`
|
||||||
pEq :: Expr -> Expr -> Prop'
|
pEq :: Expr -> Expr -> Prop'
|
||||||
pEq x (K (Nat 0)) = pEq0 x
|
pEq x (K (Nat 0)) = pEq0 x
|
||||||
pEq x (K (Nat 1)) = pEq1 x
|
pEq x (K (Nat 1)) = pEq1 x
|
||||||
@ -496,11 +504,13 @@ pEq (K (Nat 1)) y = pEq1 y
|
|||||||
pEq x y = pIf (pInf x) (pInf y)
|
pEq x y = pIf (pInf x) (pInf y)
|
||||||
$ pAnd (pFin y) (pAtom (AEq x y))
|
$ pAnd (pFin y) (pAtom (AEq x y))
|
||||||
|
|
||||||
|
-- | Implementation of `>=`
|
||||||
pGeq :: Expr -> Expr -> Prop'
|
pGeq :: Expr -> Expr -> Prop'
|
||||||
pGeq x y = pIf (pInf x) pTrue
|
pGeq x y = pIf (pInf x) pTrue
|
||||||
$ pIf (pFin y) (pAtom (AGt (x :+ one) y))
|
$ pIf (pFin y) (pAtom (AGt (x :+ one) y))
|
||||||
pFalse
|
pFalse
|
||||||
|
|
||||||
|
-- | Implementation of `Fin` on expressions.
|
||||||
pFin :: Expr -> Prop'
|
pFin :: Expr -> Prop'
|
||||||
pFin expr =
|
pFin expr =
|
||||||
case expr of
|
case expr of
|
||||||
@ -530,12 +540,15 @@ pFin expr =
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
-- | False
|
||||||
pFalse :: Prop'
|
pFalse :: Prop'
|
||||||
pFalse = Return False
|
pFalse = Return False
|
||||||
|
|
||||||
|
-- | True
|
||||||
pTrue :: Prop'
|
pTrue :: Prop'
|
||||||
pTrue = Return True
|
pTrue = Return True
|
||||||
|
|
||||||
|
-- | NEgation
|
||||||
pNot :: Prop' -> Prop'
|
pNot :: Prop' -> Prop'
|
||||||
pNot p =
|
pNot p =
|
||||||
case p of
|
case p of
|
||||||
@ -543,12 +556,15 @@ pNot p =
|
|||||||
Return a -> Return (not a)
|
Return a -> Return (not a)
|
||||||
If c t e -> If c (pNot t) (pNot e)
|
If c t e -> If c (pNot t) (pNot e)
|
||||||
|
|
||||||
|
-- | Sugar for `and`
|
||||||
pAnd :: Prop' -> Prop' -> Prop'
|
pAnd :: Prop' -> Prop' -> Prop'
|
||||||
pAnd p q = pIf p q pFalse
|
pAnd p q = pIf p q pFalse
|
||||||
|
|
||||||
|
-- | Sugar for `or`
|
||||||
pOr :: Prop' -> Prop' -> Prop'
|
pOr :: Prop' -> Prop' -> Prop'
|
||||||
pOr p q = pIf p pTrue q
|
pOr p q = pIf p pTrue q
|
||||||
|
|
||||||
|
-- | If-then-else with non-atom at decision.
|
||||||
pIf :: (Eq a, Eq p) =>
|
pIf :: (Eq a, Eq p) =>
|
||||||
IfExpr' p Bool -> IfExpr' p a -> IfExpr' p a -> IfExpr' p a
|
IfExpr' p Bool -> IfExpr' p a -> IfExpr' p a -> IfExpr' p a
|
||||||
pIf c t e =
|
pIf c t e =
|
||||||
@ -559,6 +575,7 @@ pIf c t e =
|
|||||||
_ | t == e -> t
|
_ | t == e -> t
|
||||||
If p t1 e1 -> If p (pIf t1 t e) (pIf e1 t e) -- duplicates
|
If p t1 e1 -> If p (pIf t1 t e) (pIf e1 t e) -- duplicates
|
||||||
|
|
||||||
|
-- | Atoms to propositions.
|
||||||
pAtom :: Atom -> Prop'
|
pAtom :: Atom -> Prop'
|
||||||
pAtom p = do a <- case p of
|
pAtom p = do a <- case p of
|
||||||
AFin _ -> return p
|
AFin _ -> return p
|
||||||
@ -566,9 +583,12 @@ pAtom p = do a <- case p of
|
|||||||
AGt x y -> liftM2 AGt (eNoInf x) (eNoInf y)
|
AGt x y -> liftM2 AGt (eNoInf x) (eNoInf y)
|
||||||
If a pTrue pFalse
|
If a pTrue pFalse
|
||||||
|
|
||||||
|
-- | Implement `e1 > e2`.
|
||||||
pGt :: Expr -> Expr -> Prop'
|
pGt :: Expr -> Expr -> Prop'
|
||||||
pGt x y = pIf (pFin y) (pIf (pFin x) (pAtom (AGt x y)) pTrue) pFalse
|
pGt x y = pIf (pFin y) (pIf (pFin x) (pAtom (AGt x y)) pTrue) pFalse
|
||||||
|
|
||||||
|
-- | Special rules implementing `e == 0`
|
||||||
|
-- Assuming the original expression was well-formed.
|
||||||
pEq0 :: Expr -> Prop'
|
pEq0 :: Expr -> Prop'
|
||||||
pEq0 expr =
|
pEq0 expr =
|
||||||
case expr of
|
case expr of
|
||||||
@ -588,6 +608,8 @@ pEq0 expr =
|
|||||||
LenFromThen _ _ _ -> pFalse
|
LenFromThen _ _ _ -> pFalse
|
||||||
LenFromThenTo x y z -> pIf (pGt x y) (pGt z x) (pGt x z)
|
LenFromThenTo x y z -> pIf (pGt x y) (pGt z x) (pGt x z)
|
||||||
|
|
||||||
|
-- | Special rules implementing `e == 1`
|
||||||
|
-- Assuming the original expression was well-formed.
|
||||||
pEq1 :: Expr -> Prop'
|
pEq1 :: Expr -> Prop'
|
||||||
pEq1 expr =
|
pEq1 expr =
|
||||||
case expr of
|
case expr of
|
||||||
@ -620,6 +642,7 @@ pEq1 expr =
|
|||||||
pInf :: Expr -> Prop'
|
pInf :: Expr -> Prop'
|
||||||
pInf = pNot . pFin
|
pInf = pNot . pFin
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
type IExpr = IfExpr' Atom Expr
|
type IExpr = IfExpr' Atom Expr
|
||||||
@ -976,6 +999,8 @@ normSum = posTerm . go 0 Map.empty Nothing . splitSum
|
|||||||
posTerm (Neg,x) = K (Nat 0) :- x
|
posTerm (Neg,x) = K (Nat 0) :- x
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
crySimpExprStep :: Expr -> Maybe Expr
|
crySimpExprStep :: Expr -> Maybe Expr
|
||||||
crySimpExprStep e =
|
crySimpExprStep e =
|
||||||
case crySimpExprStep1 e of
|
case crySimpExprStep1 e of
|
||||||
|
Loading…
Reference in New Issue
Block a user