diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 24 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 55 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 4 | ||||
| -rw-r--r-- | interp/constrextern.ml | 119 | ||||
| -rw-r--r-- | interp/constrextern.mli | 12 | ||||
| -rw-r--r-- | interp/constrintern.ml | 70 | ||||
| -rw-r--r-- | interp/constrintern.mli | 5 |
7 files changed, 205 insertions, 84 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b3f06faa1c..b14c325f69 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -13,10 +13,23 @@ open Libnames (** {6 Concrete syntax for terms } *) -(** [constr_expr] is the abstract syntax tree produced by the parser *) -type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl +(** Universes *) +type sort_name_expr = + | CSProp | CProp | CSet + | CType of qualid + | CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *) + +type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen +type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen + +type instance_expr = univ_level_expr list + +(** Constraints don't have anonymous universes *) +type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr + +type universe_decl_expr = (lident list, univ_constraint_expr list) UState.gen_universe_decl type cumul_univ_decl_expr = - ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl + ((lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl type ident_decl = lident * universe_decl_expr option type cumul_ident_decl = lident * cumul_univ_decl_expr option @@ -64,8 +77,7 @@ type prim_token = | Number of NumTok.Signed.t | String of string -type instance_expr = Glob_term.glob_level list - +(** [constr_expr] is the abstract syntax tree produced by the parser *) type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname | CPatCstr of qualid @@ -114,7 +126,7 @@ and constr_expr_r = | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list - | CSort of Glob_term.glob_sort + | CSort of sort_expr | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a60dc11b57..f02874253e 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -18,6 +18,25 @@ open Glob_term open Notation open Constrexpr +(***********) +(* Universes *) + +let sort_name_expr_eq c1 c2 = match c1, c2 with + | CSProp, CSProp + | CProp, CProp + | CSet, CSet -> true + | CType q1, CType q2 -> Libnames.qualid_eq q1 q2 + | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2 + | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false + +let univ_level_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2 + +let sort_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq + (List.equal (fun (x,m) (y,n) -> sort_name_expr_eq x y && Int.equal m n)) + u1 u2 + (***********************) (* For binders parsing *) @@ -59,13 +78,11 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with Id.equal id1 id2 | _ -> false -let eq_ast f { CAst.v = x } { CAst.v = y } = f x y - let rec cases_pattern_expr_eq p1 p2 = if CAst.(p1.v == p2.v) then true else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> - eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 + CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -108,10 +125,10 @@ let rec constr_expr_eq e1 e2 = else match CAst.(e1.v, e2.v) with | 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 && + lident_eq id1 id2 && List.equal fix_expr_eq fl1 fl2 | CCoFix(id1,fl1), CCoFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal cofix_expr_eq fl1 fl2 | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal local_binder_eq bl1 bl2 && @@ -120,7 +137,7 @@ let rec constr_expr_eq e1 e2 = List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) -> - eq_ast Name.equal na1 na2 && + CAst.eq Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 @@ -144,14 +161,14 @@ let rec constr_expr_eq e1 e2 = List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> - List.equal (eq_ast Name.equal) n1 n2 && - Option.equal (eq_ast Name.equal) m1 m2 && + List.equal (CAst.eq Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) m1 m2 && Option.equal constr_expr_eq e1 e2 && constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -161,7 +178,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Glob_ops.glob_sort_eq s1 s2 + sort_expr_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> @@ -187,12 +204,12 @@ let rec constr_expr_eq e1 e2 = | CGeneralization _ | CDelimiters _ | CArray _), _ -> false and args_eq (a1,e1) (a2,e2) = - Option.equal (eq_ast explicitation_eq) e1 e2 && + Option.equal (CAst.eq explicitation_eq) e1 e2 && constr_expr_eq a1 a2 and case_expr_eq (e1, n1, p1) (e2, n2, p2) = constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = @@ -200,35 +217,35 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = constr_expr_eq e1 e2 and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and recursion_order_expr_eq_r r1 r2 = match r1, r2 with - | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CStructRec i1, CStructRec i2 -> lident_eq i1 i2 | CWfRec (i1,e1), CWfRec (i2,e2) -> constr_expr_eq e1 e2 | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> - Option.equal (eq_ast Id.equal) i1 i2 && + Option.equal lident_eq i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false -and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 +and recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2 and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (* Don't care about the [binder_kind] *) - List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 + List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index dfa51918d1..ffa7c8ec10 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -16,6 +16,10 @@ open Constrexpr (** {6 Equalities on [constr_expr] related types} *) +val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool +val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool +val sort_expr_eq : sort_expr -> sort_expr -> bool + val explicitation_eq : explicitation -> explicitation -> bool (** Equality on [explicitation]. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 378adb566c..3969c7ea1f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -923,22 +923,44 @@ let extern_float f scopes = (**********************************************************************) (* mapping glob_constr to constr_expr *) -let extern_glob_sort = function +type extern_env = Id.Set.t * UnivNames.universe_binders +let extern_env env sigma = vars_of_env env, Evd.universe_binders sigma +let empty_extern_env = Id.Set.empty, Id.Map.empty + +let extern_glob_sort_name uvars = function + | GSProp -> CSProp + | GProp -> CProp + | GSet -> CSet + | GLocalUniv u -> CType (qualid_of_lident u) + | GRawUniv u -> CRawType u + | GUniv u -> begin match UnivNames.qualid_of_level uvars u with + | Some qid -> CType qid + | None -> CRawType u + end + +let extern_glob_sort uvars = + map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars))) + +(** wrapper to handle print_universes: don't forget small univs *) +let extern_glob_sort uvars = function (* In case we print a glob_constr w/o having passed through detyping *) - | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> extern_glob_sort uvars u | UNamed _ when not !print_universes -> UAnonymous {rigid=true} - | UNamed _ | UAnonymous _ as u -> u + | UNamed _ | UAnonymous _ as u -> extern_glob_sort uvars u -let extern_universes = function - | Some _ as l when !print_universes -> l +let extern_instance uvars = function + | Some l when !print_universes -> + Some (List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) l) | _ -> None -let extern_ref vars ref us = +let extern_ref (vars,uvars) ref us = extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference vars ref) (extern_universes us) + (extern_reference vars ref) (extern_instance uvars us) let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) +let add_vname (vars,uvars) na = add_vname vars na, uvars + let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> @@ -995,7 +1017,7 @@ let rec extern inctx ?impargs scopes vars r = (* Otherwise... *) extern_applied_ref inctx (select_stronger_impargs (implicits_of_global ref)) - (ref,extern_reference ?loc vars ref) (extern_universes us) args) + (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args) | _ -> let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in let head = sub_extern false scopes vars f in @@ -1015,7 +1037,8 @@ let rec extern inctx ?impargs scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (Name.fold_right Id.Set.add) - (cases_predicate_names tml) vars in + (cases_predicate_names tml) (fst vars) in + let vars' = vars', snd vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na, DAst.get tm with @@ -1035,7 +1058,7 @@ let rec extern inctx ?impargs scopes vars r = Option.map (fun {CAst.loc;v=(ind,nal)} -> let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in - extern_ind_pattern_in_scope scopes vars ind fullargs + extern_ind_pattern_in_scope scopes (fst vars) ind fullargs ) x)) tml in @@ -1058,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r = sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) | GRec (fk,idv,blv,tyv,bv) -> - let vars' = Array.fold_right Id.Set.add idv vars in + let vars' = on_fst (Array.fold_right Id.Set.add idv) vars in (match fk with | GFix (nv,n) -> let listdecl = @@ -1066,8 +1089,8 @@ let rec extern inctx ?impargs scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in let n = match nv.(i) with | None -> None @@ -1082,14 +1105,14 @@ let rec extern inctx ?impargs scopes vars r = Array.mapi (fun i fi -> let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) - | GSort s -> CSort (extern_glob_sort s) + | GSort s -> CSort (extern_glob_sort (snd vars) s) | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) @@ -1105,7 +1128,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) | GArray(u,t,def,ty) -> - CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) in insert_entry_coercion coercion (CAst.make ?loc c) @@ -1127,7 +1150,7 @@ and factorize_prod ?impargs scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) @@ -1168,7 +1191,7 @@ and factorize_lambda inctx scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) @@ -1196,7 +1219,7 @@ and extern_local_binder scopes vars = function match DAst.get b with | GLocalDef (na,bk,bd,ty) -> let (assums,ids,l) = - extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in + extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in (assums,na::ids, CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern_typ scopes vars) ty) :: l) @@ -1204,7 +1227,7 @@ and extern_local_binder scopes vars = function | GLocalAssum (na,bk,ty) -> let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in - (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with + (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') @@ -1219,7 +1242,7 @@ and extern_local_binder scopes vars = function | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in + let p = mkCPatOr (List.map (extern_cases_pattern (fst vars)) p) in let (assums,ids,l) = extern_local_binder scopes vars l in let p = match ty with | None -> p @@ -1227,7 +1250,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern p :: l) and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = - let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes (fst vars))) pll in make ?loc (pll,extern inctx scopes vars c) and extern_notations inctx scopes vars nargs t = @@ -1277,6 +1300,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = end | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) + let vars, uvars = vars in let terms,termlists,binders,binderlists = match_notation_constr ~print_univ:(!print_universes) t ~vars pat in (* Try availability of interpretation ... *) @@ -1300,35 +1324,43 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true - (subentry,(scopt,scl@scopes')) vars c) - terms in + (subentry,(scopt,scl@scopes')) (vars,uvars) c) + terms + in let ll = List.map (fun ((vars,l),(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) - termlists in + List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l) + termlists + in let bl = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)), - Explicit) - binders in + (mkCPatOr (List.map + (extern_cases_pattern_in_scope + (subentry,(scopt,scl@scopes')) vars) + bl)), + Explicit) + binders + in let bll = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) - binderlists in + pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl)) + binderlists + in let c = make_notation loc specific_ntn (l,ll,bl,bll) in let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> - extern true (subentry,(scopt,scl@snd scopes)) vars c) - terms in + extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c) + terms + in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in let a = CRef (cf,None) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in if isCRef_no_univ c.CAst.v && entry_has_global custom then c else match availability_of_entry_coercion custom InConstrEntrySomeLevel with @@ -1348,7 +1380,7 @@ let extern_glob_type ?impargs vars c = let extern_constr ?lax ?(inctx=false) ?scope env sigma t = let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r let extern_constr_in_scope ?lax ?inctx scope env sigma t = @@ -1364,16 +1396,16 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in - extern_glob_type ?impargs (vars_of_env env) r + extern_glob_type ?impargs (extern_env env sigma) r -let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) +let extern_sort sigma s = extern_glob_sort (Evd.universe_binders sigma) (detype_sort sigma s) let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t = let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r (******************************************************************) @@ -1491,10 +1523,13 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with GArray (None, Array.map glob_of t, glob_of def, glob_of ty) let extern_constr_pattern env sigma pat = - extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) + extern true (InConstrEntrySomeLevel,(None,[])) + (* XXX no vars? *) + (Id.Set.empty, Evd.universe_binders sigma) + (glob_of_pat Id.Set.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in - let vars = vars_of_env env in + let vars = extern_env env sigma in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f85e49d2df..298b52f0be 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -23,9 +23,12 @@ open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) +type extern_env = Id.Set.t * UnivNames.universe_binders +val extern_env : env -> Evd.evar_map -> extern_env + val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -43,7 +46,7 @@ val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr -val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort +val extern_sort : Evd.evar_map -> Sorts.t -> sort_expr val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list @@ -96,3 +99,6 @@ val toggle_scope_printing : val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + +(** Probably shouldn't be used *) +val empty_extern_env : extern_env diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0645636255..cf2f333596 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -254,9 +254,12 @@ let contract_curly_brackets_pat ntn (l,ll) = (* side effect; don't inline *) (InConstrEntry,!ntn'),(l,ll) +type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool } + type intern_env = { - ids: Names.Id.Set.t; + ids: Id.Set.t; unb: bool; + local_univs: local_univs; tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; @@ -1160,6 +1163,32 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1225,6 +1254,7 @@ let check_applied_projection isproj realref qid = let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid = let loc = qid.CAst.loc in + let us = intern_instance ~local_univs:env.local_univs us in if qualid_is_ident qid then try let res = intern_var env lvar namedctx loc (qualid_basename qid) us in @@ -1256,7 +1286,8 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us let interp_reference vars r = let (r,_,_),_ = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) - {ids = Id.Set.empty; unb = false ; + {ids = Id.Set.empty; unb = false; + local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *) tmp_scope = None; scopes = []; impls = empty_internalization_env; binder_block_names = None} Environ.empty_named_context_val @@ -2269,12 +2300,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* end *) | CSort s -> DAst.make ?loc @@ - GSort s + GSort (intern_sort ~local_univs:env.local_univs s) | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) | CArray(u,t,def,ty) -> - DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) + DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) @@ -2446,6 +2477,8 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty +let bound_univs sigma = Evd.universe_binders sigma + let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope env sigma typ @@ -2468,8 +2501,9 @@ let intern_gen kind env sigma let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []; - impls; binder_block_names = Some (k,Id.Map.domain impls)} + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope = tmp_scope; scopes = []; + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2558,7 +2592,9 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; + {ids; unb = false; + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope; scopes = []; impls; binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c @@ -2568,8 +2604,11 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} - false (empty_ltac_sign, vl) a in + {ids; unb = false; + local_univs = { bound = Id.Map.empty; unb_univs = false }; + tmp_scope = None; scopes = []; impls; binder_block_names = None} + false (empty_ltac_sign, vl) a + in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in @@ -2596,7 +2635,7 @@ let interp_binder_evars env sigma na t = let my_intern_constr env lvar acc c = internalize env acc false lvar c -let intern_context env impl_env binders = +let intern_context env ~bound_univs impl_env binders = let lvar = (empty_ltac_sign, Id.Map.empty) in let ids = (* We assume all ids around are parts of the prefix of the current @@ -2607,6 +2646,7 @@ let intern_context env impl_env binders = let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) ({ids; unb = false; + local_univs = { bound = bound_univs; unb_univs = true }; tmp_scope = None; scopes = []; impls = impl_env; binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) @@ -2643,17 +2683,21 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl = sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params = - let int_env,bl = intern_context env impl_env params in + let int_env,bl = intern_context env ~bound_univs:(bound_univs sigma) impl_env params in let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in sigma, (int_env, x) (** Local universe and constraint declarations. *) +let interp_known_level evd u = + let u = intern_sort_name ~local_univs:{bound = bound_univs evd; unb_univs=false} u in + Pretyping.known_glob_level evd u + 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 ul = interp_known_level evd u in + let u'l = interp_known_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 diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0de6c3e89d..f92a54e23f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -88,7 +88,8 @@ val intern_gen : typing_constraint -> env -> evar_map -> val intern_pattern : env -> cases_pattern_expr -> lident list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list +val intern_context : env -> bound_univs:UnivNames.universe_binders -> + internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -198,6 +199,8 @@ val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit (** Check that a list of record field definitions doesn't contain duplicates. *) +val interp_known_level : Evd.evar_map -> sort_name_expr -> Univ.Level.t + (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl |