Respond to review comments

Author: robdockins

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -72,15 +72,7 @@ mkTypedTerm sc trm = do
 --   This operation fails if the type of the argument does
 --   not match the function.
 applyTypedTerm :: SharedContext -> TypedTerm -> TypedTerm -> IO TypedTerm
-applyTypedTerm sc (TypedTerm _tp t1) (TypedTerm _ t2) =
-  do trm <- scApply sc t1 t2
-     ty <- scTypeCheckError sc trm
-     ct <- scCryptolType sc ty
-     let ttt = case ct of
-           Nothing        -> TypedTermOther ty
-           Just (Left k)  -> TypedTermKind k
-           Just (Right t) -> TypedTermSchema (C.tMono t)
-     return (TypedTerm ttt trm)
+applyTypedTerm sc x y = applyTypedTerms sc x [y]
 
 -- | Apply a 'TypedTerm' to a list of arguments. This operation fails
 -- if the first 'TypedTerm' does not have a function type of
@@ -90,6 +82,10 @@ applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm
 applyTypedTerms sc (TypedTerm _ fn) args =
   do trm <- foldM (scApply sc) fn (map ttTerm args)
      ty <- scTypeCheckError sc trm
+     -- NB, scCryptolType can behave in strange ways due to the non-injectivity
+     -- of the mapping from Cryptol to SAWCore types. Perhaps we would be better
+     -- to combine the incoming type information instead of applying and then
+     -- reconstructing here.
      ct <- scCryptolType sc ty
      let ttt = case ct of
            Nothing        -> TypedTermOther ty

src/SAWScript/Builtins.hs

@@ -643,6 +643,14 @@ congruence_for tt =
      congTm <- io $ build_congruence sc (ttTerm tt)
      io $ mkTypedTerm sc congTm
 
+-- | Given an input term, construct another term that
+--   represents a congruence law for that term.
+--   This term will be a Curry-Howard style theorem statement
+--   that can be dispatched to solvers, and should have
+--   type "Prop".
+--
+--   This will only work for terms that represent non-dependent
+--   functions.
 build_congruence :: SharedContext -> Term -> IO Term
 build_congruence sc tm =
   do ty <- scTypeOf sc tm