From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 10:18:48 +0100 Subject: "Standardizing" the name LocalPatten into LocalRawPattern. --- intf/constrexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 0cbb29575d..1499ed70e9 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -125,7 +125,7 @@ and recursion_order_expr = and local_binder = | LocalRawDef of Name.t located * constr_expr | LocalRawAssum of Name.t located list * binder_kind * constr_expr - | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option + | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = constr_expr list * (** for constr subterms *) -- cgit v1.2.3 From a1e5a87c9d4368fe17d93988b010acfb1c96771b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 17:03:10 +0100 Subject: Cleaning phase around local binder at glob level: Aligned the type binder_data to the naming scheme used in (raw) local_binder and Rel.Declaration.t. Made some code factorization. Still to do: align type Glob_term.glob_binder to the Assum/Def format too. Note: this includes fix of anomaly with 'pat in cofix (dec77f282). --- intf/glob_term.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'intf') diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b3159c860c..f83ff97b21 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -78,6 +78,8 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr) of [t] are members of [il]. *) and cases_clauses = cases_clause list +type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) + (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken from the Ltac environment. *) -- cgit v1.2.3 From 8965549b994262a27f5dd204d9c4012501d1a040 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 17:10:43 +0100 Subject: Standardized the order of constructors for binders: Assum then Def. --- intf/constrexpr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 1499ed70e9..f7aa722799 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -123,8 +123,8 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder = - | LocalRawDef of Name.t located * constr_expr | LocalRawAssum of Name.t located list * binder_kind * constr_expr + | LocalRawDef of Name.t located * constr_expr | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = -- cgit v1.2.3 From 68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:00:07 +0100 Subject: Merging glob_binder and glob_decl. --- intf/glob_term.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'intf') diff --git a/intf/glob_term.mli b/intf/glob_term.mli index f83ff97b21..b3159c860c 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -78,8 +78,6 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr) of [t] are members of [il]. *) and cases_clauses = cases_clause list -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) - (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken from the Ltac environment. *) -- cgit v1.2.3 From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:21:51 +0100 Subject: Renaming local_binder into local_binder_expr. This is a bit long, but it is to keep a symmetry with constr_expr. --- intf/constrexpr.mli | 8 ++++---- intf/vernacexpr.mli | 18 +++++++++--------- 2 files changed, 13 insertions(+), 13 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index f7aa722799..c2ace9dc27 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -111,10 +111,10 @@ and binder_expr = and fix_expr = Id.t located * (Id.t located option * recursion_order_expr) * - local_binder list * constr_expr * constr_expr + local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t located * local_binder list * constr_expr * constr_expr + Id.t located * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -122,7 +122,7 @@ and recursion_order_expr = | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) (** Anonymous defs allowed ?? *) -and local_binder = +and local_binder_expr = | LocalRawAssum of Name.t located list * binder_kind * constr_expr | LocalRawDef of Name.t located * constr_expr | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option @@ -130,7 +130,7 @@ and local_binder = and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder list list (** for binders subexpressions *) + local_binder_expr list list (** for binders subexpressions *) type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8827bc132e..a9f7106395 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -175,15 +175,15 @@ type plident = lident * lident list option type sort_expr = glob_sort type definition_expr = - | ProveBody of local_binder list * constr_expr - | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type fixpoint_expr = - plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = - plident * local_binder list * constr_expr * constr_expr option + plident * local_binder_expr list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -202,14 +202,14 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - plident with_coercion * local_binder list * constr_expr option * inductive_kind * + plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - plident * local_binder list * constr_expr option * constructor_expr list + plident * local_binder_expr list * constr_expr option * constructor_expr list type proof_expr = - plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -370,12 +370,12 @@ type vernac_expr = (* Type classes *) | VernacInstance of bool * (* abstract instance *) - local_binder list * (* super *) + local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) hint_info_expr - | VernacContext of local_binder list + | VernacContext of local_binder_expr list | VernacDeclareInstances of (reference * hint_info_expr) list (* instances names, priorities and patterns *) -- cgit v1.2.3 From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- intf/constrexpr.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index c2ace9dc27..d1b5697d75 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -123,9 +123,9 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = - | LocalRawAssum of Name.t located list * binder_kind * constr_expr - | LocalRawDef of Name.t located * constr_expr - | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option + | CLocalAssum of Name.t located list * binder_kind * constr_expr + | CLocalDef of Name.t located * constr_expr + | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = constr_expr list * (** for constr subterms *) -- cgit v1.2.3 From 71cd2838bf3eb23a8f29df973d8012ebe2ec77b0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 20:21:14 +0100 Subject: Using the same type of binders for interning and externing. Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml. --- intf/glob_term.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'intf') diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b3159c860c..ce862cf8a7 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -78,6 +78,11 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr) of [t] are members of [il]. *) and cases_clauses = cases_clause list +type extended_glob_local_binder = + | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr + | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr + (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken from the Ltac environment. *) -- cgit v1.2.3 From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- intf/constrexpr.mli | 4 ++-- intf/glob_term.mli | 4 ++-- intf/notation_term.mli | 2 +- intf/pattern.mli | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index d1b5697d75..49bafadc8e 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -72,7 +72,7 @@ and constr_expr = | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr - | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr + | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list @@ -124,7 +124,7 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = | CLocalAssum of Name.t located list * binder_kind * constr_expr - | CLocalDef of Name.t located * constr_expr + | CLocalDef of Name.t located * constr_expr * constr_expr option | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = diff --git a/intf/glob_term.mli b/intf/glob_term.mli index ce862cf8a7..ced5a8b44f 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -42,7 +42,7 @@ type glob_constr = | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr - | GLetIn of Loc.t * Name.t * glob_constr * glob_constr + | GLetIn of Loc.t * Name.t * glob_constr * glob_constr option * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * @@ -80,7 +80,7 @@ and cases_clauses = cases_clause list type extended_glob_local_binder = | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr - | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr (** A globalised term together with a closure representing the value diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 1ab9980a5c..753fa657a8 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -30,7 +30,7 @@ type notation_constr = | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr - | NLetIn of Name.t * notation_constr * notation_constr + | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list diff --git a/intf/pattern.mli b/intf/pattern.mli index 329ae837e1..a32e7e4b94 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -68,7 +68,7 @@ type constr_pattern = | PProj of projection * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern - | PLetIn of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern -- cgit v1.2.3 From 584a832d4f681d34c7cbdd87d9ceb7a742b39959 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 00:23:10 +0100 Subject: [stm] Remove some obsolete vernacs/classification. This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away. --- intf/vernacexpr.mli | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) (limited to 'intf') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8827bc132e..f782dd639d 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,14 +283,9 @@ type bullet = | Plus of int (** {6 Types concerning Stm} *) -type 'a stm_vernac = +type stm_vernac = | JoinDocument - | Finish | Wait - | PrintDag - | Observe of Stateid.t - | Command of 'a (* An out of flow command not to be recorded by Stm *) - | PGLast of 'a (* To ease the life of PG *) (** {6 Types concerning the module layer} *) @@ -450,8 +445,9 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor *) - | VernacStm of vernac_expr stm_vernac + (* Stm backdoor: used in fake_id, will be removed when fake_ide + becomes aware of feedback about completed jobs. *) + | VernacStm of stm_vernac (* Proof management *) | VernacGoal of constr_expr @@ -509,16 +505,11 @@ and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) 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_is_alias = bool and vernac_part_of_script = bool and vernac_control = - | VtFinish | VtWait | VtJoinDocument - | VtPrintDag - | VtObserve of Stateid.t | VtBack of Stateid.t - | VtPG and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) -- cgit v1.2.3