Update comments relating to the way iota reductions work.

Minor other fixes.

saw-core/src/Verifier/SAW/Module.hs

@@ -151,24 +151,25 @@ data Ctor =
     -- where the @ps@ are the parameters and the @ix@s are the indices of
     -- datatype @d@
   , ctorIotaReduction ::
-       Term   {- ^ eliminator term -} ->
+       Term   {- ^ recursor term -} ->
        Map VarIndex Term {- ^ constructor eliminators -} ->
        [Term] {- ^ constructor arguments -} ->
        IO Term
     -- ^ Cached functon for computing the result of one step of iota
     --   reduction of the term
     --
-    -- > RecursorApp d params p_ret elims ixs (c params args)
+    -- > RecursorApp rec ixs (c params args)
     --
-    -- where @params@, @p_ret@, @elims@, and @args@ are distinct free variables,
-    -- in that order, so that the last @arg@ is the most recently-bound
-    -- variable, i.e., has deBruijn index 0.  This means that an iota reduction
-    -- of the above recursor application can be performed by passing the
-    -- concrete parameters, eliminators, and constructor arguments to this function.
-    -- Note that we are assuming that the @elims@ are in the same order as they are
-    -- listed in the corresponding 'DataType' for this constructor.
+    --   The arguments to this function are the recusor value, the
+    --   the map from the recursor that maps constructors to eliminator
+    --   functions, and the arguments to the constructor.
 
   , ctorIotaTemplate :: Term
+    -- ^ Cached term used for computing iota reductions.  It has free variables
+    --   @rec@, @elim@ and @args@, in that order so that the last @arg@ is the
+    --   most recently-bound variable with deBruijn index 0.  The @rec@ variable
+    --   represents the recursor value, @elim@ represents the eliminator function
+    --   for the constructor, and @args@ represent the arguments to this constructor.
   }
 
 -- | Return the number of parameters of a constructor

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -532,12 +532,19 @@ asRecordRedex t =
 -- constructor application; specifically, this function recognizes
 --
 -- > RecursorApp rec _ (CtorApp c _ args)
+--
+-- Note that this function does not recognize applications of
+-- recursors to concrete Nat values; see @asNatIotaRedex@.
 asIotaRedex :: R.Recognizer Term (Term, CompiledRecursor Term, PrimName Term, [Term])
 asIotaRedex t =
   do (rec, crec, _, arg) <- R.asRecursorApp t
      (c, _, args) <- R.asCtorParams arg
      return (rec, crec, c, args)
 
+-- | An iota redex whose argument is a concrete nautral number; specifically,
+--   this function recognizes
+--
+--   > RecursorApp rec _ n
 asNatIotaRedex :: R.Recognizer Term (Term, CompiledRecursor Term, Natural)
 asNatIotaRedex t =
   do (rec, crec, _, arg) <- R.asRecursorApp t

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -624,17 +624,18 @@ scBuildCtor ::
 scBuildCtor sc d c arg_struct =
   do
     -- Step 0: allocate a fresh unique varaible index for this constructor
+    -- and register its name in the naming environment
     varidx <- scFreshGlobalVar sc
     scRegisterName sc varidx (ModuleIdentifier c)
 
-    -- Step 1: build the types for the constructor
+    -- Step 1: build the types for the constructor and the type required
+    -- of its eliminator functions
     tp <- scShCtxM sc $ ctxCtorType d arg_struct
     let cec = PrimName varidx c tp
     elim_tp_fun <- scShCtxM sc $ mkCtorElimTypeFun d cec arg_struct
 
-    -- Step 2: build free variables for params, p_ret, the elims, and the ctor
-    -- arguments
-    -- let num_params = bindingsLength $ ctorParams arg_struct
+    -- Step 2: build free variables for rec, elim and the
+    -- constructor argument variables
     let num_args =
           case arg_struct of
             CtorArgStruct {..} -> bindingsLength ctorArgs
@@ -644,7 +645,7 @@ scBuildCtor sc d c arg_struct =
     rec_var  <- scLocalVar sc (num_args+1)
 
     -- Step 3: pass these variables to ctxReduceRecursor to build the
-    -- ctorIotaReduction field
+    -- ctorIotaTemplate field
     iota_red <- scShCtxM sc $
       ctxReduceRecursor rec_var elim_var vars arg_struct
 
@@ -701,9 +702,9 @@ scRecursorRetTypeType sc dt params s =
 -- | Reduce an application of a recursor. This is known in the Coq literature as
 -- an iota reduction. More specifically, the call
 --
--- > scReduceRecursor sc d [p1, .., pn] P [(c1,f1), .., (cm,fm)] ci [x1, .., xk]
+-- > scReduceRecursor sc rec crec ci [x1, .., xk]
 --
--- reduces the term @(RecursorApp d ps P cs_fs ixs (CtorApp ci ps xs))@ to
+-- reduces the term @(RecursorApp rec ixs (CtorApp ci ps xs))@ to
 --
 -- > fi x1 (maybe rec_tm_1) .. xk (maybe rec_tm_k)
 --
@@ -714,7 +715,7 @@ scRecursorRetTypeType sc dt params s =
 scReduceRecursor ::
   SharedContext ->
   Term {- ^ recusor term -} ->
-  CompiledRecursor Term ->
+  CompiledRecursor Term {- ^ concrete data included in the recursor term -} ->
   PrimName Term {- ^ constructor name -} ->
   [Term] {- ^ constructor arguments -} ->
   IO Term
