diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 8 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 6 | ||||
| -rw-r--r-- | engine/nameops.ml | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 95 | ||||
| -rw-r--r-- | engine/termops.mli | 5 | ||||
| -rw-r--r-- | engine/uState.ml | 42 | ||||
| -rw-r--r-- | engine/uState.mli | 8 | ||||
| -rw-r--r-- | engine/univNames.ml | 64 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
11 files changed, 98 insertions, 141 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3385b78958..cfc4bea85f 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -99,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false + +let rec isType sigma c = match kind sigma c with + | Sort s -> (match ESorts.kind sigma s with + | Sorts.Type _ -> true + | _ -> false ) + | Cast (c,_,_) -> isType sigma c + | _ -> false + let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false let isRelN sigma n c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 1edc0ee12b..6532e08e9d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -157,6 +157,8 @@ val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool +val isType : Evd.evar_map -> constr -> bool + type arity = rel_context * ESorts.t val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool diff --git a/engine/evd.ml b/engine/evd.ml index 3a77a2b440..6345046431 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -483,6 +483,8 @@ let is_typeclass_evar evd evk = let flags = evd.evar_flags in Evar.Set.mem evk flags.typeclass_evars +let get_obligation_evars evd = evd.evar_flags.obligation_evars + let set_obligation_evar evd evk = let flags = evd.evar_flags in let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in @@ -889,6 +891,9 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } +let make_nonalgebraic_variable evd u = + { evd with universes = UState.make_nonalgebraic_variable evd.universes u } + (****************************************) (* Operations on constants *) (****************************************) diff --git a/engine/evd.mli b/engine/evd.mli index b0e3c2b869..0a8d1f3287 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -262,6 +262,9 @@ val get_typeclass_evars : evar_map -> Evar.Set.t val is_typeclass_evar : evar_map -> Evar.t -> bool (** Is the evar declared resolvable for typeclass resolution *) +val get_obligation_evars : evar_map -> Evar.Set.t +(** The set of obligation evars *) + val set_obligation_evar : evar_map -> Evar.t -> evar_map (** Declare an evar as an obligation *) @@ -558,6 +561,9 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map (** See [UState.make_flexible_variable] *) +val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map +(** See [UState.make_nonalgebraic_variable]. *) + val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) diff --git a/engine/nameops.ml b/engine/nameops.ml index 735a59fe51..15e201347c 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -69,7 +69,7 @@ let root_of_id id = [bar0] ↦ [bar1] [bar00] ↦ [bar01] [bar1] ↦ [bar2] - [bar01] ↦ [bar01] + [bar01] ↦ [bar02] [bar9] ↦ [bar10] [bar09] ↦ [bar10] [bar99] ↦ [bar100] diff --git a/engine/termops.ml b/engine/termops.ml index f720e5195d..ada6311067 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -24,84 +24,13 @@ module CompactedDecl = Context.Compacted.Declaration module Internal = struct -(* Sorts and sort family *) - -let print_sort = function - | Set -> (str "Set") - | Prop -> (str "Prop") - | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") - -let pr_sort_family = function - | InSet -> (str "Set") - | InProp -> (str "Prop") - | InType -> (str "Type") - -let pr_con sp = str(Constant.to_string sp) - -let pr_fix pr_constr ((t,i),(lna,tl,bl)) = - let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in - hov 1 - (str"fix " ++ int i ++ spc() ++ str"{" ++ - v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ - cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ - str"}") - -let pr_puniverses p u = - if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - -(* Minimalistic constr printer, typically for debugging *) - -let rec pr_constr c = match kind c with - | Rel n -> str "#"++int n - | Meta n -> str "Meta(" ++ int n ++ str ")" - | Var id -> Id.print id - | Sort s -> print_sort s - | Cast (c,_, t) -> hov 1 - (str"(" ++ pr_constr c ++ cut() ++ - str":" ++ pr_constr t ++ str")") - | Prod (Name(id),t,c) -> hov 1 - (str"forall " ++ Id.print id ++ str":" ++ pr_constr t ++ str"," ++ - spc() ++ pr_constr c) - | Prod (Anonymous,t,c) -> hov 0 - (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ - pr_constr c ++ str")") - | Lambda (na,t,c) -> hov 1 - (str"fun " ++ Name.print na ++ str":" ++ - pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) - | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++ - str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ - pr_constr c) - | App (c,l) -> hov 1 - (str"(" ++ pr_constr c ++ spc() ++ - prlist_with_sep spc pr_constr (Array.to_list l) ++ str")") - | Evar (e,l) -> hov 1 - (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ - prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") - | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")" - | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")" - | Construct (((sp,i),j),u) -> - str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" - | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")" - | Case (ci,p,c,bl) -> v 0 - (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ - pr_constr c ++ str"of") ++ cut() ++ - prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++ - cut() ++ str"end") - | Fix f -> pr_fix pr_constr f - | CoFix(i,(lna,tl,bl)) -> - let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in - hov 1 - (str"cofix " ++ int i ++ spc() ++ str"{" ++ - v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - Name.print na ++ str":" ++ pr_constr ty ++ - cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ - str"}") - -let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c) -let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c) +let pr_sort_family = Sorts.pr_sort_family +[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] +let pr_fix = Constr.debug_print_fix +[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] + +let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c) +let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c) let term_printer = ref debug_print_constr_env let print_constr_env env sigma t = !term_printer (env:env) sigma (t:Evd.econstr) @@ -366,12 +295,18 @@ let pr_evar_map_gen with_univs pr_evars env sigma = else str "TYPECLASSES:" ++ brk (0, 1) ++ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () + and obligations = + let evars = Evd.get_obligation_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "OBLIGATIONS:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma in - evs ++ svs ++ cstrs ++ typeclasses ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas let pr_evar_list env sigma l = let open Evd in @@ -1173,7 +1108,7 @@ let isGlobalRef sigma c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let is_template_polymorphic env sigma f = +let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false diff --git a/engine/termops.mli b/engine/termops.mli index 1054fbbc5e..6c3d4fa612 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -17,9 +17,10 @@ open Environ open EConstr (** printers *) -val print_sort : Sorts.t -> Pp.t val pr_sort_family : Sorts.family -> Pp.t +[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t +[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] (** about contexts *) val push_rel_assum : Name.t * types -> env -> env @@ -282,7 +283,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool +val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool diff --git a/engine/uState.ml b/engine/uState.ml index aa7ec63a6f..5747ae2ad4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local let const_univ_entry ~poly uctx = let open Entries in - if poly then Polymorphic_const_entry (context uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = context uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Polymorphic_const_entry (nas, uctx) else Monomorphic_const_entry (context_set uctx) (* does not support cumulativity since you need more info *) let ind_univ_entry ~poly uctx = let open Entries in - if poly then Polymorphic_ind_entry (context uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = context uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Polymorphic_ind_entry (nas, uctx) else Monomorphic_ind_entry (context_set uctx) let of_context_set ctx = { empty with uctx_local = ctx } @@ -140,7 +148,25 @@ let of_binders b = in { ctx with uctx_names = b, rmap } -let universe_binders ctx = fst ctx.uctx_names +let invent_name (named,cnt) u = + let rec aux i = + let na = Id.of_string ("u"^(string_of_int i)) in + if Id.Map.mem na named then aux (i+1) + else Id.Map.add na u named, i+1 + in + aux cnt + +let universe_binders ctx = + let open Univ in + let named, rev = ctx.uctx_names in + let named, _ = LSet.fold (fun u named -> + match LMap.find u rev with + | exception Not_found -> (* not sure if possible *) invent_name named u + | { uname = None } -> invent_name named u + | { uname = Some _ } -> named) + (ContextSet.levels ctx.uctx_local) (named, 0) + in + named let instantiate_variable l b v = try v := Univ.LMap.set l (Some b) !v @@ -394,8 +420,11 @@ let check_univ_decl ~poly uctx decl = let ctx = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in - if poly - then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = universe_context ~names ~extensible uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Entries.Polymorphic_const_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in Entries.Monomorphic_const_entry uctx.uctx_local @@ -566,6 +595,9 @@ let make_flexible_variable ctx ~algebraic u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} +let make_nonalgebraic_variable ctx u = + { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } + let make_flexible_nonalgebraic ctx = {ctx with uctx_univ_algebraic = Univ.LSet.empty} diff --git a/engine/uState.mli b/engine/uState.mli index 8053a7bf83..ad0cd5c1bb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -126,9 +126,15 @@ val add_global_univ : t -> Univ.Level.t -> t Turn the variable [l] flexible, and algebraic if [algebraic] is true and [l] can be. That is if there are no strict upper constraints on [l] and and it does not appear in the instance of any non-algebraic - universe. Otherwise the variable is just made flexible. *) + universe. Otherwise the variable is just made flexible. + + If [l] is already algebraic it will remain so even with [algebraic:false]. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +val make_nonalgebraic_variable : t -> Univ.Level.t -> t +(** Make the level non algebraic. Undefined behaviour on + already-defined algebraics. *) + (** Turn all undefined flexible algebraic variables into simply flexible ones. Can be used in case the variables might appear in universe instances (typically for polymorphic program obligations). *) diff --git a/engine/univNames.ml b/engine/univNames.ml index a71f9c5736..ad91d31f87 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -36,69 +36,28 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" - -let universe_binders_of_global ref : Id.t list = - try - let l = GlobRef.Map.find ref !universe_binders_table in l - with Not_found -> [] - -let cache_ubinder (_,(ref,l)) = - universe_binders_table := GlobRef.Map.add ref l !universe_binders_table - -let subst_ubinder (subst,(ref,l as orig)) = - let ref' = fst (Globnames.subst_global subst ref) in - if ref == ref' then orig else ref', l +let universe_binders_of_global ref : Name.t array = + try AUContext.names (Environ.universes_of_global (Global.env ()) ref) + with Not_found -> [||] let name_universe lvl = (** Best-effort naming from the string representation of the level. This is completely hackish and should be solved in upper layers instead. *) Id.of_string_soft (Level.to_string lvl) -let discharge_ubinder (_,(ref,l)) = - (** Expand polymorphic binders with the section context *) - let info = Lib.section_segment_of_reference ref in - let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in - let map lvl = match Level.name lvl with - | None -> (* Having Prop/Set/Var as section universes makes no sense *) - assert false - | Some na -> - try - let qid = Nametab.shortest_qualid_of_universe na in - snd (Libnames.repr_qualid qid) - with Not_found -> name_universe lvl - in - let l = List.map map sec_inst @ l in - Some (ref, l) - -let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj = - let open Libobject in - declare_object { (default_object "universe binder") with - cache_function = cache_ubinder; - load_function = (fun _ x -> cache_ubinder x); - classify_function = (fun x -> Substitute x); - subst_function = subst_ubinder; - discharge_function = discharge_ubinder; - rebuild_function = (fun x -> x); } - -let register_universe_binders ref ubinders = - (** TODO: change the API to register a [Name.t list] instead. This is the last - part of the code that depends on the internal representation of names in - abstract contexts, but removing it requires quite a rework of the - callers. *) - let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in +let compute_instance_binders inst ubinders = let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in let map lvl = - try LMap.find lvl revmap - with Not_found -> name_universe lvl + try Name (LMap.find lvl revmap) + with Not_found -> Name (name_universe lvl) in - let ubinders = Array.map_to_list map (Instance.to_array univs) in - if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders)) + Array.map map (Instance.to_array inst) type univ_name_list = Names.lname list let universe_binders_with_opt_names ref names = let orig = universe_binders_of_global ref in + let orig = Array.to_list orig in let udecl = match names with | None -> orig | Some udecl -> @@ -106,11 +65,14 @@ let universe_binders_with_opt_names ref names = List.map2 (fun orig {CAst.v = na} -> match na with | Anonymous -> orig - | Name id -> id) orig udecl + | Name id -> Name id) orig udecl with Invalid_argument _ -> let len = List.length orig in CErrors.user_err ~hdr:"universe_binders_with_opt_names" Pp.(str "Universe instance should have length " ++ int len) in - let fold i acc na = Names.Id.Map.add na (Level.var i) acc in + let fold i acc na = match na with + | Name id -> Names.Id.Map.add id (Level.var i) acc + | Anonymous -> acc + in List.fold_left_i fold 0 empty_binders udecl diff --git a/engine/univNames.mli b/engine/univNames.mli index bd4062ade4..dc669f45d6 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders -val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit +val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array type univ_name_list = Names.lname list |