diff options
38 files changed, 504 insertions, 331 deletions
diff --git a/.gitattributes b/.gitattributes index e087e1737..a5edcdb5b 100644 --- a/.gitattributes +++ b/.gitattributes @@ -5,48 +5,51 @@ # Because our commit hook automatically does [apply whitespace=fix] we # disable whitespace checking for all files except those where we want # it. Otherwise rogue global configuration and forgotten local -# configuration can break commits. +# configuration can break commits. Note that git cannot fix but can +# detect a blank-at-eof when it comes from removing a chunk of text at +# the end of the file, leaving an extra newline from before that +# chunk, so we disable blank-at-eof. * -whitespace # tabs are allowed in Makefiles. -Makefile* whitespace=trailing-space -tools/CoqMakefile.in whitespace=trailing-space +Makefile* whitespace=blank-at-eol +tools/CoqMakefile.in whitespace=blank-at-eol # in general we don't want tabs. -*.asciidoc whitespace=trailing-space,tab-in-indent -*.bib whitespace=trailing-space,tab-in-indent -*.c whitespace=trailing-space,tab-in-indent -*.css whitespace=trailing-space,tab-in-indent -*.dtd whitespace=trailing-space,tab-in-indent -*.el whitespace=trailing-space,tab-in-indent -*.g whitespace=trailing-space,tab-in-indent -*.h whitespace=trailing-space,tab-in-indent -*.html whitespace=trailing-space,tab-in-indent -*.hva whitespace=trailing-space,tab-in-indent -*.js whitespace=trailing-space,tab-in-indent -*.json whitespace=trailing-space,tab-in-indent -*.lang whitespace=trailing-space,tab-in-indent -*.md whitespace=trailing-space,tab-in-indent -*.merlin whitespace=trailing-space,tab-in-indent -*.ml whitespace=trailing-space,tab-in-indent -*.ml4 whitespace=trailing-space,tab-in-indent -*.mli whitespace=trailing-space,tab-in-indent -*.mll whitespace=trailing-space,tab-in-indent -*.mllib whitespace=trailing-space,tab-in-indent -*.mlp whitespace=trailing-space,tab-in-indent -*.mlpack whitespace=trailing-space,tab-in-indent -*.nsh whitespace=trailing-space,tab-in-indent -*.nsi whitespace=trailing-space,tab-in-indent -*.py whitespace=trailing-space,tab-in-indent -*.rst whitespace=trailing-space,tab-in-indent -*.sh whitespace=trailing-space,tab-in-indent -*.sty whitespace=trailing-space,tab-in-indent -*.tex whitespace=trailing-space,tab-in-indent -*.tokens whitespace=trailing-space,tab-in-indent -*.txt whitespace=trailing-space,tab-in-indent -*.v whitespace=trailing-space,tab-in-indent -*.xml whitespace=trailing-space,tab-in-indent -*.yml whitespace=trailing-space,tab-in-indent +*.asciidoc whitespace=blank-at-eol,tab-in-indent +*.bib whitespace=blank-at-eol,tab-in-indent +*.c whitespace=blank-at-eol,tab-in-indent +*.css whitespace=blank-at-eol,tab-in-indent +*.dtd whitespace=blank-at-eol,tab-in-indent +*.el whitespace=blank-at-eol,tab-in-indent +*.g whitespace=blank-at-eol,tab-in-indent +*.h whitespace=blank-at-eol,tab-in-indent +*.html whitespace=blank-at-eol,tab-in-indent +*.hva whitespace=blank-at-eol,tab-in-indent +*.js whitespace=blank-at-eol,tab-in-indent +*.json whitespace=blank-at-eol,tab-in-indent +*.lang whitespace=blank-at-eol,tab-in-indent +*.md whitespace=blank-at-eol,tab-in-indent +*.merlin whitespace=blank-at-eol,tab-in-indent +*.ml whitespace=blank-at-eol,tab-in-indent +*.ml4 whitespace=blank-at-eol,tab-in-indent +*.mli whitespace=blank-at-eol,tab-in-indent +*.mll whitespace=blank-at-eol,tab-in-indent +*.mllib whitespace=blank-at-eol,tab-in-indent +*.mlp whitespace=blank-at-eol,tab-in-indent +*.mlpack whitespace=blank-at-eol,tab-in-indent +*.nsh whitespace=blank-at-eol,tab-in-indent +*.nsi whitespace=blank-at-eol,tab-in-indent +*.py whitespace=blank-at-eol,tab-in-indent +*.rst whitespace=blank-at-eol,tab-in-indent +*.sh whitespace=blank-at-eol,tab-in-indent +*.sty whitespace=blank-at-eol,tab-in-indent +*.tex whitespace=blank-at-eol,tab-in-indent +*.tokens whitespace=blank-at-eol,tab-in-indent +*.txt whitespace=blank-at-eol,tab-in-indent +*.v whitespace=blank-at-eol,tab-in-indent +*.xml whitespace=blank-at-eol,tab-in-indent +*.yml whitespace=blank-at-eol,tab-in-indent # CR is desired for these Windows files. -*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent +*.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent @@ -25,6 +25,9 @@ Tactics - Deprecated the Implicit Tactic family of commands. +- The `simple apply` tactic now respects the `Opaque` flag when called from + Ltac (`auto` still does not respect it). + Tools - Coq_makefile lets one override or extend the following variables from diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh new file mode 100644 index 000000000..e6c48d10a --- /dev/null +++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then + Equations_CI_BRANCH=unification-returns-option + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh new file mode 100644 index 000000000..6939ead2b --- /dev/null +++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then + + # this branch contains a commit not present on coq-master that triggers + # the universe restriction bug #7472 + Elpi_CI_BRANCH=overlay-7495 + Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4838dd734..bb8189efc 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -28,6 +28,10 @@ Proof engine should indicate what the canonical form is. An important change is the move of `Globnames.global_reference` to `Names.GlobRef.t`. +- Unification API returns `evar_map option` instead of `bool * evar_map` + with the guarantee that the `evar_map` was unchanged if the boolean + was false. + ML Libraries used by Coq - Introduction of a "Smart" module for collecting "smart*" functions, e.g. diff --git a/engine/univops.ml b/engine/univops.ml index 76dbaa250..3fd518490 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -35,79 +35,14 @@ let universes_of_constr env c = | _ -> Constr.fold aux s c in aux LSet.empty c -type graphnode = { - mutable up : constraint_type LMap.t; - mutable visited : bool -} - -let merge_types d d0 = - match d, d0 with - | _, Lt | Lt, _ -> Lt - | Le, _ | _, Le -> Le - | Eq, Eq -> Eq - -let merge_up d b up = - let find = try Some (LMap.find b up) with Not_found -> None in - match find with - | Some d0 -> - let d = merge_types d d0 in - if d == d0 then up else LMap.add b d up - | None -> LMap.add b d up - -let add_up a d b graph = - let node, graph = - try LMap.find a graph, graph - with Not_found -> - let node = { up = LMap.empty; visited = false } in - node, LMap.add a node graph - in - node.up <- merge_up d b node.up; - graph - -(* for each node transitive close until you find a non removable, discard the rest *) -let transitive_close removable graph = - let rec do_node a node = - if not node.visited - then - let keepup = - LMap.fold (fun b d keepup -> - if not (LSet.mem b removable) - then merge_up d b keepup - else - begin - match LMap.find b graph with - | bnode -> - do_node b bnode; - LMap.fold (fun k d' keepup -> - merge_up (merge_types d d') k keepup) - bnode.up keepup - | exception Not_found -> keepup - end - ) - node.up LMap.empty - in - node.up <- keepup; - node.visited <- true - in - LMap.iter do_node graph - -let restrict_universe_context (univs,csts) keep = - let removable = LSet.diff univs keep in - let (csts, rem) = - Constraint.fold (fun (a,d,b as cst) (csts, rem) -> - if LSet.mem a removable || LSet.mem b removable - then (csts, add_up a d b rem) - else (Constraint.add cst csts, rem)) - csts (Constraint.empty, LMap.empty) - in - transitive_close removable rem; - let csts = - LMap.fold (fun a node csts -> - if LSet.mem a removable - then csts - else - LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts) - node.up csts) - rem csts - in +let restrict_universe_context (univs, csts) keep = + let removed = LSet.diff univs keep in + if LSet.is_empty removed then univs, csts + else + let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in + let g = UGraph.empty_universes in + let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.merge_constraints csts g in + let allkept = LSet.diff allunivs removed in + let csts = UGraph.constraints_for ~kept:allkept g in (LSet.inter univs keep, csts) diff --git a/engine/univops.mli b/engine/univops.mli index d1585414c..0b37ab975 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -14,5 +14,8 @@ open Univ (** The universes of monomorphic constants appear. *) val universes_of_constr : Environ.env -> constr -> LSet.t -(** Shrink a universe context to a restricted set of variables *) +(** [restrict_universe_context (univs,csts) keep] restricts [univs] to + the universes in [keep]. The constraints [csts] are adjusted so + that transitive constraints between remaining universes (those in + [keep] and those not in [univs]) are preserved. *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/kernel/constr.ml b/kernel/constr.ml index 8f83d6baa..c11b9ebf4 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -479,6 +479,34 @@ let iter_with_binders g f n c = match kind c with Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl +(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate + subterms of [c] starting from [acc] and proceeding from left to + right according to the usual representation of the constructions as + [fold_constr] but it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive *) + +let fold_constr_with_binders g f n acc c = + match kind c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g n) (f n acc t) c + | Lambda (na,t,c) -> f (g n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (p,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) diff --git a/kernel/constr.mli b/kernel/constr.mli index b35ea6653..742a13919 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -402,6 +402,15 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +(** [iter_with_binders g f n c] iters [f n] on the immediate + subterms of [c]; it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive and the order with which + subterms are processed is not specified *) + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + type constr_compare_fn = int -> constr -> constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 913c13173..7bd70c050 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -52,7 +52,7 @@ type inline = int option type projection_body = { proj_ind : MutInd.t; proj_npars : int; - proj_arg : int; + proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) proj_eta : constr * types; (* Eta-expanded term and type *) proj_body : constr; (* For compatibility with VMs only, the match version *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 036cd4847..8257dc8b8 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -53,7 +53,7 @@ type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) | Gconstant of string * Constant.t (* prefix, constant name *) - | Gproj of string * Constant.t (* prefix, constant name *) + | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *) | Gcase of Label.t option * int | Gpred of Label.t option * int | Gfixtype of Label.t option * int @@ -108,7 +108,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 9 (String.hash s) | Grel i -> combinesmall 10 (Int.hash i) | Gnamed id -> combinesmall 11 (Id.hash id) -| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p)) +| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i)) let case_ctr = ref (-1) @@ -152,6 +152,7 @@ type symbol = | SymbMeta of metavariable | SymbEvar of Evar.t | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) let dummy_symb = SymbValue (dummy_value ()) @@ -166,6 +167,7 @@ let eq_symbol sy1 sy2 = | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 + | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2 | _, _ -> false let hash_symbol symb = @@ -179,6 +181,7 @@ let hash_symbol symb = | SymbMeta m -> combinesmall 7 m | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) + | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k) module HashedTypeSymbol = struct type t = symbol @@ -241,6 +244,11 @@ let get_level tbl i = | SymbLevel u -> u | _ -> anomaly (Pp.str "get_level failed.") +let get_proj tbl i = + match tbl.(i) with + | SymbProj p -> p + | _ -> anomaly (Pp.str "get_proj failed.") + let push_symbol x = try HashtblSymbol.find symb_tbl x with Not_found -> @@ -885,6 +893,10 @@ let get_level_code i = MLapp (MLglobal (Ginternal "get_level"), [|MLglobal symbols_tbl_name; MLint i|]) +let get_proj_code i = + MLapp (MLglobal (Ginternal "get_proj"), + [|MLglobal symbols_tbl_name; MLint i|]) + type rlist = | Rnil | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' @@ -1070,7 +1082,7 @@ let ml_of_instance instance u = | Lconst (prefix, (c, u)) -> let args = ml_of_instance env.env_univ u in mkMLapp (MLglobal(Gconstant (prefix, c))) args - | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) + | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in compile_prim decl cond paux @@ -1544,8 +1556,8 @@ let string_of_gname g = Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) - | Gproj (prefix, c) -> - Format.sprintf "%sproj_%s" prefix (string_of_con c) + | Gproj (prefix, (mind, n), i) -> + Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i | Gcase (l,i) -> Format.sprintf "case_%s_%i" (string_of_label_def l) i | Gpred (l,i) -> @@ -1858,8 +1870,6 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - match cb.const_proj with - | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,39 +1913,6 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | true -> - let pb = lookup_projection (Projection.make con false) env in - let mind = pb.proj_ind in - let ind = (mind,0) in - let mib = lookup_mind mind env in - let oib = mib.mind_packets.(0) in - let tbl = oib.mind_reloc_tbl in - (* Building info *) - let prefix = get_mind_prefix env mind in - let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; - ci_cstr_nargs = [|0|]; - ci_cstr_ndecls = [||] (*FIXME*); - ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in - let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; - asw_reloc = tbl; asw_finite = true } in - let c_uid = fresh_lname Anonymous in - let cf_uid = fresh_lname Anonymous in - let _, arity = tbl.(0) in - let ci_uid = fresh_lname Anonymous in - let cargs = Array.init arity - (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) - in - let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in - let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in - let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("",con) in - let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in - let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal - arg|]))):: - [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -1962,10 +1939,12 @@ let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = let u = Declareops.inductive_polymorphic_context mb in + (** Generate data for every block *) let f i stack ob = - let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in - let j = push_symbol (SymbInd (mind,i)) in - let name = Gind ("", (mind, i)) in + let ind = (mind, i) in + let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd ind) in + let name = Gind ("", ind) in let accu = let args = if Int.equal (Univ.AUContext.size u) 0 then @@ -1979,12 +1958,41 @@ let compile_mind prefix ~interactive mb mind stack = Array.init nparams (fun i -> {lname = param_name; luid = i}) in let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in - let c = (mind,i), (j+1) in + let c = ind, (j+1) in Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in - Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in + let add_proj j acc pb = + let tbl = ob.mind_reloc_tbl in + (* Building info *) + let ci = { ci_ind = ind; ci_npar = nparams; + ci_cstr_nargs = [|0|]; + ci_cstr_ndecls = [||] (*FIXME*); + ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in + let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci; + asw_reloc = tbl; asw_finite = true } in + let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in + let _, arity = tbl.(0) in + let ci_uid = fresh_lname Anonymous in + let cargs = Array.init arity + (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + in + let i = push_symbol (SymbProj (ind, j)) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in + let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in + let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in + Glet (gn, mkMLlam [|c_uid|] code) :: acc + in + let projs = match mb.mind_record with + | None | Some None -> [] + | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs + in + projs @ constructors @ gtype :: accu :: stack in Array.fold_left_i f stack mb.mind_packets @@ -2017,25 +2025,22 @@ let compile_mind_deps env prefix ~interactive (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) -let rec compile_deps env sigma prefix ~interactive init t = +let compile_deps env sigma prefix ~interactive init t = + let rec aux env lvl init t = match kind t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in - let cb,(nameref,_) = lookup_constant_key c env in - let (_, (_, const_updates)) = init in - if is_code_loaded ~interactive nameref - || (Cmap_env.mem c const_updates) - then init - else + let c,u = get_alias env c in + let cb,(nameref,_) = lookup_constant_key c env in + let (_, (_, const_updates)) = init in + if is_code_loaded ~interactive nameref + || (Cmap_env.mem c const_updates) + then init + else let comp_stack, (mind_updates, const_updates) = - match cb.const_proj, cb.const_body with - | false, Def t -> - compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | true, _ -> - let pb = lookup_projection (Projection.make c false) env in - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + match cb.const_body with + | Def t -> + aux env lvl init (Mod_subst.force_constr t) | _ -> init in let code, name = @@ -2046,13 +2051,32 @@ let rec compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - let term = mkApp (mkConst (Projection.constant p), [|c|]) in - compile_deps env sigma prefix ~interactive init term + let pb = lookup_projection p env in + let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in + aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in - Constr.fold (compile_deps env sigma prefix ~interactive) init t - | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t + fold_constr_with_binders succ (aux env) lvl init t + | Var id -> + let open Context.Named.Declaration in + begin match lookup_named id env with + | LocalDef (_,t,_) -> + aux env lvl init t + | _ -> init + end + | Rel n when n > lvl -> + let open Context.Rel.Declaration in + let decl = lookup_rel n env in + let env = env_of_rel n env in + begin match decl with + | LocalDef (_,t,_) -> + aux env lvl init t + | LocalAssum _ -> init + end + | _ -> fold_constr_with_binders succ (aux env) lvl init t + in + aux env 0 init t let compile_constant_field env prefix con acc cb = let (gl, _) = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 42f2cbc2e..684983a87 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t +val get_proj : symbols -> int -> inductive * int + val get_symbols : unit -> symbols type code_location_update diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c07025660..e97dbd0d6 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu = let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu - | Aproj(p1,ac1), Aproj(p2,ac2) -> - if not (Constant.equal p1 p2) then raise NotConvertible + | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> + if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index c319be32d..eaad8ee0c 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -31,7 +31,7 @@ and lambda = | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 8b61ed0c5..0325a00b4 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -296,15 +296,17 @@ let is_value lc = match lc with | Lval _ -> true | Lmakeblock(_,_,_,args) when Array.is_empty args -> true + | Luint (UintVal _) -> true | _ -> false - + let get_value lc = match lc with | Lval v -> v - | Lmakeblock(_,_,tag,args) when Array.is_empty args -> + | Lmakeblock(_,_,tag,args) when Array.is_empty args -> Nativevalues.mk_int tag + | Luint (UintVal i) -> Nativevalues.mk_uint i | _ -> raise Not_found - + let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) @@ -517,8 +519,11 @@ let rec lambda_of_constr env sigma c = | Construct _ -> lambda_of_app env sigma c empty_args | Proj (p, c) -> - let kn = Projection.constant p in - mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|] + let pb = lookup_projection p !global_env in + (** FIXME: handle mutual records *) + let ind = (pb.proj_ind, 0) in + let prefix = get_mind_prefix !global_env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index cfcb0a485..da4413a0a 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -64,7 +64,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t * t array - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 4a58a3c7d..649853f06 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -54,7 +54,7 @@ type atom = | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of Evar.t * t (* type *) * t array (* arguments *) - | Aproj of Constant.t * accumulator + | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -71,7 +71,7 @@ val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : Evar.t -> t -> t array -> t -val mk_proj_accu : Constant.t -> accumulator -> t +val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e6b27077b..4a9467de5 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g = let () = cleanup_universes g in raise e -let add_universe vlev strict g = +let add_universe_gen vlev g = try let _arcv = UMap.find vlev g.entries in raise AlreadyDeclared @@ -520,8 +520,14 @@ let add_universe vlev strict g = } in let entries = UMap.add vlev (Canonical v) g.entries in - let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in - insert_edge strict (get_set_arc g) v g + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v + +let add_universe vlev strict g = + let g, v = add_universe_gen vlev g in + insert_edge strict (get_set_arc g) v g + +let add_universe_unconstrained vlev g = + fst (add_universe_gen vlev g) exception Found_explanation of explanation @@ -696,6 +702,9 @@ let enforce_univ_lt u v g = error_inconsistency Lt u v (get_explanation false v u g) let empty_universes = + { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + +let initial_universes = let set_arc = Canonical { univ = Level.set; ltle = LMap.empty; @@ -718,9 +727,6 @@ let empty_universes = let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in enforce_univ_lt Level.prop Level.set empty -(* Prop = Set is forbidden here. *) -let initial_universes = empty_universes - let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries let enforce_constraint cst g = @@ -780,6 +786,42 @@ let constraints_of_universes g = let csts = UMap.fold constraints_of g.entries Constraint.empty in csts, UF.partition uf +(* domain g.entries = kept + removed *) +let constraints_for ~kept g = + (* rmap: partial map from canonical universes to kept universes *) + let rmap, csts = LSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if LSet.mem arcu.univ kept then + LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts + else + match LMap.find arcu.univ rmap with + | v -> rmap, enforce_eq_level u v csts + | exception Not_found -> LMap.add arcu.univ u rmap, csts) + kept (LMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match LMap.find v.univ rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept universe *) + let todo = LMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + LSet.fold (fun u csts -> + let arc = repr g u in + LMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts + (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index cca2eb472..e6dd629e4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -49,13 +49,15 @@ exception AlreadyDeclared val add_universe : Level.t -> bool -> t -> t +(** Add a universe without (Prop,Set) <= u *) +val add_universe_unconstrained : Level.t -> t -> t + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t (** The empty graph of universes *) val empty_universes : t -[@@ocaml.deprecated "Use UGraph.initial_universes"] val sort_universes : t -> t @@ -64,6 +66,12 @@ val sort_universes : t -> t of the universes into equivalence classes. *) val constraints_of_universes : t -> Constraint.t * LSet.t list +(** [constraints_for ~kept g] returns the constraints about the + universes [kept] in [g] up to transitivity. + + eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *) +val constraints_for : kept:LSet.t -> t -> Constraint.t + val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 93c63d522..b1c5e131f 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -312,20 +312,22 @@ let unif_HO_args env ise0 pa i ca = (* for HO evars, though hopefully Miller patterns can pick up some of *) (* those cases, and HO matching will mop up the rest. *) let flags_FO env = + let oracle = Environ.oracle env in + let ts = Conv_oracle.get_transp_state oracle in let flags = - { (Unification.default_no_delta_unify_flags ()).Unification.core_unify_flags + { (Unification.default_no_delta_unify_flags ts).Unification.core_unify_flags with Unification.modulo_conv_on_closed_terms = None; Unification.modulo_eta = true; Unification.modulo_betaiota = true; - Unification.modulo_delta_types = Conv_oracle.get_transp_state (Environ.oracle env)} + Unification.modulo_delta_types = ts } in { Unification.core_unify_flags = flags; Unification.merge_unify_flags = flags; Unification.subterm_unify_flags = flags; Unification.allow_K_in_toplevel_higher_order_unification = false; Unification.resolve_evars = - (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars + (Unification.default_no_delta_unify_flags ts).Unification.resolve_evars } let unif_FO env ise p c = Unification.w_unify env ise Reduction.CONV ~flags:(flags_FO env) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 062136ff5..6d08f66c1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = - try - let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd term1 term2 - in - if b then Success evd - else UnifFailure (evd, ConversionFailed (env,term1,term2)) - with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) + match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with + | Some evd -> Success evd + | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)) + | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with | UnifFailure (evd, e) when not (is_ground_env evd env) -> None diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 978ceed1e..4b8e0e096 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,6 +188,14 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch +let get_proj env ((mind, _n), i) = + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | None | Some None -> + CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") + | Some (Some (_, projs, _)) -> + Projection.make projs.(i) true + let rec nf_val env sigma v typ = match kind_of_value v with | Vaccu accu -> nf_accu env sigma accu @@ -279,9 +287,10 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aproj(p,c) -> + | Aproj (p, c) -> let c = nf_accu env sigma c in - mkProj(Projection.make p true,c) + let p = get_proj env p in + mkProj(p, c) | _ -> fst (nf_atom_type env sigma atom) and nf_atom_type env sigma atom = @@ -303,10 +312,10 @@ and nf_atom_type env sigma atom = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env + hnf_prod_applist_assum env nparamdecls (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma ind mip params p pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in @@ -357,25 +366,30 @@ and nf_atom_type env sigma atom = | Aproj(p,c) -> let c,tc = nf_accu_type env sigma c in let cj = make_judge c tc in - let uj = Typeops.judge_of_projection env (Projection.make p true) cj in + let p = get_proj env p in + let uj = Typeops.judge_of_projection env p cj in uj.uj_val, uj.uj_type and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let name,dom,codom = - try decompose_prod env pT with - DestKO -> - CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") - in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> false, nf_type env sigma v + end + | _ -> + match kind_of_value v with + | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in let name = Name (Id.of_string "c") in @@ -385,7 +399,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_type env sigma v + | _ -> false, nf_type env sigma v and nf_evar env sigma evk ty args = let evi = try Evd.find sigma evk with Not_found -> assert false in diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 67b7a2a40..4997d0bf0 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 92f87ab95..b2507b5f2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then - let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ?loc (str "Cannot check cast with vm: " ++ @@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in - if b then (evdref := evd; cj, tval) - else + match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with + | Some evd -> (evdref := evd; cj, tval) + | None -> error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6fde86837..7fb1a0a57 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) try - let b, sigma = - let ans = - if pb == Reduction.CUMUL then + let ans = match pb with + | Reduction.CUMUL -> EConstr.leq_constr_universes env sigma x y - else + | Reduction.CONV -> EConstr.eq_constr_universes env sigma x y in let ans = match ans with @@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with - | None -> false, sigma - | Some sigma -> true, sigma - in - if b then sigma, true - else + | Some sigma -> ans + | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in - sigma', true + Some sigma' with - | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ when catch_incon -> sigma, false + | Reduction.NotConvertible -> None + | Univ.UniverseInconsistency _ when catch_incon -> None | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index ad280d9f3..9256fa7ce 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool) -> unit + evar_map option) -> unit val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a @@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5f7faa13e..5cf6e4b26 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -398,8 +398,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with modulo_betaiota = false; } -let default_no_delta_unify_flags () = - let flags = default_no_delta_core_unify_flags () in { +let default_no_delta_unify_flags ts = + let flags = default_no_delta_core_unify_flags () in + let flags = { flags with + modulo_conv_on_closed_terms = Some ts; + modulo_delta_types = ts + } in + { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = flags; @@ -579,16 +584,16 @@ let constr_cmp pb env sigma flags t u = in match cstrs with | Some cstrs -> - begin try Evd.add_universe_constraints sigma cstrs, true - with Univ.UniverseInconsistency _ -> sigma, false + begin try Some (Evd.add_universe_constraints sigma cstrs) + with Univ.UniverseInconsistency _ -> None | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true - with Univ.UniverseInconsistency _ -> sigma, false - else sigma, false + try Some (Evd.add_universe_constraints sigma (force_eqs cstrs)) + with Univ.UniverseInconsistency _ -> None + else None end | None -> - sigma, false + None let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state @@ -623,9 +628,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in - if b then sigma - else error_cannot_unify env sigma (m,n) + match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with + | Some sigma -> sigma + | None -> error_cannot_unify env sigma (m,n) else sigma @@ -740,11 +745,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb env sigma flags cM cN in - if b then - sigma',metasubst,evarsubst - else + begin match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> + sigma, metasubst, evarsubst + | None -> sigma,metasubst,((curenv,ev,cN)::evarsubst) + end | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) && not (occur_evar sigma evk cN) -> @@ -942,9 +948,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb env sigma flags cM cN in - if b then (sigma', metas, evars) - else + match constr_cmp cv_pb env sigma flags cM cN with + | Some sigma -> (sigma, metas, evars) + | None -> try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = @@ -1001,12 +1007,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in - let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in - if b then Some (sigma, metasubst, evarsubst) - else - if is_ground_term sigma m1 && is_ground_term sigma n1 then - error_cannot_unify curenv sigma (cM,cN) - else None + match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with + | Some sigma -> + Some (sigma, metasubst, evarsubst) + | None -> + if is_ground_term sigma m1 && is_ground_term sigma n1 then + error_cannot_unify curenv sigma (cM,cN) + else None in match res with | Some substn -> substn @@ -1109,11 +1116,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e then None else - let sigma, b = match flags.modulo_conv_on_closed_terms with + let ans = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in - if b then Some sigma - else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with + match ans with + | Some sigma -> ans + | None -> + if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k | None,(dl_id, dl_k) -> @@ -1603,8 +1612,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> - let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in - if b then Some (evd, c1, x) else raise (NotUnifiable None) + begin match infer_conv ~pb:CONV env evd c1 c2 with + | Some evd -> Some (evd, c1, x) + | None -> raise (NotUnifiable None) + end | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in @@ -1921,10 +1932,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in - if not b then + match infer_conv ~pb:CUMUL env evd' predtyp typp with + | None -> error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; + | Some evd' -> w_merge env false flags.merge_unify_flags (evd',[p,pred,(Conv,TypeProcessed)],[]) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 16ce5c93d..e2e261ae7 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Constr open EConstr open Environ @@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags val default_no_delta_core_unify_flags : unit -> core_unify_flags val default_unify_flags : unit -> unify_flags -val default_no_delta_unify_flags : unit -> unify_flags +val default_no_delta_unify_flags : transparent_state -> unify_flags val elim_flags : unit -> unify_flags val elim_no_delta_flags : unit -> unify_flags diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index a1ba4a6a9..14c9f49b1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params dep p in @@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let dep,body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + dep, mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) - | Vfun f, _ -> + | _ -> assert false + end + | _ -> + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in let name = Name (Id.of_string "c") in @@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in true, mkLambda(name,dom,body) - | _, _ -> false, nf_val env sigma v crazy_type + | _ -> false, nf_val env sigma v crazy_type and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in diff --git a/proofs/logic.ml b/proofs/logic.ml index 218b2671e..95c30d815 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -309,9 +309,10 @@ let check_meta_variables env sigma c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in - if b then evm - else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in + match ans with + | Some evm -> evm + | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 58c62af85..b571b347d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k = let sigma = if check then begin ignore (Typing.unsafe_type_of env sigma ty); - let sigma,b = Reductionops.infer_conv env sigma ty conclty in - if not b then error "Not convertible."; - sigma + match Reductionops.infer_conv env sigma ty conclty with + | None -> error "Not convertible." + | Some sigma -> sigma end else sigma in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in @@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> - try - let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in - if b then Proofview.Unsafe.tclEVARS sigma - else Tacticals.New.tclFAIL 0 (str "Not convertible") - with (* Reduction.NotConvertible *) _ -> + match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with + | Some sigma -> Proofview.Unsafe.tclEVARS sigma + | None -> Tacticals.New.tclFAIL 0 (str "Not convertible") + | exception _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") end @@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in - let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in - if not b then + match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with + | None -> if isSort sigma (whd_all env sigma t1) && isSort sigma (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.") - else sigma + | Some sigma -> sigma end else if not (isSort sigma (whd_all env sigma t1)) then @@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = let (sigma, t') = t sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in - let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); - (sigma, t') + match infer_conv ~pb:cv_pb env sigma t' c with + | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible."); + | Some sigma -> (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb deep t where env sigma c = @@ -1638,13 +1637,11 @@ let tclORELSEOPT t k = Proofview.tclZERO ~info e | Some tac -> tac) -let general_apply with_delta with_destruct with_evars clear_flag - {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = +let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars + clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let flags = - if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -1653,7 +1650,12 @@ let general_apply with_delta with_destruct with_evars clear_flag Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - + let ts = + if respect_opaque then Conv_oracle.get_transp_state (oracle env) + else full_transparent_state + in + let flags = + if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try @@ -1719,14 +1721,14 @@ let rec apply_with_bindings_gen b e = function (general_apply b b e k cb) (apply_with_bindings_gen b e cbl) -let apply_with_delayed_bindings_gen b e l = +let apply_with_delayed_bindings_gen b e l = let one k {CAst.loc;v=f} = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma, cb) = f env sigma in Tacticals.New.tclWITHHOLES e - (general_apply b b e k CAst.(make ?loc cb)) sigma + (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma end in let rec aux = function @@ -1801,14 +1803,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = in aux (make_clenv_binding env sigma (d,thm) lbind) -let apply_in_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,{ CAst.loc; v= d,lbind}) tac = +let apply_in_once ?(respect_opaque = false) sidecond_first with_delta + with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let flags = - if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in @@ -1816,6 +1816,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in + let ts = + if respect_opaque then Conv_oracle.get_transp_state (oracle env) + else full_transparent_state + in + let flags = + if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause @@ -1835,14 +1841,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming aux [] with_destruct d end -let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,{CAst.loc;v=f}) tac = +let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta + with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars - (apply_in_once sidecond_first with_delta with_destruct with_evars + (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -1934,16 +1940,19 @@ let assumption = let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let (sigma, is_same_type) = - if only_eq then (sigma, EConstr.eq_constr sigma t concl) + let ans = + if only_eq then + if EConstr.eq_constr sigma t concl then Some sigma + else None else let env = Proofview.Goal.env gl in infer_conv env sigma t concl in - if is_same_type then + match ans with + | Some sigma -> (Proofview.Unsafe.tclEVARS sigma) <*> exact_no_check (mkVar (NamedDecl.get_id decl)) - else arec gl only_eq rest + | None -> arec gl only_eq rest in let assumption_tac gl = let hyps = Proofview.Goal.hyps gl in @@ -2529,11 +2538,11 @@ let assert_as first hd ipat t = (* apply in as *) -let general_apply_in sidecond_first with_delta with_destruct with_evars - id lemmas ipat = +let general_apply_in ?(respect_opaque=false) sidecond_first with_delta + with_destruct with_evars id lemmas ipat = let tac (naming,lemma) tac id = - apply_in_delayed_once sidecond_first with_delta with_destruct with_evars - naming id lemma tac in + apply_in_delayed_once ~respect_opaque sidecond_first with_delta + with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) @@ -2564,7 +2573,7 @@ let apply_in simple with_evars id lemmas ipat = general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = - general_apply_in false simple simple with_evars id lemmas ipat + general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat (*****************************) (* Tactics abstracting terms *) diff --git a/test-suite/Makefile b/test-suite/Makefile index f41fb5b1e..32e245e36 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ + output=$*.out.real; \ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ - > $$tmpoutput; \ - diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ + rm $$output; \ else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ $(FAIL); \ fi; \ - rm $$tmpoutput; \ } > "$@" +.PHONY: approve-output +approve-output: output + $(HIDE)for f in output/*.out.real; do \ + mv "$$f" "$${f%.real}"; \ + echo "Updated $${f%.real}!"; \ + done + # the expected output for the MExtraction test is # /plugins/micromega/micromega.ml except with additional newline output/MExtraction.out: ../plugins/micromega/micromega.ml diff --git a/test-suite/README.md b/test-suite/README.md index 4572c98cf..ef2e574ec 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -76,3 +76,17 @@ There are also output tests in `test-suite/output` which consist of a `.v` file There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use `make unit-tests' in the unit-tests directory to run them. + +## Fixing output tests + +When an output test `output/foo.v` fails, the output is stored in +`output/foo.out.real`. Move that file to the reference file +`output/foo.out` to update the test, approving the new output. Target +`approve-output` will do this for all failing output tests +automatically. + +Don't forget to check the updated `.out` files into git! + +Note that `output/MExtraction.out` is special: it is copied from +`micromega/micromega.ml` in the plugin source directory. Automatic +approval will incorrectly update the copy. diff --git a/test-suite/bugs/closed/7068.v b/test-suite/bugs/closed/7068.v new file mode 100644 index 000000000..9fadb195b --- /dev/null +++ b/test-suite/bugs/closed/7068.v @@ -0,0 +1,6 @@ +(* These tests are only about a subset of #7068 *) +(* The original issue is still open *) + +Inductive foo : let T := Type in T := . +Definition bob1 := Eval vm_compute in foo_rect. +Definition bob2 := Eval native_compute in foo_rect. diff --git a/test-suite/bugs/closed/7076.v b/test-suite/bugs/closed/7076.v new file mode 100644 index 000000000..0abc88c28 --- /dev/null +++ b/test-suite/bugs/closed/7076.v @@ -0,0 +1,4 @@ +(* These calls were raising an anomaly at some time *) +Inductive A : nat -> id (nat->Type) := . +Eval vm_compute in fun x => match x in A y z return y = z with end. +Eval native_compute in fun x => match x in A y z return y = z with end. diff --git a/test-suite/bugs/closed/7631.v b/test-suite/bugs/closed/7631.v new file mode 100644 index 000000000..34eb8b867 --- /dev/null +++ b/test-suite/bugs/closed/7631.v @@ -0,0 +1,21 @@ +Module NamedContext. + +Definition foo := true. + +Section Foo. + +Let bar := foo. + +Eval native_compute in bar. + +End Foo. + +End NamedContext. + +Module RelContext. + +Definition foo := true. + +Definition bar (x := foo) := Eval native_compute in x. + +End RelContext. diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index c6836a1c7..ed4d69ab0 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -82,7 +82,7 @@ End Retracts. (** This lemma is basically a commutation of implication and existential quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) + intuitionistic logic). *) Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. @@ -136,7 +136,7 @@ trivial. Qed. -Theorem classical_proof_irrelevence : T = F. +Theorem classical_proof_irrelevance : T = F. Proof. generalize not_has_fixpoint. unfold Not_b. @@ -148,4 +148,7 @@ intros not_true is_true. elim not_true; trivial. Qed. + +Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). + End Berardis_paradox. diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index dd8149d0a..b6523981c 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -631,8 +631,8 @@ GEXTEND Gram t = class_rawexpr -> VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) - | IDENT "Context"; c = binders -> - VernacContext c + | IDENT "Context"; c = LIST1 binder -> + VernacContext (List.flatten c) | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; |