aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.mli4
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/evarconv.ml3
-rw-r--r--pretyping/evardefine.ml2
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/geninterp.ml100
-rw-r--r--pretyping/geninterp.mli72
-rw-r--r--pretyping/patternops.ml10
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/unification.ml19
13 files changed, 209 insertions, 19 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 3a139b7b03..43dbc31058 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -13,8 +13,8 @@ open Environ
open EConstr
open Inductiveops
open Glob_term
-open Evarutil
open Ltac_pretype
+open Evardefine
(** {5 Compilation of pattern-matching } *)
@@ -116,7 +116,7 @@ type 'a pattern_matching_problem =
val compile : 'a pattern_matching_problem -> unsafe_judgment
val prepare_predicate : ?loc:Loc.t ->
- (Evarutil.type_constraint ->
+ (type_constraint ->
Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
Environ.env ->
Evd.evar_map ->
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3a91798138..20ef65c884 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -371,7 +371,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
| PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
Array.fold_left2 (sorec ctx env) subst args1 args2
- | _ -> raise PatternMatchingFailure
+ | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
+ | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
+ | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure
in
sorec [] env (Id.Map.empty, Id.Map.empty) pat c
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 681eb17d3c..18e0c31dd6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -9,7 +9,6 @@
open CErrors
open Util
open Names
-open Term
open Constr
open Termops
open Environ
@@ -49,7 +48,7 @@ let _ = Goptions.declare_bool_option {
"data.id.type" etc... *)
let impossible_default_case () =
let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
- let (_, u) = Term.destConst c in
+ let (_, u) = Constr.destConst c in
Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
let coq_unit_judge =
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 18dbbea1bd..b646a37f8a 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -6,10 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Sorts
open Util
open Pp
open Names
-open Term
open Constr
open Termops
open EConstr
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fba1542912..e6d1e59b3a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,10 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Sorts
open Util
open CErrors
open Names
-open Term
open Constr
open Environ
open Termops
diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml
new file mode 100644
index 0000000000..768ef3cfd9
--- /dev/null
+++ b/pretyping/geninterp.ml
@@ -0,0 +1,100 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Genarg
+
+module TacStore = Store.Make ()
+
+(** Dynamic toplevel values *)
+
+module ValT = Dyn.Make ()
+
+module Val =
+struct
+
+ type 'a typ = 'a ValT.tag
+
+ type _ tag =
+ | Base : 'a typ -> 'a tag
+ | List : 'a tag -> 'a list tag
+ | Opt : 'a tag -> 'a option tag
+ | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+ type t = Dyn : 'a typ * 'a -> t
+
+ let eq = ValT.eq
+ let repr = ValT.repr
+ let create = ValT.create
+
+ let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t)
+
+ let typ_list = ValT.create "list"
+ let typ_opt = ValT.create "option"
+ let typ_pair = ValT.create "pair"
+
+ let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
+ | Base t -> Dyn (t, x)
+ | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x)
+ | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x)
+ | Pair (tag1, tag2) ->
+ Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x)))
+
+end
+
+module ValTMap = ValT.Map
+
+module ValReprObj =
+struct
+ type ('raw, 'glb, 'top) obj = 'top Val.tag
+ let name = "valrepr"
+ let default _ = None
+end
+
+module ValRepr = Register(ValReprObj)
+
+let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
+| ListArg t -> Val.List (val_tag t)
+| OptArg t -> Val.Opt (val_tag t)
+| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
+| ExtraArg s -> ValRepr.obj (ExtraArg s)
+
+let val_tag = function Topwit t -> val_tag t
+
+let register_val0 wit tag =
+ let tag = match tag with
+ | None ->
+ let name = match wit with
+ | ExtraArg s -> ArgT.repr s
+ | _ -> assert false
+ in
+ Val.Base (Val.create name)
+ | Some tag -> tag
+ in
+ ValRepr.register0 wit tag
+
+(** Interpretation functions *)
+
+type interp_sign = {
+ lfun : Val.t Id.Map.t;
+ extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
+
+module InterpObj =
+struct
+ type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun
+ let name = "interp"
+ let default _ = None
+end
+
+module Interp = Register(InterpObj)
+
+let interp = Interp.obj
+
+let register_interp0 = Interp.register0
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
new file mode 100644
index 0000000000..ae0b26e594
--- /dev/null
+++ b/pretyping/geninterp.mli
@@ -0,0 +1,72 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Interpretation functions for generic arguments and interpreted Ltac
+ values. *)
+
+open Names
+open Genarg
+
+(** {6 Dynamic toplevel values} *)
+
+module Val :
+sig
+ type 'a typ
+
+ val create : string -> 'a typ
+
+ type _ tag =
+ | Base : 'a typ -> 'a tag
+ | List : 'a tag -> 'a list tag
+ | Opt : 'a tag -> 'a option tag
+ | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+ type t = Dyn : 'a typ * 'a -> t
+
+ val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
+ val repr : 'a typ -> string
+ val pr : 'a typ -> Pp.t
+
+ val typ_list : t list typ
+ val typ_opt : t option typ
+ val typ_pair : (t * t) typ
+
+ val inject : 'a tag -> 'a -> t
+
+end
+
+module ValTMap (M : Dyn.TParam) :
+ Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+
+(** Dynamic types for toplevel values. While the generic types permit to relate
+ objects at various levels of interpretation, toplevel values are wearing
+ their own type regardless of where they came from. This allows to use the
+ same runtime representation for several generic types. *)
+
+val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
+(** Retrieve the dynamic type associated to a toplevel genarg. *)
+
+val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit
+(** Register the representation of a generic argument. If no tag is given as
+ argument, a new fresh tag with the same name as the argument is associated
+ to the generic type. *)
+
+(** {6 Interpretation functions} *)
+
+module TacStore : Store.S
+
+type interp_sign = {
+ lfun : Val.t Id.Map.t;
+ extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
+
+val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun
+
+val register_interp0 :
+ ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 4d8c09c50a..41e09004c6 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -59,7 +59,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
fixpoint_eq f1 f2
| PCoFix f1, PCoFix f2 ->
cofixpoint_eq f1 f2
-| _ -> false
+| PProj (p1, t1), PProj (p2, t2) ->
+ Projection.equal p1 p2 && constr_pattern_eq t1 t2
+| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
+ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
+ | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false
(** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -442,8 +446,8 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
one non-trivial branch. These facts are used in [Constrextern]. *)
PCase (info, pred, pat_of_raw metas vars c, brs)
- | r -> err ?loc (Pp.str "Non supported pattern.")
- )
+ | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+ err ?loc (Pp.str "Non supported pattern."))
and pats_of_glob_branches loc metas vars ind brs =
let get_arg p = match DAst.get p with
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eb2b435bf6..b2735ee22c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -17,8 +17,8 @@ open Environ
open Evd
open EConstr
open Glob_term
-open Evarutil
open Ltac_pretype
+open Evardefine
(** An auxiliary function for searching for fixpoint guard indexes *)
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 9904b73540..1da5b4567f 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,3 +1,4 @@
+Geninterp
Ltac_pretype
Locusops
Pretype_errors
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e6d8a0af26..9ff9a75b3e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -213,7 +213,7 @@ let compute_canonical_projections warn (con,ind) =
let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
let t = EConstr.Unsafe.to_constr t in
let lt = List.rev_map snd sign in
- let args = snd (Term.decompose_app t) in
+ let args = snd (decompose_app t) in
let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
lookup_structure ind in
let params, projs = List.chop p args in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 04374c88b4..ba0502ca45 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1167,7 +1167,8 @@ let local_whd_state_gen flags sigma =
|_ -> s
else s
- | x -> s
+ | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s
+
in
whrec
@@ -1771,8 +1772,8 @@ let meta_reducible_instance evd b =
let is_coerce = match s with CoerceToType -> true | _ -> false in
if not is_coerce then irec g else u
with Not_found -> u)
- | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) ->
- let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in
+ | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
+ let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
(match
try
let g, s = Metamap.find m metas in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a4e2f90d4c..84ffab4260 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -573,7 +573,9 @@ let is_rigid_head sigma flags t =
| Ind (i,u) -> true
| Construct _ -> true
| Fix _ | CoFix _ -> true
- | _ -> false
+ | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _)
+ | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _)
+ | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
let force_eqs c =
Universes.Constraints.fold
@@ -654,7 +656,10 @@ let rec is_neutral env sigma ts t =
| Evar _ | Meta _ -> true
| Case (_, p, c, cl) -> is_neutral env sigma ts c
| Proj (p, c) -> is_neutral env sigma ts c
- | _ -> false
+ | Lambda _ | LetIn _ | Construct _ | CoFix _ -> false
+ | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
+ | Fix _ -> false (* This is an approximation *)
+ | App _ -> assert false
let is_eta_constructor_app env sigma ts f l1 term =
match EConstr.kind sigma f with
@@ -1788,7 +1793,9 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
with ex when precatchable_exception ex ->
matchrec c)
- | _ -> user_err Pp.(str "Match_subterm")))
+ | Cast (_, _, _) (* Is this expected? *)
+ | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
+ | Construct _ -> user_err Pp.(str "Match_subterm")))
in
try matchrec cl
with ex when precatchable_exception ex ->
@@ -1854,7 +1861,11 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
| Lambda (_,t,c) ->
bind (matchrec t) (matchrec c)
- | _ -> fail "Match_subterm"))
+ | Cast (_, _, _) -> fail "Match_subterm" (* Is this expected? *)
+
+ | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
+ | Construct _ -> fail "Match_subterm"))
+
in
let res = matchrec cl [] in
match res with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:35:41 +0000