diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 58 | ||||
| -rw-r--r-- | proofs/clenv.mli | 1 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 12 | ||||
| -rw-r--r-- | proofs/goal.ml | 16 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 57 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/logic_monad.ml | 321 | ||||
| -rw-r--r-- | proofs/logic_monad.mli | 162 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 53 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 9 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 52 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 16 | ||||
| -rw-r--r-- | proofs/proof_using.ml | 8 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 135 | ||||
| -rw-r--r-- | proofs/proofview.mli | 104 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 275 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 148 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/refiner.mli | 3 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 43 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 53 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 318 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 79 |
27 files changed, 368 insertions, 1582 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 88e1bce95a..1ef0b087ba 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -24,6 +24,7 @@ open Pretype_errors open Evarutil open Unification open Misctypes +open Sigma.Notations (* Abbreviations *) @@ -119,7 +120,7 @@ let clenv_environments evd bound t = clrec (evd,[]) bound t let mk_clenv_from_env env sigma n (c,cty) = - let evd = create_goal_evar_defs sigma in + let evd = clear_metas sigma in let (evd,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; @@ -335,22 +336,15 @@ let clenv_pose_metas_as_evars clenv dep_mvs = else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in - let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in + let evd = Sigma.Unsafe.of_evar_map clenv.evd in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs (******************************************************************) -let connect_clenv gls clenv = - let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in - { clenv with - evd = evd ; - env = Goal.V82.env evd (sig_it gls) } - -(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *) -(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *) - (* [clenv_fchain mv clenv clenv'] * * Resolves the value of "mv" (which must be undefined) in clenv to be @@ -432,6 +426,44 @@ let check_bindings bl = str " occurs more than once in binding list.") | [] -> () +let explain_no_such_bound_variable evd id = + let fold l (n, clb) = + let na = match clb with + | Cltyp (na, _) -> na + | Clval (na, _, _) -> na + in + if na != Anonymous then out_name na :: l else l + in + let mvl = List.fold_left fold [] (Evd.meta_list evd) in + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id ++ + (if mvl == [] then str " (no bound variables at all in the expression)." + else + (str" (possible name" ++ + str (if List.length mvl == 1 then " is: " else "s are: ") ++ + pr_enum pr_id mvl ++ str")."))) + +let meta_with_name evd id = + let na = Name id in + let fold (l1, l2 as l) (n, clb) = + let (na',def) = match clb with + | Cltyp (na, _) -> (na, false) + | Clval (na, _, _) -> (na, true) + in + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l + in + let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in + match mvnodef, mvl with + | _,[] -> + explain_no_such_bound_variable evd id + | ([n],_|_,[n]) -> + n + | _ -> + errorlabstrm "Evd.meta_with_name" + (str "Binder name \"" ++ pr_id id ++ + strbrk "\" occurs more than once in clause.") + let meta_of_binder clause loc mvs = function | NamedHyp s -> meta_with_name clause.evd s | AnonHyp n -> @@ -576,7 +608,9 @@ let make_evar_clause env sigma ?len t = | Cast (t, _, _) -> clrec (sigma, holes) n t | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in - let sigma, ev = new_evar ~store env sigma t1 in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let sigma = Sigma.to_evar_map sigma in let dep = dependent (mkRel 1) t2 in let hole = { hole_evar = ev; diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 7ecc26ec91..59b166ea01 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -49,7 +49,6 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst (** {6 linking of clenvs } *) -val connect_clenv : Goal.goal sigma -> clausenv -> clausenv val clenv_fchain : ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8e92259927..08e6c91de6 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -16,7 +16,7 @@ open Logic open Reduction open Tacmach open Clenv - +open Proofview.Notations (* This function put casts around metavariables whose type could not be * infered by the refiner, that is head of applications, predicates and @@ -83,10 +83,10 @@ open Unification let dft = default_unify_flags let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let clenv gl = clenv_unique_resolver ~flags clenv gl in clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) - end + end } (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en particulier ne semblent pas vérifier que des instances différentes @@ -118,12 +118,12 @@ let fail_quick_unif_flags = { (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unify ?(flags=fail_quick_unif_flags) m = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in let n = Tacmach.New.pf_nf_concl gl in - let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in + let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' with e when Errors.noncritical e -> Proofview.tclZERO e - end + end } diff --git a/proofs/goal.ml b/proofs/goal.ml index 43a3024e50..111a947a9c 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,6 +9,8 @@ open Util open Pp open Term +open Sigma.Notations +open Context.Named.Declaration (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated @@ -70,10 +72,12 @@ module V82 = struct Evd.evar_extra = extra } in let evi = Typeclasses.mark_unresolvable evi in - let (evars, evk) = Evarutil.new_pure_evar_full evars evi in + let evars = Sigma.Unsafe.of_evar_map evars in + let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in + let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in + let inst = Array.map_of_list (mkVar % get_id) ctxt in let ev = Term.mkEvar (evk,inst) in (evk, ev, evars) @@ -126,8 +130,10 @@ module V82 = struct let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in - let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = new_sigma; } + let sigma = Sigma.Unsafe.of_evar_map Evd.empty in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in + let sigma = Sigma.to_evar_map sigma in + { Evd.it = evk ; sigma = sigma; } (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = @@ -142,7 +148,7 @@ module V82 = struct let env = env sigma gl in let genv = Global.env () in let is_proof_var decl = - try ignore (Environ.lookup_named (Util.pi1 decl) genv); false + try ignore (Environ.lookup_named (get_id decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then diff --git a/proofs/goal.mli b/proofs/goal.mli index 6152826ca1..8a3d6e815a 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -67,7 +67,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index ed3a1df1a9..09f308abef 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -22,6 +22,7 @@ open Proof_type open Type_errors open Retyping open Misctypes +open Context.Named.Declaration type refiner_error = @@ -95,12 +96,12 @@ let check_typability env sigma c = forces the user to give them in order). *) let clear_hyps env sigma ids sign cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in (hyps, cl, !evdref) let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in (hyps, t, cl, !evdref) @@ -160,7 +161,8 @@ let reorder_context env sign ord = | _ -> (match ctxt_head with | [] -> error_no_such_hypothesis (List.hd ord) - | (x,_,_ as d) :: ctxt -> + | d :: ctxt -> + let x = get_id d in if Id.Set.mem x expected then step ord (Id.Set.remove x expected) ctxt (push_item x d moved_hyps) ctxt_tail @@ -175,7 +177,8 @@ let reorder_val_context env sign ord = -let check_decl_position env sign (x,_,_ as d) = +let check_decl_position env sign d = + let x = get_id d in let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then @@ -200,16 +203,17 @@ let move_location_eq m1 m2 = match m1, m2 with let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h - | (hyp,_,_) :: right -> - if Id.equal hyp h then - match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst + | d :: right -> + if Id.equal (get_id d) h then + match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst else get_hyp_after h right let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom - | (hyp,c,typ) as d :: right -> + | d :: right -> + let hyp,_,typ = to_tuple d in if Id.equal hyp hfrom then (left,right,d, toleft || move_location_eq hto MoveLast) else @@ -227,27 +231,28 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = +let move_hyp toleft (left,declfrom,right) hto = let env = Global.env() in - let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = + let test_dep d d2 = if toleft - then occur_var_in_decl env hyp2 d - else occur_var_in_decl env hyp d2 + then occur_var_in_decl env (get_id d2) d + else occur_var_in_decl env (get_id d) d2 in let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle - | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) -> + | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) -> List.rev first @ List.rev middle @ right - | (hyp,_,_) as d :: right -> + | d :: right -> + let hyp = get_id d in let (first',middle') = if List.exists (test_dep d) middle then if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ + errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") @@ -483,12 +488,14 @@ and mk_casegoals sigma goal goalacc p c = (acc'',lbrty,conclty,sigma,p',c') -let convert_hyp check sign sigma (id,b,bt as d) = +let convert_hyp check sign sigma d = + let id,b,bt = to_tuple d in let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp sign id - (fun _ (_,c,ct) _ -> + (fun _ d' _ -> + let _,c,ct = to_tuple d' in let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then errorlabstrm "Logic.convert_hyp" @@ -522,17 +529,17 @@ let prim_refiner r sigma goal = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp false ([],(id,None,t),named_context_of_val sign) + move_hyp false ([], LocalAssum (id,t),named_context_of_val sign) nexthyp, t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then errorlabstrm "Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); - push_named_context_val (id,None,t) sign,t,cl,sigma) in + push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in + let oterm = Term.mkNamedLetIn id ev1 t ev2 in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) @@ -546,7 +553,8 @@ let prim_refiner r sigma goal = with Not_found -> error "Cannot do a fixpoint on a non inductive type." else - check_ind (push_rel (na,None,c1) env) (k-1) b + let open Context.Rel.Declaration in + check_ind (push_rel (LocalAssum (na,c1)) env) (k-1) b | _ -> error "Not enough products." in let ((sp,_),u) = check_ind env n cl in @@ -560,7 +568,7 @@ let prim_refiner r sigma goal = if !check && mem_named_context f (named_context_of_val sign) then errorlabstrm "Logic.prim_refiner" (str "Name " ++ pr_id f ++ str " already used in the environment"); - mk_sign (push_named_context_val (f,None,ar) sign) oth + mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth | [] -> Evd.Monad.List.map (fun (_,_,c) sigma -> let gl,ev,sig' = @@ -584,7 +592,8 @@ let prim_refiner r sigma goal = let rec check_is_coind env cl = let b = whd_betadeltaiota env sigma cl in match kind_of_term b with - | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b + | Prod (na,c1,b) -> let open Context.Rel.Declaration in + check_is_coind (push_rel (LocalAssum (na,c1)) env) b | _ -> try let _ = find_coinductive env sigma b in () @@ -601,7 +610,7 @@ let prim_refiner r sigma goal = error "Name already used in the environment.") with | Not_found -> - mk_sign (push_named_context_val (f,None,ar) sign) oth) + mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth) | [] -> Evd.Monad.List.map (fun (_,c) sigma -> let gl,ev,sigma = diff --git a/proofs/logic.mli b/proofs/logic.mli index ed99d3a38a..9aa4ac2074 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -53,4 +53,4 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.named_declaration -> Environ.named_context_val + Context.Named.Declaration.t -> Environ.named_context_val diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml deleted file mode 100644 index 68efa71e87..0000000000 --- a/proofs/logic_monad.ml +++ /dev/null @@ -1,321 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file defines the low-level monadic operations used by the - tactic monad. The monad is divided into two layers: a non-logical - layer which consists in operations which will not (or cannot) be - backtracked in case of failure (input/output or persistent state) - and a logical layer which handles backtracking, proof - manipulation, and any other effect which needs to backtrack. *) - - -(** {6 Exceptions} *) - - -(** To help distinguish between exceptions raised by the IO monad from - the one used natively by Coq, the former are wrapped in - [Exception]. It is only used internally so that [catch] blocks of - the IO monad would only catch exceptions raised by the [raise] - function of the IO monad, and not for instance, by system - interrupts. Also used in [Proofview] to avoid capturing exception - from the IO monad ([Proofview] catches errors in its compatibility - layer, and when lifting goal-level expressions). *) -exception Exception of exn -(** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout -(** This exception is used by the tactics to signal failure by lack of - successes, rather than some other exceptions (like system - interrupts). *) -exception TacticFailure of exn - -let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") - | Exception e -> Errors.print e - | TacticFailure e -> Errors.print e - | _ -> Pervasives.raise Errors.Unhandled -end - -(** {6 Non-logical layer} *) - -(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The - operations are simple wrappers around corresponding usual - operations and require little documentation. *) -module NonLogical = -struct - - (* The functions in this module follow the pattern that they are - defined with the form [(); fun ()->...]. This is an optimisation - which signals to the compiler that the function is usually partially - applied up to the [();]. Without this annotation, partial - applications can be significantly slower. - - Documentation of this behaviour can be found at: - https://ocaml.janestreet.com/?q=node/30 *) - - include Monad.Make(struct - type 'a t = unit -> 'a - - let return a = (); fun () -> a - let (>>=) a k = (); fun () -> k (a ()) () - let (>>) a k = (); fun () -> a (); k () - let map f a = (); fun () -> f (a ()) - end) - - type 'a ref = 'a Pervasives.ref - - let ignore a = (); fun () -> ignore (a ()) - - let ref a = (); fun () -> Pervasives.ref a - - (** [Pervasives.(:=)] *) - let (:=) r a = (); fun () -> r := a - - (** [Pervasives.(!)] *) - let (!) = fun r -> (); fun () -> ! r - - (** [Pervasives.raise]. Except that exceptions are wrapped with - {!Exception}. *) - let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) - - (** [try ... with ...] but restricted to {!Exception}. *) - let catch = fun s h -> (); - fun () -> try s () - with Exception e as src -> - let (src, info) = Errors.push src in - h (e, info) () - - let read_line = fun () -> try Pervasives.read_line () with e -> - let (e, info) = Errors.push e in raise ~info e () - - let print_char = fun c -> (); fun () -> print_char c - - let timeout = fun n t -> (); fun () -> - Control.timeout n t (Exception Timeout) - - let make f = (); fun () -> - try f () - with e when Errors.noncritical e -> - let (e, info) = Errors.push e in - Util.iraise (Exception e, info) - - (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) - let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) - let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) - - let run = fun x -> - try x () with Exception e as src -> - let (src, info) = Errors.push src in - Util.iraise (e, info) -end - -(** {6 Logical layer} *) - -(** The logical monad is a backtracking monad on top of which is - layered a state monad (which is used to implement all of read/write, - read only, and write only effects). The state monad being layered on - top of the backtracking monad makes it so that the state is - backtracked on failure. - - Backtracking differs from regular exception in that, writing (+) - for exception catching and (>>=) for bind, we require the - following extra distributivity laws: - - x+(y+z) = (x+y)+z - - zero+x = x - - x+zero = x - - (x+y)>>=k = (x>>=k)+(y>>=k) *) - -(** A view type for the logical monad, which is a form of list, hence - we can decompose it with as a list. *) -type ('a, 'b) list_view = - | Nil of Exninfo.iexn - | Cons of 'a * 'b - -module type Param = sig - - (** Read only *) - type e - - (** Write only *) - type w - - (** [w] must be a monoid *) - val wunit : w - val wprod : w -> w -> w - - (** Read-write *) - type s - - (** Update-only. Essentially a writer on [u->u]. *) - type u - - (** [u] must be pointed. *) - val uunit : u - -end - - -module Logical (P:Param) = -struct - - (** All three of environment, writer and state are coded as a single - state-passing-style monad.*) - type state = { - rstate : P.e; - ustate : P.u; - wstate : P.w; - sstate : P.s; - } - - (** Double-continuation backtracking monads are reasonable folklore - for "search" implementations (including the Tac interactive - prover's tactics). Yet it's quite hard to wrap your head around - these. I recommand reading a few times the "Backtracking, - Interleaving, and Terminating Monad Transformers" paper by - O. Kiselyov, C. Shan, D. Friedman, and A. Sabry. The peculiar - shape of the monadic type is reminiscent of that of the - continuation monad transformer. - - The paper also contains the rationale for the [split] abstraction. - - An explanation of how to derive such a monad from mathematical - principles can be found in "Kan Extensions for Program - Optimisation" by Ralf Hinze. - - A somewhat concrete view is that the type ['a iolist] is, in fact - the impredicative encoding of the following stream type: - - [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist' - and 'a iolist = 'a _iolist NonLogical.t] - - Using impredicative encoding avoids intermediate allocation and - is, empirically, very efficient in Ocaml. It also has the - practical benefit that the monadic operation are independent of - the underlying monad, which simplifies the code and side-steps - the limited inlining of Ocaml. - - In that vision, [bind] is simply [concat_map] (though the cps - version is significantly simpler), [plus] is concatenation, and - [split] is pattern-matching. *) - type rich_exn = Exninfo.iexn - - type 'a iolist = - { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) -> - ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } - - include Monad.Make(struct - - type 'a t = 'a iolist - - let return x = - { iolist = fun s nil cons -> cons x s nil } - - let (>>=) m f = - { iolist = fun s nil cons -> - m.iolist s nil (fun x s next -> (f x).iolist s next cons) } - - let (>>) m f = - { iolist = fun s nil cons -> - m.iolist s nil (fun () s next -> f.iolist s next cons) } - - let map f m = - { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) } - - end) - - let zero e = - { iolist = fun _ nil cons -> nil e } - - let plus m1 m2 = - { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons } - - let ignore m = - { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } - - let lift m = - { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } - - (** State related *) - - let get = - { iolist = fun s nil cons -> cons s.sstate s nil } - - let set (sstate : P.s) = - { iolist = fun s nil cons -> cons () { s with sstate } nil } - - let modify (f : P.s -> P.s) = - { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil } - - let current = - { iolist = fun s nil cons -> cons s.rstate s nil } - - let local e m = - { iolist = fun s nil cons -> - m.iolist { s with rstate = e } nil - (fun x s' next -> cons x {s' with rstate = s.rstate} next) } - - let put w = - { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil } - - let update (f : P.u -> P.u) = - { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil } - - (** List observation *) - - let once m = - { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) } - - let break f m = - { iolist = fun s nil cons -> - m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e)) - } - - (** For [reflect] and [split] see the "Backtracking, Interleaving, - and Terminating Monad Transformers" paper. *) - type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t - - let rec reflect (m : ('a * state) reified) : 'a iolist = - { iolist = fun s0 nil cons -> - let next = function - | Nil e -> nil e - | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) - in - NonLogical.(m >>= next) - } - - let split m : ('a, rich_exn -> 'a t) list_view t = - let rnil e = NonLogical.return (Nil e) in - let rcons p s l = NonLogical.return (Cons ((p, s), l)) in - { iolist = fun s nil cons -> - let open NonLogical in - m.iolist s rnil rcons >>= begin function - | Nil e -> cons (Nil e) s nil - | Cons ((x, s), l) -> - let l e = reflect (l e) in - cons (Cons (x, l)) s nil - end } - - let run m r s = - let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let rnil e = NonLogical.return (Nil e) in - let rcons x s l = - let p = (x, s.sstate, s.wstate, s.ustate) in - NonLogical.return (Cons (p, l)) - in - m.iolist s rnil rcons - - let repr x = x - - end diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli deleted file mode 100644 index 96655d538c..0000000000 --- a/proofs/logic_monad.mli +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file defines the low-level monadic operations used by the - tactic monad. The monad is divided into two layers: a non-logical - layer which consists in operations which will not (or cannot) be - backtracked in case of failure (input/output or persistent state) - and a logical layer which handles backtracking, proof - manipulation, and any other effect which needs to backtrack. *) - - -(** {6 Exceptions} *) - - -(** To help distinguish between exceptions raised by the IO monad from - the one used natively by Coq, the former are wrapped in - [Exception]. It is only used internally so that [catch] blocks of - the IO monad would only catch exceptions raised by the [raise] - function of the IO monad, and not for instance, by system - interrupts. Also used in [Proofview] to avoid capturing exception - from the IO monad ([Proofview] catches errors in its compatibility - layer, and when lifting goal-level expressions). *) -exception Exception of exn -(** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout -(** This exception is used by the tactics to signal failure by lack of - successes, rather than some other exceptions (like system - interrupts). *) -exception TacticFailure of exn - - -(** {6 Non-logical layer} *) - -(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The - operations are simple wrappers around corresponding usual - operations and require little documentation. *) -module NonLogical : sig - - include Monad.S - - val ignore : 'a t -> unit t - - type 'a ref - - val ref : 'a -> 'a ref t - (** [Pervasives.(:=)] *) - val (:=) : 'a ref -> 'a -> unit t - (** [Pervasives.(!)] *) - val (!) : 'a ref -> 'a t - - val read_line : string t - val print_char : char -> unit t - - (** Loggers. The buffer is also flushed. *) - val print_debug : Pp.std_ppcmds -> unit t - val print_warning : Pp.std_ppcmds -> unit t - val print_notice : Pp.std_ppcmds -> unit t - val print_info : Pp.std_ppcmds -> unit t - val print_error : Pp.std_ppcmds -> unit t - - (** [Pervasives.raise]. Except that exceptions are wrapped with - {!Exception}. *) - val raise : ?info:Exninfo.info -> exn -> 'a t - (** [try ... with ...] but restricted to {!Exception}. *) - val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t - val timeout : int -> 'a t -> 'a t - - (** Construct a monadified side-effect. Exceptions raised by the argument are - wrapped with {!Exception}. *) - val make : (unit -> 'a) -> 'a t - - (** [run] performs effects. *) - val run : 'a t -> 'a - -end - - -(** {6 Logical layer} *) - -(** The logical monad is a backtracking monad on top of which is - layered a state monad (which is used to implement all of read/write, - read only, and write only effects). The state monad being layered on - top of the backtracking monad makes it so that the state is - backtracked on failure. - - Backtracking differs from regular exception in that, writing (+) - for exception catching and (>>=) for bind, we require the - following extra distributivity laws: - - x+(y+z) = (x+y)+z - - zero+x = x - - x+zero = x - - (x+y)>>=k = (x>>=k)+(y>>=k) *) - -(** A view type for the logical monad, which is a form of list, hence - we can decompose it with as a list. *) -type ('a, 'b) list_view = -| Nil of Exninfo.iexn -| Cons of 'a * 'b - -(** The monad is parametrised in the types of state, environment and - writer. *) -module type Param = sig - - (** Read only *) - type e - - (** Write only *) - type w - - (** [w] must be a monoid *) - val wunit : w - val wprod : w -> w -> w - - (** Read-write *) - type s - - (** Update-only. Essentially a writer on [u->u]. *) - type u - - (** [u] must be pointed. *) - val uunit : u - -end - -module Logical (P:Param) : sig - - include Monad.S - - val ignore : 'a t -> unit t - - val set : P.s -> unit t - val get : P.s t - val modify : (P.s -> P.s) -> unit t - val put : P.w -> unit t - val current : P.e t - val local : P.e -> 'a t -> 'a t - val update : (P.u -> P.u) -> unit t - - val zero : Exninfo.iexn -> 'a t - val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t - val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t - val once : 'a t -> 'a t - val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t - - val lift : 'a NonLogical.t -> 'a t - - type 'a reified - - val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t - - val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified - -end diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b635cc9632..20d696fd91 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -138,7 +138,8 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - start_proof id goal_kind evd sign typ (fun _ -> ()); + let terminator = Proof_global.make_terminator (fun _ -> ()) in + start_proof id goal_kind evd sign typ terminator; try let status = by tac in let _,(const,univs,_) = cook_proof () in @@ -214,7 +215,7 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 541f299d4f..d19dc5ba0f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -92,6 +92,9 @@ type pstate = { universe_binders: universe_binders option; } +let make_terminator f = f +let apply_terminator f = f + (* The head of [!pstates] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) @@ -264,18 +267,19 @@ let _ = Goptions.declare_bool_option Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } let set_used_variables l = + let open Context.Named.Declaration in let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with - | (x,None,_) -> + | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig else (ctx, all_safe, (Loc.ghost,x)::to_clear) - | (x,Some bo, ty) as decl -> + | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe @@ -299,6 +303,11 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf +let constrain_variables init uctx = + let levels = Univ.Instance.levels (Univ.UContext.instance init) in + let cstrs = UState.constrain_variables levels uctx in + Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) + let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in @@ -329,7 +338,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) @@ -338,7 +347,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* Since the proof is computed now, we can simply have 1 set of * constraints in which we merge the ones for the body and the ones * for the typ *) @@ -353,7 +362,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let initunivs = Evd.evar_context_universe_context initial_euctx in Future.from_val (initunivs, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff) + (pt,constrain_variables initunivs (Future.force univs)),eff) in let entries = Future.map2 (fun p (_, t) -> @@ -458,7 +467,7 @@ module Bullet = struct type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> std_ppcmds } let behaviors = Hashtbl.create 4 @@ -468,7 +477,7 @@ module Bullet = struct let none = { name = "None"; put = (fun x _ -> x); - suggest = (fun _ -> None) + suggest = (fun _ -> mt ()) } let _ = register_behavior none @@ -484,26 +493,20 @@ module Bullet = struct (* give a message only if more informative than the standard coq message *) let suggest_on_solved_goal sugg = match sugg with - | NeedClosingBrace -> Some "Try unfocusing with \"}\"." - | NoBulletInUse -> None - | ProofFinished -> None - | Suggest b -> Some ("Focus next goal with bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^".") - | Unfinished b -> Some ("The current bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is unfinished.") + | NeedClosingBrace -> str"Try unfocusing with \"}\"." + | NoBulletInUse -> mt () + | ProofFinished -> mt () + | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"." + | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished." (* give always a message. *) let suggest_on_error sugg = match sugg with - | NeedClosingBrace -> "Try unfocusing with \"}\"." + | NeedClosingBrace -> str"Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> "No more subgoals." - | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is mandatory here.") - | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is not finished.") + | ProofFinished -> str"No more subgoals." + | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here." + | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." exception FailedBullet of t * suggestion @@ -511,8 +514,8 @@ module Bullet = struct Errors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in - Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) + let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in + Errors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg) | _ -> raise Errors.Unhandled) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 7fbd183e68..ebe7f6d6f3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -70,9 +70,12 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object -type proof_terminator = proof_ending -> unit +type proof_terminator type closed_proof = proof_object * proof_terminator +val make_terminator : (proof_ending -> unit) -> proof_terminator +val apply_terminator : proof_terminator -> proof_ending -> unit + (** [start_proof id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -169,7 +172,7 @@ module Bullet : sig type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> Pp.std_ppcmds } (** A registered behavior can then be accessed in Coq @@ -186,7 +189,7 @@ module Bullet : sig (** Handles focusing/defocusing with bullets: *) val put : Proof.proof -> t -> Proof.proof - val suggest : Proof.proof -> string option + val suggest : Proof.proof -> Pp.std_ppcmds end diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml deleted file mode 100644 index dd2c7b253d..0000000000 --- a/proofs/proof_type.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i*) -open Evd -open Names -open Term -open Tacexpr -open Glob_term -open Nametab -open Misctypes -(*i*) - -(* This module defines the structure of proof tree and the tactic type. So, it - is used by Proof_tree and Refiner *) - -(** Types of goals, tactics, rules ... *) - -type goal = Goal.goal - -type tactic = goal sigma -> goal list sigma - -type prim_rule = - | Cut of bool * bool * Id.t * types - | FixRule of Id.t * int * (Id.t * int * constr) list * int - | Cofix of Id.t * (Id.t * constr) list * int - | Refine of constr - | Thin of Id.t list - | Move of Id.t * Id.t move_location - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -(** Ltac traces *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index aa05f58ab6..b4c9dae2a3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -57,19 +57,3 @@ type rule = prim_rule type goal = Goal.goal type tactic = goal sigma -> goal list sigma - -(** Ltac traces *) - -(** TODO: Move those definitions somewhere sensible *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -val ltac_trace_info : ltac_trace Exninfo.t diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a69645b116..681a7fa1ad 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -10,6 +10,7 @@ open Names open Environ open Util open Vernacexpr +open Context.Named.Declaration let to_string e = let rec aux = function @@ -33,7 +34,8 @@ let in_nameset = let rec close_fwd e s = let s' = - List.fold_left (fun s (id,b,ty) -> + List.fold_left (fun s decl -> + let (id,b,ty) = Context.Named.Declaration.to_tuple decl in let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in let vty = global_vars_set e ty in let vbty = Id.Set.union vb vty in @@ -61,13 +63,13 @@ and set_of_id env ty id = Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty else if CList.mem_assoc_f Id.equal id !known_names then process_expr env (CList.assoc_f Id.equal id !known_names) [] else Id.Set.singleton id and full_set env = - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 32bf5576fa..08556d62ec 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,10 +2,7 @@ Miscprint Goal Evar_refiner Proof_using -Proof_type Proof_errors -Logic_monad -Proofview_monad Logic Proofview Proof @@ -14,6 +11,5 @@ Redexpr Refiner Tacmach Pfedit -Tactic_debug Clenv Clenvtac diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6d7dcb9257..a382e9873f 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -16,6 +16,8 @@ open Pp open Util open Proofview_monad +open Sigma.Notations +open Context.Named.Declaration (** Main state of tactics *) type proofview = Proofview_monad.proofview @@ -64,7 +66,9 @@ let dependent_init = let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in @@ -350,7 +354,7 @@ exception NoSuchGoals of int (* This hook returns a string to be appended to the usual message. Primarily used to add a suggestion about the right bullet to use to focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> string option) ref = ref ((fun n -> None)) +let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ()) let set_nosuchgoals_hook f = nosuchgoals_hook := f @@ -358,10 +362,9 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f (* This uses the hook above *) let _ = Errors.register_handler begin function | NoSuchGoals n -> - let suffix:string option = (!nosuchgoals_hook) n in + let suffix = !nosuchgoals_hook n in Errors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." - ++ pr_opt str suffix) + (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) | _ -> raise Errors.Unhandled end @@ -748,9 +751,15 @@ module Progress = struct let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = let open Environ in let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 - && (eq_constr sigma1 sigma2) t1 t2 + let eq_named_declaration d1 d2 = + match d1, d2 with + | LocalAssum (i1,t1), LocalAssum (i2,t2) -> + Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2 + | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) -> + Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2 + && eq_constr sigma1 sigma2 t1 t2 + | _ -> + false in List.equal eq_named_declaration c1 c2 let eq_evar_body sigma1 sigma2 b1 b2 = @@ -907,19 +916,11 @@ module Unsafe = struct end +module UnsafeRepr = Proof.Unsafe - -(** {7 Notations} *) - -module Notations = struct - let (>>=) = tclBIND - let (<*>) = tclTHEN - let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) -end - -open Notations - - +let (>>=) = tclBIND +let (<*>) = tclTHEN +let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) (** {6 Goal-dependent tactics} *) @@ -933,17 +934,20 @@ let catchable_exception = function module Goal = struct - type 'a t = { + type ('a, 'r) t = { env : Environ.env; sigma : Evd.evar_map; concl : Term.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } - let assume (gl : 'a t) = (gl :> [ `NF ] t) + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } + + let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) let env { env=env } = env - let sigma { sigma=sigma } = sigma + let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma let hyps { env=env } = Environ.named_context env let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self @@ -969,7 +973,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) with e when catchable_exception e -> let (e, info) = Errors.push e in tclZERO ~info e @@ -987,7 +991,7 @@ module Goal = struct gmake_with info env sigma goal let enter f = - let f gl = InfoL.tag (Info.DBranch) (f gl) in + let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> Env.get >>= fun env -> @@ -999,6 +1003,41 @@ module Goal = struct end end + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } + + let s_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let gl = gmake env sigma goal in + let Sigma (tac, sigma, _) = f.s_enter gl in + let sigma = Sigma.to_evar_map sigma in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + + let nf_s_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let (gl, sigma) = nf_gmake env sigma goal in + let Sigma (tac, sigma, _) = f.s_enter gl in + let sigma = Sigma.to_evar_map sigma in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + let goals = Pv.get >>= fun step -> let sigma = step.solution in @@ -1018,6 +1057,8 @@ module Goal = struct (* compatibility *) let goal { self=self } = self + let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) + end @@ -1041,12 +1082,13 @@ struct let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) - let type_hyp (sigma, env) (na, body, t as decl) = + let type_hyp (sigma, env) decl = + let t = get_type decl in let evdref = ref sigma in - let _ = Typing.sort_of env evdref t in - let () = match body with - | None -> () - | Some body -> Typing.check env evdref body t + let _ = Typing.e_sort_of env evdref t in + let () = match decl with + | LocalAssum _ -> () + | LocalDef (_,body,_) -> Typing.e_check env evdref body t in (!evdref, Environ.push_named decl env) in @@ -1055,19 +1097,20 @@ struct let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) let evdref = ref sigma in - let _ = Typing.sort_of env evdref (Evd.evar_concl info) in + let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in !evdref let typecheck_proof c concl env sigma = let evdref = ref sigma in - let () = Typing.check env evdref c concl in + let () = Typing.e_check env evdref c concl in !evdref let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () - let refine ?(unsafe = true) f = Goal.enter begin fun gl -> + let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl -> let sigma = Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Goal.env gl in let concl = Goal.concl gl in (** Save the [future_goals] state to restore them after the @@ -1075,7 +1118,7 @@ struct let prev_future_goals = Evd.future_goals sigma in let prev_principal_goal = Evd.principal_future_goal sigma in (** Create the refinement term *) - let (sigma, c) = f (Evd.reset_future_goals sigma) in + let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in (** Check that the introduced evars are well-typed *) @@ -1106,7 +1149,7 @@ struct let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.modify (fun ps -> { ps with solution = sigma; comb; }) - end + end } (** Useful definitions *) @@ -1118,12 +1161,16 @@ struct in evd , j'.Environ.uj_val - let refine_casted ?unsafe f = Goal.enter begin fun gl -> + let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl -> let concl = Goal.concl gl in let env = Goal.env gl in - let f h = let (h, c) = f h in with_type env h c concl in + let f = { run = fun h -> + let Sigma (c, h, p) = f.run h in + let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) + } in refine ?unsafe f - end + end } end @@ -1258,3 +1305,15 @@ module V82 = struct let (e, info) = Errors.push e in tclZERO ~info e end + +(** {7 Notations} *) + +module Notations = struct + let (>>=) = tclBIND + let (<*>) = tclTHEN + let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } +end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2157459f46..dc97e44b6f 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -235,7 +235,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic This hook is used to add a suggestion about bullets when applicable. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> string option) -> unit +val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic @@ -409,65 +409,84 @@ module Unsafe : sig val mark_as_goal : proofview -> Evar.t -> proofview end -(** {7 Notations} *) - -module Notations : sig - - (** {!tclBIND} *) - val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - (** {!tclTHEN} *) - val (<*>) : unit tactic -> 'a tactic -> 'a tactic - (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) - val (<+>) : 'a tactic -> 'a tactic -> 'a tactic - +(** This module gives access to the innards of the monad. Its use is + restricted to very specific cases. *) +module UnsafeRepr : +sig + type state = Proofview_monad.Logical.Unsafe.state + val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t + val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic end - (** {6 Goal-dependent tactics} *) module Goal : sig - (** The type of goals. The parameter type is a phantom argument indicating - whether the data contained in the goal has been normalized w.r.t. the - current sigma. If it is the case, it is flagged [ `NF ]. You may still - access the un-normalized data using {!assume} if you known you do not rely - on the assumption of being normalized, at your own risk. *) - type 'a t + (** Type of goals. + + The first parameter type is a phantom argument indicating whether the data + contained in the goal has been normalized w.r.t. the current sigma. If it + is the case, it is flagged [ `NF ]. You may still access the un-normalized + data using {!assume} if you known you do not rely on the assumption of + being normalized, at your own risk. + + The second parameter is a stage indicating where the goal belongs. See + module {!Sigma}. + *) + type ('a, 'r) t (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t + val assume : ('a, 'r) t -> ([ `NF ], 'r) t (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic + val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : [ `NF ] t -> Term.constr - val hyps : [ `NF ] t -> Context.named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t + val concl : ([ `NF ], 'r) t -> Term.constr + val hyps : ([ `NF ], 'r) t -> Context.Named.t + val env : ('a, 'r) t -> Environ.env + val sigma : ('a, 'r) t -> 'r Sigma.t + val extra : ('a, 'r) t -> Evd.Store.t (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : 'a t -> Term.constr + val raw_concl : ('a, 'r) t -> Term.constr + + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic + val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic + val enter : ([ `LZ ], unit tactic) enter -> unit tactic + + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } - (** Recover the list of current goals under focus, without evar-normalization *) - val goals : [ `LZ ] t tactic list tactic + (** A variant of {!enter} allows to work with a monotonic state. The evarmap + returned by the argument is put back into the current state before firing + the returned tactic. *) + val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic + + (** Like {!s_enter}, but normalizes the goal beforehand. *) + val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic + + (** Recover the list of current goals under focus, without evar-normalization. + FIXME: encapsulate the level in an existential type. *) + val goals : ([ `LZ ], 'r) t tactic list tactic (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t + val goal : ([ `NF ], 'r) t -> Evar.t + + (** Every goal is valid at a later stage. FIXME: take a later evarmap *) + val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t end @@ -482,7 +501,7 @@ module Refine : sig (** {7 Refinement primitives} *) - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic + 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 @@ -498,7 +517,7 @@ module Refine : sig (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) - val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic + val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) @@ -578,3 +597,20 @@ module V82 : sig the monad. *) val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic end + +(** {7 Notations} *) + +module Notations : sig + + (** {!tclBIND} *) + val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic + (** {!tclTHEN} *) + val (<*>) : unit tactic -> 'a tactic -> 'a tactic + (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) + val (<+>) : 'a tactic -> 'a tactic -> 'a tactic + + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } +end diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml deleted file mode 100644 index e9bc7761e9..0000000000 --- a/proofs/proofview_monad.ml +++ /dev/null @@ -1,275 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file defines the datatypes used as internal states by the - tactic monad, and specialises the [Logic_monad] to these type. *) - -(** {6 Trees/forest for traces} *) - -module Trace = struct - - (** The intent is that an ['a forest] is a list of messages of type - ['a]. But messages can stand for a list of more precise - messages, hence the structure is organised as a tree. *) - type 'a forest = 'a tree list - and 'a tree = Seq of 'a * 'a forest - - (** To build a trace incrementally, we use an intermediary data - structure on which we can define an S-expression like language - (like a simplified xml except the closing tags do not carry a - name). Note that nodes are built from right to left in ['a - incr], the result is mirrored when returning so that in the - exposed interface, the forest is read from left to right. - - Concretely, we want to add a new tree to a forest: and we are - building it by adding new trees to the left of its left-most - subtrees which is built the same way. *) - type 'a incr = { head:'a forest ; opened: 'a tree list } - - (** S-expression like language as ['a incr] transformers. It is the - responsibility of the library builder not to use [close] when no - tag is open. *) - let empty_incr = { head=[] ; opened=[] } - let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened } - let close { head ; opened } = - match opened with - | [a] -> { head = a::head ; opened=[] } - | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened } - | [] -> assert false - let leaf a s = close (opn a s) - - (** Returning a forest. It is the responsibility of the library - builder to close all the tags. *) - (* spiwack: I may want to close the tags instead, to deal with - interruptions. *) - let rec mirror f = List.rev_map mirror_tree f - and mirror_tree (Seq(a,f)) = Seq(a,mirror f) - - let to_tree = function - | { head ; opened=[] } -> mirror head - | { head ; opened=_::_} -> assert false - -end - - - -(** {6 State types} *) - -(** We typically label nodes of [Trace.tree] with messages to - print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds -let pr_lazy_msg msg = msg () - -(** Info trace. *) -module Info = struct - - (** The type of the tags for [info]. *) - type tag = - | Msg of lazy_msg (** A simple message *) - | Tactic of lazy_msg (** A tactic call *) - | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *) - | DBranch (** A special marker to delimit individual branch of a dispatch. *) - - type state = tag Trace.incr - type tree = tag Trace.forest - - - - let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)") - - let unbranch = function - | Trace.Seq (DBranch,brs) -> brs - | _ -> assert false - - - let is_empty_branch = let open Trace in function - | Seq(DBranch,[]) -> true - | _ -> false - - (** Dispatch with empty branches are (supposed to be) equivalent to - [idtac] which need not appear, so they are removed from the - trace. *) - let dispatch brs = - let open Trace in - if CList.for_all is_empty_branch brs then None - else Some (Seq(Dispatch,brs)) - - let constr = let open Trace in function - | Dispatch -> dispatch - | t -> fun br -> Some (Seq(t,br)) - - let rec compress_tree = let open Trace in function - | Seq(t,f) -> constr t (compress f) - and compress f = - CList.map_filter compress_tree f - - let rec is_empty = let open Trace in function - | Seq(Dispatch,brs) -> List.for_all is_empty brs - | Seq(DBranch,br) -> List.for_all is_empty br - | _ -> false - - (** [with_sep] is [true] when [Tactic m] must be printed with a - trailing semi-colon. *) - let rec pr_tree with_sep = let open Trace in function - | Seq (Msg m,[]) -> pr_in_comments m - | Seq (Tactic m,_) -> - let tail = if with_sep then Pp.str";" else Pp.mt () in - Pp.(pr_lazy_msg m ++ tail) - | Seq (Dispatch,brs) -> - let tail = if with_sep then Pp.str";" else Pp.mt () in - Pp.(pr_dispatch brs++tail) - | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false - and pr_dispatch brs = - let open Pp in - let brs = List.map unbranch brs in - match brs with - | [br] -> pr_forest br - | _ -> - let sep () = spc()++str"|"++spc() in - let branches = prlist_with_sep sep pr_forest brs in - str"[>"++spc()++branches++spc()++str"]" - and pr_forest = function - | [] -> Pp.mt () - | [tr] -> pr_tree false tr - | tr::l -> Pp.(pr_tree true tr ++ pr_forest l) - - let print f = - pr_forest (compress f) - - let rec collapse_tree n t = - let open Trace in - match n , t with - | 0 , t -> [t] - | _ , (Seq(Tactic _,[]) as t) -> [t] - | n , Seq(Tactic _,f) -> collapse (pred n) f - | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))] - | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))] - | _ , (Seq(Msg _,_) as t) -> [t] - and collapse n f = - CList.map_append (collapse_tree n) f -end - - -(** Type of proof views: current [evar_map] together with the list of - focused goals. *) -type proofview = { - solution : Evd.evar_map; - comb : Goal.goal list; - shelf : Goal.goal list; -} - -(** {6 Instantiation of the logic monad} *) - -(** Parameters of the logic monads *) -module P = struct - - type s = proofview * Environ.env - - (** Recording info trace (true) or not. *) - type e = bool - - (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list - - let wunit = true , [] - let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 - - type u = Info.state - - let uunit = Trace.empty_incr - -end - -module Logical = Logic_monad.Logical(P) - - -(** {6 Lenses to access to components of the states} *) - -module type State = sig - type t - val get : t Logical.t - val set : t -> unit Logical.t - val modify : (t->t) -> unit Logical.t -end - -module type Writer = sig - type t - val put : t -> unit Logical.t -end - -module Pv : State with type t := proofview = struct - let get = Logical.(map fst get) - let set p = Logical.modify (fun (_,e) -> (p,e)) - let modify f= Logical.modify (fun (p,e) -> (f p,e)) -end - -module Solution : State with type t := Evd.evar_map = struct - let get = Logical.map (fun {solution} -> solution) Pv.get - let set s = Pv.modify (fun pv -> { pv with solution = s }) - let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution }) -end - -module Comb : State with type t = Evar.t list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list - let get = Logical.map (fun {comb} -> comb) Pv.get - let set c = Pv.modify (fun pv -> { pv with comb = c }) - let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb }) -end - -module Env : State with type t := Environ.env = struct - let get = Logical.(map snd get) - let set e = Logical.modify (fun (p,_) -> (p,e)) - let modify f = Logical.modify (fun (p,e) -> (p,f e)) -end - -module Status : Writer with type t := bool = struct - let put s = Logical.put (s, []) -end - -module Shelf : State with type t = Evar.t list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list - let get = Logical.map (fun {shelf} -> shelf) Pv.get - let set c = Pv.modify (fun pv -> { pv with shelf = c }) - let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) -end - -module Giveup : Writer with type t = Evar.t list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list - let put gs = Logical.put (true, gs) -end - -(** Lens and utilies pertaining to the info trace *) -module InfoL = struct - let recording = Logical.current - let if_recording t = - let open Logical in - recording >>= fun r -> - if r then t else return () - - let record_trace t = Logical.local true t - - let raw_update = Logical.update - let update f = if_recording (raw_update f) - let opn a = update (Trace.opn a) - let close = update Trace.close - let leaf a = update (Trace.leaf a) - - let tag a t = - let open Logical in - recording >>= fun r -> - if r then begin - raw_update (Trace.opn a) >> - t >>= fun a -> - raw_update Trace.close >> - return a - end else - t -end diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli deleted file mode 100644 index 7a6ea10fe3..0000000000 --- a/proofs/proofview_monad.mli +++ /dev/null @@ -1,148 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file defines the datatypes used as internal states by the - tactic monad, and specialises the [Logic_monad] to these type. *) - -(** {6 Traces} *) - -module Trace : sig - - (** The intent is that an ['a forest] is a list of messages of type - ['a]. But messages can stand for a list of more precise - messages, hence the structure is organised as a tree. *) - type 'a forest = 'a tree list - and 'a tree = Seq of 'a * 'a forest - - (** To build a trace incrementally, we use an intermediary data - structure on which we can define an S-expression like language - (like a simplified xml except the closing tags do not carry a - name). *) - type 'a incr - val to_tree : 'a incr -> 'a forest - - (** [open a] opens a tag with name [a]. *) - val opn : 'a -> 'a incr -> 'a incr - - (** [close] closes the last open tag. It is the responsibility of - the user to close all the tags. *) - val close : 'a incr -> 'a incr - - (** [leaf] creates an empty tag with name [a]. *) - val leaf : 'a -> 'a incr -> 'a incr - -end - -(** {6 State types} *) - -(** We typically label nodes of [Trace.tree] with messages to - print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds - -(** Info trace. *) -module Info : sig - - (** The type of the tags for [info]. *) - type tag = - | Msg of lazy_msg (** A simple message *) - | Tactic of lazy_msg (** A tactic call *) - | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *) - | DBranch (** A special marker to delimit individual branch of a dispatch. *) - - type state = tag Trace.incr - type tree = tag Trace.forest - - val print : tree -> Pp.std_ppcmds - - (** [collapse n t] flattens the first [n] levels of [Tactic] in an - info trace, effectively forgetting about the [n] top level of - names (if there are fewer, the last name is kept). *) - val collapse : int -> tree -> tree - -end - -(** Type of proof views: current [evar_map] together with the list of - focused goals. *) -type proofview = { - solution : Evd.evar_map; - comb : Goal.goal list; - shelf : Goal.goal list; -} - -(** {6 Instantiation of the logic monad} *) - -module P : sig - type s = proofview * Environ.env - - (** Status (safe/unsafe) * given up *) - type w = bool * Evar.t list - - val wunit : w - val wprod : w -> w -> w - - (** Recording info trace (true) or not. *) - type e = bool - - type u = Info.state - - val uunit : u -end - -module Logical : module type of Logic_monad.Logical(P) - - -(** {6 Lenses to access to components of the states} *) - -module type State = sig - type t - val get : t Logical.t - val set : t -> unit Logical.t - val modify : (t->t) -> unit Logical.t -end - -module type Writer = sig - type t - val put : t -> unit Logical.t -end - -(** Lens to the [proofview]. *) -module Pv : State with type t := proofview - -(** Lens to the [evar_map] of the proofview. *) -module Solution : State with type t := Evd.evar_map - -(** Lens to the list of focused goals. *) -module Comb : State with type t = Evar.t list - -(** Lens to the global environment. *) -module Env : State with type t := Environ.env - -(** Lens to the tactic status ([true] if safe, [false] if unsafe) *) -module Status : Writer with type t := bool - -(** Lens to the list of goals which have been shelved during the - execution of the tactic. *) -module Shelf : State with type t = Evar.t list - -(** Lens to the list of goals which were given up during the execution - of the tactic. *) -module Giveup : Writer with type t = Evar.t list - -(** Lens and utilies pertaining to the info trace *) -module InfoL : sig - (** [record_trace t] behaves like [t] and compute its [info] trace. *) - val record_trace : 'a Logical.t -> 'a Logical.t - - val update : (Info.state -> Info.state) -> unit Logical.t - val opn : Info.tag -> unit Logical.t - val close : unit Logical.t - val leaf : Info.tag -> unit Logical.t - - (** [tag a t] opens tag [a] runs [t] then closes the tag. *) - val tag : Info.tag -> 'a Logical.t -> 'a Logical.t -end diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ea21917ac4..2d886b8e1f 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -158,8 +158,6 @@ let make_flag env f = f.rConst red in red -let is_reference = function PRef _ | PVar _ -> true | _ -> false - (* table of custom reductino fonctions, not synchronized, filled via ML calls to [declare_reduction] *) let reduction_tab = ref String.Map.empty @@ -196,7 +194,7 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let e_red f env evm c = evm, f env evm c +let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl only reduce at the head when an evaluable reference is given, e.g. diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458cf..186525e159 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -13,7 +13,7 @@ open Evd open Environ open Proof_type open Logic - +open Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -197,12 +197,12 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.named_context = pf_hyps goal in + let oldhyps:Context.Named.t = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.named_context list = + let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in + let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,7 +215,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in pp (str (emacs_str "<infoH>") diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 13a9be59e3..dd9153a023 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Evd open Proof_type @@ -16,7 +15,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a75b6fa0fd..33cef7486b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -18,6 +18,8 @@ open Tacred open Proof_type open Logic open Refiner +open Sigma.Notations +open Context.Named.Declaration let re_sig it gc = { it = it; sigma = gc; } @@ -40,21 +42,22 @@ let pf_hyps = Refiner.pf_hyps let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) let pf_hyps_types gls = let sign = Environ.named_context (pf_env gls) in - List.map (fun (id,_,x) -> (id, x)) sign + List.map (function LocalAssum (id,x) + | LocalDef (id,_,x) -> id, x) + sign -let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id +let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = try - Context.lookup_named id (pf_hyps gls) + Context.Named.lookup id (pf_hyps gls) with Not_found -> raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - let (_,_,ty)= (pf_get_hyp gls id) in - ty + pf_get_hyp gls id |> get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -70,7 +73,10 @@ let pf_get_new_ids ids gls = let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_reduction_of_red_expr gls re c = - (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c + let (redfun, _) = reduction_of_red_expr (pf_env gls) re in + let sigma = Sigma.Unsafe.of_evar_map (project gls) in + let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in + (Sigma.to_evar_map sigma, c) let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = @@ -95,7 +101,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv @@ -158,11 +164,15 @@ let pr_glls glls = (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct + let project gl = + let sigma = Proofview.Goal.sigma gl in + Sigma.to_evar_map sigma + let pf_apply f gl = - f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + f (Proofview.Goal.env gl) (project gl) let of_old f gl = - f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl } + f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } let pf_global id gl = (** We only check for the existence of an [id] in [hyps] *) @@ -194,29 +204,30 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.hyps gl in let sign = - try Context.lookup_named id hyps + try Context.Named.lookup id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign let pf_get_hyp_typ id gl = - let (_,_,ty) = pf_get_hyp id gl in - ty + pf_get_hyp id gl |> get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in let sign = Environ.named_context env in - List.map (fun (id,_,x) -> (id, x)) sign + List.map (function LocalAssum (id,x) + | LocalDef (id,_,x) -> id, x) + sign let pf_last_hyp gl = let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) = (** We normalize the conclusion just after *) let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = project gl in nf_evar sigma concl let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t @@ -235,6 +246,6 @@ module New = struct let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t + let pf_nf_evar gl t = nf_evar (project gl) t end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7e943cb18d..f786b5f218 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Evd open Proof_type @@ -34,18 +33,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration +val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> named_declaration +val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -106,36 +105,38 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : identifier -> 'a Proofview.Goal.t -> constr - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + (** FIXME: encapsulate the level in an existential type. *) + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : [ `NF ] Proofview.Goal.t -> types + val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map + val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types - val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool - val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list + val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> [ `NF ] Proofview.Goal.t -> types - val pf_last_hyp : [ `NF ] Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr end diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml deleted file mode 100644 index a4a447e88f..0000000000 --- a/proofs/tactic_debug.ml +++ /dev/null @@ -1,318 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names -open Pp -open Tacexpr -open Termops -open Nameops - -let (prtac, tactic_printer) = Hook.make () -let (prmatchpatt, match_pattern_printer) = Hook.make () -let (prmatchrl, match_rule_printer) = Hook.make () - - -(* This module intends to be a beginning of debugger for tactic expressions. - Currently, it is quite simple and we can hope to have, in the future, a more - complete panel of commands dedicated to a proof assistant framework *) - -(* Debug information *) -type debug_info = - | DebugOn of int - | DebugOff - -(* An exception handler *) -let explain_logic_error = ref (fun e -> mt()) - -let explain_logic_error_no_anomaly = ref (fun e -> mt()) - -let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) -let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) - -(* Prints the goal *) - -let db_pr_goal gl = - let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - let penv = print_named_context env in - let pc = print_constr_env env concl in - str" " ++ hv 0 (penv ++ fnl () ++ - str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () - -let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> - let pg = db_pr_goal gl in - Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) - end - - -(* Prints the commands *) -let help () = - msg_tac_debug (str "Commands: <Enter> = Continue" ++ fnl() ++ - str " h/? = Help" ++ fnl() ++ - str " r <num> = Run <num> times" ++ fnl() ++ - str " r <string> = Run up to next idtac <string>" ++ fnl() ++ - str " s = Skip" ++ fnl() ++ - str " x = Exit") - -(* Prints the goal and the command to be executed *) -let goal_com tac = - Proofview.tclTHEN - db_pr_goal - (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac))) - -(* [run (new_ref _)] gives us a ref shared among [NonLogical.t] - expressions. It avoids parametrizing everything over a - reference. *) -let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) -let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) -let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None) - -let rec drop_spaces inst i = - if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1) - else i - -let possibly_unquote s = - if String.length s >= 2 && s.[0] == '"' && s.[String.length s - 1] == '"' then - String.sub s 1 (String.length s - 2) - else - s - -(* (Re-)initialize debugger *) -let db_initialize = - let open Proofview.NonLogical in - (skip:=0) >> (skipped:=0) >> (breakpoint:=None) - -let int_of_string s = - try Proofview.NonLogical.return (int_of_string s) - with e -> Proofview.NonLogical.raise e - -let string_get s i = - try Proofview.NonLogical.return (String.get s i) - with e -> Proofview.NonLogical.raise e - -(* Gives the number of steps or next breakpoint of a run command *) -let run_com inst = - let open Proofview.NonLogical in - string_get inst 0 >>= fun first_char -> - if first_char ='r' then - let i = drop_spaces inst 1 in - if String.length inst > i then - let s = String.sub inst i (String.length inst - i) in - if inst.[0] >= '0' && inst.[0] <= '9' then - int_of_string s >>= fun num -> - (if num<0 then invalid_arg "run_com" else return ()) >> - (skip:=num) >> (skipped:=0) - else - breakpoint:=Some (possibly_unquote s) - else - invalid_arg "run_com" - else - invalid_arg "run_com" - -(* Prints the run counter *) -let run ini = - let open Proofview.NonLogical in - if not ini then - begin - Proofview.NonLogical.print_notice (str"\b\r\b\r") >> - !skipped >>= fun skipped -> - msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl()) - end >> - !skipped >>= fun x -> - skipped := x+1 - else - return () - -(* Prints the prompt *) -let rec prompt level = - (* spiwack: avoid overriding by the open below *) - let runtrue = run true in - begin - let open Proofview.NonLogical in - Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> - let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in - Proofview.NonLogical.catch Proofview.NonLogical.read_line - begin function (e, info) -> match e with - | End_of_file -> exit - | e -> raise ~info e - end - >>= fun inst -> - match inst with - | "" -> return (DebugOn (level+1)) - | "s" -> return (DebugOff) - | "x" -> Proofview.NonLogical.print_char '\b' >> exit - | "h"| "?" -> - begin - help () >> - prompt level - end - | _ -> - Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1))) - begin function (e, info) -> match e with - | Failure _ | Invalid_argument _ -> prompt level - | e -> raise ~info e - end - end - -(* Prints the state and waits for an instruction *) -(* spiwack: the only reason why we need to take the continuation [f] - as an argument rather than returning the new level directly seems to - be that [f] is wrapped in with "explain_logic_error". I don't think - it serves any purpose in the current design, so we could just drop - that. *) -let debug_prompt lev tac f = - (* spiwack: avoid overriding by the open below *) - let runfalse = run false in - let open Proofview.NonLogical in - let (>=) = Proofview.tclBIND in - (* What to print and to do next *) - let newlevel = - Proofview.tclLIFT !skip >= fun initial_skip -> - if Int.equal initial_skip 0 then - Proofview.tclLIFT !breakpoint >= fun breakpoint -> - if Option.is_empty breakpoint then Proofview.tclTHEN (goal_com tac) (Proofview.tclLIFT (prompt lev)) - else Proofview.tclLIFT(runfalse >> return (DebugOn (lev+1))) - else Proofview.tclLIFT begin - (!skip >>= fun s -> skip:=s-1) >> - runfalse >> - !skip >>= fun new_skip -> - (if Int.equal new_skip 0 then skipped:=0 else return ()) >> - return (DebugOn (lev+1)) - end in - newlevel >= fun newlevel -> - (* What to execute *) - Proofview.tclOR - (f newlevel) - begin fun (reraise, info) -> - Proofview.tclTHEN - (Proofview.tclLIFT begin - (skip:=0) >> (skipped:=0) >> - if Logic.catchable_exception reraise then - msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise) - else return () - end) - (Proofview.tclZERO ~info reraise) - end - -let is_debug db = - let open Proofview.NonLogical in - !breakpoint >>= fun breakpoint -> - match db, breakpoint with - | DebugOff, _ -> return false - | _, Some _ -> return false - | _ -> - !skip >>= fun skip -> - return (Int.equal skip 0) - -(* Prints a constr *) -let db_constr debug env c = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c) - else return () - -(* Prints the pattern rule *) -let db_pattern_rule debug num r = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - begin - msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++ - str "|" ++ spc () ++ Hook.get prmatchrl r) - end - else return () - -(* Prints the hypothesis pattern identifier if it exists *) -let hyp_bound = function - | Anonymous -> str " (unbound)" - | Name id -> str " (bound to " ++ pr_id id ++ str ")" - -(* Prints a matched hypothesis *) -let db_matched_hyp debug env (id,_,c) ido = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env c) - else return () - -(* Prints the matched conclusion *) -let db_matched_concl debug env c = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c) - else return () - -(* Prints a success message when the goal has been matched *) -let db_mc_pattern_success debug = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++ - str "Let us execute the right-hand side part..." ++ fnl()) - else return () - -(* Prints a failure message for an hypothesis pattern *) -let db_hyp_pattern_failure debug env sigma (na,hyp) = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ - str " cannot match: " ++ - Hook.get prmatchpatt env sigma hyp) - else return () - -(* Prints a matching failure message for a rule *) -let db_matching_failure debug = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++ - str "Let us try the next one...") - else return () - -(* Prints an evaluation failure message for a rule *) -let db_eval_failure debug s = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - let s = str "message \"" ++ s ++ str "\"" in - msg_tac_debug - (str "This rule has failed due to \"Fail\" tactic (" ++ - s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") - else return () - -(* Prints a logic failure message for a rule *) -let db_logic_failure debug err = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - begin - msg_tac_debug (Pervasives.(!) explain_logic_error err) >> - msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++ - str "Let us try the next one...") - end - else return () - -let is_breakpoint brkname s = match brkname, s with - | Some s, MsgString s'::_ -> String.equal s s' - | _ -> false - -let db_breakpoint debug s = - let open Proofview.NonLogical in - !breakpoint >>= fun opt_breakpoint -> - match debug with - | DebugOn lev when not (CList.is_empty s) && is_breakpoint opt_breakpoint s -> - breakpoint:=None - | _ -> - return () diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli deleted file mode 100644 index 215c5b29b5..0000000000 --- a/proofs/tactic_debug.mli +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Environ -open Pattern -open Names -open Tacexpr -open Term -open Evd - -(** This module intends to be a beginning of debugger for tactic expressions. - Currently, it is quite simple and we can hope to have, in the future, a more - complete panel of commands dedicated to a proof assistant framework *) - -val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t -val match_pattern_printer : - (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t -val match_rule_printer : - ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t - -(** Debug information *) -type debug_info = - | DebugOn of int - | DebugOff - -(** Prints the state and waits *) -val debug_prompt : - int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic - -(** Initializes debugger *) -val db_initialize : unit Proofview.NonLogical.t - -(** Prints a constr *) -val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t - -(** Prints the pattern rule *) -val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t - -(** Prints a matched hypothesis *) -val db_matched_hyp : - debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t - -(** Prints the matched conclusion *) -val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t - -(** Prints a success message when the goal has been matched *) -val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t - -(** Prints a failure message for an hypothesis pattern *) -val db_hyp_pattern_failure : - debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t - -(** Prints a matching failure message for a rule *) -val db_matching_failure : debug_info -> unit Proofview.NonLogical.t - -(** Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t - -(** An exception handler *) -val explain_logic_error: (exn -> Pp.std_ppcmds) ref - -(** For use in the Ltac debugger: some exception that are usually - consider anomalies are acceptable because they are caught later in - the process that is being debugged. One should not require - from users that they report these anomalies. *) -val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref - -(** Prints a logic failure message for a rule *) -val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t - -(** Prints a logic failure message for a rule *) -val db_breakpoint : debug_info -> - Id.t Loc.located message_token list -> unit Proofview.NonLogical.t |