aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xdev/tools/merge-pr.sh18
-rw-r--r--interp/constrextern.ml12
-rw-r--r--intf/vernacexpr.ml15
-rw-r--r--parsing/g_vernac.ml415
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--printing/ppvernac.ml5
-rw-r--r--stm/stm.ml17
-rw-r--r--stm/vernac_classifier.ml10
-rw-r--r--test-suite/output/Projections.out2
-rw-r--r--test-suite/output/Projections.v11
-rw-r--r--vernac/vernacentries.ml21
11 files changed, 62 insertions, 68 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 2f6f1af54..ecfdfab94 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -61,10 +61,12 @@ fi
# Fetching PR metadata
-TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title')
+PRDATA=$(curl -s "$API/pulls/$PR")
+
+TITLE=$(echo "$PRDATA" | jq -r '.title')
info "title for PR $PR is ${BLUE}$TITLE"
-BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
+BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label')
info "PR $PR targets branch ${BLUE}$BASE_BRANCH"
CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
@@ -107,17 +109,17 @@ fi;
# Sanity check: CI failed
-STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
+STATUS=$(curl -s "$API/commits/$COMMIT/status")
-if [ "$STATUS" != "success" ]; then
- error "CI unsuccessful on ${BLUE}$(curl -s "$API/commits/$COMMIT/status" |
+if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then
+ error "CI unsuccessful on ${BLUE}$(echo "$STATUS" |
jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')"
ask_confirmation
fi;
# Sanity check: has labels named "needs:"
-NEEDS_LABELS=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
+NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)')
if [ "$NEEDS_LABELS" != "[]" ]; then
error "needs:something labels still present: ${BLUE}$NEEDS_LABELS"
ask_confirmation
@@ -125,7 +127,7 @@ fi
# Sanity check: has milestone
-MILESTONE=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title')
+MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title')
if [ "$MILESTONE" = "null" ]; then
error "no milestone set, please set one"
ask_confirmation
@@ -133,7 +135,7 @@ fi
# Sanity check: has kind
-KIND=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
+KIND=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
if [ "$KIND" = "[]" ]; then
error "no kind:something label set, please set one"
ask_confirmation
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 48ddd9496..bb5fd5294 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -589,11 +589,17 @@ let explicitize inctx impl (cf,f) args =
let expl () =
match ip with
| Some i ->
- if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
- raise Expl
+ (* Careful: It is possible to have declared implicits ending
+ before the principal argument *)
+ let is_impl =
+ try is_status_implicit (List.nth impl (i-1))
+ with Failure _ -> false
+ in
+ if is_impl
+ then raise Expl
else
let (args1,args2) = List.chop i args in
- let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
+ let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
let ip = Some (List.length args1) in
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 0e84a07aa..06f969f19 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -297,13 +297,9 @@ type inline =
type module_ast_inl = module_ast * inline
type module_binder = bool option * lident list * module_ast_inl
-(** Cumulativity can be set globally, locally or unset locally and it
- can not enabled at all. *)
-type cumulative_inductive_parsing_flag =
- | GlobalCumulativity
- | GlobalNonCumulativity
- | LocalCumulativity
- | LocalNonCumulativity
+(** [Some b] if locally enabled/disabled according to [b], [None] if
+ we should use the global flag. *)
+type vernac_cumulative = VernacCumulative | VernacNonCumulative
(** {6 The type of vernacular expressions} *)
@@ -338,7 +334,7 @@ type nonrec vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
inline * (ident_decl list * constr_expr) with_coercion list
- | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
| VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
| VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
| VernacScheme of (lident option * scheme) list
@@ -501,14 +497,13 @@ type vernac_type =
| VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
- | VtQuery of vernac_part_of_script * Feedback.route_id
+ | VtQuery
(* To be removed *)
| VtMeta
| VtUnknown
and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
and vernac_start = string * opacity_guarantee * Id.t list
and vernac_sideff_type = Id.t list
-and vernac_part_of_script = bool
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8b445985b..593dcbf58 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -161,20 +161,10 @@ GEXTEND Gram
| IDENT "Let"; id = identref; b = def_body ->
VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b)
(* Gallina inductive declarations *)
- | cum = cumulativity_token; priv = private_token; f = finite_token;
+ | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
let (k,f) = f in
let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
- let cum =
- match cum with
- Some true -> LocalCumulativity
- | Some false -> LocalNonCumulativity
- | None ->
- if Flags.is_polymorphic_inductive_cumulativity () then
- GlobalCumulativity
- else
- GlobalNonCumulativity
- in
VernacInductive (cum, priv,f,indl)
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
VernacFixpoint (NoDischarge, recs)
@@ -257,7 +247,8 @@ GEXTEND Gram
| IDENT "Class" -> (Class true,BiFinite) ] ]
;
cumulativity_token:
- [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ]
+ [ [ IDENT "Cumulative" -> VernacCumulative
+ | IDENT "NonCumulative" -> VernacNonCumulative ] ]
;
private_token:
[ [ IDENT "Private" -> true | -> false ] ]
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 49f7aae43..319b410df 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1512,7 +1512,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1527,7 +1527,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index bbf0e2b60..7eb8396ac 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -767,8 +767,9 @@ open Decl_kinds
if p then
let cm =
match cum with
- | GlobalCumulativity | LocalCumulativity -> "Cumulative"
- | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+ | Some VernacCumulative -> "Cumulative"
+ | Some VernacNonCumulative -> "NonCumulative"
+ | None -> ""
in
cm ^ " " ^ kind
else kind
diff --git a/stm/stm.ml b/stm/stm.ml
index a0305efee..ba0a2017a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2782,16 +2782,9 @@ let process_transaction ?(newtip=Stateid.fresh ())
| VtMeta, _ ->
let id, w = Backtrack.undo_vernac_classifier expr in
process_back_meta_command ~newtip ~head id x w
+
(* Query *)
- | VtQuery (false,route), VtNow ->
- let query_sid = VCS.cur_tip () in
- (try
- let st = Vernacstate.freeze_interp_state `No in
- ignore(stm_vernac_interp ~route query_sid st x)
- with e ->
- let e = CErrors.push e in
- Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok
- | VtQuery (true, route), w ->
+ | VtQuery, w ->
let id = VCS.new_node ~id:newtip () in
let queue =
if !cur_opt.async_proofs_full then `QueryQueue (ref false)
@@ -2803,9 +2796,6 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.commit id (mkTransCmd x [] false queue);
Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
- | VtQuery (false,_), VtLater ->
- anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
-
(* Proof *)
| VtStartProof (mode, guarantee, names), w ->
let id = VCS.new_node ~id:newtip () in
@@ -3048,8 +3038,9 @@ let query ~doc ~at ~route s =
let { CAst.loc; v=ast } = parse_sentence ~doc at s in
let indentation, strlen = compute_indentation ?loc at in
CWarnings.set_current_loc loc;
+ let st = State.get_cached at in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
- ignore(process_transaction aast (VtQuery (false,route), VtNow))
+ ignore(stm_vernac_interp ~route at st aast)
done;
with
| End_of_input -> ()
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index eecee40df..c08cc6e36 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -16,8 +16,6 @@ open Vernacexpr
let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
-let string_of_in_script b = if b then " (inside script)" else ""
-
let string_of_parallel = function
| `Yes (solve,abs) ->
"par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -34,7 +32,7 @@ let string_of_vernac_type = function
"ProofStep " ^ string_of_parallel parallel ^
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
- | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+ | VtQuery -> "Query"
| VtMeta -> "Meta "
let string_of_vernac_when = function
@@ -70,7 +68,7 @@ let classify_vernac e =
| VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
(* Query *)
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
- | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
+ | VernacCheckMayEval _ -> VtQuery, VtLater
(* ProofStep *)
| VernacProof _
| VernacFocus _ | VernacUnfocus
@@ -205,7 +203,7 @@ let classify_vernac e =
static_control_classifier ~poly e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier ~poly e with
- | ( VtQuery _ | VtProofStep _ | VtSideff _
+ | ( VtQuery | VtProofStep _ | VtSideff _
| VtProofMode _ | VtMeta), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
@@ -214,6 +212,6 @@ let classify_vernac e =
in
static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
-let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
+let classify_as_query = VtQuery, VtLater
let classify_as_sideeff = VtSideff [], VtLater
let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
new file mode 100644
index 000000000..e9c28faf1
--- /dev/null
+++ b/test-suite/output/Projections.out
@@ -0,0 +1,2 @@
+fun S : store => S.(store_funcs)
+ : store -> host_func
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
new file mode 100644
index 000000000..098a518dc
--- /dev/null
+++ b/test-suite/output/Projections.v
@@ -0,0 +1,11 @@
+
+Set Printing Projections.
+
+Class HostFunction := host_func : Type.
+
+Section store.
+ Context `{HostFunction}.
+ Record store := { store_funcs : host_func }.
+End store.
+
+Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0e8ca2289..b44c7cccb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl =
if not status then Feedback.feedback Feedback.AddedAxiom
let should_treat_as_cumulative cum poly =
- if poly then
- match cum with
- | GlobalCumulativity | LocalCumulativity -> true
- | GlobalNonCumulativity | LocalNonCumulativity -> false
- else
- match cum with
- | GlobalCumulativity | GlobalNonCumulativity -> false
- | LocalCumulativity ->
- user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
- | LocalNonCumulativity ->
- user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+ match cum with
+ | Some VernacCumulative ->
+ if poly then true
+ else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+ | Some VernacNonCumulative ->
+ if poly then false
+ else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+ | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
let vernac_record cum k poly finite struc binders sort nameopt cfs =
let is_cumulative = should_treat_as_cumulative cum poly in
@@ -565,7 +562,6 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
indicates whether the type is inductive, co-inductive or
neither. *)
let vernac_inductive ~atts cum lo finite indl =
- let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -602,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl =
| _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
in
let indl = List.map unpack indl in
+ let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
let vernac_fixpoint ~atts discharge l =
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-07 19:14:44 +0000