diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 13 | ||||
| -rw-r--r-- | engine/engine.mllib | 7 | ||||
| -rw-r--r-- | engine/evarutil.ml | 4 | ||||
| -rw-r--r-- | engine/evarutil.mli | 5 | ||||
| -rw-r--r-- | engine/evd.ml | 6 | ||||
| -rw-r--r-- | engine/evd.mli | 13 | ||||
| -rw-r--r-- | engine/geninterp.ml | 100 | ||||
| -rw-r--r-- | engine/geninterp.mli | 72 | ||||
| -rw-r--r-- | engine/nameops.ml | 216 | ||||
| -rw-r--r-- | engine/nameops.mli | 138 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 3 | ||||
| -rw-r--r-- | engine/uState.mli | 5 | ||||
| -rw-r--r-- | engine/universes.mli | 1 | ||||
| -rw-r--r-- | engine/univops.ml | 40 | ||||
| -rw-r--r-- | engine/univops.mli | 15 |
16 files changed, 446 insertions, 194 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bcfbc8081..afdceae06 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -9,7 +9,6 @@ open CErrors open Util open Names -open Term open Constr open Context open Evd @@ -55,7 +54,7 @@ struct type t = Sorts.t let make s = s let kind sigma = function - | Type u -> sort_of_univ (Evd.normalize_universe sigma u) + | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u) | s -> s let unsafe_to_sorts s = s end @@ -85,16 +84,16 @@ let rec whd_evar sigma c = | Some c -> whd_evar sigma c | None -> c end - | App (f, args) when Term.isEvar f -> + | App (f, args) when isEvar f -> (** Enforce smart constructor invariant on applications *) - let ev = Term.destEvar f in + let ev = destEvar f in begin match safe_evar_value sigma ev with | None -> c | Some f -> whd_evar sigma (mkApp (f, args)) end - | Cast (c0, k, t) when Term.isEvar c0 -> + | Cast (c0, k, t) when isEvar c0 -> (** Enforce smart constructor invariant on casts. *) - let ev = Term.destEvar c0 in + let ev = destEvar c0 in begin match safe_evar_value sigma ev with | None -> c | Some c -> whd_evar sigma (mkCast (c, k, t)) @@ -115,7 +114,7 @@ let rec to_constr sigma c = match Constr.kind c with | Some c -> to_constr sigma c | None -> Constr.map (fun c -> to_constr sigma c) c end -| Sort (Type u) -> +| Sort (Sorts.Type u) -> let u' = Evd.normalize_universe sigma u in if u' == u then c else mkSort (Sorts.sort_of_univ u') | Const (c', u) when not (Univ.Instance.is_empty u) -> diff --git a/engine/engine.mllib b/engine/engine.mllib index afc02d7f6..a3614f6c4 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,12 +1,13 @@ -Logic_monad Universes +Univops UState +Nameops Evd EConstr Namegen Termops -Proofview_monad Evarutil +Logic_monad +Proofview_monad Proofview Ftactic -Geninterp diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df4ef2ce7..14d07ccae 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -11,11 +11,11 @@ open Util open Names open Term open Constr -open Termops -open Namegen open Pre_env open Environ open Evd +open Termops +open Namegen module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 62288ced4..42f2d5f25 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -238,7 +238,8 @@ val subterm_source : existential_key -> Evar_kinds.t Loc.located -> val meta_counter_summary_name : string -(** Deprecater *) - +(** Deprecated *) type type_constraint = types option +[@@ocaml.deprecated "use the version in Evardefine"] type val_constraint = constr option +[@@ocaml.deprecated "use the version in Evardefine"] diff --git a/engine/evd.ml b/engine/evd.ml index 8d465384b..60bd6de2a 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -243,7 +243,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args + evar_instance_array (NamedDecl.get_id %> isVarId) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -707,10 +707,10 @@ let extract_all_conv_pbs evd = extract_conv_pbs evd (fun _ -> true) let loc_of_conv_pb evd (pbty,env,t1,t2) = - match kind (fst (Term.decompose_app t1)) with + match kind (fst (decompose_app t1)) with | Evar (evk1,_) -> fst (evar_source evk1 evd) | _ -> - match kind (fst (Term.decompose_app t2)) with + match kind (fst (decompose_app t2)) with | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None diff --git a/engine/evd.mli b/engine/evd.mli index af5373582..17fa15045 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -599,11 +599,16 @@ type open_constr = evar_map * constr (* Special case when before is empty *) type unsolvability_explanation = SeveralInstancesFound of int (** Failure explanation. *) +(** {5 Summary names} *) + +(* This stuff is internal and should not be used. Currently a hack in + the STM relies on it. *) +val evar_counter_summary_name : string + (** {5 Deprecated functions} *) +val create_evar_defs : evar_map -> evar_map +(* XXX: This is supposed to be deprecated by used by ssrmatching, what + should the replacement be? *) -val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) -(** {5 Summary names} *) - -val evar_counter_summary_name : string diff --git a/engine/geninterp.ml b/engine/geninterp.ml deleted file mode 100644 index 768ef3cfd..000000000 --- a/engine/geninterp.ml +++ /dev/null @@ -1,100 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Genarg - -module TacStore = Store.Make () - -(** Dynamic toplevel values *) - -module ValT = Dyn.Make () - -module Val = -struct - - type 'a typ = 'a ValT.tag - - type _ tag = - | Base : 'a typ -> 'a tag - | List : 'a tag -> 'a list tag - | Opt : 'a tag -> 'a option tag - | Pair : 'a tag * 'b tag -> ('a * 'b) tag - - type t = Dyn : 'a typ * 'a -> t - - let eq = ValT.eq - let repr = ValT.repr - let create = ValT.create - - let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t) - - let typ_list = ValT.create "list" - let typ_opt = ValT.create "option" - let typ_pair = ValT.create "pair" - - let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with - | Base t -> Dyn (t, x) - | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x) - | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x) - | Pair (tag1, tag2) -> - Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x))) - -end - -module ValTMap = ValT.Map - -module ValReprObj = -struct - type ('raw, 'glb, 'top) obj = 'top Val.tag - let name = "valrepr" - let default _ = None -end - -module ValRepr = Register(ValReprObj) - -let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function -| ListArg t -> Val.List (val_tag t) -| OptArg t -> Val.Opt (val_tag t) -| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) -| ExtraArg s -> ValRepr.obj (ExtraArg s) - -let val_tag = function Topwit t -> val_tag t - -let register_val0 wit tag = - let tag = match tag with - | None -> - let name = match wit with - | ExtraArg s -> ArgT.repr s - | _ -> assert false - in - Val.Base (Val.create name) - | Some tag -> tag - in - ValRepr.register0 wit tag - -(** Interpretation functions *) - -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } - -type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t - -module InterpObj = -struct - type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun - let name = "interp" - let default _ = None -end - -module Interp = Register(InterpObj) - -let interp = Interp.obj - -let register_interp0 = Interp.register0 diff --git a/engine/geninterp.mli b/engine/geninterp.mli deleted file mode 100644 index ae0b26e59..000000000 --- a/engine/geninterp.mli +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Interpretation functions for generic arguments and interpreted Ltac - values. *) - -open Names -open Genarg - -(** {6 Dynamic toplevel values} *) - -module Val : -sig - type 'a typ - - val create : string -> 'a typ - - type _ tag = - | Base : 'a typ -> 'a tag - | List : 'a tag -> 'a list tag - | Opt : 'a tag -> 'a option tag - | Pair : 'a tag * 'b tag -> ('a * 'b) tag - - type t = Dyn : 'a typ * 'a -> t - - val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option - val repr : 'a typ -> string - val pr : 'a typ -> Pp.t - - val typ_list : t list typ - val typ_opt : t option typ - val typ_pair : (t * t) typ - - val inject : 'a tag -> 'a -> t - -end - -module ValTMap (M : Dyn.TParam) : - Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ - -(** Dynamic types for toplevel values. While the generic types permit to relate - objects at various levels of interpretation, toplevel values are wearing - their own type regardless of where they came from. This allows to use the - same runtime representation for several generic types. *) - -val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag -(** Retrieve the dynamic type associated to a toplevel genarg. *) - -val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit -(** Register the representation of a generic argument. If no tag is given as - argument, a new fresh tag with the same name as the argument is associated - to the generic type. *) - -(** {6 Interpretation functions} *) - -module TacStore : Store.S - -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } - -type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t - -val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun - -val register_interp0 : - ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit diff --git a/engine/nameops.ml b/engine/nameops.ml new file mode 100644 index 000000000..5105d7bec --- /dev/null +++ b/engine/nameops.ml @@ -0,0 +1,216 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names + +(* Identifiers *) + +let pr_id id = Id.print id + +(* Utilities *) + +let code_of_0 = Char.code '0' +let code_of_9 = Char.code '9' + +let cut_ident skip_quote s = + let s = Id.to_string s in + let slen = String.length s in + (* [n'] is the position of the first non nullary digit *) + let rec numpart n n' = + if Int.equal n 0 then + (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *) + slen + else + let c = Char.code (String.get s (n-1)) in + if Int.equal c code_of_0 && not (Int.equal n slen) then + numpart (n-1) n' + else if code_of_0 <= c && c <= code_of_9 then + numpart (n-1) (n-1) + else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then + numpart (n-1) (n-1) + else + n' + in + numpart slen slen + +let repr_ident s = + let numstart = cut_ident false s in + let s = Id.to_string s in + let slen = String.length s in + if Int.equal numstart slen then + (s, None) + else + (String.sub s 0 numstart, + Some (int_of_string (String.sub s numstart (slen - numstart)))) + +let make_ident sa = function + | Some n -> + let c = Char.code (String.get sa (String.length sa -1)) in + let s = + if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) + else sa ^ "_" ^ (string_of_int n) in + Id.of_string s + | None -> Id.of_string sa + +let root_of_id id = + let suffixstart = cut_ident true id in + Id.of_string (String.sub (Id.to_string id) 0 suffixstart) + +(* Return the same identifier as the original one but whose {i subscript} is incremented. + If the original identifier does not have a suffix, [0] is appended to it. + + Example mappings: + + [bar] ↦ [bar0] + [bar0] ↦ [bar1] + [bar00] ↦ [bar01] + [bar1] ↦ [bar2] + [bar01] ↦ [bar01] + [bar9] ↦ [bar10] + [bar09] ↦ [bar10] + [bar99] ↦ [bar100] +*) +let increment_subscript id = + let id = Id.to_string id in + let len = String.length id in + let rec add carrypos = + let c = id.[carrypos] in + if is_digit c then + if Int.equal (Char.code c) (Char.code '9') then begin + assert (carrypos>0); + add (carrypos-1) + end + else begin + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); + newid + end + else begin + let newid = Bytes.of_string (id^"0") in + if carrypos < len-1 then begin + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' + end; + newid + end + in Id.of_bytes (add (len-1)) + +let has_subscript id = + let id = Id.to_string id in + is_digit (id.[String.length id - 1]) + +let forget_subscript id = + let numstart = cut_ident false id in + let newid = Bytes.make (numstart+1) '0' in + String.blit (Id.to_string id) 0 newid 0 numstart; + (Id.of_bytes newid) + +let add_suffix id s = Id.of_string (Id.to_string id ^ s) +let add_prefix s id = Id.of_string (s ^ Id.to_string id) + +let atompart_of_id id = fst (repr_ident id) + +(* Names *) + +module type ExtName = +sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a + val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a + val iter : (Id.t -> unit) -> t -> unit + val map : (Id.t -> Id.t) -> t -> t + val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t + val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a + val get_id : t -> Id.t + val pick : t -> t -> t + val cons : t -> Id.t list -> Id.t list + val to_option : Name.t -> Id.t option + +end + +module Name : ExtName = +struct + + include Names.Name + + exception IsAnonymous + + let fold_left f a = function + | Name id -> f a id + | Anonymous -> a + + let fold_right f na a = + match na with + | Name id -> f id a + | Anonymous -> a + + let iter f na = fold_right (fun x () -> f x) na () + + let map f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + + let fold_left_map f a = function + | Name id -> let (a, id) = f a id in (a, Name id) + | Anonymous -> a, Anonymous + + let fold_right_map f na a = match na with + | Name id -> let (id, a) = f id a in (Name id, a) + | Anonymous -> Anonymous, a + + let get_id = function + | Name id -> id + | Anonymous -> raise IsAnonymous + + let pick na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 + + let cons na l = + match na with + | Anonymous -> l + | Name id -> id::l + + let to_option = function + | Anonymous -> None + | Name id -> Some id + +end + +open Name + +(* Compatibility *) +let out_name = get_id +let name_fold = fold_right +let name_iter = iter +let name_app = map +let name_fold_map = fold_left_map +let name_cons = cons +let name_max = pick +let pr_name = print + +let pr_lab l = Label.print l + +(* Metavariables *) +let pr_meta = Pp.int +let string_of_meta = string_of_int + +(* Deprecated *) +open Libnames +let default_library = default_library +let coq_string = coq_string +let coq_root = coq_root +let default_root_prefix = default_root_prefix + diff --git a/engine/nameops.mli b/engine/nameops.mli new file mode 100644 index 000000000..0fec8a925 --- /dev/null +++ b/engine/nameops.mli @@ -0,0 +1,138 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names + +(** Identifiers and names *) + +val make_ident : string -> int option -> Id.t +val repr_ident : Id.t -> string * int option + +val atompart_of_id : Id.t -> string (** remove trailing digits *) +val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) + +val add_suffix : Id.t -> string -> Id.t +val add_prefix : string -> Id.t -> Id.t + +(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *) + +val has_subscript : Id.t -> bool + +val increment_subscript : Id.t -> Id.t +(** Return the same identifier as the original one but whose {i subscript} is incremented. + If the original identifier does not have a suffix, [0] is appended to it. + + Example mappings: + + [bar] ↦ [bar0] + + [bar0] ↦ [bar1] + + [bar00] ↦ [bar01] + + [bar1] ↦ [bar2] + + [bar01] ↦ [bar01] + + [bar9] ↦ [bar10] + + [bar09] ↦ [bar10] + + [bar99] ↦ [bar100] +*) + +val forget_subscript : Id.t -> Id.t + +module Name : sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a + (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *) + + val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *) + + val iter : (Id.t -> unit) -> Name.t -> unit + (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *) + + val map : (Id.t -> Id.t) -> Name.t -> t + (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *) + + val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t + (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')]. + It is [a,Anonymous] otherwise. *) + + val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a + (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')]. + It is [Anonymous,a] otherwise. *) + + val get_id : Name.t -> Id.t + (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *) + + val pick : Name.t -> Name.t -> Name.t + (** [pick na na'] returns [Anonymous] if both names are [Anonymous]. + Pick one of [na] or [na'] otherwise. *) + + val cons : Name.t -> Id.t list -> Id.t list + (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *) + + val to_option : Name.t -> Id.t option + (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *) + +end + +(** Metavariables *) +val pr_meta : Constr.metavariable -> Pp.t +val string_of_meta : Constr.metavariable -> string + +val out_name : Name.t -> Id.t +[@@ocaml.deprecated "Same as [Name.get_id]"] + +val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a +[@@ocaml.deprecated "Same as [Name.fold_right]"] + +val name_iter : (Id.t -> unit) -> Name.t -> unit +[@@ocaml.deprecated "Same as [Name.iter]"] + +val name_app : (Id.t -> Id.t) -> Name.t -> Name.t +[@@ocaml.deprecated "Same as [Name.map]"] + +val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t +[@@ocaml.deprecated "Same as [Name.fold_left_map]"] + +val name_max : Name.t -> Name.t -> Name.t +[@@ocaml.deprecated "Same as [Name.pick]"] + +val name_cons : Name.t -> Id.t list -> Id.t list +[@@ocaml.deprecated "Same as [Name.cons]"] + +val pr_name : Name.t -> Pp.t +[@@ocaml.deprecated "Same as [Name.print]"] + +val pr_id : Id.t -> Pp.t +[@@ocaml.deprecated "Same as [Names.Id.print]"] + +val pr_lab : Label.t -> Pp.t +[@@ocaml.deprecated "Same as [Names.Label.print]"] + +(** Deprecated stuff to libnames *) +val default_library : DirPath.t +[@@ocaml.deprecated "Same as [Libnames.default_library]"] + +val coq_root : module_ident (** "Coq" *) +[@@ocaml.deprecated "Same as [Libnames.coq_root]"] + +val coq_string : string (** "Coq" *) +[@@ocaml.deprecated "Same as [Libnames.coq_string]"] + +val default_root_prefix : DirPath.t +[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"] + diff --git a/engine/proofview.ml b/engine/proofview.ml index 598358c47..3b945c87f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1200,7 +1200,7 @@ module V82 = struct { Evd.it = comb ; sigma = solution } let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in + let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } let top_evars initial = diff --git a/engine/uState.ml b/engine/uState.ml index dfea25dd0..01a479821 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -437,6 +437,9 @@ let make_flexible_variable ctx ~algebraic u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} +let make_flexible_nonalgebraic ctx = + {ctx with uctx_univ_algebraic = Univ.LSet.empty} + let is_sort_variable uctx s = match s with | Sorts.Type u -> diff --git a/engine/uState.mli b/engine/uState.mli index b31e94b28..1c906fcb2 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -104,6 +104,11 @@ val add_global_univ : t -> Univ.Level.t -> t universe. Otherwise the variable is just made flexible. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +(** 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). *) +val make_flexible_nonalgebraic : t -> t + val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t diff --git a/engine/universes.mli b/engine/universes.mli index 24613c4b9..a960099ed 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -169,6 +169,7 @@ val constr_of_global : Globnames.global_reference -> constr (** ** DEPRECATED ** synonym of [constr_of_global] *) val constr_of_reference : Globnames.global_reference -> constr +[@@ocaml.deprecated "synonym of [constr_of_global]"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the diff --git a/engine/univops.ml b/engine/univops.ml new file mode 100644 index 000000000..d498b2e0d --- /dev/null +++ b/engine/univops.ml @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Univ +open Constr + +let universes_of_constr c = + let rec aux s c = + match kind c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = Sorts.univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> Constr.fold aux s c + in aux LSet.empty c + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/engine/univops.mli b/engine/univops.mli new file mode 100644 index 000000000..9af568bcb --- /dev/null +++ b/engine/univops.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Constr +open Univ + +(** Shrink a universe context to a restricted set of variables *) + +val universes_of_constr : constr -> LSet.t +val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t |