diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 3 | ||||
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 9 | ||||
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 134 | ||||
| -rw-r--r-- | dev/top_printers.ml | 25 |
5 files changed, 157 insertions, 15 deletions
diff --git a/dev/base_include b/dev/base_include index 242405ae29..608624d06e 100644 --- a/dev/base_include +++ b/dev/base_include @@ -147,9 +147,6 @@ open Refiner open Tacmach open Tactic_debug -open Decl_proof_instr -open Decl_mode - open Hints open Auto open Autorewrite diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 0285747432..bb193ebb55 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -20,3 +20,12 @@ # the name of the branch from which the PR originated. "" if the # current job is a push build. +echo $TRAVIS_PULL_REQUEST_BRANCH +echo $TRAVIS_PULL_REQUEST +echo $TRAVIS_BRANCH +echo $TRAVIS_COMMIT + +if [ $TRAVIS_PULL_REQUEST == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then + mathcomp_CI_BRANCH=no_camlp4_compat + mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git +fi @@ -28,6 +28,7 @@ install_printer Top_printers.pppattern install_printer Top_printers.ppglob_constr install_printer Top_printers.ppconstr +install_printer Top_printers.ppeconstr install_printer Top_printers.ppuni install_printer Top_printers.ppuniverses install_printer Top_printers.ppconstraints diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md new file mode 100644 index 0000000000..db69b08a20 --- /dev/null +++ b/dev/doc/proof-engine.md @@ -0,0 +1,134 @@ +Tutorial on the new proof engine for ML tactic writers +====================================================== + +Starting from Coq 8.5, a new proof engine has been introduced, replacing the old +meta-based engine which had a lot of drawbacks, ranging from expressivity to +soundness, the major one being that the type of tactics was transparent. This +was pervasively abused and made virtually impossible to tweak the implementation +of the engine. + +The old engine is deprecated and is slowly getting removed from the source code. + +The new engine relies on a monadic API defined in the `Proofview` module. Helper +functions and higher-level operations are defined in the `Tacmach` and +`Tacticals` modules, and end-user tactics are defined amongst other in the +`Tactics` module. + +At the root of the engine is a representation of proofs as partial terms that +can contain typed holes, called evars, short for *existential variable*. An evar +is essentially defined by its context and return type, that we will write +`?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type +`Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by +applying `EConstr.mkEvar`, and which we will write `?e{σ}`. + +The engine monad features a notion of global state called `evar_map`, defined in +the `Evd` module, which is the structure containing the incremental refinement +of evars. `Evd` is a low-level API and its use is discouraged in favour of the +`Evarutil` module which provides more abstract primitives. + +In addition to this state, the monad also features a goal state, that is +an ordered list of current holes to be filled. While these holes are referred +to as goals at a high-enough level, they are actually no more than evars. The +API provided to deal with these holes can be found in the `Proofview.Goal` +module. Tactics are naturally operating on several goals at once, so that it is +usual to use the `Proofview.Goal.enter` function and its variants to dispatch a +tactic to each of the goals under focus. + +Primitive tactics by term refining +------------------------------------- + +A typical low-level tactic will be defined by plugging partial terms in the +goal holes thanks to the `Refine` module, and in particular to the +`Refine.refine` primitive. + +```ocaml +val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine ?unsafe t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [unsafe] is [false] (default is [true]) [t] is + type-checked beforehand. *) +``` + +In a first approximation, we can think of `'a Sigma.run` as +`evar_map -> 'a * evar_map`. What the function does is first evaluate the +`Constr.t Sigma.run` argument in the current proof state, and then use the +resulting term as a filler for the proof under focus. All evars that have been +created by the invocation of this thunk are then turned into new goals added in +the order of their creation. + +To see how we can use it, let us have a look at an idealized example, the `cut` +tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` +with a term `let x : X := ?e2{Γ} in ?e1{Γ} x` where `x` is a fresh variable and +`?e1 : [Γ ⊢ _ : X -> A]` and `?e2 : [Γ ⊢ _ : X]`. The current goal is solved and +two new holes `[e1, e2]` are added to the goal state in this order. + +```ocaml +let cut c = + let open Sigma in + Proofview.Goal.nf_enter { enter = begin fun gl -> + (** In this block, we focus on one goal at a time indicated by gl *) + let env = Proofview.Goal.env gl in + (** Get the context of the goal, essentially [Γ] *) + let concl = Proofview.Goal.concl gl in + (** Get the conclusion [A] of the goal *) + let hyps = Tacmach.New.pf_ids_of_hyps gl in + (** List of hypotheses from the context of the goal *) + let id = Namegen.next_name_away Anonymous hyps in + (** Generate a fresh identifier *) + let t = mkArrow c (Vars.lift 1 concl) in + (** Build [X -> A]. Note the lifting of [A] due to being on the right hand + side of the arrow. *) + Refine.refine { run = begin fun sigma -> + (** All evars generated by this block will be added as goals *) + let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the + term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity + substitution for [Γ] is extracted from the [env] argument, so that + one must be careful to pass the correct context here in order for the + resulting term to be well-typed. The [p] return value is a proof term + used to enforce sigma monotonicity. *) + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return + [x := Γ ⊢ ?e2{Γ} : X]. *) + let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in + (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) + Sigma (r, sigma, p +> q) + (** Fills the current hole with [r]. The [p +> q] thingy ensures + monotonicity of sigma. *) + end } + end } +``` + +The `Evarutil.new_evar` function is the preferred way to generate evars in +tactics. It returns a ready-to-use term, so that one does not have to call +the `mkEvar` primitive. There are lower-level variants whose use is dedicated to +special use cases, *e.g.* whenever one wants a non-identity substitution. One +should take care to call it with the proper `env` argument so that the evar +and term it generates make sense in the context they will be plugged in. + +For the sake of completeness, the old engine was relying on the `Tacmach.refine` +function to provide a similar feature. Nonetheless, it was using untyped metas +instead of evars, so that it had to mangle the argument term to actually produce +the term that would be put into the hole. For instance, to work around the +untypedness, some metas had to be coerced with a cast to enforce their type, +otherwise leading to runtime errors. This was working for very simple +instances, but was unreliable for everything else. + +High-level composition of tactics +------------------------------------ + +It is possible to combine low-level refinement tactics to create more powerful +abstractions. While it was the standard way of doing things in the old engine +to overcome its technical limitations (namely that one was forced to go through +a limited set of derivation rules), it is recommended to generate proofs as +much as possible by refining in ML tactics when it is possible and easy enough. +Indeed, this prevents dependence on fragile constructions such as unification. + +Obviously, it does not forbid the use of tacticals to mimick what one would do +in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple +semantics. A list of such tacticals can be found in the `Tacticals` module. Most +of them are a porting of the tacticals from the old engine to the new one, so +that if they share the same name they are expected to have the same semantics. diff --git a/dev/top_printers.ml b/dev/top_printers.ml index cd464801b0..474cc85c17 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -70,9 +70,10 @@ let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) (* term printers *) let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) -let ppconstr x = pp (Termops.print_constr x) +let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) +let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) -let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x)) let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -97,9 +98,9 @@ let ppidmap pr l = pp (pridmap pr l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr c ++ + (Termops.print_constr (EConstr.of_constr c) ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ - Termops.print_constr c ++ str">") ++ + Termops.print_constr (EConstr.of_constr c) ++ str">") ++ (if id = id0 then mt () else spc () ++ str "<canonical: " ++ pr_id id ++ str ">")))) @@ -158,15 +159,15 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) -let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) -let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd) +let ppmetas metas = pp(Termops.pr_metaset metas) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = @@ -177,14 +178,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) -let ppgoalsigma g = pp(Printer.pr_goal g ++ pr_evar_map None (Refiner.project g)) +let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g)) let pphintdb db = pp(Hints.pr_hint_db db) let ppproofview p = let gls,sigma = Proofview.proofview p in - pp(pr_enum Goal.pr_goal gls ++ fnl () ++ pr_evar_map (Some 1) sigma) + pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (pr_evar_map (Some 2) evd ++ pr_constr c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) @@ -215,7 +216,7 @@ let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) -let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) +let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = |