diff options
49 files changed, 1260 insertions, 905 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index c49bc3b08b..9b0cc21197 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -54,10 +54,17 @@ opam-switch: &opam-switch steps: - checkout - run: *before_script + - run: + name: Cache selection + command: | + source ~/.profile + # We can't use environment variables in cache names + # So put it in a file and use the checksum + echo "$COMPILER" > COMPILER - restore_cache: keys: - - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}- # this grabs old cache if checksum doesn't match + - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}- # this grabs old cache if checksum doesn't match - run: name: Update opam lists command: | @@ -76,7 +83,7 @@ opam-switch: &opam-switch source ~/.profile rm -rf ~/.opam/log/ - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}- + key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- paths: - ~/.opam - persist_to_workspace: diff --git a/.travis.yml b/.travis.yml index 8f1f1e699b..19e7075f22 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,10 +20,19 @@ addons: apt: sources: - avsm - packages: - - opam - - aspcud - - gcc-multilib +## Due to issues like +## https://github.com/travis-ci/travis-ci/issues/8507 , +## https://github.com/travis-ci/travis-ci/issues/9000 , +## https://github.com/travis-ci/travis-ci/issues/9081 , and +## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent +## failures with using `packages`. Therefore, for most targets, we +## instead invoke `apt-get update` manually with `travis_retry` before +## invoking `apt-get install`, manually, below in the `install:` +## target. +# packages: +# - opam +# - aspcud +# - gcc-multilib env: global: @@ -46,33 +55,68 @@ env: - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}" - - TEST_TARGET="ci-bignums" - - TEST_TARGET="ci-color" - - TEST_TARGET="ci-compcert" - - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - - TEST_TARGET="ci-coquelicot" - - TEST_TARGET="ci-equations" - - TEST_TARGET="ci-geocoq" - - TEST_TARGET="ci-fiat-crypto" - - TEST_TARGET="ci-fiat-parsers" - - TEST_TARGET="ci-flocq" - - TEST_TARGET="ci-formal-topology" - - TEST_TARGET="ci-hott" - - TEST_TARGET="ci-iris-lambda-rust" - - TEST_TARGET="ci-ltac2" - - TEST_TARGET="ci-math-classes" - - TEST_TARGET="ci-math-comp" - - TEST_TARGET="ci-sf" - - TEST_TARGET="ci-unimath" - - TEST_TARGET="ci-vst" - # Not ready yet for 8.7 - # - TEST_TARGET="ci-cpdt" - # - TEST_TARGET="ci-metacoq" - # - TEST_TARGET="ci-tlc" matrix: include: + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-bignums" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-color" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-compcert" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-coquelicot" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-equations" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-geocoq" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-fiat-crypto" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-fiat-parsers" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-flocq" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-formal-topology" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-hott" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-iris-lambda-rust" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-ltac2" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-math-classes" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-math-comp" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-sf" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-unimath" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-vst" + - env: - TEST_TARGET="lint" install: [] @@ -212,6 +256,8 @@ before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi install: +- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi +- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib; fi - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list diff --git a/checker/declarations.ml b/checker/declarations.ml index 884a1ef18c..15b1f0a0c6 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -484,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true - | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 - | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 + | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2 + | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2 | _ -> false let eq_wf_paths = Rtree.equal eq_recarg diff --git a/checker/indtypes.ml b/checker/indtypes.ml index bb0db8cfe9..4de5977666 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -502,10 +502,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc indlc in mk_paths (Mrec ind) irecargs +let prrecarg = function + | Norec -> str "Norec" + | Mrec (mind,i) -> + str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + | Imbr (mind,i) -> + str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + let check_subtree t1 t2 = let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in if not (Rtree.equiv eq_recarg cmp_labels t1 t2) - then failwith "bad recursive trees" + then user_err Pp.(str "Bad recursive tree: found " ++ fnl () + ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl () + ++ Rtree.pp_tree prrecarg t2) (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) let check_positivity env_ar mind params nrecp inds = diff --git a/checker/inductive.ml b/checker/inductive.ml index 22353ec168..8d426a3c05 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -381,7 +381,7 @@ let type_case_branches env (pind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) || + not (eq_ind_chk indsp ci.ci_ind) || (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || (mip.mind_consnrealargs <> ci.ci_cstr_nargs) @@ -435,20 +435,14 @@ type subterm_spec = | Dead_code | Not_subterm -let eq_recarg r1 r2 = match r1, r2 with -| Norec, Norec -> true -| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 -| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 -| _ -> false - let eq_wf_paths = Rtree.equal eq_recarg let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 | Imbr i1, Imbr i2 -| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None -| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None +| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None | _ -> None let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec @@ -544,7 +538,7 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | (Mrec i | Imbr i) -> eq_ind ind i + | (Mrec i | Imbr i) -> eq_ind_chk ind i | Norec -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} @@ -645,7 +639,7 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' -> + | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' -> build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 1838db5d01..05fa33e972 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,6 +2,10 @@ set -xe +# default value for NJOBS +: "${NJOBS:=1}" +export NJOBS + if [ -n "${GITLAB_CI}" ]; then export COQBIN="$PWD/_install_ci/bin" diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fc3cef3426..6a0ce2aefa 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,7 +5,7 @@ source ${ci_dir}/ci-common.sh CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert -opam install -j ${NJOBS} -y menhir +opam install -j "$NJOBS" -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} ( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh new file mode 100644 index 0000000000..8a50fb1111 --- /dev/null +++ b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then + Equations_CI_BRANCH=fix-6535 + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh new file mode 100755 index 0000000000..f8bf6bed41 --- /dev/null +++ b/dev/tools/sudo-apt-get-update.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err +! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $? diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 8e43bf6ed0..f819d2e6a9 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -3,7 +3,7 @@ open Term open Names open Cbytecodes open Cemitcodes -open Vm +open Vmvalues let ppripos (ri,pos) = (match ri with diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 374fdce722..f82ffccdc3 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -257,22 +257,6 @@ let make_pure_subst evi args = * we have the property that u and phi(t) are convertible in env. *) -let csubst_subst (k, s) c = - (** Safe because this is a substitution *) - let c = EConstr.Unsafe.to_constr c in - let rec subst n c = match Constr.kind c with - | Rel m -> - if m <= n then c - else if m - n <= k then EConstr.Unsafe.to_constr (Int.Map.find (k - m + n) s) - else mkRel (m - k) - | _ -> Constr.map_with_binders succ subst n c - in - let c = if k = 0 then c else subst 0 c in - EConstr.of_constr c - -let subst2 subst vsubst c = - csubst_subst subst (EConstr.Vars.replace_vars vsubst c) - let next_ident_away id avoid = let avoid id = Id.Set.mem id avoid in next_ident_away_from id avoid @@ -282,19 +266,79 @@ let next_name_away na avoid = let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in next_ident_away_from id avoid -type csubst = int * EConstr.t Int.Map.t +type subst_val = +| SRel of int +| SVar of Id.t + +type csubst = { + csubst_len : int; + (** Cardinal of [csubst_rel] *) + csubst_var : Constr.t Id.Map.t; + (** A mapping of variables to variables. We use the more general + [Constr.t] to share allocations, but all values are of shape [Var _]. *) + csubst_rel : Constr.t Int.Map.t; + (** A contiguous mapping of integers to variables. Same remark for values. *) + csubst_rev : subst_val Id.Map.t; + (** Reverse mapping of the substitution *) +} +(** This type represent a name substitution for the named and De Bruijn parts of + a environment. For efficiency we also store the reverse substitution. + Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel] + must be pairwise distinct. *) + +let empty_csubst = { + csubst_len = 0; + csubst_rel = Int.Map.empty; + csubst_var = Id.Map.empty; + csubst_rev = Id.Map.empty; +} -let empty_csubst = (0, Int.Map.empty) +let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c = + (** Safe because this is a substitution *) + let c = EConstr.Unsafe.to_constr c in + let rec subst n c = match Constr.kind c with + | Rel m -> + if m <= n then c + else if m - n <= k then Int.Map.find (k - m + n) s + else mkRel (m - k) + | Var id -> + begin try Id.Map.find id v with Not_found -> c end + | _ -> Constr.map_with_binders succ subst n c + in + let c = if k = 0 && Id.Map.is_empty v then c else subst 0 c in + EConstr.of_constr c type ext_named_context = - csubst * (Id.t * EConstr.constr) list * - Id.Set.t * EConstr.named_context - -let push_var id (n, s) = - let s = Int.Map.add n (EConstr.mkVar id) s in - (succ n, s) - -let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) = + csubst * Id.Set.t * EConstr.named_context + +let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } = + let s = Int.Map.add n (Constr.mkVar id) s in + let r = Id.Map.add id (SRel n) r in + { csubst_len = succ n; csubst_var = v; csubst_rel = s; csubst_rev = r } + +(** Post-compose the substitution with the generator [src ↦ tgt] *) +let update_var src tgt subst = + let cur = + try Some (Id.Map.find src subst.csubst_rev) + with Not_found -> None + in + match cur with + | None -> + (** Missing keys stand for identity substitution [src ↦ src] *) + let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in + let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in + { subst with csubst_var; csubst_rev } + | Some bnd -> + let csubst_rev = Id.Map.add tgt bnd (Id.Map.remove src subst.csubst_rev) in + match bnd with + | SRel m -> + let csubst_rel = Int.Map.add m (Constr.mkVar tgt) subst.csubst_rel in + { subst with csubst_rel; csubst_rev } + | SVar id -> + let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in + { subst with csubst_var; csubst_rev } + +let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = @@ -330,18 +374,17 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) = binding named [id], we will keep [id0] (the name given by the user) and rename [id0] into [id] in the named 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 = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (subst2 subst vsubst) in + let subst = update_var id0 id subst in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) 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) + (push_var id0 subst, Id.Set.add id avoid, d :: nc) | _ -> (* spiwack: if [id0] is a section variable renaming it is 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 = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in - (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in + (push_var id subst, Id.Set.add id avoid, d :: nc) let push_rel_context_to_named_context env sigma typ = (* compute the instances relative to the named context and rel_context *) @@ -350,17 +393,17 @@ let push_rel_context_to_named_context env sigma typ = let ids = List.map get_id (named_context env) in let inst_vars = List.map mkVar ids in if List.is_empty (Environ.rel_context env) then - (named_context_val env, typ, inst_vars, empty_csubst, []) + (named_context_val env, typ, inst_vars, empty_csubst) else let avoid = List.fold_right Id.Set.add ids Id.Set.empty in let inst_rels = List.rev (rel_list 0 (nb_rel env)) in (* move the rel context to a named context and extend the named instance *) (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) - let (subst, vsubst, _, env) = + let (subst, _, env) = Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) - (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in - (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) in + (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) (*------------------------------------* * Entry points to define new evars * @@ -425,8 +468,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env evd typ in - let map c = subst2 subst vsubst c in + let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in + let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = match filter with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 37f5968ad8..923bf49a9c 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -222,14 +222,13 @@ val empty_csubst : csubst val csubst_subst : csubst -> constr -> constr type ext_named_context = - csubst * (Id.t * constr) list * - Id.Set.t * named_context + csubst * Id.Set.t * named_context val push_rel_decl_to_named_context : evar_map -> rel_declaration -> ext_named_context -> ext_named_context val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> - named_context_val * types * constr list * csubst * (Id.t*constr) list + named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/proofview.ml b/engine/proofview.ml index 0a64351950..47b9b406d8 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1086,7 +1086,7 @@ module Goal = struct end end - let enter_one f = + let enter_one ?(__LOC__=__LOC__) f = let open Proof in Comb.get >>= function | [goal] -> begin @@ -1097,7 +1097,8 @@ module Goal = struct let (e, info) = CErrors.push e in tclZERO ~info e end - | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *) + | _ -> + CErrors.anomaly Pp.(str __LOC__ ++ str " enter_one") let goals = Pv.get >>= fun step -> diff --git a/engine/proofview.mli b/engine/proofview.mli index 59728a2fd1..b02fde3a80 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -499,7 +499,7 @@ module Goal : sig (** Like {!enter}, but assumes exactly one goal under focus, raising *) (** a fatal error otherwise. *) - val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic + val enter_one : ?__LOC__:string -> ([ `LZ ] t -> 'a tactic) -> 'a tactic (** Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type. *) diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index a7e9003dbe..fcc242e074 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -19,8 +19,12 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) let number = [ '0'-'9' ]+ +let string = "\"" _+ "\"" + let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ +let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number + let dot_sep = '.' (space | eof) let utf8_extra_byte = [ '\x80' - '\xBF' ] @@ -67,7 +71,7 @@ and sentence initial stamp = parse stamp (utf8_lexeme_start lexbuf) Tags.Script.sentence; sentence true stamp lexbuf } - | undotted_sep { + | (vernac_control space+)* undotted_sep { (* Separators like { or } and bullets * - + are only active at the start of a sentence *) if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; diff --git a/kernel/constr.ml b/kernel/constr.ml index 5930cfadc6..1ff1fcc4c0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1178,8 +1178,3 @@ let hcons = Id.hcons) (* let hcons_types = hcons_constr *) - -(*******) -(* Type of abstract machine values *) -(** FIXME: nothing to do there *) -type values diff --git a/kernel/constr.mli b/kernel/constr.mli index 98bf713082..19ffa8fe30 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -459,7 +459,3 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr - -(**************************************) - -type values diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 712c66f11d..2bbb867cd4 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -15,7 +15,7 @@ open Util open Names open Constr -open Vm +open Vmvalues open Cemitcodes open Cbytecodes open Declarations diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 91bb30e7ed..fc935f6ee9 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -12,7 +12,7 @@ open Names open Constr open Pre_env -val val_of_constr : env -> constr -> values +val val_of_constr : env -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 28a09b81b0..722705bd70 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -796,18 +796,18 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in - (match subt with - | Subterm (s, wf) -> - (* We take the subterm specs of the constructor of the record *) - let wf_args = (dest_subterms wf).(0) in - (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in - Subterm (Strict, List.nth wf_args n) - | Dead_code -> Dead_code - | Not_subterm -> Not_subterm) + (match subt with + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | CoFix _ -> Not_subterm diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 917e4f6f14..749854b8cd 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -16,6 +16,7 @@ Cemitcodes Opaqueproof Declarations Entries +Vmvalues Nativevalues CPrimitives Declareops diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ffe19510a6..613b2f2ec0 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1919,15 +1919,17 @@ let compile_constant env sigma prefix ~interactive con cb = 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 c_uid|]) 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 c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) 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 diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 3ef15105ae..6c5e1cde5a 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,6 @@ open Util open Names -open Constr open Declarations module NamedDecl = Context.Named.Declaration @@ -50,7 +49,7 @@ type stratification = { } type val_kind = - | VKvalue of (values * Id.Set.t) CEphemeron.key + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 335ca1057f..a6b57bd1b3 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -36,9 +36,9 @@ type stratification = { type lazy_val -val force_lazy_val : lazy_val -> (values * Id.Set.t) option +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit type named_context_val = private { env_named_ctx : Context.Named.t; diff --git a/kernel/term.ml b/kernel/term.ml index aa88059524..fae990d45f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | CoFix of ('constr, 'types) pcofixpoint | Proj of projection * 'constr -type values = Constr.values +type values = Vmvalues.values (**********************************************************************) (** Redeclaration of functions from module Constr *) diff --git a/kernel/term.mli b/kernel/term.mli index f5cb72f4e8..c9a8cf6e1e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -572,8 +572,8 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Proj of projection * 'constr [@@ocaml.deprecated "Alias for Constr.kind_of_term"] -type values = Constr.values -[@@ocaml.deprecated "Alias for Constr.values"] +type values = Vmvalues.values +[@@ocaml.deprecated "Alias for Vmvalues.values"] val hash_constr : Constr.constr -> int [@@ocaml.deprecated "Alias for Constr.hash"] diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3ef297b1f4..8c76581478 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -3,6 +3,7 @@ open Names open Environ open Reduction open Vm +open Vmvalues open Csymtable let val_of_constr env c = diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 7f727df475..c3c9636e89 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -19,4 +19,4 @@ val vm_conv : conv_pb -> types kernel_conversion_function val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function (** Precompute a VM value from a constr *) -val val_of_constr : env -> constr -> values +val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/vm.ml b/kernel/vm.ml index 51101f88e4..352ea74a41 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,47 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Sorts -open Constr open Cbytecodes +open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" -(******************************************) -(* Utility Functions about Obj ************) -(******************************************) - -external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" -external offset : Obj.t -> int = "coq_offset" - -(*******************************************) -(* Initalization of the abstract machine ***) -(*******************************************) - -external init_vm : unit -> unit = "init_coq_vm" - -let _ = init_vm () - -(*******************************************) -(* Machine code *** ************************) -(*******************************************) - -type tcode -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) - -external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" -external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -external int_tcode : tcode -> int -> int = "coq_int_tcode" - -external accumulate : unit -> tcode = "accumulate_code" -let accumulate = accumulate () - -external is_accumulate : tcode -> bool = "coq_is_accumulate_code" - let popstop_tbl = ref (Array.init 30 mkPopStopCode) let popstop_code i = @@ -62,106 +28,6 @@ let popstop_code i = let stop = popstop_code 0 -(******************************************************) -(* Abstract data types and utility functions **********) -(******************************************************) - -(* Values of the abstract machine *) -let val_of_obj v = ((Obj.obj v):values) -let crazy_val = (val_of_obj (Obj.repr 0)) - -(* Abstract data *) -type vprod -type vfun -type vfix -type vcofix -type vblock -type arguments - -type vm_env -type vstack = values array - -type vswitch = { - sw_type_code : tcode; - sw_code : tcode; - sw_annot : annot_switch; - sw_stk : vstack; - sw_env : vm_env - } - -(* Representation of values *) -(* + Products : *) -(* - vprod = 0_[ dom | codom] *) -(* dom : values, codom : vfun *) -(* *) -(* + Functions have two representations : *) -(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) -(* C:tcode, fvi : values *) -(* Remark : a function and its environment is the same value. *) -(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) -(* *) -(* + Fixpoints : *) -(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) -(* One single block to represent all of the fixpoints, each fixpoint *) -(* is the pointer to the field holding the pointer to its code, and *) -(* the infix tag is used to know where the block starts. *) -(* - Partial application follows the scheme of partially applied *) -(* functions. Note: only fixpoints not having been applied to its *) -(* recursive argument are coded this way. When the rec. arg. is *) -(* applied, either it's a constructor and the fix reduces, or it's *) -(* and the fix is coded as an accumulator. *) -(* *) -(* + Cofixpoints : see cbytegen.ml *) -(* *) -(* + vblock's encode (non constant) constructors as in Ocaml, but *) -(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) -(* accumulators. *) -(* *) -(* + vm_env is the type of the machine environments (i.e. a function or *) -(* a fixpoint) *) -(* *) -(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) -(* - representation of [accu] : tag_[....] *) -(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) -(* -- 10_[accu|proj name] : a projection blocked by an accu *) -(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 12_[accu|vswitch] : a match blocked by an accu *) -(* -- 13_[fcofix] : a cofix function *) -(* -- 14_[fcofix|val] : a cofix function, val represent the value *) -(* of the function applied to arg1 ... argn *) -(* The [arguments] type, which is abstracted as an array, represents : *) -(* tag[ _ | _ |v1|... | vn] *) -(* Generally the first field is a code pointer. *) - -(* Do not edit this type without editing C code, especially "coq_values.h" *) - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(* Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix*arguments (* Possibly empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up = values - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t (************************************************) (* Abstract machine *****************************) @@ -178,389 +44,72 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" external interprete : tcode -> values -> vm_env -> int -> values = "coq_interprete_ml" - - (* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i)) (* Apply a value to arguments contained in [vargs] *) let apply_arguments vf vargs = let n = nargs vargs in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end (* Apply value [vf] to an array of argument values [varray] *) let apply_varray vf varray = let n = Array.length varray in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; (* The fun code of [vf] will make sure we have enough stack, so we put 0 here. *) push_vstack varray 0; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(*************************************************) -(* Destructors ***********************************) -(*************************************************) - -let uni_lvl_val (v : values) : Univ.Level.t = - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - CErrors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr ++ str ".") - -let rec whd_accu a stk = - let stk = - if Int.equal (Obj.size a) 2 then stk - else Zapp (Obj.obj a) :: stk in - let at = Obj.field a 1 in - match Obj.tag at with - | i when Int.equal i type_atom_tag -> - begin match stk with - | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) - | _ -> assert false - end - | i when i <= max_atom_tag -> - Vatom_stk(Obj.magic at, stk) - | i when Int.equal i proj_tag -> - let zproj = Zproj (Obj.obj (Obj.field at 0)) in - whd_accu (Obj.field at 1) (zproj :: stk) - | i when Int.equal i fix_app_tag -> - let fa = Obj.field at 1 in - let zfix = - Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in - whd_accu (Obj.field at 0) (zfix :: stk) - | i when Int.equal i switch_tag -> - let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in - whd_accu (Obj.field at 0) (zswitch :: stk) - | i when Int.equal i cofix_tag -> - let vcfx = Obj.obj (Obj.field at 0) in - let to_up = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcfx, to_up, None) - | [Zapp args] -> Vcofix(vcfx, to_up, Some args) - | _ -> assert false - end - | i when Int.equal i cofix_evaluated_tag -> - let vcofix = Obj.obj (Obj.field at 0) in - let res = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcofix, res, None) - | [Zapp args] -> Vcofix(vcofix, res, Some args) - | _ -> assert false - end - | tg -> - CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") - -external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" - -let whd_val : values -> whd = - fun v -> - let o = Obj.repr v in - if Obj.is_int o then Vconstr_const (Obj.obj o) - else - let tag = Obj.tag o in - if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) - else - if tag = Obj.closure_tag || tag = Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) - else - Vconstr_block(Obj.obj o) - -(**********************************************) -(* Constructors *******************************) -(**********************************************) - -let obj_of_atom : atom -> Obj.t = - fun a -> - let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); - Obj.set_field res 1 (Obj.repr a); - res - -(* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = - match str with - | Const_sorts s -> Obj.repr (Vsort s) - | Const_ind ind -> obj_of_atom (Aind ind) - | Const_proj p -> Obj.repr p - | Const_b0 tag -> Obj.repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) - done; - res - | Const_univ_level l -> Obj.repr (Vuniv_level l) - | Const_type u -> obj_of_atom (Atype u) - -let val_of_obj o = ((Obj.obj o) : values) - -let val_of_str_const str = val_of_obj (obj_of_str_const str) - -let val_of_atom a = val_of_obj (obj_of_atom a) - -let atom_of_proj kn v = - let r = Obj.new_block proj_tag 2 in - Obj.set_field r 0 (Obj.repr kn); - Obj.set_field r 1 (Obj.repr v); - ((Obj.obj r) : atom) - -let val_of_proj kn v = - val_of_atom (atom_of_proj kn v) - -module IdKeyHash = -struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal - open Hashset.Combine - let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) - | VarKey id -> combinesmall 2 (Id.hash id) - | RelKey i -> combinesmall 3 (Int.hash i) -end - -module KeyTable = Hashtbl.Make(IdKeyHash) - -let idkey_tbl = KeyTable.create 31 - -let val_of_idkey key = - try KeyTable.find idkey_tbl key - with Not_found -> - let v = val_of_atom (Aid key) in - KeyTable.add idkey_tbl key v; - v - -let val_of_rel k = val_of_idkey (RelKey k) - -let val_of_named id = val_of_idkey (VarKey id) - -let val_of_constant c = val_of_idkey (ConstKey c) - -external val_of_annot_switch : annot_switch -> values = "%identity" - +(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) - -(*************************************************) -(** Operations manipulating data types ***********) -(*************************************************) - -(* Functions over products *) - -let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) -let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) - -(* Functions over vfun *) - -external closure_arity : vfun -> int = "coq_closure_arity" - -let body_of_vfun k vf = +let reduce_fun k vf = let vargs = mkrel_vstack k 1 in - apply_varray (Obj.magic vf) vargs + apply_varray vf vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_varray (Obj.magic vf1) vargs in - let v2 = apply_varray (Obj.magic vf2) vargs in + let v1 = apply_varray vf1 vargs in + let v2 = apply_varray vf2 vargs in arity, v1, v2 -(* Functions over fixpoint *) - -let first o = (offset_closure o (offset o)) -let last o = (Obj.field o (Obj.size o - 1)) - -let current_fix vf = - (offset (Obj.repr vf) / 2) - -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - -let rec_args vf = - let fb = first (Obj.repr vf) in - let size = Obj.size (last fb) in - Array.init size (unsafe_rec_arg fb) - -exception FALSE - -let check_fix f1 f2 = - let i1, i2 = current_fix f1, current_fix f2 in - (* Checking starting point *) - if i1 = i2 then - let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in - let n = Obj.size (last fb1) in - (* Checking number of definitions *) - if n = Obj.size (last fb2) then - (* Checking recursive arguments *) - try - for i = 0 to n - 1 do - if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i - then raise FALSE - done; - true - with FALSE -> false - else false - else false - (* Functions over vfix *) -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" - -let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; - ref (Array.init len mkAccuCode) - -let relaccu_code i = - let len = Array.length !relaccu_tbl in - if i < len then !relaccu_tbl.(i) - else - begin - realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; - relaccu_tbl := - Array.init nl - (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); - !relaccu_tbl.(i) - end let reduce_fix k vf = - let fb = first (Obj.repr vf) in + let fb = first_fix vf in (* computing types *) - let fc_typ = ((Obj.obj (last fb)) : tcode array) in + let fc_typ = fix_types fb in let ndef = Array.length fc_typ in - let et = offset_closure fb (2*(ndef - 1)) in + let et = offset_closure_fix fb (2*(ndef - 1)) in let ftyp = Array.map - (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in + (fun c -> interprete c crazy_val et 0) fc_typ in (* Construction of the environment of fix bodies *) - let e = Obj.dup fb in - for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) - done; - let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in - let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); - Obj.set_field res 1 (offset_closure e (2*i)); - ((Obj.obj res) : vfun) in - (Array.init ndef fix_body, ftyp) - -(* Functions over vcofix *) - -let get_fcofix vcf i = - match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with - | Vcofix(vcfi, _, _) -> vcfi - | _ -> assert false - -let current_cofix vcf = - let ndef = Obj.size (last (Obj.repr vcf)) in - let rec find_cofix pos = - if pos < ndef then - if get_fcofix vcf pos == vcf then pos - else find_cofix (pos+1) - else raise Not_found in - try find_cofix 0 - with Not_found -> assert false - -let check_cofix vcf1 vcf2 = - (current_cofix vcf1 = current_cofix vcf2) && - (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + (mk_fix_body k ndef fb, ftyp) let reduce_cofix k vcf = - let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in + let fc_typ = cofix_types vcf in let ndef = Array.length fc_typ in let ftyp = (* Evaluate types *) - Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in + Array.map (fun c -> interprete c crazy_val (cofix_env vcf) 0) fc_typ in (* Construction of the environment of cofix bodies *) - let e = Obj.dup (Obj.repr vcf) in - for i = 0 to ndef - 1 do - Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) - done; - - let cofix_body i = - let vcfi = get_fcofix vcf i in - let c = Obj.field (Obj.repr vcfi) 0 in - Obj.set_field e 0 c; - let atom = Obj.new_block cofix_tag 1 in - let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); - Obj.set_field self 1 (Obj.repr atom); - apply_varray (Obj.obj e) [|Obj.obj self|] in - (Array.init ndef cofix_body, ftyp) - - -(* Functions over vblock *) - -let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) -let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) -let bfield b i = - if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) - else invalid_arg "Vm.bfield" - - -(* Functions over vswitch *) - -let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl - -let case_info sw = sw.sw_annot.ci + (mk_cofix_body apply_varray k ndef vcf, ftyp) let type_of_switch sw = (* The fun code of types will make sure we have enough stack, so we put 0 @@ -568,20 +117,6 @@ let type_of_switch sw = push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 -let branch_arg k (tag,arity) = - if Int.equal arity 0 then ((Obj.magic tag):values) - else - let b, ofs = - if tag < last_variant_tag then Obj.new_block tag arity, 0 - else - let b = Obj.new_block last_variant_tag (arity+1) in - Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); - b,1 in - for i = ofs to ofs + arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done; - val_of_obj b - let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then @@ -603,8 +138,8 @@ let branch_of_switch k sw = (* t = a stk --> t v *) let rec apply_stack a stk v = match stk with - | [] -> apply_varray a [|v|] - | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v + | [] -> apply_varray (fun_of_val a) [|v|] + | Zapp args :: stk -> apply_stack (apply_arguments (fun_of_val a) args) stk v | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v | Zfix(f,args) :: stk -> let a,stk = @@ -615,7 +150,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args+ nargs args') in a, stk | _ -> @@ -623,7 +158,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) in a, stk in apply_stack a stk v @@ -634,50 +169,21 @@ let apply_whd k whd = let v = val_of_rel k in match whd with | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false - | Vfun f -> body_of_vfun k f + | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; push_val v; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) 0 + interprete (fix_code f) (fix_val f) (fix_env f) 0 | Vfix(f, Some args) -> push_ra stop; push_val v; push_arguments args; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) | Vcofix(_,to_up,_) -> push_ra stop; push_val v; - interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 + interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let rec pr_atom a = - Pp.(match a with - | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Constant.print c - | RelKey i -> str "#" ++ int i - | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") -and pr_whd w = - Pp.(match w with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" - | Vuniv_level _ -> assert false) -and pr_stack stk = - Pp.(match stk with - | [] -> str "[]" - | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) -and pr_zipper z = - Pp.(match z with - | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index bc38452d4f..c6d92ba266 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -6,118 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Constr -open Cbytecodes +open Vmvalues (** Debug printing *) val set_drawinstr : unit -> unit -(** Machine code *) - -type tcode - -(** Values *) - -type vprod -type vfun -type vfix -type vcofix -type vblock -type vswitch -type arguments - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(** Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix * arguments (** might be empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t - -(** For debugging purposes only *) - -val pr_atom : atom -> Pp.t -val pr_whd : whd -> Pp.t -val pr_stack : stack -> Pp.t - -(** Constructors *) - -val val_of_str_const : structured_constant -> values -val val_of_rel : int -> values -val val_of_named : Id.t -> values -val val_of_constant : Constant.t -> values - -external val_of_annot_switch : annot_switch -> values = "%identity" - -(** Destructors *) - -val whd_val : values -> whd -val uni_lvl_val : values -> Univ.Level.t - -(** Arguments *) - -val nargs : arguments -> int -val arg : arguments -> int -> values - -(** Product *) - -val dom : vprod -> values -val codom : vprod -> vfun - -(** Function *) - -val body_of_vfun : int -> vfun -> values -val decompose_vfun2 : int -> vfun -> vfun -> int * values * values - -(** Fix *) - -val current_fix : vfix -> int -val check_fix : vfix -> vfix -> bool -val rec_args : vfix -> int array val reduce_fix : int -> vfix -> vfun array * values array (** bodies , types *) -(** CoFix *) - -val current_cofix : vcofix -> int -val check_cofix : vcofix -> vcofix -> bool val reduce_cofix : int -> vcofix -> values array * values array (** bodies , types *) -(** Block *) +val type_of_switch : vswitch -> values -val btag : vblock -> int -val bsize : vblock -> int -val bfield : vblock -> int -> values +val branch_of_switch : int -> vswitch -> (int * values) array -(** Switch *) +val reduce_fun : int -> vfun -> values -val check_switch : vswitch -> vswitch -> bool -val case_info : vswitch -> case_info -val type_of_switch : vswitch -> values -val branch_of_switch : int -> vswitch -> (int * values) array +(** [decompose_vfun2 k f1 f2] takes two functions [f1] and [f2] at current + DeBruijn level [k], with [n] lambdas in common, returns [n] and the reduced + bodies under those lambdas. *) +val decompose_vfun2 : int -> vfun -> vfun -> int * values * values (** Apply a value *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml new file mode 100644 index 0000000000..1102cdec18 --- /dev/null +++ b/kernel/vmvalues.ml @@ -0,0 +1,525 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Sorts +open Cbytecodes + +(*******************************************) +(* Initalization of the abstract machine ***) +(* Necessary for [relaccu_tbl] *) +(*******************************************) + +external init_vm : unit -> unit = "init_coq_vm" + +let _ = init_vm () + +(******************************************************) +(* Abstract data types and utility functions **********) +(******************************************************) + +(* Values of the abstract machine *) +type values +let val_of_obj v = ((Obj.obj v):values) +let crazy_val = (val_of_obj (Obj.repr 0)) + +(* Abstract data *) +type vprod +type vfun +type vfix +type vcofix +type vblock +type arguments + +let fun_val v = (Obj.magic v : values) +let fix_val v = (Obj.magic v : values) +let cofix_upd_val v = (Obj.magic v : values) + +type vm_env +let fun_env v = (Obj.magic v : vm_env) +let fix_env v = (Obj.magic v : vm_env) +let cofix_env v = (Obj.magic v : vm_env) +let cofix_upd_env v = (Obj.magic v : vm_env) +type vstack = values array + +let fun_of_val v = (Obj.magic v : vfun) + +(*******************************************) +(* Machine code *** ************************) +(*******************************************) + +type tcode + +external mkAccuCode : int -> tcode = "coq_makeaccu" +external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" + +let tcode_of_obj v = ((Obj.obj v):tcode) +let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) +let fix_code v = fun_code v +let cofix_upd_code v = fun_code v + + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +(* Representation of values *) +(* + Products : *) +(* - vprod = 0_[ dom | codom] *) +(* dom : values, codom : vfun *) +(* *) +(* + Functions have two representations : *) +(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) +(* C:tcode, fvi : values *) +(* Remark : a function and its environment is the same value. *) +(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* *) +(* + Fixpoints : *) +(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) +(* One single block to represent all of the fixpoints, each fixpoint *) +(* is the pointer to the field holding the pointer to its code, and *) +(* the infix tag is used to know where the block starts. *) +(* - Partial application follows the scheme of partially applied *) +(* functions. Note: only fixpoints not having been applied to its *) +(* recursive argument are coded this way. When the rec. arg. is *) +(* applied, either it's a constructor and the fix reduces, or it's *) +(* and the fix is coded as an accumulator. *) +(* *) +(* + Cofixpoints : see cbytegen.ml *) +(* *) +(* + vblock's encode (non constant) constructors as in Ocaml, but *) +(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) +(* accumulators. *) +(* *) +(* + vm_env is the type of the machine environments (i.e. a function or *) +(* a fixpoint) *) +(* *) +(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) +(* - representation of [accu] : tag_[....] *) +(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) +(* -- 10_[accu|proj name] : a projection blocked by an accu *) +(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 12_[accu|vswitch] : a match blocked by an accu *) +(* -- 13_[fcofix] : a cofix function *) +(* -- 14_[fcofix|val] : a cofix function, val represent the value *) +(* of the function applied to arg1 ... argn *) +(* The [arguments] type, which is abstracted as an array, represents : *) +(* tag[ _ | _ |v1|... | vn] *) +(* Generally the first field is a code pointer. *) + +(* Do not edit this type without editing C code, especially "coq_values.h" *) + +type atom = + | Aid of Vars.id_key + | Aind of inductive + | Atype of Univ.Universe.t + +(* Zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix*arguments (* Possibly empty *) + | Zswitch of vswitch + | Zproj of Constant.t (* name of the projection *) + +type stack = zipper list + +type to_update = values + +type whd = + | Vsort of Sorts.t + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_update * arguments option + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack + | Vuniv_level of Univ.Level.t + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else invalid_arg + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i)) + +(*************************************************) +(* Destructors ***********************************) +(*************************************************) + +let uni_lvl_val (v : values) : Univ.Level.t = + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + CErrors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr ++ str ".") + +let rec whd_accu a stk = + let stk = + if Int.equal (Obj.size a) 2 then stk + else Zapp (Obj.obj a) :: stk in + let at = Obj.field a 1 in + match Obj.tag at with + | i when Int.equal i type_atom_tag -> + begin match stk with + | [Zapp args] -> + let u = ref (Obj.obj (Obj.field at 0)) in + for i = 0 to nargs args - 1 do + u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) + done; + Vsort (Type !u) + | _ -> assert false + end + | i when i <= max_atom_tag -> + Vatom_stk(Obj.magic at, stk) + | i when Int.equal i proj_tag -> + let zproj = Zproj (Obj.obj (Obj.field at 0)) in + whd_accu (Obj.field at 1) (zproj :: stk) + | i when Int.equal i fix_app_tag -> + let fa = Obj.field at 1 in + let zfix = + Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in + whd_accu (Obj.field at 0) (zfix :: stk) + | i when Int.equal i switch_tag -> + let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in + whd_accu (Obj.field at 0) (zswitch :: stk) + | i when Int.equal i cofix_tag -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + begin match stk with + | [] -> Vcofix(vcfx, to_up, None) + | [Zapp args] -> Vcofix(vcfx, to_up, Some args) + | _ -> assert false + end + | i when Int.equal i cofix_evaluated_tag -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + begin match stk with + | [] -> Vcofix(vcofix, res, None) + | [Zapp args] -> Vcofix(vcofix, res, Some args) + | _ -> assert false + end + | tg -> + CErrors.anomaly + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") + +external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" +external is_accumulate : tcode -> bool = "coq_is_accumulate_code" +external int_tcode : tcode -> int -> int = "coq_int_tcode" +external accumulate : unit -> tcode = "accumulate_code" +let accumulate = accumulate () + +let whd_val : values -> whd = + fun v -> + let o = Obj.repr v in + if Obj.is_int o then Vconstr_const (Obj.obj o) + else + let tag = Obj.tag o in + if tag = accu_tag then + ( + if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) + else + if is_accumulate (fun_code o) then whd_accu o [] + else Vprod(Obj.obj o)) + else + if tag = Obj.closure_tag || tag = Obj.infix_tag then + (match kind_of_closure o with + | 0 -> Vfun(Obj.obj o) + | 1 -> Vfix(Obj.obj o, None) + | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) + | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) + else + Vconstr_block(Obj.obj o) + +(**********************************************) +(* Constructors *******************************) +(**********************************************) + +let obj_of_atom : atom -> Obj.t = + fun a -> + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr accumulate); + Obj.set_field res 1 (Obj.repr a); + res + +(* obj_of_str_const : structured_constant -> Obj.t *) +let rec obj_of_str_const str = + match str with + | Const_sorts s -> Obj.repr (Vsort s) + | Const_ind ind -> obj_of_atom (Aind ind) + | Const_proj p -> Obj.repr p + | Const_b0 tag -> Obj.repr tag + | Const_bn(tag, args) -> + let len = Array.length args in + let res = Obj.new_block tag len in + for i = 0 to len - 1 do + Obj.set_field res i (obj_of_str_const args.(i)) + done; + res + | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_type u -> obj_of_atom (Atype u) + +let val_of_obj o = ((Obj.obj o) : values) + +let val_of_str_const str = val_of_obj (obj_of_str_const str) + +let val_of_atom a = val_of_obj (obj_of_atom a) + +let atom_of_proj kn v = + let r = Obj.new_block proj_tag 2 in + Obj.set_field r 0 (Obj.repr kn); + Obj.set_field r 1 (Obj.repr v); + ((Obj.obj r) : atom) + +let val_of_proj kn v = + val_of_atom (atom_of_proj kn v) + +module IdKeyHash = +struct + type t = Constant.t tableKey + let equal = Names.eq_table_key Constant.equal + open Hashset.Combine + let hash = function + | ConstKey c -> combinesmall 1 (Constant.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) +end + +module KeyTable = Hashtbl.Make(IdKeyHash) + +let idkey_tbl = KeyTable.create 31 + +let val_of_idkey key = + try KeyTable.find idkey_tbl key + with Not_found -> + let v = val_of_atom (Aid key) in + KeyTable.add idkey_tbl key v; + v + +let val_of_rel k = val_of_idkey (RelKey k) + +let val_of_named id = val_of_idkey (VarKey id) + +let val_of_constant c = val_of_idkey (ConstKey c) + +external val_of_annot_switch : annot_switch -> values = "%identity" + +(*************************************************) +(** Operations manipulating data types ***********) +(*************************************************) + +(* Functions over products *) + +let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) +let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) + +(* Functions over vfun *) + +external closure_arity : vfun -> int = "coq_closure_arity" + +(* Functions over fixpoint *) + +external offset : Obj.t -> int = "coq_offset" +external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" +external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" + +let first o = (offset_closure o (offset o)) +let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) + +let last o = (Obj.field o (Obj.size o - 1)) +let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) + +let current_fix vf = - (offset (Obj.repr vf) / 2) + +let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) + +let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 + +let rec_args vf = + let fb = first (Obj.repr vf) in + let size = Obj.size (last fb) in + Array.init size (unsafe_rec_arg fb) + +exception FALSE + +let check_fix f1 f2 = + let i1, i2 = current_fix f1, current_fix f2 in + (* Checking starting point *) + if i1 = i2 then + let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in + let n = Obj.size (last fb1) in + (* Checking number of definitions *) + if n = Obj.size (last fb2) then + (* Checking recursive arguments *) + try + for i = 0 to n - 1 do + if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i + then raise FALSE + done; + true + with FALSE -> false + else false + else false + +external atom_rel : unit -> atom array = "get_coq_atom_tbl" +external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" + +let relaccu_tbl = + let atom_rel = atom_rel() in + let len = Array.length atom_rel in + for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; + ref (Array.init len mkAccuCode) + +let relaccu_code i = + let len = Array.length !relaccu_tbl in + if i < len then !relaccu_tbl.(i) + else + begin + realloc_atom_rel i; + let atom_rel = atom_rel () in + let nl = Array.length atom_rel in + for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; + relaccu_tbl := + Array.init nl + (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); + !relaccu_tbl.(i) + end + +let mk_fix_body k ndef fb = + let e = Obj.dup (Obj.repr fb) in + for i = 0 to ndef - 1 do + Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + done; + let fix_body i = + let jump_grabrec c = offset_tcode c 2 in + let c = jump_grabrec (unsafe_fb_code fb i) in + let res = Obj.new_block Obj.closure_tag 2 in + Obj.set_field res 0 (Obj.repr c); + Obj.set_field res 1 (offset_closure e (2*i)); + ((Obj.obj res) : vfun) in + Array.init ndef fix_body + +(* Functions over vcofix *) + +let get_fcofix vcf i = + match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with + | Vcofix(vcfi, _, _) -> vcfi + | _ -> assert false + +let current_cofix vcf = + let ndef = Obj.size (last (Obj.repr vcf)) in + let rec find_cofix pos = + if pos < ndef then + if get_fcofix vcf pos == vcf then pos + else find_cofix (pos+1) + else raise Not_found in + try find_cofix 0 + with Not_found -> assert false + +let check_cofix vcf1 vcf2 = + (current_cofix vcf1 = current_cofix vcf2) && + (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + +let mk_cofix_body apply_varray k ndef vcf = + let e = Obj.dup (Obj.repr vcf) in + for i = 0 to ndef - 1 do + Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) + done; + + let cofix_body i = + let vcfi = get_fcofix vcf i in + let c = Obj.field (Obj.repr vcfi) 0 in + Obj.set_field e 0 c; + let atom = Obj.new_block cofix_tag 1 in + let self = Obj.new_block accu_tag 2 in + Obj.set_field self 0 (Obj.repr accumulate); + Obj.set_field self 1 (Obj.repr atom); + apply_varray (Obj.obj e) [|Obj.obj self|] in + Array.init ndef cofix_body + +(* Functions over vblock *) + +let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) +let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) +let bfield b i = + if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) + else invalid_arg "Vm.bfield" + + +(* Functions over vswitch *) + +let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + +let branch_arg k (tag,arity) = + if Int.equal arity 0 then ((Obj.magic tag):values) + else + let b, ofs = + if tag < last_variant_tag then Obj.new_block tag arity, 0 + else + let b = Obj.new_block last_variant_tag (arity+1) in + Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); + b,1 in + for i = ofs to ofs + arity - 1 do + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) + done; + val_of_obj b + +(* Printing *) + +let rec pr_atom a = + Pp.(match a with + | Aid c -> str "Aid(" ++ (match c with + | ConstKey c -> Constant.print c + | RelKey i -> str "#" ++ int i + | _ -> str "...") ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" + | Atype _ -> str "Atype(") +and pr_whd w = + Pp.(match w with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" + | Vuniv_level _ -> assert false) +and pr_stack stk = + Pp.(match stk with + | [] -> str "[]" + | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) +and pr_zipper z = + Pp.(match z with + | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" + | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch s -> str "Zswitch(...)" + | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli new file mode 100644 index 0000000000..350f71372f --- /dev/null +++ b/kernel/vmvalues.mli @@ -0,0 +1,144 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Cbytecodes + +(** Values *) + +type values +type vm_env +type vprod +type vfun +type vfix +type vcofix +type vblock +type arguments +type vstack = values array +type to_update + +val fun_val : vfun -> values +val fix_val : vfix -> values +val cofix_upd_val : to_update -> values + +val fun_env : vfun -> vm_env +val fix_env : vfix -> vm_env +val cofix_env : vcofix -> vm_env +val cofix_upd_env : to_update -> vm_env + +(** Cast a value known to be a function, unsafe in general *) +val fun_of_val : values -> vfun + +val crazy_val : values + +(** Machine code *) + +type tcode + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +external mkAccuCode : int -> tcode = "coq_makeaccu" + +val fun_code : vfun -> tcode +val fix_code : vfix -> tcode +val cofix_upd_code : to_update -> tcode + +type atom = + | Aid of Vars.id_key + | Aind of inductive + | Atype of Univ.Universe.t + +(** Zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix * arguments (** might be empty *) + | Zswitch of vswitch + | Zproj of Constant.t (* name of the projection *) + +type stack = zipper list + +type whd = + | Vsort of Sorts.t + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_update * arguments option + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack + | Vuniv_level of Univ.Level.t + +(** For debugging purposes only *) + +val pr_atom : atom -> Pp.t +val pr_whd : whd -> Pp.t +val pr_stack : stack -> Pp.t + +(** Constructors *) + +val val_of_str_const : structured_constant -> values +val val_of_rel : int -> values +val val_of_named : Id.t -> values +val val_of_constant : Constant.t -> values +val val_of_proj : Constant.t -> values -> values +val val_of_atom : atom -> values + +external val_of_annot_switch : annot_switch -> values = "%identity" + +(** Destructors *) + +val whd_val : values -> whd +val uni_lvl_val : values -> Univ.Level.t + +(** Arguments *) + +val nargs : arguments -> int +val arg : arguments -> int -> values + +(** Product *) + +val dom : vprod -> values +val codom : vprod -> vfun + +(** Fun *) +external closure_arity : vfun -> int = "coq_closure_arity" + +(** Fix *) + +val current_fix : vfix -> int +val check_fix : vfix -> vfix -> bool +val rec_args : vfix -> int array +val first_fix : vfix -> vfix +val fix_types : vfix -> tcode array +val cofix_types : vcofix -> tcode array +external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +val mk_fix_body : int -> int -> vfix -> vfun array + +(** CoFix *) + +val current_cofix : vcofix -> int +val check_cofix : vcofix -> vcofix -> bool +val mk_cofix_body : (vfun -> vstack -> values) -> int -> int -> vcofix -> values array + +(** Block *) + +val btag : vblock -> int +val bsize : vblock -> int +val bfield : vblock -> int -> values + +(** Switch *) + +val check_switch : vswitch -> vswitch -> bool +val branch_arg : int -> Cbytecodes.tag * int -> values diff --git a/lib/flags.ml b/lib/flags.ml index ee4c0734af..01361dad55 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,18 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let with_modified_ref r nf f x = +(* If [restore] is false, whenever [f] modifies the ref, we will + preserve the modification. *) +let with_modified_ref ?(restore=true) r nf f x = let old_ref = !r in r := nf !r; - try let res = f x in r := old_ref; res + try + let pre = !r in + let res = f x in + (* If r was modified don't restore its old value *) + if restore || pre == !r then r := old_ref; + res with reraise -> let reraise = Backtrace.add_backtrace reraise in r := old_ref; Exninfo.iraise reraise -let with_option o f x = with_modified_ref o (fun _ -> true) f x -let without_option o f x = with_modified_ref o (fun _ -> false) f x +let with_option o f x = with_modified_ref ~restore:false o (fun _ -> true) f x +let without_option o f x = with_modified_ref ~restore:false o (fun _ -> false) f x let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x +(* hide the [restore] option as internal *) +let with_modified_ref r nf f x = with_modified_ref r nf f x + let with_options ol f x = let vl = List.map (!) ol in let () = List.iter (fun r -> r := true) ol in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5a9248d478..d6fd2f2a0f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -190,7 +190,6 @@ let with_full_print f a = Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; - Impargs.make_contextual_implicit_args false; Dumpglob.pause (); try let res = f a in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 192eca63bb..e42576d95b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk = let cofixp_reducible flgs _ stk = if red_set flgs fCOFIX then match stk with - | (CASE _ | APP(_,CASE _)) -> true + | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true | _ -> false else false diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b930c5db83..92dab24e26 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -70,7 +70,7 @@ let get_extra env sigma = let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) - (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } let rel_context env = rel_context env.env @@ -90,12 +90,11 @@ let push_rel_context sigma ctx env = { let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = - let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in - let (subst, vsubst, _, nc) = Lazy.force env.extra in - let typ' = subst2 subst vsubst typ in + let (subst, _, nc) = Lazy.force env.extra in + let typ' = csubst_subst subst typ in let instance = inst_rels @ inst_vars in let sign = val_of_named_context nc in let sigma = !evdref in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index e395bdbc63..b21fbf0eb2 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -15,6 +15,7 @@ open Vars open Environ open Inductive open Reduction +open Vmvalues open Vm open Context.Rel.Declaration @@ -134,7 +135,7 @@ let build_case_type dep p realargs c = (* La fonction de normalisation *) -let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t +let rec nf_val env sigma v t = nf_whd env sigma (Vmvalues.whd_val v) t and nf_vtype env sigma v = nf_val env sigma v crazy_type @@ -144,7 +145,7 @@ and nf_whd env sigma whd typ = | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in - let vc = body_of_vfun (nb_rel env) (codom p) in + let vc = reduce_fun (nb_rel env) (codom p) in let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in mkProd(name,dom,codom) | Vfun f -> nf_fun env sigma f typ @@ -191,7 +192,7 @@ and nf_univ_args ~nb_univs mk env sigma stk = else match stk with | Zapp args :: _ -> let inst = - Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i)) + Array.init nb_univs (fun i -> uni_lvl_val (arg args i)) in Univ.Instance.of_array inst | _ -> assert false @@ -254,7 +255,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in - let ci = case_info sw in + let ci = sw.sw_annot.Cbytecodes.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -266,14 +267,14 @@ and nf_predicate env sigma ind mip params v pT = match whd_val v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in - let vb = body_of_vfun k f 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, _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in @@ -307,7 +308,7 @@ and nf_bargs env sigma b ofs t = and nf_fun env sigma f typ = let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = try decompose_prod env typ with DestKO -> diff --git a/stm/stm.ml b/stm/stm.ml index 5f4fe6565d..07d8b39bd2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -26,31 +26,50 @@ open Vernacexpr module AsyncOpts = struct - let async_proofs_n_workers = ref 1 - let async_proofs_n_tacworkers = ref 2 - type cache = Force - let async_proofs_cache : cache option ref = ref None - type async_proofs = APoff | APonLazy | APon - let async_proofs_mode = ref APoff + type tac_error_filter = [ `None | `Only of string list | `All ] - let async_proofs_private_flags = ref None - let async_proofs_full = ref false - let async_proofs_never_reopen_branch = ref false + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; - type tac_error_filter = [ `None | `Only of string list | `All ] - let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) - let async_proofs_cmd_error_resilience = ref true + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; + + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } - let async_proofs_delegation_threshold = ref 0.03 + let default_opts = { + async_proofs_n_workers = 1; + async_proofs_n_tacworkers = 2; + async_proofs_cache = None; + + async_proofs_mode = APoff; + + async_proofs_private_flags = None; + async_proofs_full = false; + async_proofs_never_reopen_branch = false; + + async_proofs_tac_error_resilience = `Only [ "curly" ]; + async_proofs_cmd_error_resilience = true; + async_proofs_delegation_threshold = 0.03; + } + + let cur_opt = ref default_opts end open AsyncOpts -let async_proofs_is_master () = - !async_proofs_mode = APon && +let async_proofs_is_master opt = + opt.async_proofs_mode = APon && !Flags.async_proofs_worker_id = "master" (* Protect against state changes *) @@ -558,7 +577,7 @@ end = struct (* {{{ *) | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- s; - if async_proofs_is_master () then Hooks.(call state_ready id) + if async_proofs_is_master !cur_opt then Hooks.(call state_ready id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -1150,7 +1169,7 @@ end = struct (* {{{ *) " the \"-async-proofs-cache force\" option to Coq.")) let undo_vernac_classifier v = - if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force + if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match Vernacprop.under_control v with @@ -1286,7 +1305,7 @@ let prev_node { id } = let cur_node id = mk_doc_node id (VCS.visit id) let is_block_name_enabled name = - match !async_proofs_tac_error_resilience with + match !cur_opt.async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l @@ -1294,7 +1313,7 @@ let is_block_name_enabled name = let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in if is_block_name_enabled name && - (async_proofs_is_master () || Flags.async_proofs_is_worker ()) + (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () @@ -1396,7 +1415,7 @@ end = struct (* {{{ *) let task_match age t = match age, t with | Fresh, BuildProof { t_states } -> - not !async_proofs_full || + not !cur_opt.async_proofs_full || List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l @@ -1433,7 +1452,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !async_proofs_full || t_drop + if !cur_opt.async_proofs_full || t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, @@ -1607,8 +1626,8 @@ end = struct (* {{{ *) let queue = ref None let init () = - if async_proofs_is_master () then - queue := Some (TaskQueue.create !async_proofs_n_workers) + if async_proofs_is_master !cur_opt then + queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers) else queue := Some (TaskQueue.create 0) @@ -2074,7 +2093,7 @@ end = struct (* {{{ *) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch let init () = queue := Some (TaskQueue.create - (if !async_proofs_full then 1 else 0)) + (if !cur_opt.async_proofs_full then 1 else 0)) end (* }}} *) @@ -2090,14 +2109,14 @@ let async_policy () = let open Flags in if is_universe_polymorphism () then false else if VCS.is_interactive () = `Yes then - (async_proofs_is_master () || !async_proofs_mode = APonLazy) + (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else - (VCS.is_vio_doc () || !async_proofs_mode <> APoff) + (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff) let delegate name = - get_hint_bp_time name >= !async_proofs_delegation_threshold + get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !async_proofs_full + || !cur_opt.async_proofs_full let warn_deprecated_nested_proofs = CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" @@ -2212,7 +2231,7 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached_and_valid id) || !async_proofs_full) + (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2294,9 +2313,9 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if !async_proofs_tac_error_resilience = `None || - (async_proofs_is_master () && - !async_proofs_mode = APoff) + if !cur_opt.async_proofs_tac_error_resilience = `None || + (async_proofs_is_master !cur_opt && + !cur_opt.async_proofs_mode = APoff) then f () else try f () @@ -2305,9 +2324,9 @@ let known_state ?(redefine_qed=false) ~cache id = error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = - if not !async_proofs_cmd_error_resilience || - (async_proofs_is_master () && - !async_proofs_mode = APoff) + if not !cur_opt.async_proofs_cmd_error_resilience || + (async_proofs_is_master !cur_opt && + !cur_opt.async_proofs_mode = APoff) then f x else try f x @@ -2353,10 +2372,10 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !async_proofs_n_tacworkers view.next id x) + !cur_opt.async_proofs_n_tacworkers view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } - when async_proofs_is_master () -> (fun () -> + when async_proofs_is_master !cur_opt -> (fun () -> reach view.next; Query.vernac_interp ~cancel_switch view.next id x ), cache, false @@ -2370,7 +2389,7 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - (match !async_proofs_mode with + (match !cur_opt.async_proofs_mode with | APon | APonLazy -> resilient_command reach view.next | APoff -> reach view.next); @@ -2500,7 +2519,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !async_proofs_cache = Some Force then `Yes + if !cur_opt.async_proofs_cache = Some Force then `Yes else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; @@ -2516,6 +2535,7 @@ end (* }}} *) type stm_init_options = { doc_type : stm_doc_type; require_libs : (string * string option * bool option) list; + stm_options : AsyncOpts.stm_opt; (* fb_handler : Feedback.feedback -> unit; iload_path : (string list * string * bool) list; @@ -2531,10 +2551,11 @@ let doc_type_module_name (std : stm_doc_type) = *) let init_core () = - if !async_proofs_mode = APon then Control.enable_thread_delay := true; + if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let new_doc { doc_type ; require_libs } = +let new_doc { doc_type ; stm_options; require_libs } = + let load_objs libs = let rq_file (dir, from, exp) = let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in @@ -2543,6 +2564,9 @@ let new_doc { doc_type ; require_libs } = List.(iter rq_file (rev libs)) in + (* Set the options from the new documents *) + AsyncOpts.cur_opt := stm_options; + (* We must reset the whole state before creating a document! *) State.restore_root_state (); @@ -2570,10 +2594,10 @@ let new_doc { doc_type ; require_libs } = State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); - if async_proofs_is_master () then begin + if async_proofs_is_master !cur_opt then begin stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); - let opts = match !async_proofs_private_flags with + let opts = match !cur_opt.async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in begin try @@ -2772,7 +2796,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = - if !async_proofs_full then `QueryQueue (ref false) + if !cur_opt.async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && may_pierce_opaque (Vernacprop.under_control x.expr) @@ -3104,7 +3128,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !async_proofs_full then + if not !cur_opt.async_proofs_full then Reach.known_state ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in @@ -3120,7 +3144,7 @@ let edit_at ~doc id = | _, Some _, None -> assert false | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && is_pure qed_id && not !async_proofs_never_reopen_branch + if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some { qed = qed_id }, Some(mode,bn) -> diff --git a/stm/stm.mli b/stm/stm.mli index 587b756422..8b5581979d 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -10,6 +10,33 @@ open Names (** state-transaction-machine interface *) +(* Flags *) +module AsyncOpts : sig + + type cache = Force + type async_proofs = APoff | APonLazy | APon + type tac_error_filter = [ `None | `Only of string list | `All ] + + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; + + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; + + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } + + val default_opts : stm_opt + +end + (** The STM doc type determines some properties such as what uncompleted proofs are allowed and recording of aux files. *) type stm_doc_type = @@ -21,6 +48,7 @@ type stm_doc_type = type stm_init_options = { doc_type : stm_doc_type; require_libs : (string * string option * bool option) list; + stm_options : AsyncOpts.stm_opt; (* fb_handler : Feedback.feedback -> unit; iload_path : (string list * string * bool) list; @@ -228,27 +256,3 @@ val get_all_proof_names : doc:doc -> Id.t list (** Enable STM debugging *) val stm_debug : bool ref - -(* Flags *) -module AsyncOpts : sig - - (* Defaults for worker creation *) - val async_proofs_n_workers : int ref - val async_proofs_n_tacworkers : int ref - - type async_proofs = APoff | APonLazy | APon - val async_proofs_mode : async_proofs ref - - type cache = Force - val async_proofs_cache : cache option ref - - val async_proofs_private_flags : string option ref - val async_proofs_full : bool ref - val async_proofs_never_reopen_branch : bool ref - - type tac_error_filter = [ `None | `Only of string list | `All ] - val async_proofs_tac_error_resilience : tac_error_filter ref - val async_proofs_cmd_error_resilience : bool ref - val async_proofs_delegation_threshold : float ref - -end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9e4d132d4e..cfadfc5353 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1569,7 +1569,7 @@ let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = - let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env sigma gl in + let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in let (ev, _) = destEvar sigma t in diff --git a/test-suite/bugs/closed/5286.v b/test-suite/bugs/closed/5286.v new file mode 100644 index 0000000000..98d4e5c968 --- /dev/null +++ b/test-suite/bugs/closed/5286.v @@ -0,0 +1,9 @@ +Set Primitive Projections. + +CoInductive R := mkR { p : unit }. + +CoFixpoint foo := mkR tt. + +Check (eq_refl tt : p foo = tt). +Check (eq_refl tt <: p foo = tt). +Check (eq_refl tt <<: p foo = tt). diff --git a/test-suite/bugs/closed/6534.v b/test-suite/bugs/closed/6534.v new file mode 100644 index 0000000000..f5013994c5 --- /dev/null +++ b/test-suite/bugs/closed/6534.v @@ -0,0 +1,7 @@ +Goal forall x : nat, x = x. +Proof. +intros x. +refine ((fun x x => _ tt) tt tt). +let t := match goal with [ |- ?P ] => P end in +let _ := type of t in +idtac. diff --git a/test-suite/coqchk/include.v b/test-suite/coqchk/include.v new file mode 100644 index 0000000000..6232c1b80f --- /dev/null +++ b/test-suite/coqchk/include.v @@ -0,0 +1,11 @@ +(* See https://github.com/coq/coq/issues/5747 *) +Module Type S. +End S. + +Module N. +Inductive I := . +End N. + +Module M : S. + Include N. +End M. diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 176dfb3c93..b3b5375bf8 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,13 +59,23 @@ let load_rcfile ~time doc sid = doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) -let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml = - let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in - Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init +let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = + let open Mltop in + let add_ml = if with_ml then AddRecML else AddNoML in + { recursive = true; + path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } + } -let add_userlib_path ~unix_path = - Mltop.add_rec_path Mltop.AddRecML ~unix_path - ~coq_root:Libnames.default_root_prefix ~implicit:false +let build_userlib_path ~unix_path = + let open Mltop in + { recursive = true; + path_spec = VoPath { + unix_path; + coq_path = Libnames.default_root_prefix; + has_ml = Mltop.AddRecML; + implicit = false; + } + } (* Options -I, -I-as, and -R of the command line *) let includes = ref [] @@ -74,51 +84,65 @@ let push_include s alias implicit = let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes +let ml_path_if c p = + let open Mltop in + let f x = { recursive = false; path_spec = MlPath x } in + if c then List.map f p else [] + (* Initializes the LoadPath *) let init_load_path ~load_init = + let open Mltop in let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in let coqpath = Envars.coqpath in - let coq_root = Names.DirPath.make [Libnames.coq_root] in - (* NOTE: These directories are searched from last to first *) - (* first, developer specific directory to open *) - if Coq_config.local then - Mltop.add_ml_dir (coqlib/"dev"); - (* main loops *) - if Coq_config.local || !Flags.boot then begin - Mltop.add_ml_dir (coqlib/"stm"); - Mltop.add_ml_dir (coqlib/"ide") - end; - if System.exists_dir (coqlib/"toploop") then - Mltop.add_ml_dir (coqlib/"toploop"); - (* then standard library *) - add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; - (* then plugins *) - add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; - (* then user-contrib *) - if Sys.file_exists user_contrib then - add_userlib_path ~unix_path:user_contrib; - (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) - List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; - (* then directories in COQPATH *) - List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; - (* then current directory (not recursively!) *) - Mltop.add_ml_dir "."; - Loadpath.add_load_path "." Libnames.default_root_prefix ~implicit:false; - (* additional loadpath, given with options -Q and -R *) - List.iter - (fun (unix_path, coq_root, implicit) -> - Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit) - (List.rev !includes); - (* additional ml directories, given with option -I *) - List.iter Mltop.add_ml_dir (List.rev !ml_includes) + let coq_path = Names.DirPath.make [Libnames.coq_root] in + + (* NOTE: These directories are searched from last to first *) + (* first, developer specific directory to open *) + ml_path_if Coq_config.local [coqlib/"dev"] @ + + (* main loops *) + ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @ + ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] @ + + (* then standard library and plugins *) + [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; + build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @ + + (* then user-contrib *) + (if Sys.file_exists user_contrib then + [build_userlib_path ~unix_path:user_contrib] else [] + ) @ + + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @ + + (* then current directory (not recursively!) *) + [ { recursive = false; + path_spec = VoPath { unix_path = "."; + coq_path = Libnames.default_root_prefix; + implicit = false; + has_ml = AddTopML } + } ] @ + + (* additional loadpaths, given with options -Q and -R *) + List.map + (fun (unix_path, coq_path, implicit) -> + { recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) + (List.rev !includes) @ + + (* additional ml directories, given with option -I *) + List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes) (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = + let open Mltop in + let lp s = { recursive = false; path_spec = MlPath s } in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl]) + Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) in - Mltop.add_ml_dir (Envars.coqlib ()); + Mltop.add_coq_path (lp (Envars.coqlib ())); List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c3fd727541..089847f5d9 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -19,7 +19,5 @@ val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) val push_ml_include : string -> unit - -val init_load_path : load_init:bool -> unit - +val init_load_path : load_init:bool -> Mltop.coq_path list val init_ocaml_path : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a3a4e20af8..572092e746 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -291,6 +291,8 @@ let ensure_exists f = if not (Sys.file_exists f) then compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) +let top_stm_options = ref Stm.AsyncOpts.default_opts + (* Compile a vernac file *) let compile ~time ~verbosely ~f_in ~f_out = let check_pending_proofs () = @@ -314,7 +316,8 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; - require_libs = require_libs () + require_libs = require_libs (); + stm_options = !top_stm_options; }) in let doc, sid = load_init_vernaculars ~time doc sid in @@ -349,7 +352,8 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; - require_libs = require_libs () + require_libs = require_libs (); + stm_options = !top_stm_options; }) in let doc, sid = load_init_vernaculars ~time doc sid in @@ -489,11 +493,11 @@ exception NoCoqLib let usage batch = begin - try - Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); - Coqinit.init_load_path ~load_init:!load_init; - with NoCoqLib -> usage_no_coqlib () + try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) + with NoCoqLib -> usage_no_coqlib () end; + let lp = Coqinit.init_load_path ~load_init:!load_init in + List.iter Mltop.add_coq_path lp; if batch then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex @@ -650,23 +654,47 @@ let parse_args arglist = (* Options with one arg *) |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) |"-async-proofs" -> - Stm.AsyncOpts.async_proofs_mode := get_async_proofs_mode opt (next()) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) + } |"-async-proofs-j" -> - Stm.AsyncOpts.async_proofs_n_workers := (get_int opt (next ())) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) + } |"-async-proofs-cache" -> - Stm.AsyncOpts.async_proofs_cache := get_cache opt (next ()) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) + } |"-async-proofs-tac-j" -> - Stm.AsyncOpts.async_proofs_n_tacworkers := (get_int opt (next ())) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) + } |"-async-proofs-worker-priority" -> WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()) |"-async-proofs-private-flags" -> - Stm.AsyncOpts.async_proofs_private_flags := Some (next ()); + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); + } |"-async-proofs-tactic-error-resilience" -> - Stm.AsyncOpts.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()); + } |"-async-proofs-command-error-resilience" -> - Stm.AsyncOpts.async_proofs_cmd_error_resilience := get_bool opt (next ()) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) + } |"-async-proofs-delegation-threshold" -> - Stm.AsyncOpts.async_proofs_delegation_threshold:= get_float opt (next ()) + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) + } |"-worker-id" -> set_worker_id opt (next ()) |"-compat" -> let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in @@ -706,9 +734,15 @@ let parse_args arglist = |"-async-queries-always-delegate" |"-async-proofs-always-delegate" |"-async-proofs-full" -> - Stm.AsyncOpts.async_proofs_full := true; + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_full = true; + } |"-async-proofs-never-reopen-branch" -> - Stm.AsyncOpts.async_proofs_never_reopen_branch := true; + top_stm_options := + { !top_stm_options with + Stm.AsyncOpts.async_proofs_never_reopen_branch = true; + } |"-batch" -> set_batch_mode () |"-test-mode" -> Flags.test_mode := true |"-beautify" -> Flags.beautify := true @@ -776,7 +810,8 @@ let init_toplevel arglist = if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - Coqinit.init_load_path ~load_init:!load_init; + let lp = Coqinit.init_load_path ~load_init:!load_init in + List.iter Mltop.add_coq_path lp; Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in if not (CList.is_empty extras) then begin @@ -811,7 +846,8 @@ let init_toplevel arglist = try let doc, sid = Stm.(new_doc { doc_type = Interactive !toplevel_name; - require_libs = require_libs () + require_libs = require_libs (); + stm_options = !top_stm_options; }) in Some (load_init_vernaculars ~time:!measure_time doc sid) with any -> flush_all(); fatal_error any diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 00554e3bae..053b9d0705 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -184,10 +184,28 @@ let warn_cannot_open_path = type add_ml = AddNoML | AddTopML | AddRecML -let add_rec_path add_ml ~unix_path ~coq_root ~implicit = +type vo_path_spec = { + unix_path : string; + coq_path : Names.DirPath.t; + implicit : bool; + has_ml : add_ml; +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in if exists_dir unix_path then - let dirs = all_subdirs ~unix_path in - let prefix = Names.DirPath.repr coq_root in + let dirs = if recursive then all_subdirs ~unix_path else [] in + let prefix = Names.DirPath.repr lp.coq_path in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in @@ -195,17 +213,23 @@ let add_rec_path add_ml ~unix_path ~coq_root ~implicit = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let () = match add_ml with + let () = match lp.has_ml with | AddNoML -> () | AddTopML -> add_ml_dir unix_path | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in let add (path, dir) = Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~implicit coq_root + Loadpath.add_load_path unix_path ~implicit lp.coq_path else warn_cannot_open_path unix_path +let add_coq_path { recursive; path_spec } = match path_spec with + | VoPath lp -> + add_vo_path ~recursive lp + | MlPath dir -> + if recursive then add_rec_ml_dir dir else add_ml_dir dir + (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = if Filename.check_suffix name ".cmo" then diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 324a66d382..e44a7c2438 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -42,14 +42,26 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the ML paths *) -val add_ml_dir : string -> unit -val add_rec_ml_dir : string -> unit - +(** Adds a path to the Coq and ML paths *) type add_ml = AddNoML | AddTopML | AddRecML -(** Adds a path to the Coq and ML paths *) -val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit +type vo_path_spec = { + unix_path : string; (* Filesystem path contaning vo/ml files *) + coq_path : Names.DirPath.t; (* Coq prefix for the path *) + implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +val add_coq_path : coq_path -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3358951f4c..1a02a22a5c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -905,9 +905,11 @@ let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = + let open Mltop in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in - Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit + add_coq_path { recursive = true; + path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } } let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) @@ -915,7 +917,8 @@ let vernac_remove_loadpath path = (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) + let open Mltop in + add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~atts l = let local = make_locality atts.locality in |