Bool values aren't injected into Cryptol expressions

[RyanGlScott]

The SAW manual claims:

• Any variable in scope that has SAWScript type Bool is visible in Cryptol expressions as a value of type Bit.

This doesn't appear to be true in practice, however:

$ ~/Software/saw-0.8/bin/saw 
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.8



sawscript> let b = true;
sawscript> {{ b }}

Cryptol error:
[error] at <stdin>:1:4--1:5 Value not in scope: b

[brianhuffman]

To implement this feature, we'll just need to add a new case for constructor VBool to function extendEnv in module SAWScript.Value:

saw-script/src/SAWScript/Value.hs

Lines 560 to 584 in d3a8872

	extendEnv ::
	SharedContext ->
	SS.LName -> Maybe SS.Schema -> Maybe String -> Value -> TopLevelRW -> IO TopLevelRW
	extendEnv sc x mt md v rw =
	do ce' <-
	case v of
	VTerm t ->
	pure $ CEnv.bindTypedTerm (ident, t) ce
	VType s ->
	pure $ CEnv.bindType (ident, s) ce
	VInteger n ->
	pure $ CEnv.bindInteger (ident, n) ce
	VCryptolModule m ->
	pure $ CEnv.bindCryptolModule (modname, m) ce
	VString s ->
	do tt <- typedTermOfString sc (unpack s)
	pure $ CEnv.bindTypedTerm (ident, tt) ce
	_ ->
	pure ce
	pure $
	rw { rwValues = M.insert name v (rwValues rw)
	, rwTypes = maybeInsert name mt (rwTypes rw)
	, rwDocs = maybeInsert (SS.getVal name) md (rwDocs rw)
	, rwCryptol = ce'
	}

[brianhuffman]

Adding this case should do it:

         VBool b ->
           do t <- scBool sc b
              let schema = Cryptol.tMono Cryptol.tBit
              let tt = TypedTerm (TypedTermSchema schema) t
              pure $ CEnv.bindTypedTerm (ident, tt) ce