aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comFixpoint.ml25
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comProgramFixpoint.ml32
-rw-r--r--vernac/g_vernac.mlg20
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/ppvernac.ml21
-rw-r--r--vernac/proof_using.ml3
-rw-r--r--vernac/proof_using.mli3
-rw-r--r--vernac/vernacentries.ml18
-rw-r--r--vernac/vernacexpr.ml15
11 files changed, 73 insertions, 72 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2aadbd224f..1912646ffd 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -329,16 +329,27 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
pstate
-let extract_decreasing_argument limit = function
- | (na,CStructRec) -> na
- | (na,_) when not limit -> na
+let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
+ | CStructRec na -> na
+ | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
+ | CMeasureRec (None,_,_) when not structonly ->
+ user_err Pp.(str "Decreasing argument must be specificed in measure clause.")
| _ -> user_err Pp.(str
- "Only structural decreasing is supported for a non-Program Fixpoint")
+ "Well-founded induction requires Program Fixpoint or Function.")
-let extract_fixpoint_components limit l =
+let extract_fixpoint_components ~structonly l =
let fixl, ntnl = List.split l in
let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
- let ann = extract_decreasing_argument limit ann in
+ (* This is a special case: if there's only one binder, we pick it as the
+ recursive argument if none is provided. *)
+ let ann = Option.map (fun ann -> match bl, ann with
+ | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+ CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+ | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+ CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+ | _, x -> x) ann
+ in
+ let ann = Option.map (extract_decreasing_argument ~structonly) ann in
{fix_name = id; fix_annot = ann; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
fixl, List.flatten ntnl
@@ -356,7 +367,7 @@ let check_safe () =
flags.check_universes && flags.check_guarded
let do_fixpoint ~ontop local poly l =
- let fixl, ntns = extract_fixpoint_components true l in
+ let fixl, ntns = extract_fixpoint_components ~structonly:true l in
let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
let possible_indexes =
List.map compute_possible_guardness_evidences info in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 15ff5f4498..5937842f17 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -62,7 +62,7 @@ val interp_recursive :
(** Extracting the semantical components out of the raw syntax of
(co)fixpoints declarations *)
-val extract_fixpoint_components : bool ->
+val extract_fixpoint_components : structonly:bool ->
(fixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 350b2d2945..20a2db7ca2 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -85,7 +85,7 @@ let rec telescope sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -304,22 +304,26 @@ let do_program_recursive local poly fixkind fixl ntns =
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
- | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
- let recarg =
- match n with
- | Some n -> mkIdentC n.CAst.v
- | None ->
- user_err ~hdr:"do_program_fixpoint"
- (str "Recursive argument required for well-founded fixpoints")
- in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
+ | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+ let recarg = mkIdentC n.CAst.v in
+ build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn
- | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
- build_wellfounded (id, pl, n, bl, typ, out_def def) poly
+ | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+ (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *)
+ let r = match n, r with
+ | Some id, None ->
+ let loc = id.CAst.loc in
+ Some (CAst.make ?loc @@ CRef(qualid_of_ident ?loc id.CAst.v,None))
+ | Some _, Some _ ->
+ user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
+ | _, _ -> r
+ in
+ build_wellfounded (id, pl, bl, typ, out_def def) poly
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
- | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
- let fixl,ntns = extract_fixpoint_components true l in
- let fixkind = Obligations.IsFixpoint g in
+ | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
+ let fixl,ntns = extract_fixpoint_components ~structonly:true l in
+ let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
do_program_recursive local poly fixkind fixl ntns
| _, _ ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1533d0ccd3..3f491d1dd4 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -875,10 +875,10 @@ GRAMMAR EXTEND Gram
GLOBAL: command query_command class_rawexpr gallina_ext;
gallina_ext:
- [ [ IDENT "Export"; "Set"; table = option_table; v = option_value ->
+ [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting ->
{ VernacSetOption (true, table, v) }
| IDENT "Export"; IDENT "Unset"; table = option_table ->
- { VernacUnsetOption (true, table) }
+ { VernacSetOption (true, table, OptionUnset) }
] ];
command:
@@ -943,10 +943,10 @@ GRAMMAR EXTEND Gram
{ VernacAddMLPath (true, dir) }
(* For acting on parameter tables *)
- | "Set"; table = option_table; v = option_value ->
+ | "Set"; table = option_table; v = option_setting ->
{ VernacSetOption (false, table, v) }
| IDENT "Unset"; table = option_table ->
- { VernacUnsetOption (false, table) }
+ { VernacSetOption (false, table, OptionUnset) }
| IDENT "Print"; IDENT "Table"; table = option_table ->
{ VernacPrintOption table }
@@ -1057,10 +1057,10 @@ GRAMMAR EXTEND Gram
| IDENT "Library"; qid = global -> { LocateLibrary qid }
| IDENT "Module"; qid = global -> { LocateModule qid } ] ]
;
- option_value:
- [ [ -> { BoolValue true }
- | n = integer -> { IntValue (Some n) }
- | s = STRING -> { StringValue s } ] ]
+ option_setting:
+ [ [ -> { OptionSetTrue }
+ | n = integer -> { OptionSetInt n }
+ | s = STRING -> { OptionSetString s } ] ]
;
option_ref_value:
[ [ id = global -> { QualidRefValue id }
@@ -1130,10 +1130,10 @@ GRAMMAR EXTEND Gram
(* Tactic Debugger *)
| IDENT "Debug"; IDENT "On" ->
- { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) }
+ { VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue) }
| IDENT "Debug"; IDENT "Off" ->
- { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) }
+ { VernacSetOption (false, ["Ltac";"Debug"], OptionUnset) }
(* registration of a custom reduction *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 07194578c1..1b1c618dc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,7 +295,7 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of lident option list
| IsCoFixpoint
type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -486,7 +486,7 @@ let rec lam_index n t acc =
lam_index n b (succ acc)
| _ -> raise Not_found
-let compute_possible_guardness_evidences (n,_) fixbody fixtype =
+let compute_possible_guardness_evidences n fixbody fixtype =
match n with
| Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
| None ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1b7b1ec90..d25daeed9c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -70,7 +70,7 @@ type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of lident option list
| IsCoFixpoint
val add_mutual_definitions :
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b602e134da..4e4d431e89 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -173,15 +173,10 @@ open Pputils
pr_opt (prlist_with_sep sep pr_option_ref_value) b
let pr_set_option a b =
- let pr_opt_value = function
- | IntValue None -> assert false
- (* This should not happen because of the grammar *)
- | IntValue (Some n) -> spc() ++ int n
- | StringValue s -> spc() ++ str s
- | StringOptValue None -> mt()
- | StringOptValue (Some s) -> spc() ++ str s
- | BoolValue b -> mt()
- in pr_printoption a None ++ pr_opt_value b
+ pr_printoption a None ++ (match b with
+ | OptionUnset | OptionSetTrue -> mt()
+ | OptionSetInt n -> spc() ++ int n
+ | OptionSetString s -> spc() ++ quote (str s))
let pr_opt_hintbases l = match l with
| [] -> mt()
@@ -1140,15 +1135,11 @@ open Pputils
hov 1 (keyword "Strategy" ++ spc() ++
hv 0 (prlist_with_sep sep pr_line l))
)
- | VernacUnsetOption (export, na) ->
- let export = if export then keyword "Export" ++ spc () else mt () in
- return (
- hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
- )
| VernacSetOption (export, na,v) ->
let export = if export then keyword "Export" ++ spc () else mt () in
+ let set = if v == OptionUnset then "Unset" else "Set" in
return (
- hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
+ hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v)
)
| VernacAddOption (na,l) ->
return (
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 526845084a..1d089d0a55 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -172,11 +172,12 @@ let value = ref None
let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
+let proof_using_opt_name = ["Default";"Proof";"Using"]
let () =
Goptions.(declare_stringopt_option
{ optdepr = false;
optname = "default value for Proof using";
- optkey = ["Default";"Proof";"Using"];
+ optkey = proof_using_opt_name;
optread = (fun () -> Option.map using_to_string !value);
optwrite = (fun b -> value := Option.map using_from_string b);
})
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index 7d1110aaa2..702043a4a9 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -21,3 +21,6 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit
val suggest_variable : Environ.env -> Names.Id.t -> unit
val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
+
+val proof_using_opt_name : string list
+(** For the stm *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c24b9ec75..3a305c3b61 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1707,18 +1707,17 @@ let get_option_locality export local =
let vernac_set_option0 ~local export key opt =
let locality = get_option_locality export local in
match opt with
- | StringValue s -> set_string_option_value_gen ~locality key s
- | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
- | StringOptValue None -> unset_option_value_gen ~locality key
- | IntValue n -> set_int_option_value_gen ~locality key n
- | BoolValue b -> set_bool_option_value_gen ~locality key b
+ | OptionUnset -> unset_option_value_gen ~locality key
+ | OptionSetString s -> set_string_option_value_gen ~locality key s
+ | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n)
+ | OptionSetTrue -> set_bool_option_value_gen ~locality key true
let vernac_set_append_option ~local export key s =
let locality = get_option_locality export local in
set_string_option_append_value_gen ~locality key s
let vernac_set_option ~local export table v = match v with
-| StringValue s ->
+| OptionSetString s ->
(* We make a special case for warnings because appending is their
natural semantics *)
if CString.List.equal table ["Warnings"] then
@@ -1731,10 +1730,6 @@ let vernac_set_option ~local export table v = match v with
vernac_set_option0 ~local export table v
| _ -> vernac_set_option0 ~local export table v
-let vernac_unset_option ~local export key =
- let locality = get_option_locality export local in
- unset_option_value_gen ~locality key
-
let vernac_add_option key lv =
let f = function
| StringRefValue s -> (get_string_table key)#add s
@@ -2462,9 +2457,6 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
| VernacSetOption (export, key,v) ->
vernac_set_option ~local:(only_locality atts) export key v;
pstate
- | VernacUnsetOption (export, key) ->
- vernac_unset_option ~local:(only_locality atts) export key;
- pstate
| VernacRemoveOption (key,v) ->
unsupported_attributes atts;
vernac_remove_option key v;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ebfc473522..d0dae1aa53 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -109,11 +109,11 @@ type onlyparsing_flag = Flags.compat_version option
which this notation is trying to be compatible with *)
type locality_flag = bool (* true = Local *)
-type option_value = Goptions.option_value =
- | BoolValue of bool
- | IntValue of int option
- | StringValue of string
- | StringOptValue of string option
+type option_setting =
+ | OptionUnset
+ | OptionSetTrue
+ | OptionSetInt of int
+ | OptionSetString of string
type option_ref_value =
| StringRefValue of string
@@ -129,7 +129,7 @@ type definition_expr =
* constr_expr option
type fixpoint_expr =
- ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+ ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option
type cofixpoint_expr =
ident_decl * local_binder_expr list * constr_expr * constr_expr option
@@ -363,8 +363,7 @@ type nonrec vernac_expr =
| VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
| VernacSetStrategy of
(Conv_oracle.level * qualid or_by_notation list) list
- | VernacUnsetOption of export_flag * Goptions.option_name
- | VernacSetOption of export_flag * Goptions.option_name * option_value
+ | VernacSetOption of export_flag * Goptions.option_name * option_setting
| VernacAddOption of Goptions.option_name * option_ref_value list
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:59:08 +0000