summaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml107
1 files changed, 72 insertions, 35 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 004c9356..23d0536d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,12 +10,13 @@
open Pp
open Util
-open CAst
open Names
open Nameops
open Libnames
+open Namegen
+open Glob_term
open Constrexpr
-open Misctypes
+open Notation
open Decl_kinds
(***********************)
@@ -72,22 +73,22 @@ let rec cases_pattern_expr_eq p1 p2 =
| CPatAlias(a1,i1), CPatAlias(a2,i2) ->
eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
- eq_reference c1 c2 &&
+ qualid_eq c1 c2 &&
Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
| CPatAtom(r1), CPatAtom(r2) ->
- Option.equal eq_reference r1 r2
+ Option.equal qualid_eq r1 r2
| CPatOr a1, CPatOr a2 ->
List.equal cases_pattern_expr_eq a1 a2
| CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
- String.equal n1 n2 &&
+ notation_eq n1 n2 &&
cases_pattern_notation_substitution_eq s1 s2 &&
List.equal cases_pattern_expr_eq l1 l2
| CPatPrim i1, CPatPrim i2 ->
prim_token_eq i1 i2
| CPatRecord l1, CPatRecord l2 ->
let equal (r1, e1) (r2, e2) =
- eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
+ qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2
in
List.equal equal l1 l2
| CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
@@ -107,7 +108,7 @@ let eq_universes u1 u2 =
let rec constr_expr_eq e1 e2 =
if CAst.(e1.v == e2.v) then true
else match CAst.(e1.v, e2.v) with
- | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
+ | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2
| CFix(id1,fl1), CFix(id2,fl2) ->
eq_ast Id.equal id1 id2 &&
List.equal fix_expr_eq fl1 fl2
@@ -127,7 +128,7 @@ let rec constr_expr_eq e1 e2 =
constr_expr_eq b1 b2
| CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
Option.equal Int.equal proj1 proj2 &&
- eq_reference r1 r2 &&
+ qualid_eq r1 r2 &&
List.equal constr_expr_eq al1 al2
| CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
Option.equal Int.equal proj1 proj2 &&
@@ -135,7 +136,7 @@ let rec constr_expr_eq e1 e2 =
List.equal args_eq al1 al2
| CRecord l1, CRecord l2 ->
let field_eq (r1, e1) (r2, e2) =
- eq_reference r1 r2 && constr_expr_eq e1 e2
+ qualid_eq r1 r2 && constr_expr_eq e1 e2
in
List.equal field_eq l1 l2
| CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
@@ -161,11 +162,11 @@ let rec constr_expr_eq e1 e2 =
| CEvar (id1, c1), CEvar (id2, c2) ->
Id.equal id1 id2 && List.equal instance_eq c1 c2
| CSort s1, CSort s2 ->
- Miscops.glob_sort_eq s1 s2
+ Glob_ops.glob_sort_eq s1 s2
| CCast(t1,c1), CCast(t2,c2) ->
constr_expr_eq t1 t2 && cast_expr_eq c1 c2
| CNotation(n1, s1), CNotation(n2, s2) ->
- String.equal n1 n2 &&
+ notation_eq n1 n2 &&
constr_notation_substitution_eq s1 s2
| CPrim i1, CPrim i2 ->
prim_token_eq i1 i2
@@ -179,7 +180,7 @@ let rec constr_expr_eq e1 e2 =
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _), _ -> false
+ | CGeneralization _ | CDelimiters _ ), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -277,7 +278,9 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
| CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
- | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a
+ | CPatAtom (Some qid)
+ when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+ f (qualid_basename qid) a
| CPatPrim _ | CPatAtom _ -> a
| CPatCast ({CAst.loc},_) ->
CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
@@ -358,7 +361,9 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
- | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
+ | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+ let id = qualid_basename qid in
+ if Id.List.mem id bdvars then l else Id.Set.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
in aux [] Id.Set.empty c
@@ -391,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
| CLetIn (na,a,t,b) ->
CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
- | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
+ | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
| CNotation (n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
@@ -433,11 +438,13 @@ let map_constr_expr_with_binders g f e = CAst.map (function
)
(* Used in constrintern *)
-let rec replace_vars_constr_expr l = function
- | { CAst.loc; v = CRef ({v=Ident id},us) } as x ->
- (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x)
- | c -> map_constr_expr_with_binders Id.Map.remove
- replace_vars_constr_expr l c
+let rec replace_vars_constr_expr l r =
+ match r with
+ | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid ->
+ let id = qualid_basename qid in
+ (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us)
+ with Not_found -> x)
+ | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn
(* Returns the ranges of locs of the notation that are not occupied by args *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)
@@ -506,7 +513,7 @@ let split_at_annot bl na =
(** Pseudo-constructors *)
-let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None)
+let mkIdentC id = CAst.make @@ CRef (qualid_of_ident id,None)
let mkRefC r = CAst.make @@ CRef (r,None)
let mkCastC (a,k) = CAst.make @@ CCast (a,k)
let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
@@ -525,21 +532,23 @@ let mkCProdN ?loc bll c =
let mkCLambdaN ?loc bll c =
CAst.make ?loc @@ CLambdaN (bll,c)
-let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function
- | Ident id -> id
- | Qualid _ ->
- CErrors.user_err ?loc ~hdr:"coerce_reference_to_id"
- (str "This expression should be a simple identifier."))
+let coerce_reference_to_id qid =
+ if qualid_is_ident qid then qualid_basename qid
+ else
+ CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id"
+ (str "This expression should be a simple identifier.")
let coerce_to_id = function
- | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id
+ | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+ CAst.make ?loc @@ qualid_basename qid
| { CAst.loc; _ } -> CErrors.user_err ?loc
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_name = function
- | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id
- | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
+ | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+ CAst.make ?loc @@ Name (qualid_basename qid)
+ | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous
| { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
(str "This expression should be a name.")
@@ -563,9 +572,10 @@ let mkAppPattern ?loc p lp =
let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
| CRef (r,None) ->
CPatAtom (Some r)
- | CHole (None,Misctypes.IntroAnonymous,None) ->
+ | CHole (None,IntroAnonymous,None) ->
CPatAtom None
- | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' ->
+ | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
+ when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
| CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
(mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
@@ -595,7 +605,34 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
}
-(************************************************************************)
-(* Deprecated *)
-let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c
-let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c
+(** Local universe and constraint declarations. *)
+
+let interp_univ_constraints env evd cstrs =
+ let interp (evd,cstrs) (u, d, u') =
+ let ul = Pretyping.interp_known_glob_level evd u in
+ let u'l = Pretyping.interp_known_glob_level evd u' in
+ let cstr = (ul,d,u'l) in
+ let cstrs' = Univ.Constraint.add cstr cstrs in
+ try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+ evd, cstrs'
+ with Univ.UniverseInconsistency e ->
+ CErrors.user_err ~hdr:"interp_constraint"
+ (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
+ in
+ List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+ let open UState in
+ let pl : lident list = decl.univdecl_instance in
+ let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
+ let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+ let decl = { univdecl_instance = pl;
+ univdecl_extensible_instance = decl.univdecl_extensible_instance;
+ univdecl_constraints = cstrs;
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+ in evd, decl
+
+let interp_univ_decl_opt env l =
+ match l with
+ | None -> Evd.from_env env, UState.default_univ_decl
+ | Some decl -> interp_univ_decl env decl
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 15:01:25 +0000