From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/term.ml | 311 ++++++++++++++++-----------------------------------------
 1 file changed, 86 insertions(+), 225 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 15f187e5..e1affb1c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    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
@@ -11,6 +13,7 @@ open Pp
 open CErrors
 open Names
 open Vars
+open Constr
 
 (**********************************************************************)
 (**         Redeclaration of types from module Constr                 *)
@@ -20,7 +23,7 @@ type contents = Sorts.contents = Pos | Null
 
 type sorts = Sorts.t =
   | Prop of contents       (** Prop and Set *)
-  | Type of Univ.universe  (** Type *)
+  | Type of Univ.Universe.t  (** Type *)
 
 type sorts_family = Sorts.family = InProp | InSet | InType
 
@@ -30,7 +33,7 @@ type constr = Constr.t
 type types = Constr.t
 (** Same as [constr], for documentation purposes. *)
 
-type existential_key = Constr.existential_key
+type existential_key = Evar.t
 type existential = Constr.existential
 
 type metavariable = Constr.metavariable
@@ -67,30 +70,31 @@ type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
 type 'a puniverses = 'a Univ.puniverses
 
 (** Simply type aliases *)
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
-type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
+type ('constr, 'types, 'sort, 'univs) kind_of_term =
+  ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
   | Rel       of int
   | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
-  | Sort      of sorts
+  | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
   | Prod      of Name.t * 'types * 'types
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of pconstant
-  | Ind       of pinductive
-  | Construct of pconstructor
+  | Const     of (Constant.t * 'univs)
+  | Ind       of (inductive * 'univs)
+  | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of projection * 'constr
+  | Proj      of Projection.t * 'constr
 
-type values = Constr.values
+type values = Vmvalues.values
 
 (**********************************************************************)
 (**         Redeclaration of functions from module Constr             *)
@@ -142,7 +146,8 @@ let leq_constr_univs = Constr.leq_constr_univs
 let eq_constr_nounivs = Constr.eq_constr_nounivs
 
 let kind_of_term = Constr.kind
-let constr_ord = Constr.compare
+let compare = Constr.compare
+let constr_ord = compare
 let fold_constr = Constr.fold
 let map_puniverses = Constr.map_puniverses
 let map_constr = Constr.map
@@ -163,203 +168,57 @@ 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
-
-(* Destructs a DeBrujin 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
-let isMetaOf mv c =
-  match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> 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
-
+exception DestKO = DestKO
+(* Destructs a de Bruijn index *)
+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 <p>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
-
-(******************************************************************)
-(* Cast management                                                *)
-(******************************************************************)
-
-let rec strip_outer_cast c = match kind_of_term c with
-  | Cast (c,_,_) -> strip_outer_cast c
-  | _ -> c
-
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
-
-let under_outer_cast f c =  match kind_of_term c with
-  | Cast (b,k,t) -> mkCast (f b, k, f t)
-  | _ -> f c
-
-let rec under_casts f c = match kind_of_term c with
-  | Cast (c,k,t) -> mkCast (under_casts f c, k, t)
-  | _            -> f c
+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 *)
 (******************************************************************)
 
-(* flattens application lists throwing casts in-between *)
-let collapse_appl c = match kind_of_term c with
-  | App (f,cl) ->
-      let rec collapse_rec f cl2 =
-        match kind_of_term (strip_outer_cast f) with
-        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-        | _ -> mkApp (f,cl2)
-      in
-      collapse_rec f cl
-  | _ -> c
-
 let decompose_app c =
   match kind_of_term c with
     | App (f,cl) -> (f, Array.to_list cl)
@@ -465,7 +324,7 @@ let rec to_lambda n prod =
     match kind_of_term prod with
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
       | Cast (c,_,_) -> to_lambda n c
-      | _   -> errorlabstrm "to_lambda" (mt ())
+      | _   -> user_err ~hdr:"to_lambda" (mt ())
 
 let rec to_prod n lam =
   if Int.equal n 0 then
@@ -474,7 +333,7 @@ let rec to_prod n lam =
     match kind_of_term lam with
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
       | Cast (c,_,_) -> to_prod n c
-      | _   -> errorlabstrm "to_prod" (mt ())
+      | _   -> user_err ~hdr:"to_prod" (mt ())
 
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
@@ -486,7 +345,7 @@ let lambda_applist c l =
     match kind_of_term c, l with
     | Lambda(_,_,c), arg::l -> app (arg::subst) c l
     | _, [] -> substl subst c
-    | _ -> anomaly (Pp.str "Not enough lambda's") in
+    | _ -> anomaly (Pp.str "Not enough lambda's.") in
   app [] c l
 
 let lambda_appvect c v = lambda_applist c (Array.to_list v)
@@ -495,11 +354,12 @@ let lambda_applist_assum 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 "Not enough arguments")
+      else anomaly (Pp.str "Too many arguments.")
     else match kind_of_term t, l with
     | Lambda(_,_,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 lambda/let's") in
+    | _, [] -> anomaly (Pp.str "Not enough arguments.")
+    | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
   app n [] c l
 
 let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
@@ -510,7 +370,7 @@ let prod_applist c l =
     match kind_of_term c, l with
     | Prod(_,_,c), arg::l -> app (arg::subst) c l
     | _, [] -> substl subst c
-    | _ -> anomaly (Pp.str "Not enough prod's") in
+    | _ -> anomaly (Pp.str "Not enough prod's.") in
   app [] c l
 
 (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
@@ -520,11 +380,12 @@ let prod_applist_assum 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 "Not enough arguments")
+      else anomaly (Pp.str "Too many arguments.")
     else match kind_of_term 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 prod/let's") in
+    | _, [] -> anomaly (Pp.str "Not enough arguments.")
+    | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
 let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v)
@@ -556,26 +417,26 @@ let decompose_lam =
 (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_prod_n n =
-  if n < 0 then error "decompose_prod_n: integer parameter must be positive";
+  if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive");
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else match kind_of_term c with
       | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)   -> prodec_rec l n c
-      | _ -> error "decompose_prod_n: not enough products"
+      | _ -> user_err (str "decompose_prod_n: not enough products")
   in
   prodec_rec [] n
 
 (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_lam_n n =
-  if n < 0 then error "decompose_lam_n: integer parameter must be positive";
+  if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match kind_of_term c with
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)     -> lamdec_rec l n c
-      | _ -> error "decompose_lam_n: not enough abstractions"
+      | _ -> user_err (str "decompose_lam_n: not enough abstractions")
   in
   lamdec_rec [] n
 
@@ -611,7 +472,7 @@ let decompose_lam_assum =
    ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *)
 let decompose_prod_n_assum n =
   if n < 0 then
