From a0e16c9e5c3f88a8b72935dd4877f13388640f69 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 12 Oct 2017 13:55:08 +0200 Subject: Make Sorts.t private --- interp/discharge.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/discharge.ml b/interp/discharge.ml index 353b0f6057..524bf9a002 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -69,7 +69,7 @@ let refresh_polymorphic_type_of_inductive (_,mip) = | RegularArity s -> s.mind_user_arity, false | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Type ar.template_level), true + mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true let process_inductive info modlist mib = let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in -- cgit v1.2.3 From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 27 Oct 2017 14:03:51 +0200 Subject: Add a non-cumulative impredicative universe SProp. Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged. --- interp/constrextern.ml | 1 + interp/constrintern.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8e49800982..d5cb25d1fb 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -755,6 +755,7 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo (* mapping glob_constr to constr_expr *) let extern_glob_sort = function + | GSProp -> GSProp | GProp -> GProp | GSet -> GSet | GType _ as s when !print_universes -> s diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7f1dc70d95..b4c570d444 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1020,6 +1020,7 @@ let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option let glob_sort_of_level (level: glob_level) : glob_sort = match level with + | GSProp -> GSProp | GProp -> GProp | GSet -> GSet | GType info -> GType [sort_info_of_level_info info] -- cgit v1.2.3 From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Oct 2017 17:04:02 +0100 Subject: Add relevance marks on binders. Kernel should be mostly correct, higher levels do random stuff at times. --- interp/constrintern.ml | 13 ++++++++----- interp/declare.ml | 2 +- interp/discharge.ml | 2 +- interp/impargs.ml | 5 +++-- interp/implicit_quantifiers.ml | 5 +++-- 5 files changed, 16 insertions(+), 11 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b4c570d444..5ede9d6a99 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -16,6 +16,7 @@ open Names open Nameops open Namegen open Constr +open Context open Libnames open Globnames open Impargs @@ -2183,7 +2184,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (add_name match_acc CAst.(make ?loc x)) (CAst.make ?loc x::var_acc) | _ -> let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in + Namegen.next_name_away_with_default_using_types "iV" cano_name.binder_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (Id.Set.add fresh forbidden_names) ((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc) end @@ -2432,9 +2433,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = in let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in match b with - None -> - let d = LocalAssum (na,t) in - let impls = + None -> + let r = Retyping.relevance_of_type env sigma t in + let d = LocalAssum (make_annot na r,t) in + let impls = if k == Implicit then let na = match na with Name n -> Some n | Anonymous -> None in (ExplByPos (n, na), (true, true, true)) :: impls @@ -2443,7 +2445,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = (push_rel d env, sigma, d::params, succ n, impls) | Some b -> let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in - let d = LocalDef (na, c, t) in + let r = Retyping.relevance_of_type env sigma t in + let d = LocalDef (make_annot na r, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) in sigma, ((env, par), impls) diff --git a/interp/declare.ml b/interp/declare.ml index 4371b15c82..08a6ac5f7b 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -370,7 +370,7 @@ let declare_projections univs mind = let mib = Environ.lookup_mind mind env in match mib.mind_record with | PrimRecord info -> - let iter_ind i (_, labs, _) = + let iter_ind i (_, labs, _, _) = let ind = (mind, i) in let projs = Inductiveops.compute_projections env ind in Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs diff --git a/interp/discharge.ml b/interp/discharge.ml index 524bf9a002..1efd13adb1 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -103,7 +103,7 @@ let process_inductive info modlist mib = let (params',inds') = abstract_inductive section_decls' nparamdecls inds in let record = match mib.mind_record with | PrimRecord info -> - Some (Some (Array.map pi1 info)) + Some (Some (Array.map (fun (x,_,_,_) -> x) info)) | FakeRecord -> Some None | NotRecord -> None in diff --git a/interp/impargs.ml b/interp/impargs.ml index 0f9bff7f1d..d83a0ce918 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -243,7 +243,7 @@ let compute_implicits_names_gen all env sigma t = let t = whd_all env sigma t in match kind sigma t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in + let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b | _ -> List.rev names in aux env Id.Set.empty [] t @@ -445,7 +445,8 @@ let compute_mib_implicits flags kn = (fun i mip -> (* No need to care about constraints here *) let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in - Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) + let r = Inductive.relevance_of_inductive env (kn,i) in + Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in let imps_one_inductive i mip = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4f3037b1fc..854651e7b7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -10,6 +10,7 @@ (*i*) open Names +open Context open Decl_kinds open CErrors open Util @@ -175,10 +176,10 @@ let combine_params avoid fn applied needed = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named -> + | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need -> + | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need -> aux (x :: ids) avoid app need | _, (Some cl, _ as d) :: need -> -- cgit v1.2.3