diff options
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 46 |
1 files changed, 37 insertions, 9 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 4ee13c961..d626630ef 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -14,8 +14,9 @@ open CAst open Names open Nameops open Libnames +open Namegen +open Glob_term open Constrexpr -open Misctypes open Decl_kinds (***********************) @@ -161,7 +162,7 @@ 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) -> @@ -395,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, @@ -545,7 +546,7 @@ let coerce_to_id = function 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 = 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.") @@ -569,7 +570,7 @@ 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' -> CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) @@ -601,7 +602,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 |