diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/engine.mllib | 3 | ||||
| -rw-r--r-- | engine/evarutil.ml | 48 | ||||
| -rw-r--r-- | engine/evd.ml | 59 | ||||
| -rw-r--r-- | engine/evd.mli | 1 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 2 | ||||
| -rw-r--r-- | engine/namegen.ml | 60 | ||||
| -rw-r--r-- | engine/namegen.mli | 17 | ||||
| -rw-r--r-- | engine/proofview.ml | 45 | ||||
| -rw-r--r-- | engine/proofview.mli | 1 | ||||
| -rw-r--r-- | engine/termops.ml | 53 | ||||
| -rw-r--r-- | engine/termops.mli | 10 | ||||
| -rw-r--r-- | engine/uState.ml | 8 | ||||
| -rw-r--r-- | engine/universes.ml | 1130 | ||||
| -rw-r--r-- | engine/universes.mli | 231 |
14 files changed, 1552 insertions, 116 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index 9ce5af8195..53cbbd73ef 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,9 +1,10 @@ Logic_monad -Termops Namegen +Universes UState Evd Sigma +Termops Proofview_monad Evarutil Proofview diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df170c8ddc..13444cb379 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -18,6 +18,9 @@ open Environ open Evd open Sigma.Notations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let safe_evar_info sigma evk = try Some (Evd.find sigma evk) with Not_found -> None @@ -167,13 +170,11 @@ let is_ground_term evd t = not (has_undefined_evars evd t) let is_ground_env evd env = - let open Context.Rel.Declaration in let is_ground_rel_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b + | RelDecl.LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in - let open Context.Named.Declaration in let is_ground_named_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b + | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in List.for_all is_ground_rel_decl (rel_context env) && List.for_all is_ground_named_decl (named_context env) @@ -255,11 +256,10 @@ let non_instantiated sigma = (************************) let make_pure_subst evi args = - let open Context.Named.Declaration in snd (List.fold_right (fun decl (args,l) -> match args with - | a::rest -> (rest, (get_id decl, a)::l) + | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) @@ -331,21 +331,18 @@ let push_var id (n, s) = (succ n, s) let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = - let open Context.Named.Declaration in let replace_var_named_declaration id0 id decl = - let id' = get_id decl in + let id' = NamedDecl.get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - decl |> set_id id' |> map_constr (replace_vars vsubst) + decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst) in let extract_if_neq id = function | Anonymous -> None | Name id' when id_ord id id' = 0 -> None | Name id' -> Some id' in - let open Context.Rel.Declaration in - let (na, c, t) = to_tuple decl in - let open Context.Named.Declaration in + let na = RelDecl.get_name decl in let id = (* ppedrot: we want to infer nicer names for the refine tactic, but keeping at the same time backward compatibility in other code @@ -356,7 +353,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = else (** id_of_name_using_hdchar only depends on the rel context which is empty here *) - next_ident_away (id_of_name_using_hdchar empty_env t na) avoid + next_ident_away (id_of_name_using_hdchar empty_env (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with | Some id0 when not (is_section_variable id0) -> @@ -366,10 +363,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = context. Unless [id] is a section variable. *) let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in let vsubst = (id0,mkVar id)::vsubst in - let d = match c with - | None -> LocalAssum (id0, subst2 subst vsubst t) - | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) - in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> NamedDecl.map_constr (subst2 subst vsubst) in let nc = List.map (replace_var_named_declaration id0 id) nc in (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) | _ -> @@ -377,10 +371,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = incorrect. We revert to a less robust behaviour where the new binder has name [id]. Which amounts to the same behaviour than when [id=id0]. *) - let d = match c with - | None -> LocalAssum (id, subst2 subst vsubst t) - | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) - in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> NamedDecl.map_constr (subst2 subst vsubst) in (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) let push_rel_context_to_named_context env typ = @@ -560,8 +551,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let () = Id.Map.iter check ri in (* No dependency at all, we can keep this ev's context hyp *) (ri, true::filter) - with Depends id -> let open Context.Named.Declaration in - (Id.Map.add (get_id h) id ri, false::filter)) + with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)) ctxt (Array.to_list l) (Id.Map.empty,[]) in (* Check if some rid to clear in the context of ev has dependencies in the type of ev and adjust the source of the dependency *) @@ -600,10 +590,9 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in let nhyps = - let open Context.Named.Declaration in let check_context decl = - let err = OccurHypInSimpleClause (Some (get_id decl)) in - map_constr (check_and_clear_in_constr env evdref err ids global) decl + let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in + NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids global) decl in let check_value vk = match force_lazy_val vk with | None -> vk @@ -642,8 +631,8 @@ let process_dependent_evar q acc evm is_dependent e = hypotheses), they are all dependent. *) queue_term q true evi.evar_concl; List.iter begin fun decl -> - let open Context.Named.Declaration in - queue_term q true (get_type decl); + let open NamedDecl in + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b @@ -719,9 +708,8 @@ let undefined_evars_of_term evd t = evrec Evar.Set.empty t let undefined_evars_of_named_context evd nc = - let open Context.Named.Declaration in Context.Named.fold_outside - (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) + (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) nc ~init:Evar.Set.empty diff --git a/engine/evd.ml b/engine/evd.ml index c2f848291b..62d3963954 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -13,11 +13,13 @@ open Names open Nameops open Term open Vars -open Termops open Environ open Globnames open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (** Generic filters *) module Filter : sig @@ -226,7 +228,7 @@ let evar_instance_array test_id info args = if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (get_id d, c) :: instrec filter ctxt (succ i) + else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in @@ -235,7 +237,7 @@ let evar_instance_array test_id info args = let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (get_id d, c) + if test_id d c then None else Some (NamedDecl.get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -243,7 +245,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 (isVarId % get_id) 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 @@ -284,7 +286,7 @@ let metavars_of c = let rec collrec acc c = match kind_of_term c with | Meta mv -> Int.Set.add mv acc - | _ -> fold_constr collrec acc c + | _ -> Term.fold_constr collrec acc c in collrec Int.Set.empty c @@ -383,8 +385,7 @@ let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = | Misctypes.IntroAnonymous -> None | Misctypes.IntroIdentifier id -> if Idmap.mem id idtoev then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + user_err (str "Already an existential evar of name " ++ pr_id id); Some id | Misctypes.IntroFresh id -> let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in @@ -685,7 +686,7 @@ let restrict evk filter ?candidates evd = | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (mkVar % get_id) ctxt in + let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; @@ -735,23 +736,22 @@ let evar_list c = let rec evrec acc c = match kind_of_term c with | Evar (evk, _ as ev) -> ev :: acc - | _ -> fold_constr evrec acc c in + | _ -> Term.fold_constr evrec acc c in evrec [] c let evars_of_term c = let rec evrec acc c = match kind_of_term c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> fold_constr evrec acc c + | _ -> Term.fold_constr evrec acc c in evrec Evar.Set.empty c let evars_of_named_context nc = - List.fold_right (fun decl s -> - Option.fold_left (fun s t -> - Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) - nc Evar.Set.empty + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) + nc + ~init:Evar.Set.empty let evars_of_filtered_evar_info evi = Evar.Set.union (evars_of_term evi.evar_concl) @@ -1273,7 +1273,9 @@ let protect f x = try f x with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) -let print_constr a = protect print_constr a +let (f_print_constr, print_constr_hook) = Hook.make () + +let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a let pr_meta_map mmap = let pr_name = function @@ -1294,13 +1296,13 @@ let pr_meta_map mmap = prlist pr_meta_binding (metamap_to_list mmap) let pr_decl (decl,ok) = - let id = get_id decl in - match get_value decl with - | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ - print_constr c ++ str (if ok then ")" else "}") + match decl with + | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") + | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function + | Evar_kinds.NamedHole id -> pr_id id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> @@ -1409,12 +1411,11 @@ let pr_evar_universe_context ctx = h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) let print_env_short env = - let pr_body n = function - | None -> pr_name n - | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in - let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in - let pr_rel_decl decl = let open Context.Rel.Declaration in - pr_body (get_name decl) (get_value decl) in + let pr_rel_decl = function + | RelDecl.LocalAssum (n,_) -> pr_name n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + in + let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ @@ -1433,11 +1434,11 @@ let pr_evar_constraints pbs = Namegen.make_all_name_different env in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env t1 ++ spc () ++ + Hook.get f_print_constr env t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr_env env t2 + spc () ++ Hook.get f_print_constr env t2 in prlist_with_sep fnl pr_evconstr pbs diff --git a/engine/evd.mli b/engine/evd.mli index 86887f3dcc..993ed300bc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -618,6 +618,7 @@ val pr_evar_suggested_name : existential_key -> evar_map -> Id.t (** {5 Debug pretty-printers} *) +val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 17ff898b0f..6e821ea5aa 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -34,7 +34,7 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") + | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e | _ -> Pervasives.raise CErrors.Unhandled diff --git a/engine/namegen.ml b/engine/namegen.ml index 84eb986845..e56ec2877c 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,9 +21,10 @@ open Nameops open Libnames open Globnames open Environ -open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (**********************************************************************) (* Conventional names *) @@ -76,6 +77,10 @@ let is_constructor id = with Not_found -> false +let is_section_variable id = + try let _ = Global.lookup_named id in true + with Not_found -> false + (**********************************************************************) (* Generating "intuitive" names from its type *) @@ -114,9 +119,9 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env |> to_tuple with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) + try match Environ.lookup_rel (n-k) env with + | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id + | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> let id = match lna.(i) with Name id -> id | _ -> assert false in @@ -168,7 +173,7 @@ let it_mkLambda_or_LetIn_name env b hyps = (* Looks for next "good" name by lifting subscript *) let next_ident_away_from id bad = - let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in + let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id (* Restart subscript from x0 if name starts with xN, or x00 if name @@ -180,10 +185,6 @@ let restart_subscript id = *** make_ident id (Some 0) *** but compatibility would be lost... *) forget_subscript id -let rec to_avoid id = function -| [] -> false -| id' :: avoid -> Id.equal id id' || to_avoid id avoid - let visible_ids (nenv, c) = let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in let rec visible_ids n c = match kind_of_term c with @@ -205,8 +206,8 @@ let visible_ids (nenv, c) = if p > n && not (Int.Set.mem p vseen) then let vseen = Int.Set.add p vseen in let name = - try Some (lookup_name_of_rel (p - n) nenv) - with Not_found -> + try Some (List.nth nenv (p - n - 1)) + with Invalid_argument _ | Failure _ -> (* Unbound index: may happen in debug and actually also while computing temporary implicit arguments of an inductive type *) @@ -230,8 +231,8 @@ let visible_ids (nenv, c) = let next_name_away_in_cases_pattern env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in let visible = visible_ids env_t in - let bad id = to_avoid id avoid || is_constructor id - || Id.Set.mem id visible in + let bad id = Id.List.mem id avoid || is_constructor id + || Id.Set.mem id visible in next_ident_away_from id bad (* 2- Looks for a fresh name for introduction in goal *) @@ -244,8 +245,8 @@ let next_name_away_in_cases_pattern env_t na avoid = name is taken by finding a free subscript starting from 0 *) let next_ident_away_in_goal id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in + let id = if Id.List.mem id avoid then restart_subscript id else id in + let bad id = Id.List.mem id avoid || (is_global id && not (is_section_variable id)) in next_ident_away_from id bad let next_name_away_in_goal na avoid = @@ -262,16 +263,16 @@ let next_name_away_in_goal na avoid = beyond the current subscript *) let next_global_ident_away id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || is_global id in + let id = if Id.List.mem id avoid then restart_subscript id else id in + let bad id = Id.List.mem id avoid || is_global id in next_ident_away_from id bad (* 4- Looks for next fresh name outside a list; if name already used, looks for same name with lower available subscript *) let next_ident_away id avoid = - if to_avoid id avoid then - next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid) + if Id.List.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -292,15 +293,18 @@ let next_name_away_with_default_using_types default na avoid t = let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env = - let avoid = ref (ids_of_named_context (named_context env)) in - process_rel_context + (** FIXME: this is inefficient, but only used in printing *) + let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in + let sign = named_context_val env in + let rels = rel_context env in + let env0 = reset_with_named_context sign env in + Context.Rel.fold_outside (fun decl newenv -> - let (na,_,t) = to_tuple decl in - let na = named_hd newenv t na in + let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; - push_rel (set_name (Name id) decl) newenv) - env + push_rel (RelDecl.set_name (Name id) decl) newenv) + rels ~init:env0 (* 5- Looks for next fresh name outside a list; avoids also to use names that would clash with short name of global references; if name is already used, @@ -309,7 +313,7 @@ let make_all_name_different env = let next_ident_away_for_default_printing env_t id avoid = let visible = visible_ids env_t in - let bad id = to_avoid id avoid || Id.Set.mem id visible in + let bad id = Id.List.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad let next_name_away_for_default_printing env_t na avoid = @@ -380,12 +384,12 @@ let rename_bound_vars_as_displayed avoid env c = let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkProd (na', c1, rename avoid' (add_name na' env) c2) + mkProd (na', c1, rename avoid' (na' :: env) c2) | LetIn (na,c1,t,c2) -> let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2) + mkLetIn (na',c1,t, rename avoid' (na' :: env) c2) | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) | _ -> c in diff --git a/engine/namegen.mli b/engine/namegen.mli index 97c7c34a56..33ce9a34d0 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -54,7 +54,22 @@ val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr (** Avoid clashing with a name satisfying some predicate *) val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t -(** Avoid clashing with a name of the given list *) +(** [next_ident_away original_id unwanted_ids] returns a new identifier as close as possible + to the [original_id] while avoiding all [unwanted_ids]. + + In particular: + {ul {- if [original_id] does not appear in the list of [unwanted_ids], then [original_id] is returned.} + {- if [original_id] appears in the list of [unwanted_ids], + then this function returns a new id that: + {ul {- has the same {i root} as the [original_id],} + {- does not occur in the list of [unwanted_ids],} + {- has the smallest possible {i subscript}.}}}} + + where by {i subscript} of some identifier we mean last part of it that is composed + only from (decimal) digits and by {i root} of some identifier we mean + the whole identifier except for the {i subscript}. + + E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) val next_ident_away : Id.t -> Id.t list -> Id.t (** Avoid clashing with a name already used in current module *) diff --git a/engine/proofview.ml b/engine/proofview.ml index c01879765b..721389af4f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -22,6 +22,8 @@ open Context.Named.Declaration (** Main state of tactics *) type proofview = Proofview_monad.proofview +(* The first items in pairs below are proofs (under construction). + The second items in the pairs below are statements that are being proved. *) type entry = (Term.constr * Term.types) list (** Returns a stylised view of a proofview for use by, for instance, @@ -341,7 +343,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in - CErrors.errorlabstrm "" + CErrors.user_err (str "No such " ++ str (String.plural n "goal") ++ str "." ++ pr_non_empty_arg (fun x -> x) suffix) | _ -> raise CErrors.Unhandled @@ -421,13 +423,13 @@ let tclFOCUSID id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function - | SizeMismatch (i,_) -> + | SizeMismatch (i,j) -> let open Pp in let errmsg = str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str")." + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." in - CErrors.errorlabstrm "" errmsg + CErrors.user_err errmsg | _ -> raise CErrors.Unhandled end @@ -451,6 +453,25 @@ let iter_goal i = Solution.get >>= fun evd -> Comb.set CList.(undefined evd (flatten (rev subgoals))) +(** List iter but allocates a list of results *) +let map_goal i = + let rev = List.rev in (* hem... Proof masks List... *) + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> + Solution.get >>= fun step -> + match Evarutil.advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >>= fun res -> + Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x -> + return (res :: acc, x) + end ([],[]) initial >>= fun (results_rev, subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return (rev results_rev) + (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved @@ -583,7 +604,15 @@ let tclINDEPENDENT tac = let tac = InfoL.tag (Info.DBranch) tac in InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - +let tclINDEPENDENTL tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT [] + | [_] -> tac >>= fun x -> return [x] + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac)) (** {7 Goal manipulation} *) @@ -839,11 +868,11 @@ let tclPROGRESS t = if not test then tclUNIT res else - tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> Pervasives.raise CErrors.Unhandled end @@ -1050,7 +1079,7 @@ module Goal = struct exception NotExactlyOneSubgoal let _ = CErrors.register_handler begin function | NotExactlyOneSubgoal -> - CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.") + CErrors.user_err (Pp.str"Not exactly one subgoal.") | _ -> raise CErrors.Unhandled end diff --git a/engine/proofview.mli b/engine/proofview.mli index 90be2f90ab..294b03dca2 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -292,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact independent of backtracking in another. It is equivalent to [tclEXTEND [] tac []]. *) val tclINDEPENDENT : unit tactic -> unit tactic +val tclINDEPENDENTL: 'a tactic -> 'a list tactic (** {7 Goal manipulation} *) diff --git a/engine/termops.ml b/engine/termops.ml index 697b9a5f15..2f4c5e2049 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -17,6 +17,7 @@ open Environ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.Declaration (* Sorts and sort family *) @@ -100,6 +101,7 @@ let term_printer = ref (fun _ -> pr_constr) let print_constr_env t = !term_printer t let print_constr t = !term_printer (Global.env()) t let set_print_constr f = term_printer := f +let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c) let pr_var_decl env decl = let open NamedDecl in @@ -607,7 +609,10 @@ let vars_of_global_reference env gr = [m] is appropriately lifted through abstractions of [t] *) let dependent_main noevar univs m t = - let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in + let eqc x y = + if univs then not (Option.is_empty (Universes.eq_constr_universes x y)) + else eq_constr_nounivs x y + in let rec deprec m t = if eqc m t then raise Occur @@ -673,6 +678,21 @@ let rec subst_meta bl c = | Meta i -> (try Int.List.assoc i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c +let rec strip_outer_cast c = match kind_of_term c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c + +(* flattens application lists throwing casts in-between *) +let collapse_appl c = match kind_of_term c with + | App (f,cl) -> + let rec collapse_rec f cl2 = + match kind_of_term (strip_outer_cast f) with + | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) + | _ -> mkApp (f,cl2) + in + collapse_rec f cl + | _ -> c + (* First utilities for avoiding telescope computation for subst_term *) let prefix_application eq_fun (k,c) (t : constr) = @@ -982,18 +1002,27 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false -let compact_named_context_reverse sign = +let compact_named_context sign = let compact l decl = - let (i1,c1,t1) = NamedDecl.to_tuple decl in - match l with - | [] -> [[i1],c1,t1] - | (l2,c2,t2)::q -> - if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - then (i1::l2,c2,t2)::q - else ([i1],c1,t1)::l - in Context.Named.fold_inside compact ~init:[] sign - -let compact_named_context sign = List.rev (compact_named_context_reverse sign) + match decl, l with + | NamedDecl.LocalAssum (i,t), [] -> + [CompactedDecl.LocalAssum ([i],t)] + | NamedDecl.LocalDef (i,c,t), [] -> + [CompactedDecl.LocalDef ([i],c,t)] + | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q -> + if Constr.equal t1 t2 + then CompactedDecl.LocalAssum (i1::li, t2) :: q + else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q + | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q -> + if Constr.equal c1 c2 && Constr.equal t1 t2 + then CompactedDecl.LocalDef (i1::li, c2, t2) :: q + else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q + | NamedDecl.LocalAssum (i,t), q -> + CompactedDecl.LocalAssum ([i],t) :: q + | NamedDecl.LocalDef (i,c,t), q -> + CompactedDecl.LocalDef ([i],c,t) :: q + in + sign |> Context.Named.fold_inside compact ~init:[] |> List.rev let clear_named_body id env = let open NamedDecl in diff --git a/engine/termops.mli b/engine/termops.mli index fd8edafbcf..78826f79ae 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -164,6 +164,13 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) val eta_reduce_head : constr -> constr +(** Flattens application lists *) +val collapse_appl : constr -> constr + +(** Remove recursively the casts around a term i.e. + [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) +val strip_outer_cast : constr -> constr + exception CannotFilter (** Lightweight first-order filtering procedure. Unification @@ -239,8 +246,7 @@ val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool -val compact_named_context : Context.Named.t -> Context.NamedList.t -val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t +val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env diff --git a/engine/uState.ml b/engine/uState.ml index c35f97b2e9..c66af02bb9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -255,8 +255,8 @@ let universe_context ?names ctx = let l = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> - user_err_loc (loc, "universe_context", - str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + user_err ~loc ~hdr:"universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) pl ([], [], levels) in @@ -269,8 +269,8 @@ let universe_context ?names ctx = Option.default Loc.ghost info.uloc with Not_found -> Loc.ghost in - user_err_loc (loc, "universe_context", - (str(CString.plural n "Universe") ++ spc () ++ + user_err ~loc ~hdr:"universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level ctx) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) diff --git a/engine/universes.ml b/engine/universes.ml new file mode 100644 index 0000000000..30a9ef1634 --- /dev/null +++ b/engine/universes.ml @@ -0,0 +1,1130 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Names +open Term +open Environ +open Univ +open Globnames +open Decl_kinds + +let pr_with_global_universes l = + try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) + with Not_found -> Level.pr l + +(** Local universe names of polymorphic references *) + +type universe_binders = (Id.t * Univ.universe_level) list + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> [] + +let register_universe_binders ref l = + universe_binders_table := Refmap.add ref l !universe_binders_table + +(* To disallow minimization to Set *) + +let set_minimization = ref true +let is_set_minimization () = !set_minimization + +type universe_constraint_type = ULe | UEq | ULub + +type universe_constraint = universe * universe_constraint_type * universe + +module Constraints = struct + module S = Set.Make( + struct + type t = universe_constraint + + let compare_type c c' = + match c, c' with + | ULe, ULe -> 0 + | ULe, _ -> -1 + | _, ULe -> 1 + | UEq, UEq -> 0 + | UEq, _ -> -1 + | ULub, ULub -> 0 + | ULub, _ -> 1 + + let compare (u,c,v) (u',c',v') = + let i = compare_type c c' in + if Int.equal i 0 then + let i' = Universe.compare u u' in + if Int.equal i' 0 then Universe.compare v v' + else + if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0 + else i' + else i + end) + + include S + + let add (l,d,r as cst) s = + if Universe.equal l r then s + else add cst s + + let tr_dir = function + | ULe -> Le + | UEq -> Eq + | ULub -> Eq + + let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " + + let pr c = + fold (fun (u1,op,u2) pp_std -> + pp_std ++ Universe.pr u1 ++ str (op_str op) ++ + Universe.pr u2 ++ fnl ()) c (str "") + + let equal x y = + x == y || equal x y + +end + +type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option +type 'a universe_constrained = 'a * universe_constraints + +type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints + +let enforce_eq_instances_univs strict x y c = + let d = if strict then ULub else UEq in + let ax = Instance.to_array x and ay = Instance.to_array y in + if Array.length ax != Array.length ay then + CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ + Pp.str " instances of different lengths"); + CArray.fold_right2 + (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) + ax ay c + +let subst_univs_universe_constraint fn (u,d,v) = + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in + if Universe.equal u' v' then None + else Some (u',d,v') + +let subst_univs_universe_constraints subst csts = + Constraints.fold + (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c)) + csts Constraints.empty + + +let to_constraints g s = + let tr (x,d,y) acc = + let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in + match Universe.level x, d, Universe.level y with + | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc + | _, ULe, Some l' -> enforce_leq x y acc + | _, ULub, _ -> acc + | _, d, _ -> + let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in + if f g x y then acc else + raise (Invalid_argument + "to_constraints: non-trivial algebraic constraint between universes") + in Constraints.fold tr s Constraint.empty + +let test_constr_univs_infer leq univs fold m n accu = + if m == n then Some accu + else + let cstrs = ref accu in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = + if leq then + let rec compare_leq m n = + Constr.compare_head_gen_leq eq_universes leq_sorts + eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + compare_leq m n + else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + if res then Some !cstrs else None + +let eq_constr_univs_infer univs fold m n accu = + test_constr_univs_infer false univs fold m n accu + +let leq_constr_univs_infer univs fold m n accu = + test_constr_univs_infer true univs fold m n accu + +(** Variant of [eq_constr_univs_infer] taking kind-of-term functions, + to expose subterms of [m] and [n], arguments. *) +let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = + (* spiwack: duplicates the code of [eq_constr_univs_infer] because I + haven't find a way to factor the code without destroying + pointer-equality optimisations in [eq_constr_univs_infer]. + Pointer equality is not sufficient to ensure equality up to + [kind1,kind2], because [kind1] and [kind2] may be different, + typically evaluating [m] and [n] in different evar maps. *) + let cstrs = ref accu in + let eq_universes strict = UGraph.check_eq_instances univs in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let rec eq_constr' m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n + in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in + if res then Some !cstrs else None + +let test_constr_universes leq m n = + if m == n then Some Constraints.empty + else + let cstrs = ref Constraints.empty in + let eq_universes strict l l' = + cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else (cstrs := Constraints.add + (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; + true) + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + (cstrs := Constraints.add + (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = + if leq then + let rec compare_leq m n = + Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + compare_leq m n + else + Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + if res then Some !cstrs else None + +let eq_constr_universes m n = test_constr_universes false m n +let leq_constr_universes m n = test_constr_universes true m n + +let compare_head_gen_proj env equ eqs eqc' m n = + match kind_of_term m, kind_of_term n with + | Proj (p, c), App (f, args) + | App (f, args), Proj (p, c) -> + (match kind_of_term f with + | Const (p', u) when eq_constant (Projection.constant p) p' -> + let pb = Environ.lookup_projection p env in + let npars = pb.Declarations.proj_npars in + if Array.length args == npars + 1 then + eqc' c args.(npars) + else false + | _ -> false) + | _ -> Constr.compare_head_gen equ eqs eqc' m n + +let eq_constr_universes_proj env m n = + if m == n then true, Constraints.empty + else + let cstrs = ref Constraints.empty in + let eq_universes strict l l' = + cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + (cstrs := Constraints.add + (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n + in + let res = eq_constr' m n in + res, !cstrs + +(* Generator of levels *) +let new_univ_level, set_remote_new_univ_level = + RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) + ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n) + +let new_univ_level _ = new_univ_level () + (* Univ.Level.make db (new_univ_level ()) *) + +let fresh_level () = new_univ_level (Global.current_dirpath ()) + +(* TODO: remove *) +let new_univ dp = Univ.Universe.make (new_univ_level dp) +let new_Type dp = mkType (new_univ dp) +let new_Type_sort dp = Type (new_univ dp) + +let fresh_universe_instance ctx = + Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) + (UContext.instance ctx) + +let fresh_instance_from_context ctx = + let inst = fresh_universe_instance ctx in + let constraints = instantiate_univ_constraints inst ctx in + inst, constraints + +let fresh_instance ctx = + let ctx' = ref LSet.empty in + let inst = + Instance.subst_fn (fun v -> + let u = new_univ_level (Global.current_dirpath ()) in + ctx' := LSet.add u !ctx'; u) + (UContext.instance ctx) + in !ctx', inst + +let existing_instance ctx inst = + let () = + let a1 = Instance.to_array inst + and a2 = Instance.to_array (UContext.instance ctx) in + let len1 = Array.length a1 and len2 = Array.length a2 in + if not (len1 == len2) then + CErrors.user_err ~hdr:"Universes" + (str "Polymorphic constant expected " ++ int len2 ++ + str" levels but was given " ++ int len1) + else () + in LSet.empty, inst + +let fresh_instance_from ctx inst = + let ctx', inst = + match inst with + | Some inst -> existing_instance ctx inst + | None -> fresh_instance ctx + in + let constraints = instantiate_univ_constraints inst ctx in + inst, (ctx', constraints) + +let unsafe_instance_from ctx = + (Univ.UContext.instance ctx, ctx) + +(** Fresh universe polymorphic construction *) + +let fresh_constant_instance env c inst = + let cb = lookup_constant c env in + if cb.Declarations.const_polymorphic then + let inst, ctx = + fresh_instance_from + (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst + in + ((c, inst), ctx) + else ((c,Instance.empty), ContextSet.empty) + +let fresh_inductive_instance env ind inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + ((ind,inst), ctx) + else ((ind,Instance.empty), ContextSet.empty) + +let fresh_constructor_instance env (ind,i) inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + (((ind,i),inst), ctx) + else (((ind,i),Instance.empty), ContextSet.empty) + +let unsafe_constant_instance env c = + let cb = lookup_constant c env in + if cb.Declarations.const_polymorphic then + let inst, ctx = unsafe_instance_from + (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in + ((c, inst), ctx) + else ((c,Instance.empty), UContext.empty) + +let unsafe_inductive_instance env ind = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in + ((ind,inst), ctx) + else ((ind,Instance.empty), UContext.empty) + +let unsafe_constructor_instance env (ind,i) = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in + (((ind,i),inst), ctx) + else (((ind,i),Instance.empty), UContext.empty) + +open Globnames + +let fresh_global_instance ?names env gr = + match gr with + | VarRef id -> mkVar id, ContextSet.empty + | ConstRef sp -> + let c, ctx = fresh_constant_instance env sp names in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = fresh_constructor_instance env sp names in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = fresh_inductive_instance env sp names in + mkIndU c, ctx + +let fresh_constant_instance env sp = + fresh_constant_instance env sp None + +let fresh_inductive_instance env sp = + fresh_inductive_instance env sp None + +let fresh_constructor_instance env sp = + fresh_constructor_instance env sp None + +let unsafe_global_instance env gr = + match gr with + | VarRef id -> mkVar id, UContext.empty + | ConstRef sp -> + let c, ctx = unsafe_constant_instance env sp in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = unsafe_constructor_instance env sp in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = unsafe_inductive_instance env sp in + mkIndU c, ctx + +let constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + if not (Univ.ContextSet.is_empty ctx) then + if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then + (* Should be an error as we might forget constraints, allow for now + to make firstorder work with "using" clauses *) + c + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + else c + +let constr_of_reference = constr_of_global + +let unsafe_constr_of_global gr = + unsafe_global_instance (Global.env ()) gr + +let constr_of_global_univ (gr,u) = + match gr with + | VarRef id -> mkVar id + | ConstRef sp -> mkConstU (sp,u) + | ConstructRef sp -> mkConstructU (sp,u) + | IndRef sp -> mkIndU (sp,u) + +let fresh_global_or_constr_instance env = function + | IsConstr c -> c, ContextSet.empty + | IsGlobal gr -> fresh_global_instance env gr + +let global_of_constr c = + match kind_of_term c with + | Const (c, u) -> ConstRef c, u + | Ind (i, u) -> IndRef i, u + | Construct (c, u) -> ConstructRef c, u + | Var id -> VarRef id, Instance.empty + | _ -> raise Not_found + +let global_app_of_constr c = + match kind_of_term c with + | Const (c, u) -> (ConstRef c, u), None + | Ind (i, u) -> (IndRef i, u), None + | Construct (c, u) -> (ConstructRef c, u), None + | Var id -> (VarRef id, Instance.empty), None + | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c + | _ -> raise Not_found + +open Declarations + +let type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env, ContextSet.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let ty = Typeops.type_of_constant_type env cb.const_type in + if cb.const_polymorphic then + let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in + Vars.subst_instance_constr inst ty, ctx + else ty, ContextSet.empty + + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + if mib.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.mind_universes None in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + else + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + if mib.mind_polymorphic then + let inst, ctx = fresh_instance_from mib.mind_universes None in + Inductive.type_of_constructor (cstr,inst) specif, ctx + else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + +let type_of_global t = type_of_reference (Global.env ()) t + +let unsafe_type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env + | ConstRef c -> + let cb = Environ.lookup_constant c env in + Typeops.type_of_constant_type env cb.const_type + + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let (_, inst), _ = unsafe_inductive_instance env ind in + Inductive.type_of_inductive env (specif, inst) + + | ConstructRef (ind, _ as cstr) -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let (_, inst), _ = unsafe_inductive_instance env ind in + Inductive.type_of_constructor (cstr,inst) specif + +let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t + +let fresh_sort_in_family env = function + | InProp -> prop_sort, ContextSet.empty + | InSet -> set_sort, ContextSet.empty + | InType -> + let u = fresh_level () in + Type (Univ.Universe.make u), ContextSet.singleton u + +let new_sort_in_family sf = + fst (fresh_sort_in_family (Global.env ()) sf) + +let extend_context (a, ctx) (ctx') = + (a, ContextSet.union ctx ctx') + +let new_global_univ () = + let u = fresh_level () in + (Univ.Universe.make u, ContextSet.singleton u) + +(** Simplification *) + +module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) + +let add_list_map u t map = + try + let l = LMap.find u map in + LMap.update u (t :: l) map + with Not_found -> + LMap.add u [t] map + +module UF = LevelUnionFind + +(** Precondition: flexible <= ctx *) +let choose_canonical ctx flexible algs s = + let global = LSet.diff s ctx in + let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in + (** If there is a global universe in the set, choose it *) + if not (LSet.is_empty global) then + let canon = LSet.choose global in + canon, (LSet.remove canon global, rigid, flexible) + else (** No global in the equivalence class, choose a rigid one *) + if not (LSet.is_empty rigid) then + let canon = LSet.choose rigid in + canon, (global, LSet.remove canon rigid, flexible) + else (** There are only flexible universes in the equivalence + class, choose a non-algebraic. *) + let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in + if not (LSet.is_empty nonalgs) then + let canon = LSet.choose nonalgs in + canon, (global, rigid, LSet.remove canon flexible) + else + let canon = LSet.choose algs in + canon, (global, rigid, LSet.remove canon flexible) + +let subst_univs_fn_puniverses lsubst (c, u as cu) = + let u' = Instance.subst_fn lsubst u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_opt_subst f subst = + let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in + let lsubst = Univ.level_subst_of subst in + let rec aux c = + match kind_of_term c with + | Evar (evk, args) -> + let args = Array.map aux args in + (match try f (evk, args) with Not_found -> None with + | None -> c + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> map_constr aux c + in aux + +let fresh_universe_context_set_instance ctx = + if ContextSet.is_empty ctx then LMap.empty, ctx + else + let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in + let univs',subst = LSet.fold + (fun u (univs',subst) -> + let u' = fresh_level () in + (LSet.add u' univs', LMap.add u u' subst)) + univs (LSet.empty, LMap.empty) + in + let cst' = subst_univs_level_constraints subst cst in + subst, (univs', cst') + +let normalize_univ_variable ~find ~update = + let rec aux cur = + let b = find cur in + let b' = subst_univs_universe aux b in + if Universe.equal b' b then b + else update cur b' + in aux + +let normalize_univ_variable_opt_subst ectx = + let find l = + match Univ.LMap.find l !ectx with + | Some b -> b + | None -> raise Not_found + in + let update l b = + assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); + try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false + in normalize_univ_variable ~find ~update + +let normalize_univ_variable_subst subst = + let find l = Univ.LMap.find l !subst in + let update l b = + assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); + try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in + normalize_univ_variable ~find ~update + +let normalize_universe_opt_subst subst = + let normlevel = normalize_univ_variable_opt_subst subst in + subst_univs_universe normlevel + +let normalize_universe_subst subst = + let normlevel = normalize_univ_variable_subst subst in + subst_univs_universe normlevel + +let normalize_opt_subst ctx = + let ectx = ref ctx in + let normalize = normalize_univ_variable_opt_subst ectx in + let () = + Univ.LMap.iter (fun u v -> + if Option.is_empty v then () + else try ignore(normalize u) with Not_found -> assert(false)) ctx + in !ectx + +type universe_opt_subst = universe option universe_map + +let make_opt_subst s = + fun x -> + (match Univ.LMap.find x s with + | Some u -> u + | None -> raise Not_found) + +let subst_opt_univs_constr s = + let f = make_opt_subst s in + Vars.subst_univs_fn_constr f + + +let normalize_univ_variables ctx = + let ctx = normalize_opt_subst ctx in + let undef, def, subst = + Univ.LMap.fold (fun u v (undef, def, subst) -> + match v with + | None -> (Univ.LSet.add u undef, def, subst) + | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) + ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) + in ctx, undef, def, subst + +let pr_universe_body = function + | None -> mt () + | Some v -> str" := " ++ Univ.Universe.pr v + +let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body + +let compare_constraint_type d d' = + match d, d' with + | Eq, Eq -> 0 + | Eq, _ -> -1 + | _, Eq -> 1 + | Le, Le -> 0 + | Le, _ -> -1 + | _, Le -> 1 + | Lt, Lt -> 0 + +type lowermap = constraint_type LMap.t + +let lower_union = + let merge k a b = + match a, b with + | Some _, None -> a + | None, Some _ -> b + | None, None -> None + | Some l, Some r -> + if compare_constraint_type l r >= 0 then a + else b + in LMap.merge merge + +let lower_add l c m = + try let c' = LMap.find l m in + if compare_constraint_type c c' > 0 then + LMap.add l c m + else m + with Not_found -> LMap.add l c m + +let lower_of_list l = + List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l + +exception Found of Level.t * lowermap +let find_inst insts v = + try LMap.iter (fun k (enf,alg,v',lower) -> + if not alg && enf && Universe.equal v' v then raise (Found (k, lower))) + insts; raise Not_found + with Found (f,l) -> (f,l) + +let compute_lbound left = + (** The universe variable was not fixed yet. + Compute its level using its lower bound. *) + let sup l lbound = + match lbound with + | None -> Some l + | Some l' -> Some (Universe.sup l l') + in + List.fold_left (fun lbound (d, l) -> + if d == Le (* l <= ?u *) then sup l lbound + else (* l < ?u *) + (assert (d == Lt); + if not (Universe.level l == None) then + sup (Universe.super l) lbound + else None)) + None left + +let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) = + if enforce then + let inst = Universe.make u in + let cstrs' = enforce_leq lbound inst cstrs in + (ctx, us, LSet.remove u algs, + LMap.add u (enforce,alg,lbound,lower) insts, cstrs'), + (enforce, alg, inst, lower) + else (* Actually instantiate *) + (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, + LMap.add u (enforce,alg,lbound,lower) insts, cstrs), + (enforce, alg, lbound, lower) + +type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t + +let pr_constraints_map cmap = + LMap.fold (fun l cstrs acc -> + Level.pr l ++ str " => " ++ + prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ + fnl () ++ acc) + cmap (mt ()) + +let remove_alg l (ctx, us, algs, insts, cstrs) = + (ctx, us, LSet.remove l algs, insts, cstrs) + +let remove_lower u lower = + let levels = Universe.levels u in + LSet.fold (fun l acc -> LMap.remove l acc) levels lower + +let minimize_univ_variables ctx us algs left right cstrs = + let left, lbounds = + Univ.LMap.fold (fun r lower (left, lbounds as acc) -> + if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc + else (* Fixed universe, just compute its glb for sharing *) + let lbounds' = + match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with + | None -> lbounds + | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower) + lbounds + in (Univ.LMap.remove r left, lbounds')) + left (left, Univ.LMap.empty) + in + let rec instance (ctx', us, algs, insts, cstrs as acc) u = + let acc, left, lower = + try + let l = LMap.find u left in + let acc, left, newlow, lower = + List.fold_left + (fun (acc, left', newlow, lower') (d, l) -> + let acc', (enf,alg,l',lower) = aux acc l in + let l' = + if enf then Universe.make l + else l' + in acc', (d, l') :: left', + lower_add l d newlow, lower_union lower lower') + (acc, [], LMap.empty, LMap.empty) l + in + let not_lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + in + let left = List.uniquize (List.filter not_lower left) in + (acc, left, LMap.union newlow lower) + with Not_found -> acc, [], LMap.empty + and right = + try Some (LMap.find u right) + with Not_found -> None + in + let instantiate_lbound lbound = + let alg = LSet.mem u algs in + if alg then + (* u is algebraic: we instantiate it with its lower bound, if any, + or enforce the constraints if it is bounded from the top. *) + let lower = remove_lower lbound lower in + instantiate_with_lbound u lbound lower true false acc + else (* u is non algebraic *) + match Universe.level lbound with + | Some l -> (* The lowerbound is directly a level *) + (* u is not algebraic but has no upper bounds, + we instantiate it with its lower bound if it is a + different level, otherwise we keep it. *) + let lower = LMap.remove l lower in + if not (Level.equal l u) then + (* Should check that u does not + have upper constraints that are not already in right *) + let acc' = remove_alg l acc in + instantiate_with_lbound u lbound lower false false acc' + else acc, (true, false, lbound, lower) + | None -> + try + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let can, lower = find_inst insts lbound in + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower false false acc + with Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound lower false true acc + in + let acc' acc = + match right with + | None -> acc + | Some cstrs -> + let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in + if List.is_empty dangling then acc + else + let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in + let cstrs' = List.fold_left (fun cstrs (d, r) -> + if d == Univ.Le then + enforce_leq inst (Universe.make r) cstrs + else + try let lev = Option.get (Universe.level inst) in + Constraint.add (lev, d, r) cstrs + with Option.IsNone -> failwith "") + cstrs dangling + in + (ctx', us, algs, insts, cstrs'), b + in + if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower)) + else + let lbound = compute_lbound left in + match lbound with + | None -> (* Nothing to do *) + acc' (acc, (true, false, Universe.make u, lower)) + | Some lbound -> + try acc' (instantiate_lbound lbound) + with Failure _ -> acc' (acc, (true, false, Universe.make u, lower)) + and aux (ctx', us, algs, seen, cstrs as acc) u = + try acc, LMap.find u seen + with Not_found -> instance acc u + in + LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> + if v == None then fst (aux acc u) + else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) + us (ctx, us, algs, lbounds, cstrs) + +let normalize_context_set ctx us algs = + let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in + let uf = UF.create () in + (** Keep the Prop/Set <= i constraints separate for minimization *) + let smallles, csts = + Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> + if d == Le then + if Univ.Level.is_small l then + if is_set_minimization () && LSet.mem r ctx then + (Constraint.add cstr smallles, noneqs) + else (smallles, noneqs) + else if Level.is_small r then + if Level.is_prop r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add (l,Eq,r) noneqs) + else (smallles, Constraint.add cstr noneqs) + else (smallles, Constraint.add cstr noneqs)) + csts (Constraint.empty, Constraint.empty) + in + let csts = + (* We first put constraints in a normal-form: all self-loops are collapsed + to equalities. *) + let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + ctx UGraph.empty_universes + in + let g = + Univ.Constraint.fold + (fun (l, d, r) g -> + let g = + if not (Level.is_small l || LSet.mem l ctx) then + try UGraph.add_universe l false g + with UGraph.AlreadyDeclared -> g + else g + in + let g = + if not (Level.is_small r || LSet.mem r ctx) then + try UGraph.add_universe r false g + with UGraph.AlreadyDeclared -> g + else g + in g) csts g + in + let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + UGraph.constraints_of_universes g + in + let noneqs = + Constraint.fold (fun (l,d,r as cstr) noneqs -> + if d == Eq then (UF.union l r uf; noneqs) + else (* We ignore the trivial Prop/Set <= i constraints. *) + if d == Le && Univ.Level.is_small l then noneqs + else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r + then noneqs + else Constraint.add cstr noneqs) + csts Constraint.empty + in + let noneqs = Constraint.union noneqs smallles in + let partition = UF.partition uf in + let flex x = LMap.mem x us in + let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) global + cstrs + in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) rigid + cstrs + in + let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, subst, us, cstrs)) + (ctx, LMap.empty, us, Constraint.empty) partition + in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + let noneqs = subst_univs_level_constraints subst noneqs in + (* Compute the left and right set of flexible variables, constraints + mentionning other variables remain in noneqs. *) + let noneqs, ucstrsl, ucstrsr = + Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> + let lus = LMap.mem l us and rus = LMap.mem r us in + let ucstrsl' = + if lus then add_list_map l (d, r) ucstrsl + else ucstrsl + and ucstrsr' = + add_list_map r (d, l) ucstrsr + in + let noneqs = + if lus || rus then noneq + else Constraint.add cstr noneq + in (noneqs, ucstrsl', ucstrsr')) + noneqs (Constraint.empty, LMap.empty, LMap.empty) + in + (* Now we construct the instantiation of each variable. *) + let ctx', us, algs, inst, noneqs = + minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs + in + let us = normalize_opt_subst us in + (us, algs), (ctx', Constraint.union noneqs eqs) + +(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) + +let universes_of_constr c = + let rec aux s c = + match kind_of_term 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 = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr 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 + +let simplify_universe_context (univs,csts) = + let uf = UF.create () in + let noneqs = + Constraint.fold (fun (l,d,r) noneqs -> + if d == Eq && (LSet.mem l univs || LSet.mem r univs) then + (UF.union l r uf; noneqs) + else Constraint.add (l,d,r) noneqs) + csts Constraint.empty + in + let partition = UF.partition uf in + let flex x = LSet.mem x univs in + let subst, univs', csts' = List.fold_left (fun (subst, univs, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical univs flex LSet.empty s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) + cstrs + in + let subst = LSet.fold (fun f -> LMap.add f canon) + flexible subst + in (subst, LSet.diff univs flexible, cstrs)) + (LMap.empty, univs, noneqs) partition + in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + let csts' = subst_univs_level_constraints subst csts' in + (univs', csts'), subst + +let is_trivial_leq (l,d,r) = + Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) + +(* Prop < i <-> Set+1 <= i <-> Set < i *) +let translate_cstr (l,d,r as cstr) = + if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then + (Level.set, d, r) + else cstr + +let refresh_constraints univs (ctx, cstrs) = + let cstrs', univs' = + Univ.Constraint.fold (fun c (cstrs', univs as acc) -> + let c = translate_cstr c in + if is_trivial_leq c then acc + else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) + cstrs (Univ.Constraint.empty, univs) + in ((ctx, cstrs'), univs') + + +(**********************************************************************) +(* Tools for sort-polymorphic inductive types *) + +(* Miscellaneous functions to remove or test local univ assumed to + occur only in the le constraints *) + +(* + Solve a system of universe constraint of the form + + u_s11, ..., u_s1p1, w1 <= u1 + ... + u_sn1, ..., u_snpn, wn <= un + +where + + - the ui (1 <= i <= n) are universe variables, + - the sjk select subsets of the ui for each equations, + - the wi are arbitrary complex universes that do not mention the ui. +*) + +let is_direct_sort_constraint s v = match s with + | Some u -> univ_level_mem u v + | None -> false + +let solve_constraints_system levels level_bounds level_min = + let open Univ in + let levels = + Array.mapi (fun i o -> + match o with + | Some u -> + (match Universe.level u with + | Some u -> Some u + | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) + | None -> None) + levels in + let v = Array.copy level_bounds in + let nind = Array.length v in + let clos = Array.map (fun _ -> Int.Set.empty) levels in + (* First compute the transitive closure of the levels dependencies *) + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then + clos.(i) <- Int.Set.add j clos.(i); + done; + done; + let rec closure () = + let continue = ref false in + Array.iteri (fun i deps -> + let deps' = + Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps + in + if Int.Set.equal deps deps' then () + else (clos.(i) <- deps'; continue := true)) + clos; + if !continue then closure () + else () + in + closure (); + for i=0 to nind-1 do + for j=0 to nind-1 do + if not (Int.equal i j) && Int.Set.mem j clos.(i) then + (v.(i) <- Universe.sup v.(i) level_bounds.(j)); + done; + done; + v diff --git a/engine/universes.mli b/engine/universes.mli new file mode 100644 index 0000000000..725c21d296 --- /dev/null +++ b/engine/universes.mli @@ -0,0 +1,231 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Term +open Environ +open Univ + +val set_minimization : bool ref +val is_set_minimization : unit -> bool + +(** Universes *) + +val pr_with_global_universes : Level.t -> Pp.std_ppcmds + +(** Local universe name <-> level mapping *) + +type universe_binders = (Id.t * Univ.universe_level) list + +val register_universe_binders : Globnames.global_reference -> universe_binders -> unit +val universe_binders_of_global : Globnames.global_reference -> universe_binders + +(** The global universe counter *) +val set_remote_new_univ_level : universe_level RemoteCounter.installer + +(** Side-effecting functions creating new universe levels. *) + +val new_univ_level : Names.dir_path -> universe_level +val new_univ : Names.dir_path -> universe +val new_Type : Names.dir_path -> types +val new_Type_sort : Names.dir_path -> sorts + +val new_global_univ : unit -> universe in_universe_context_set +val new_sort_in_family : sorts_family -> sorts + +(** {6 Constraints for type inference} + + When doing conversion of universes, not only do we have =/<= constraints but + also Lub constraints which correspond to unification of two levels which might + not be necessary if unfolding is performed. +*) + +type universe_constraint_type = ULe | UEq | ULub + +type universe_constraint = universe * universe_constraint_type * universe +module Constraints : sig + include Set.S with type elt = universe_constraint + + val pr : t -> Pp.std_ppcmds +end + +type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option +type 'a universe_constrained = 'a * universe_constraints +type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints + +val subst_univs_universe_constraints : universe_subst_fn -> + universe_constraints -> universe_constraints + +val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function + +val to_constraints : UGraph.t -> universe_constraints -> constraints + +(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, + application grouping, the universe constraints in [u] and additional constraints [c]. *) +val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option + +(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of + {!eq_constr_univs_infer} taking kind-of-term functions, to expose + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr,types) kind_of_term) -> + (constr -> (constr,types) kind_of_term) -> + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option + +(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] + modulo alpha, casts, application grouping, the universe constraints + in [u] and additional constraints [c]. *) +val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe constraints in [c]. *) +val eq_constr_universes : constr -> constr -> universe_constraints option + +(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe constraints in [c]. *) +val leq_constr_universes : constr -> constr -> universe_constraints option + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe constraints in [c]. *) +val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained + +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +val fresh_instance_from_context : universe_context -> + universe_instance constrained + +val fresh_instance_from : universe_context -> universe_instance option -> + universe_instance in_universe_context_set + +val fresh_sort_in_family : env -> sorts_family -> + sorts in_universe_context_set +val fresh_constant_instance : env -> constant -> + pconstant in_universe_context_set +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> + constr in_universe_context_set + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set + +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : universe_context_set -> + universe_level_subst * universe_context_set + +(** Raises [Not_found] if not a global reference. *) +val global_of_constr : constr -> Globnames.global_reference puniverses + +val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option + +val constr_of_global_univ : Globnames.global_reference puniverses -> constr + +val extend_context : 'a in_universe_context_set -> universe_context_set -> + 'a in_universe_context_set + +(** Simplification and pruning of constraints: + [normalize_context_set ctx us] + + - Instantiate the variables in [us] with their most precise + universe levels respecting the constraints. + + - Normalizes the context [ctx] w.r.t. equality constraints, + choosing a canonical universe in each equivalence class + (a global one if there is one) and transitively saturate + the constraints w.r.t to the equalities. *) + +module UF : Unionfind.PartitionSig with type elt = universe_level + +type universe_opt_subst = universe option universe_map + +val make_opt_subst : universe_opt_subst -> universe_subst_fn + +val subst_opt_univs_constr : universe_opt_subst -> constr -> constr + +val normalize_context_set : universe_context_set -> + universe_opt_subst (* The defined and undefined variables *) -> + universe_set (* univ variables that can be substituted by algebraics *) -> + (universe_opt_subst * universe_set) in_universe_context_set + +val normalize_univ_variables : universe_opt_subst -> + universe_opt_subst * universe_set * universe_set * universe_subst + +val normalize_univ_variable : + find:(universe_level -> universe) -> + update:(universe_level -> universe -> universe) -> + universe_level -> universe + +val normalize_univ_variable_opt_subst : universe_opt_subst ref -> + (universe_level -> universe) + +val normalize_univ_variable_subst : universe_subst ref -> + (universe_level -> universe) + +val normalize_universe_opt_subst : universe_opt_subst ref -> + (universe -> universe) + +val normalize_universe_subst : universe_subst ref -> + (universe -> universe) + +(** Create a fresh global in the global environment, without side effects. + BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + the constraints should be properly added to an evd. + See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for + the proper way to get a fresh copy of a global reference. *) +val constr_of_global : Globnames.global_reference -> constr + +(** ** DEPRECATED ** synonym of [constr_of_global] *) +val constr_of_reference : Globnames.global_reference -> constr + +(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic + references by taking the original universe instance that is not recorded + anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) +val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context + +(** 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 + universe counter, use with care). *) +val type_of_global : Globnames.global_reference -> types in_universe_context_set + +(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic + references by taking the original universe instance that is not recorded + anywhere. The constraints are forgotten as well. + USE with care. *) +val unsafe_type_of_global : Globnames.global_reference -> types + +(** Full universes substitutions into terms *) + +val nf_evars_and_universes_opt_subst : (existential -> constr option) -> + universe_opt_subst -> constr -> constr + +(** Shrink a universe context to a restricted set of variables *) + +val universes_of_constr : constr -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set +val simplify_universe_context : universe_context_set -> + universe_context_set * universe_level_subst + +val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t + +(** Pretty-printing *) + +val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds + +(** {6 Support for old-style sort-polymorphism } *) + +val solve_constraints_system : universe option array -> universe array -> universe array -> + universe array |