Skip to content

Commit 4b94b12

Browse files
brianhuffmanbrianhuffman
committed
saw-core: Move 'Variable' constructor from FlatTermF to TermF.
With the plan to move away from de Bruijn indices for variable binding, the 'Variable' constructor will play a more specialized role, and so it makes more sense to be out of FlatTermF.
1 parent 7670313 commit 4b94b12

File tree

15 files changed

+53
-52
lines changed

15 files changed

+53
-52
lines changed

‎cryptol-saw-core/src/CryptolSAWCore/Monadify.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,7 @@ asTypedGlobalDef t =
173173
Constant nm ->
174174
let ty = resolvedNameType (requireNameInMap nm ?mm)
175175
in Just $ GlobalDef (nameInfo nm) (nameIndex nm) ty t
176-
FTermF (Variable ec) ->
176+
Variable ec ->
177177
Just $ GlobalDef (ecName ec) (ecVarIndex ec) (ecType ec) t
178178
_ -> Nothing
179179

‎saw-central/src/SAWCentral/Crucible/Common/Override.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,7 @@ import qualified SAWSupport.Pretty as PPS (defaultOpts, limitMaxDepth)
111111
import SAWCore.Name (toShortName)
112112
import SAWCore.Prelude as SAWVerifier (scEq)
113113
import SAWCore.SharedTerm as SAWVerifier
114-
import SAWCore.Term.Functor (FlatTermF(..), unwrapTermF)
114+
import SAWCore.Term.Functor (unwrapTermF)
115115
import SAWCore.Term.Pretty (ppTerm, scPrettyTerm)
116116
import CryptolSAWCore.TypedTerm as SAWVerifier
117117

@@ -723,7 +723,7 @@ matchTerm sc md prepost real expect =
723723
do let loc = MS.conditionLoc md
724724
free <- OM (use osFree)
725725
case unwrapTermF expect of
726-
FTermF (Variable ec)
726+
Variable ec
727727
| Set.member (ecVarIndex ec) free ->
728728
do assignTerm sc md prepost (ecVarIndex ec) real
729729

‎saw-central/src/SAWCentral/MRSolver/Monad.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1015,7 +1015,7 @@ extCnsToFunName ec =
10151015
Just (EVarInfo _ _) -> return $ EVarFunName var
10161016
Just (CallVarInfo _) -> return $ CallSName var
10171017
Nothing
1018-
| Just glob <- asTypedGlobalDef (Unshared $ FTermF $ Variable ec) ->
1018+
| Just glob <- asTypedGlobalDef (Unshared $ Variable ec) ->
10191019
return $ GlobalName glob []
10201020
_ -> error "extCnsToFunName: unreachable"
10211021

‎saw-central/src/SAWCentral/MRSolver/Term.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -114,8 +114,8 @@ asGlobalFunName _ = Nothing
114114

115115
-- | Convert a 'FunName' to an unshared term, for printing
116116
funNameTerm :: FunName -> Term
117-
funNameTerm (CallSName var) = Unshared $ FTermF $ Variable $ unMRVar var
118-
funNameTerm (EVarFunName var) = Unshared $ FTermF $ Variable $ unMRVar var
117+
funNameTerm (CallSName var) = Unshared $ Variable $ unMRVar var
118+
funNameTerm (EVarFunName var) = Unshared $ Variable $ unMRVar var
119119
funNameTerm (GlobalName gdef []) = globalDefTerm gdef
120120
funNameTerm (GlobalName gdef (TermProjLeft:projs)) =
121121
Unshared $ FTermF $ PairLeft $ funNameTerm (GlobalName gdef projs)

‎saw-core-coq/src/SAWCoreCoq/Term.hs‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -470,13 +470,6 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
470470
return $ Coq.List elems
471471
StringLit s -> pure (Coq.Scope (Coq.StringLit (Text.unpack s)) "string")
472472