-    error "decompose_prod_n_assum: integer parameter must be positive";
+    user_err (str "decompose_prod_n_assum: integer parameter must be positive");
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else
@@ -620,7 +481,7 @@ let decompose_prod_n_assum n =
       | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> prodec_rec l n c
-      | c -> error "decompose_prod_n_assum: not enough assumptions"
+      | c -> user_err (str  "decompose_prod_n_assum: not enough assumptions")
   in
   prodec_rec Context.Rel.empty n
 
@@ -632,7 +493,7 @@ let decompose_prod_n_assum n =
    but n is the actual number of destructurated lambdas. *)
 let decompose_lam_n_assum n =
   if n < 0 then
-    error "decompose_lam_n_assum: integer parameter must be positive";
+    user_err (str  "decompose_lam_n_assum: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
@@ -641,14 +502,14 @@ let decompose_lam_n_assum n =
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
       | Cast (c,_,_)      -> lamdec_rec l n c
-      | c -> error "decompose_lam_n_assum: not enough abstractions"
+      | c -> user_err (str "decompose_lam_n_assum: not enough abstractions")
   in
   lamdec_rec Context.Rel.empty n
 
 (* Same, counting let-in *)
 let decompose_lam_n_decls n =
   if n < 0 then
-    error "decompose_lam_n_decls: integer parameter must be positive";
+    user_err (str "decompose_lam_n_decls: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
@@ -657,7 +518,7 @@ let decompose_lam_n_decls n =
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> lamdec_rec l n c
-      | c -> error "decompose_lam_n_decls: not enough abstractions"
+      | c -> user_err (str "decompose_lam_n_decls: not enough abstractions")
   in
   lamdec_rec Context.Rel.empty n
 
@@ -690,7 +551,7 @@ let destArity =
     | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
     | Cast (c,_,_)      -> prodec_rec l c
     | Sort s          -> l,s
-    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity.")
   in
   prodec_rec []
 
-- 
cgit v1.2.3