From 88afd8a9853c772b6b1681c7ae208e55e7daacbe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 08:11:07 +0100 Subject: [api] Deprecate Term destructors, move to Constr We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`. --- kernel/term.ml | 204 +++++++++++++-------------------------------------------- 1 file changed, 45 insertions(+), 159 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 1c970867a..4217cfac7 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -11,6 +11,7 @@ open Pp open CErrors open Names open Vars +open Constr (**********************************************************************) (** Redeclaration of types from module Constr *) @@ -165,167 +166,52 @@ let hcons_types = Constr.hcons (* Non primitive term destructors *) (**********************************************************************) -(* Destructor operations : partial functions - Raise [DestKO] if the const has not the expected form *) - -exception DestKO - +exception DestKO = DestKO (* Destructs a de Bruijn index *) -let destRel c = match kind_of_term c with - | Rel n -> n - | _ -> raise DestKO - -(* Destructs an existential variable *) -let destMeta c = match kind_of_term c with - | Meta n -> n - | _ -> raise DestKO - -let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false - -(* Destructs a variable *) -let destVar c = match kind_of_term c with - | Var id -> id - | _ -> raise DestKO - -(* Destructs a type *) -let isSort c = match kind_of_term c with - | Sort _ -> true - | _ -> false - -let destSort c = match kind_of_term c with - | Sort s -> s - | _ -> raise DestKO - -let rec isprop c = match kind_of_term c with - | Sort (Prop _) -> true - | Cast (c,_,_) -> isprop c - | _ -> false - -let rec is_Prop c = match kind_of_term c with - | Sort (Prop Null) -> true - | Cast (c,_,_) -> is_Prop c - | _ -> false - -let rec is_Set c = match kind_of_term c with - | Sort (Prop Pos) -> true - | Cast (c,_,_) -> is_Set c - | _ -> false - -let rec is_Type c = match kind_of_term c with - | Sort (Type _) -> true - | Cast (c,_,_) -> is_Type c - | _ -> false - -let is_small = Sorts.is_small - -let iskind c = isprop c || is_Type c - -(* Tests if an evar *) -let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false - -let isEvar_or_Meta c = match kind_of_term c with - | Evar _ | Meta _ -> true - | _ -> false - -(* Destructs a casted term *) -let destCast c = match kind_of_term c with - | Cast (t1,k,t2) -> (t1,k,t2) - | _ -> raise DestKO - -let isCast c = match kind_of_term c with Cast _ -> true | _ -> false - - -(* Tests if a de Bruijn index *) -let isRel c = match kind_of_term c with Rel _ -> true | _ -> false -let isRelN n c = - match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false - -(* Tests if a variable *) -let isVar c = match kind_of_term c with Var _ -> true | _ -> false -let isVarId id c = - match kind_of_term c with Var id' -> Id.equal id id' | _ -> false - -(* Tests if an inductive *) -let isInd c = match kind_of_term c with Ind _ -> true | _ -> false - -(* Destructs the product (x:t1)t2 *) -let destProd c = match kind_of_term c with - | Prod (x,t1,t2) -> (x,t1,t2) - | _ -> raise DestKO - -let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false - -(* Destructs the abstraction [x:t1]t2 *) -let destLambda c = match kind_of_term c with - | Lambda (x,t1,t2) -> (x,t1,t2) - | _ -> raise DestKO - -let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false - -(* Destructs the let [x:=b:t1]t2 *) -let destLetIn c = match kind_of_term c with - | LetIn (x,b,t1,t2) -> (x,b,t1,t2) - | _ -> raise DestKO - -let isLetIn c = match kind_of_term c with LetIn _ -> true | _ -> false - -(* Destructs an application *) -let destApp c = match kind_of_term c with - | App (f,a) -> (f, a) - | _ -> raise DestKO - +let destRel = destRel +let destMeta = destRel +let isMeta = isMeta +let destVar = destVar +let isSort = isSort +let destSort = destSort +let isprop = isprop +let is_Prop = is_Prop +let is_Set = is_Set +let is_Type = is_Type +let is_small = is_small +let iskind = iskind +let isEvar = isEvar +let isEvar_or_Meta = isEvar_or_Meta +let destCast = destCast +let isCast = isCast +let isRel = isRel +let isRelN = isRelN +let isVar = isVar +let isVarId = isVarId +let isInd = isInd +let destProd = destProd +let isProd = isProd +let destLambda = destLambda +let isLambda = isLambda +let destLetIn = destLetIn +let isLetIn = isLetIn +let destApp = destApp let destApplication = destApp - -let isApp c = match kind_of_term c with App _ -> true | _ -> false - -(* Destructs a constant *) -let destConst c = match kind_of_term c with - | Const kn -> kn - | _ -> raise DestKO - -let isConst c = match kind_of_term c with Const _ -> true | _ -> false - -(* Destructs an existential variable *) -let destEvar c = match kind_of_term c with - | Evar (kn, a as r) -> r - | _ -> raise DestKO - -(* Destructs a (co)inductive type named kn *) -let destInd c = match kind_of_term c with - | Ind (kn, a as r) -> r - | _ -> raise DestKO - -(* Destructs a constructor *) -let destConstruct c = match kind_of_term c with - | Construct (kn, a as r) -> r - | _ -> raise DestKO - -let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false - -(* Destructs a term

Case c of lc1 | lc2 .. | lcn end *) -let destCase c = match kind_of_term c with - | Case (ci,p,c,v) -> (ci,p,c,v) - | _ -> raise DestKO - -let isCase c = match kind_of_term c with Case _ -> true | _ -> false - -let isProj c = match kind_of_term c with Proj _ -> true | _ -> false - -let destProj c = match kind_of_term c with - | Proj (p, c) -> (p, c) - | _ -> raise DestKO - -let destFix c = match kind_of_term c with - | Fix fix -> fix - | _ -> raise DestKO - -let isFix c = match kind_of_term c with Fix _ -> true | _ -> false - -let destCoFix c = match kind_of_term c with - | CoFix cofix -> cofix - | _ -> raise DestKO - -let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false +let isApp = isApp +let destConst = destConst +let isConst = isConst +let destEvar = destEvar +let destInd = destInd +let destConstruct = destConstruct +let isConstruct = isConstruct +let destCase = destCase +let isCase = isCase +let isProj = isProj +let destProj = destProj +let destFix = destFix +let isFix = isFix +let destCoFix = destCoFix +let isCoFix = isCoFix (******************************************************************) (* Flattening and unflattening of embedded applications and casts *) -- cgit v1.2.3