diff --git a/saw-core/src/Verifier/SAW/Module.hs b/saw-core/src/Verifier/SAW/Module.hs index 43959879af..f1d9237247 100644 --- a/saw-core/src/Verifier/SAW/Module.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index f4b6082621..563ac409a5 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index c6b2597543..0b74d4df4a 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs index 08af32e5eb..f062565dbb 100644 --- a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs +++ b/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