package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/src/coq-core.pretyping/heads.ml.html
Source file heads.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
(************************************************************************) (* * The Coq Proof Assistant / The Coq 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 Util open Names open EConstr open Vars open Context.Named.Declaration (** Characterization of the head of a term *) (* We only compute an approximation to ensure the computation is not arbitrary long (e.g. the head constant of [h] defined to be [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch the evaluation of [phi(0)] and the head of [h] is declared unknown). *) type rigid_head_kind = | RigidParameter of Constant.t (* a Const without body. Module substitution may instantiate it with something else. *) | RigidOther (* a Var without body, inductive, product, sort, projection *) type head_approximation = | RigidHead of rigid_head_kind | ConstructorHead | FlexibleHead of int * int * int * bool (* [true] if a surrounding case *) | NotImmediatelyComputableHead let rec compute_head_const env sigma cst = let body = Environ.constant_opt_value_in env (cst,UVars.Instance.empty) in match body with | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env sigma (EConstr.of_constr c) and compute_head_var env sigma id = match lookup_named id env with | LocalDef (_,c,_) -> kind_of_head env sigma c | _ -> RigidHead RigidOther and kind_of_head env sigma t = let rec aux k l t b = match EConstr.kind sigma (Reductionops.clos_whd_flags RedFlags.betaiotazeta env sigma t) with | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) | Var id -> (try on_subterm k l b (compute_head_var env sigma id) with Not_found -> (* a goal variable *) match lookup_named id env with | LocalDef (_,c,_) -> aux k l c b | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (compute_head_const env sigma cst) with Not_found -> CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++ Names.Constant.print cst ++ str ".")) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidOther | Cast (c,_,_) -> aux k l c b | Lambda (_,_,c) -> begin match l with | [] -> let () = assert (not b) in aux (k + 1) [] c b | h :: l -> aux k l (subst1 h c) b end | LetIn _ -> assert false | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b | Proj (p,_,c) -> RigidHead RigidOther | Case (_,_,_,_,_,c,_) -> aux k [] c true | Int _ | Float _ | Array _ -> ConstructorHead | Fix ((i,j),_) -> let n = i.(j) in try aux k [] (List.nth l n) true with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true) and on_subterm k l with_case = function | FlexibleHead (n,i,q,with_subcase) -> let m = List.length l in let k',rest,a = if n > m then (* eta-expansion *) let a = if i <= m then (* we pick the head in the existing arguments *) lift (n-m) (List.nth l (i-1)) else (* we pick the head in the added arguments *) mkRel (n-i+1) in k+n-m,[],a else (* enough arguments to [cst] *) k,List.skipn n l,List.nth l (i-1) in let l' = List.make q (mkMeta 0) @ rest in aux k' l' a (with_subcase || with_case) | ConstructorHead when with_case -> NotImmediatelyComputableHead | x -> x in aux 0 [] t false let is_rigid env sigma t = match kind_of_head env sigma t with | RigidHead _ | ConstructorHead -> true | _ -> false
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>