diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 41 |
1 files changed, 37 insertions, 4 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 150dad16c2..4508633858 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* 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 *) @@ -119,6 +119,20 @@ let isVarId sigma id c = let isRelN sigma n c = match kind sigma c with Rel n' -> Int.equal n n' | _ -> false +let isRef sigma c = match kind sigma c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +let isRefX sigma x c = + let open GlobRef in + match x, kind sigma c with + | ConstRef c, Const (c', _) -> Constant.equal c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> Id.equal id id' + | _ -> false + + let destRel sigma c = match kind sigma c with | Rel p -> p | _ -> raise DestKO @@ -723,8 +737,27 @@ let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, t -let is_global sigma gr c = - Globnames.is_global gr (to_constr sigma c) +let is_global = isRefX + +(** Kind of type *) + +type kind_of_type = + | SortType of ESorts.t + | CastType of types * t + | ProdType of Name.t Context.binder_annot * t * t + | LetInType of Name.t Context.binder_annot * t * t * t + | AtomicType of t * t array + +let kind_of_type sigma t = match kind sigma t with + | Sort s -> SortType s + | Cast (c,_,t) -> CastType (c, t) + | Prod (na,t,c) -> ProdType (na, t, c) + | LetIn (na,b,t,c) -> LetInType (na, b, t, c) + | App (c,l) -> AtomicType (c, l) + | (Rel _ | Meta _ | Var _ | Evar _ | Const _ + | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) + -> AtomicType (t,[||]) + | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" module Unsafe = struct |