Merge pull request #169 from GaloisInc/scRecursorElimTypes

Bug fix in scRecursorElimTypes
GaloisInc · Mar 9, 2021 · f82bc50 · f82bc50
2 parents 579f38e + 48012d3
commit f82bc50
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -655,7 +655,7 @@ scRecursorElimTypes :: SharedContext -> Ident -> [Term] -> Term ->
 scRecursorElimTypes sc d_id params p_ret =
   do d <- scRequireDataType sc d_id
      forM (dtCtors d) $ \ctor ->
-       do elim_type <- ctorElimTypeFun ctor params p_ret
+       do elim_type <- ctorElimTypeFun ctor params p_ret >>= scWhnf sc
           return (ctorName ctor, elim_type)
 
 

diff --git a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs
@@ -906,6 +906,10 @@ ctxCtorElimType ret (a_top :: Proxy (Typ a)) (d_top :: DataIdent d) c
 -- for the given constructor. We return the substitution function in the monad
 -- so that we only call 'ctxCtorElimType' once but can call the function many
 -- times, in order to amortize the overhead of 'ctxCtorElimType'.
+--
+-- NOTE: Because this function is defined *before* the @SharedTerm@ module, it
+-- cannot call the normalization function @scWHNF@ defined in that module, and
+-- so the terms return by the function it generates are not normalized.
 mkCtorElimTypeFun :: MonadTerm m => Ident -> Ident ->
                      CtorArgStruct d params ixs -> m ([Term] -> Term -> m Term)
 mkCtorElimTypeFun d c argStruct@(CtorArgStruct {..}) =