@@ -724,11 +725,16 @@ scReduceRecursor sc rec crec c args =
       -- we just substitute into to perform the reduction
       ctorIotaReduction ctor rec (fmap fst $ recursorElims crec) args
 
+-- | Reduce an application of a recursor to a concrete nat value.
+--   The given recursor value is assumed to be correctly-typed
+--   for the @Nat@ datatype.  It will reduce using either the
+--   elimiation function for @Zero@ or @Succ@, depending on
+--   the concrete value of the @Nat@.
 scReduceNatRecursor ::
   SharedContext ->
   Term {- ^ recusor term -} ->
-  CompiledRecursor Term ->
-  Natural ->
+  CompiledRecursor Term {- ^ concrete data included in the recursor term -} ->
+  Natural {- ^ Concrete natural value to eliminate -} ->
   IO Term
 scReduceNatRecursor sc rec crec n
   | n == 0 =
@@ -1014,12 +1020,11 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
           s <- sort motive_ty
           lift $ scSort sc s
         Recursor rec -> do
-          mty <- memo (recursorMotive rec)
           lift $ scFlatTermF sc $
              RecursorType (recursorDataType rec)
                           (recursorParams rec)
                           (recursorMotive rec)
-                          mty
+                          (recursorMotiveTy rec)
         RecursorApp rec ixs arg ->
           do tp <- (liftIO . scWhnf sc) =<< memo rec
              case asRecursorType tp of

saw-core/src/Verifier/SAW/Term/CtxTerm.hs

@@ -943,29 +943,30 @@ mkCtorElimTypeFun d c argStruct@(CtorArgStruct {..}) =
              InvNoBind NoBind ctxElimType
 
 
--- | Reduce an application of a recursor. This is known in the Coq literature as
--- an iota reduction. More specifically, the call
+-- | Reduce an application of a recursor to a particular constructor.
+-- This is known in the Coq literature as an iota reduction. More specifically,
+-- the call
 --
--- > ctxReduceRecursor d [p1, .., pn] P [(c1,f1), .., (cm,fm)] ci [x1, .., xk]
+-- > ctxReduceRecursor rec f_c [x1, .., xk]
 --
--- reduces the term @(RecursorApp d ps P cs_fs ixs (CtorApp ci ps xs))@ to
+-- reduces the term @(RecursorApp rec ixs (CtorApp c ps xs))@ to
 --
--- > fi x1 (maybe rec_tm_1) .. xk (maybe rec_tm_k)
+-- > f_c x1 (maybe rec_tm_1) .. xk (maybe rec_tm_k)
 --
--- where @maybe rec_tm_i@ indicates an optional recursive call of the recursor
--- on one of the @xi@. These recursive calls only exist for those arguments @xi@
--- that are recursive arguments, i.e., that are specified with 'RecursiveArg',
--- and are omitted for non-recursive arguments specified by 'ConstArg'.
+-- where @f_c@ is the eliminator function associated to the constructor @c@ by the
+-- recursor value @rec@.  Here @maybe rec_tm_i@ indicates an optional recursive call
+-- of the recursor on one of the @xi@. These recursive calls only exist for those
+-- arguments @xi@ that are recursive arguments, i.e., that are specified with
+-- 'RecursiveArg', and are omitted for non-recursive arguments specified by 'ConstArg'.
 --
 -- Specifically, for a @'RecursiveArg' zs ixs@ argument @xi@, which has type
 -- @\(z1::Z1) -> .. -> d p1 .. pn ix1 .. ixp@, we build the recursive call
 --
--- > \(z1::[ps/params,xs/args]Z1) -> .. ->
--- >   RecursorApp d ps P cs_fs [ps/params,xs/args]ixs (xi z1 ... zn)
+-- > \(z1::[xs/args]Z1) -> .. ->
+-- >   RecursorApp rec [xs/args]ixs (xi z1 ... zn)
 --
--- where @[ps/params,xs/args]@ substitutes the concrete parameters @pi@ for the
--- parameter variables of the inductive type and the earlier constructor
--- arguments @xs@ for the remaining free variables.
+-- where @[xs/args]@ substitutes the concrete values for the earlier
+-- constructor arguments @xs@ for the remaining free variables.
 
 ctxReduceRecursor :: forall m d params ixs.
   MonadTerm m =>
@@ -985,11 +986,15 @@ ctxReduceRecursor rec elimf c_args CtorArgStruct{..} =
        error "ctxReduceRecursorRaw: wrong number of constructor arguments!"
 
 
+-- | This operation does the real work of building the
+--   iota reduction for @ctxReduceRecursor@.  We assume
+--   the input terms we are given live in an ambient
+--   context @amb@.
 ctxReduceRecursor_ :: forall m amb d ixs elim args.
   MonadTerm m =>
-  CtxTerm amb (Rec d) ->
-  CtxTerm amb elim ->
-  CtxTerms amb args {- ^ constructor actual arguments -} ->
+  CtxTerm  amb (Rec d) {- ^ recursor value eliminatiting data type d -}->
+  CtxTerm  amb elim    {- ^ eliminator function for the constructor -} ->
+  CtxTerms amb args    {- ^ constructor actual arguments -} ->
   Bindings (CtorArg d ixs) amb args
     {- ^ telescope describing the constructor arguments -} ->
   m Term
@@ -998,6 +1003,7 @@ ctxReduceRecursor_ rec fi args0 argCtx =
      whnfTerm =<< foldM (\f arg -> mkTermF $ App f arg) (unAmb fi) args
 
  where
+   -- extract a raw term into the ambient context
     unAmb :: forall tp. CtxTerm amb tp -> Term
     unAmb (CtxTerm t) = t