package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/rocq-runtime.kernel/reduction.ml.html
Source file reduction.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors open Util open Constr open Vars open Environ open CClosure open Context.Rel.Declaration (****************************************************************************) (* Reduction Functions *) (****************************************************************************) let whd_all ?evars env t = match kind t with | (Sort _|Meta _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|String _|Array _) -> t | App (c, _) -> begin match kind c with | Ind _ | Construct _ | Meta _ | Int _ | Float _ | String _ | Array _ -> t | Sort _ | Rel _ | Var _ | Evar _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos ?evars RedFlags.all env) (create_tab ()) (inject t) end | Rel _ | Evar _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> whd_val (create_clos_infos ?evars RedFlags.all env) (create_tab ()) (inject t) let whd_allnolet ?evars env t = match kind t with | (Sort _|Meta _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _|String _|Array _) -> t | App (c, _) -> begin match kind c with | Ind _ | Construct _ | Meta _ | LetIn _ | Int _ | Float _ | String _ | Array _ -> t | Sort _ | Rel _ | Var _ | Evar _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos ?evars RedFlags.allnolet env) (create_tab ()) (inject t) end | Rel _ | Evar _ | Cast _ | Case _ | Proj _ | Const _ | Var _ -> whd_val (create_clos_infos ?evars RedFlags.allnolet env) (create_tab ()) (inject t) (* Application with on-the-fly reduction *) let beta_applist c l = let rec app subst c l = match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _ -> Term.applist (substl subst c, l) in app [] c l let beta_appvect c v = beta_applist c (Array.to_list v) let beta_app c a = beta_applist c [a] (* Compatibility *) let betazeta_appvect = Term.lambda_appvect_decls (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) (* pseudo-reduction rule: * [hnf_prod_app env (Prod(_,B)) N --> B[N] * with an HNF on the first argument to produce a product. * if this does not work, then we use the string S as part of our * error message. *) let hnf_prod_app ?evars env t n = match kind (whd_all ?evars env t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_applist ?evars env t nl = List.fold_left (hnf_prod_app ?evars env) t nl let hnf_prod_applist_decls ?evars env n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") else match kind (whd_allnolet ?evars env t), l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l (* Dealing with arities *) let whd_decompose_prod ?evars env = let rec decrec env m c = let t = whd_all ?evars env c in match kind t with | Prod (n,a,c0) -> let d = LocalAssum (n,a) in decrec (push_rel d env) (Context.Rel.add d m) c0 | _ -> m,t in decrec env Context.Rel.empty let whd_decompose_lambda ?evars env = let rec decrec env m c = let t = whd_all ?evars env c in match kind t with | Lambda (n,a,c0) -> let d = LocalAssum (n,a) in decrec (push_rel d env) (Context.Rel.add d m) c0 | _ -> m,t in decrec env Context.Rel.empty (* The same but preserving lets in the context, not internal ones. *) let whd_decompose_prod_decls ?evars env = let rec prodec_rec env l ty = let rty = whd_allnolet ?evars env ty in match kind rty with | Prod (x,t,c) -> let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c | _ -> let rty' = whd_all ?evars env rty in if Constr.equal rty' rty then l, rty else prodec_rec env l rty' in prodec_rec env Context.Rel.empty let whd_decompose_lambda_decls ?evars env = let rec lamec_rec env l ty = let rty = whd_allnolet ?evars env ty in match kind rty with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c | _ -> let rty' = whd_all ?evars env rty in if Constr.equal rty' rty then l, rty else lamec_rec env l rty' in lamec_rec env Context.Rel.empty let whd_decompose_lambda_n_assum ?evars env n = let rec lamec_rec env n l c = if Int.equal n 0 then l,c else let rc = whd_allnolet ?evars env c in match kind rc with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (n-1) (Context.Rel.add d l) c | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) n (Context.Rel.add d l) c | _ -> let c' = whd_all ?evars env c in if Constr.equal c' c then anomaly (Pp.str "whd_decompose_lambda_n_assum: not enough abstractions") else lamec_rec env n l c' in lamec_rec env n Context.Rel.empty exception NotArity let dest_arity ?evars env c = let l, c = whd_decompose_prod_decls ?evars env c in match kind c with | Sort s -> l,s | _ -> raise NotArity let is_arity ?evars env c = try let _ = dest_arity ?evars env c in true with NotArity -> false let eta_expand ?evars env t ty = let ctxt, _codom = whd_decompose_prod ?evars env ty in let ctxt',t = whd_decompose_lambda ?evars env t in let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in let eta_args = List.rev_map mkRel (List.interval 1 d) in let t = Term.applistc (Vars.lift d t) eta_args in let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in Term.it_mkLambda_or_LetIn t ctxt'
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>