Documentation

ucsd-progsys · Dec 13, 2024 · 7ee749a · 7ee749a
1 parent abd8d33
commit 7ee749a
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
@@ -589,6 +589,12 @@ bvConcatSort = FAbs 0 $ FAbs 1 $ FAbs 2 $
 interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
 interpSym x n t = (x, Thy x n t Theory)
 
+-- This variable is uded to generate the lambda names `lam_arg$n` in
+-- `Interface.hs` that will be used during defunctionalization in
+-- `Defunctionalize.hs`, is a pretty gross hack as if the user typees in the
+-- program or ple generates a term that has more than `maxLamArg` lambda binders
+-- one inside the other, the smt will crash complaining that
+-- `lam_arg${maxLamArg}` was not declared.
 maxLamArg :: Int
 maxLamArg = 20
 

diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs
@@ -655,10 +655,10 @@ eval γ ctx et = go
 evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)
 evalELam γ ctx et (x, s) e
   | not $ isEtaSymbol x = do
-    -- We need to refresh it as for some reason lamdba variables
-    -- as reflected lambdas variables for some reason are declared
-    -- two times, maybe we should define a new type of identifier
-    -- and not reuse the etabeta ones
+    -- We need to refresh it as for some reason names bound by lambdas
+    -- present in the source code are getting declared twice.
+    -- Maybe we should define a new type of identifier for this kind of fresh
+    -- variables and not reuse the etabeta ones.
     [ xFresh ] <- makeFreshEtaNames 1
     let newBody = subst (mkSubst [(x, EVar xFresh)]) e