473-
Variable ec ->
474-
do env <- view namedEnvironment <$> askTR
475-
let nm = Name (ecVarIndex ec) (ecName ec)
476-
case Map.lookup nm env of
477-
Just ident -> pure (Coq.Var ident)
478-
Nothing -> translateConstant nm
479-
480473
-- The translation of a record type {fld1:tp1, ..., fldn:tpn} is
481474
-- RecordTypeCons fld1 tp1 (... (RecordTypeCons fldn tpn RecordTypeNil)...).
482475
-- Note that SAW core equates record types up to reordering, so we sort our
@@ -800,6 +793,13 @@ translateTermUnshared t = do
800793
-- Constants
801794
Constant n -> translateConstant n
802795

796+
Variable ec ->
797+
do nenv <- view namedEnvironment <$> askTR
798+
let nm = Name (ecVarIndex ec) (ecName ec)
799+
case Map.lookup nm nenv of
800+
Just ident -> pure (Coq.Var ident)
801+
Nothing -> translateConstant nm
802+
803803
where
804804
badTerm = Except.throwError $ BadTerm t
805805

‎saw-core/src/SAWCore/ExternalFormat.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,9 @@ scWriteExternal t0 =
134134
Constant nm ->
135135
do stashName nm
136136
pure $ unwords ["Constant", show (nameIndex nm)]
137+
Variable ec ->
138+
do stashEC ec
139+
pure $ unwords ["Variable", show (ecVarIndex ec), show (ecType ec)]
137140
FTermF ftf ->
138141
case ftf of
139142
UnitValue -> pure $ unwords ["Unit"]
@@ -174,9 +177,6 @@ scWriteExternal t0 =
174177
ArrayValue e v -> pure $ unwords ("Array" : show e :
175178
map show (V.toList v))
176179
StringLit s -> pure $ unwords ["String", show s]
177-
Variable ec ->
178-
do stashEC ec
179-
pure $ unwords ["Variable",show (ecVarIndex ec), show (ecType ec)]
180180

181181

182182
-- | During parsing, we maintain two maps used for renumbering: The
@@ -343,5 +343,5 @@ scReadExternal sc input =
343343
["Nat", n] -> FTermF <$> (NatLit <$> readM n)
344344
("Array" : e : es) -> FTermF <$> (ArrayValue <$> readIdx e <*> (V.fromList <$> traverse readIdx es))
345345
("String" : ts) -> FTermF <$> (StringLit <$> (readM (unwords ts)))
346-
["Variable", i, t] -> FTermF <$> (Variable <$> readEC i t)
346+
["Variable", i, t] -> Variable <$> readEC i t
347347
_ -> fail $ "Parse error: " ++ unwords tokens

‎saw-core/src/SAWCore/OpenTerm.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1196,7 +1196,7 @@ sawLetMinimize sc t_top =
11961196
slMinTermF' tf@(LocalVar i) =
11971197
tell (varOccs1 i) >> liftIO (scTermF sc tf)
11981198
slMinTermF' tf@(Constant _) = liftIO (scTermF sc tf)
1199+
slMinTermF' tf@(Variable _) = liftIO (scTermF sc tf)
11991200

12001201
slMinFTermF :: FlatTermF Term -> SLMinM Term
1201-
slMinFTermF ftf@(Variable _) = liftIO $ scFlatTermF sc ftf
12021202
slMinFTermF ftf = traverse slMinTerm ftf >>= liftIO . scFlatTermF sc

‎saw-core/src/SAWCore/Recognizer.hs‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -346,10 +346,9 @@ asConstant _ = Nothing
346346

347347
asVariable :: Recognizer Term (ExtCns Term)
348348
asVariable t =
349-
do ftf <- asFTermF t
350-
case ftf of
351-
Variable ec -> pure ec
352-
_ -> Nothing
349+
case unwrapTermF t of
350+
Variable ec -> pure ec
351+
_ -> Nothing
353352

354353
asSort :: Recognizer Term Sort
355354
asSort t = do

