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/constr.ml | 163 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 162 insertions(+), 1 deletion(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index cec00c04b..be59f9341 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -233,7 +233,6 @@ let mkMeta n = Meta n (* Constructs a Variable named id *) let mkVar id = Var id - (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -250,6 +249,168 @@ let of_kind = function | Cast (c, knd, t) -> mkCast (c, knd, t) | k -> k +(**********************************************************************) +(* Non primitive term destructors *) +(**********************************************************************) + +(* Destructor operations : partial functions + Raise [DestKO] if the const has not the expected form *) + +exception DestKO + +let isMeta c = match kind c with Meta _ -> true | _ -> false + +(* Destructs a type *) +let isSort c = match kind c with + | Sort _ -> true + | _ -> false + +let rec isprop c = match kind c with + | Sort (Sorts.Prop _) -> true + | Cast (c,_,_) -> isprop c + | _ -> false + +let rec is_Prop c = match kind c with + | Sort (Sorts.Prop Sorts.Null) -> true + | Cast (c,_,_) -> is_Prop c + | _ -> false + +let rec is_Set c = match kind c with + | Sort (Sorts.Prop Sorts.Pos) -> true + | Cast (c,_,_) -> is_Set c + | _ -> false + +let rec is_Type c = match kind c with + | Sort (Sorts.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 c with Evar _ -> true | _ -> false +let isEvar_or_Meta c = match kind c with + | Evar _ | Meta _ -> true + | _ -> false + +let isCast c = match kind c with Cast _ -> true | _ -> false +(* Tests if a de Bruijn index *) +let isRel c = match kind c with Rel _ -> true | _ -> false +let isRelN n c = + match kind c with Rel n' -> Int.equal n n' | _ -> false +(* Tests if a variable *) +let isVar c = match kind c with Var _ -> true | _ -> false +let isVarId id c = match kind c with Var id' -> Id.equal id id' | _ -> false +(* Tests if an inductive *) +let isInd c = match kind c with Ind _ -> true | _ -> false +let isProd c = match kind c with | Prod _ -> true | _ -> false +let isLambda c = match kind c with | Lambda _ -> true | _ -> false +let isLetIn c = match kind c with LetIn _ -> true | _ -> false +let isApp c = match kind c with App _ -> true | _ -> false +let isConst c = match kind c with Const _ -> true | _ -> false +let isConstruct c = match kind c with Construct _ -> true | _ -> false +let isCase c = match kind c with Case _ -> true | _ -> false +let isProj c = match kind c with Proj _ -> true | _ -> false +let isFix c = match kind c with Fix _ -> true | _ -> false +let isCoFix c = match kind c with CoFix _ -> true | _ -> false + +(* Destructs a de Bruijn index *) +let destRel c = match kind c with + | Rel n -> n + | _ -> raise DestKO + +(* Destructs an existential variable *) +let destMeta c = match kind c with + | Meta n -> n + | _ -> raise DestKO + +(* Destructs a variable *) +let destVar c = match kind c with + | Var id -> id + | _ -> raise DestKO + +let destSort c = match kind c with + | Sort s -> s + | _ -> raise DestKO + +(* Destructs a casted term *) +let destCast c = match kind c with + | Cast (t1,k,t2) -> (t1,k,t2) + | _ -> raise DestKO + +(* Destructs the product (x:t1)t2 *) +let destProd c = match kind c with + | Prod (x,t1,t2) -> (x,t1,t2) + | _ -> raise DestKO + +(* Destructs the abstraction [x:t1]t2 *) +let destLambda c = match kind c with + | Lambda (x,t1,t2) -> (x,t1,t2) + | _ -> raise DestKO + +(* Destructs the let [x:=b:t1]t2 *) +let destLetIn c = match kind c with + | LetIn (x,b,t1,t2) -> (x,b,t1,t2) + | _ -> raise DestKO + +(* Destructs an application *) +let destApp c = match kind c with + | App (f,a) -> (f, a) + | _ -> raise DestKO + +(* Destructs a constant *) +let destConst c = match kind c with + | Const kn -> kn + | _ -> raise DestKO + +(* Destructs an existential variable *) +let destEvar c = match kind c with + | Evar (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a (co)inductive type named kn *) +let destInd c = match kind c with + | Ind (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a constructor *) +let destConstruct c = match kind c with + | Construct (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a term

Case c of lc1 | lc2 .. | lcn end *) +let destCase c = match kind c with + | Case (ci,p,c,v) -> (ci,p,c,v) + | _ -> raise DestKO + +let destProj c = match kind c with + | Proj (p, c) -> (p, c) + | _ -> raise DestKO + +let destFix c = match kind c with + | Fix fix -> fix + | _ -> raise DestKO + +let destCoFix c = match kind c with + | CoFix cofix -> cofix + | _ -> raise DestKO + + +(******************************************************************) +(* Flattening and unflattening of embedded applications and casts *) +(******************************************************************) + +let decompose_app c = + match kind c with + | App (f,cl) -> (f, Array.to_list cl) + | _ -> (c,[]) + +let decompose_appvect c = + match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) + (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) -- cgit v1.2.3