‎saw-core/src/SAWCore/Rewriter.hs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -167,7 +167,7 @@ firstOrderMatch ctxt pat term = match pat term IntMap.empty
167167
match :: Term -> Term -> IntMap Term -> Maybe (IntMap Term)
168168
match x y m =
169169
case (unwrapTermF x, unwrapTermF y) of
170-
(FTermF (Variable (ecVarIndex -> i)), _) | IntSet.member i ixs ->
170+
(Variable (ecVarIndex -> i), _) | IntSet.member i ixs ->
171171
case my' of
172172
Nothing -> Just m'
173173
Just y' -> if alphaEquiv y y' then Just m' else Nothing
@@ -260,7 +260,7 @@ scMatch sc ctxt pat term =
260260
where
261261
go js x =
262262
case unwrapTermF x of
263-
FTermF (Variable ec)
263+
Variable ec
264264
| IntSet.member (ecVarIndex ec) ixs -> Just (ecVarIndex ec, js)
265265
| otherwise -> Nothing
266266
App t (unwrapTermF -> LocalVar j)
@@ -816,6 +816,7 @@ rewriteSharedTermTypeSafe sc ss t0 =
816816
_ -> App <$> rewriteAll e1 <*> pure e2
817817
Lambda pat t e -> Lambda pat t <$> rewriteAll e
818818
Constant{} -> return tf
819+
Variable{} -> return tf
819820
_ -> return tf -- traverse rewriteAll tf
820821

821822
rewriteFTermF :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) =>
@@ -843,7 +844,6 @@ rewriteSharedTermTypeSafe sc ss t0 =
843844
NatLit{} -> return ftf -- doesn't matter
844845
ArrayValue t es -> ArrayValue t <$> traverse rewriteAll es
845846
StringLit{} -> return ftf
846-
Variable{} -> return ftf
847847

848848
rewriteTop :: (?cache :: Cache IO TermIndex Term, ?annSet :: IORef (Set a)) =>
849849
Term -> IO Term
@@ -1018,6 +1018,7 @@ doHoistIfs sc ss hoistCache = go
10181018

10191019
goF t (LocalVar _) = return (t, [])
10201020
goF t (Constant {}) = return (t, [])
1021+
goF t (Variable {}) = return (t, [])
10211022

10221023
goF _ (FTermF ftf) = do
10231024
(ftf', conds) <- runWriterT $ traverse WriterT $ (fmap go ftf)

‎saw-core/src/SAWCore/SCTypeCheck.hs‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -484,7 +484,6 @@ typeInferConstant nm =
484484
-- with special cases for primitives and constants to avoid re-type-checking
485485
-- their types as we are assuming they were type-checked when they were created
486486
instance TypeInfer (FlatTermF Term) where
487-
typeInfer (Variable ec) = return $ ecType ec
488487
typeInfer t = typeInfer =<< mapM typeInferComplete t
489488
typeInferComplete ftf =
490489
SCTypedTerm <$> liftTCM scFlatTermF ftf
@@ -518,6 +517,9 @@ instance TypeInfer (TermF SCTypedTerm) where
518517
error ("Context = " ++ show ctx)
519518
-- throwTCError (DanglingVar (i - length ctx))
520519
typeInfer (Constant nm) = typeInferConstant nm
520+
typeInfer (Variable ec) =
521+
-- FIXME: should we check that the type of ecType is a sort?
522+
typeCheckWHNF $ typedVal $ ecType ec
521523

522524
typeInferComplete tf =
523525
SCTypedTerm <$> liftTCM scTermF (fmap typedVal tf)
@@ -572,9 +574,6 @@ instance TypeInfer (FlatTermF SCTypedTerm) where
572574
forM_ vs $ \v_elem -> checkSubtype v_elem tp'
573575
liftTCM scVecType n tp'
574576
typeInfer (StringLit{}) = liftTCM scStringType
575-
typeInfer (Variable ec) =
576-
-- FIXME: should we check that the type of ecType is a sort?
577-
typeCheckWHNF $ typedVal $ ecType ec
578577

579578
typeInferComplete ftf =
580579
SCTypedTerm <$> liftTCM scFlatTermF (fmap typedVal ftf)

0 commit comments

Comments
 (0)