From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Dec 2016 18:14:58 +0100 Subject: [stm] Break stm/toplevel dependency loop. Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. --- vernac/auto_ind_decl.ml | 969 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 969 insertions(+) create mode 100644 vernac/auto_ind_decl.ml (limited to 'vernac/auto_ind_decl.ml') diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml new file mode 100644 index 000000000..594f2e944 --- /dev/null +++ b/vernac/auto_ind_decl.ml @@ -0,0 +1,969 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] + | t::q -> t::(kick_last q) + | [] -> failwith "kick_last" +and aux = function + | (0,l') -> l' + | (n,h::t) -> aux (n-1,t) + | _ -> failwith "quick_chop" + in + if n > (List.length l) then failwith "quick_chop args" + else kick_last (aux (n,l) ) + +let deconstruct_type t = + let l,r = decompose_prod t in + (List.rev_map snd l)@[r] + +exception EqNotFound of inductive * inductive +exception EqUnknown of string +exception UndefinedCst of string +exception InductiveWithProduct +exception InductiveWithSort +exception ParameterWithoutEquality of global_reference +exception NonSingletonProp of inductive +exception DecidabilityMutualNotSupported +exception NoDecidabilityCoInductive + +let dl = Loc.ghost + +let constr_of_global g = lazy (Universes.constr_of_global g) + +(* Some pre declaration of constant we are going to use *) +let bb = constr_of_global Coqlib.glob_bool + +let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop + +let andb_true_intro = fun _ -> + (Coqlib.build_bool_type()).Coqlib.andb_true_intro + +let tt = constr_of_global Coqlib.glob_true + +let ff = constr_of_global Coqlib.glob_false + +let eq = constr_of_global Coqlib.glob_eq + +let sumbool = Coqlib.build_coq_sumbool + +let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb + +let induct_on c = induction false None c None None + +let destruct_on c = destruct false None c None None + +let destruct_on_using c id = + destruct false None c + (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous]; + [dl,IntroNaming (IntroIdentifier id)]])) + None + +let destruct_on_as c l = + destruct false None c (Some (dl,l)) None + +(* reconstruct the inductive with the correct deBruijn indexes *) +let mkFullInd (ind,u) n = + let mib = Global.lookup_mind (fst ind) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + (* params context divided *) + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + if nparrec > 0 + then mkApp (mkIndU (ind,u), + Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec)) + else mkIndU (ind,u) + +let check_bool_is_defined () = + try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in () + with e when CErrors.noncritical e -> raise (UndefinedCst "bool") + +let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") + +let build_beq_scheme mode kn = + check_bool_is_defined (); + (* fetching global env *) + let env = Global.env() in + (* fetching the mutual inductive body *) + let mib = Global.lookup_mind kn in + (* number of inductives in the mutual *) + let nb_ind = Array.length mib.mind_packets in + (* number of params in the type *) + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + (* params context divided *) + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + (* predef coq's boolean type *) + (* rec name *) + let rec_name i =(Id.to_string (Array.get mib.mind_packets i).mind_typename)^ + "_eqrec" + in + (* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *) + let create_input c = + let myArrow u v = mkArrow u (lift 1 v) + and eqName = function + | Name s -> Id.of_string ("eq_"^(Id.to_string s)) + | Anonymous -> Id.of_string "eq_A" + in + let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in + let lift_cnt = ref 0 in + let eqs_typ = List.map (fun aa -> + let a = lift !lift_cnt aa in + incr lift_cnt; + myArrow a (myArrow a (Lazy.force bb)) + ) ext_rel_list in + + let eq_input = List.fold_left2 + ( fun a b decl -> (* mkLambda(n,b,a) ) *) + (* here I leave the Naming thingy so that the type of + the function is more readable for the user *) + mkNamedLambda (eqName (RelDecl.get_name decl)) b a ) + c (List.rev eqs_typ) lnamesparrec + in + List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) + (* Same here , hoping the auto renaming will do something good ;) *) + mkNamedLambda + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec + in + let make_one_eq cur = + let u = Univ.Instance.empty in + let ind = (kn,cur),u (* FIXME *) in + (* current inductive we are working on *) + let cur_packet = mib.mind_packets.(snd (fst ind)) in + (* Inductive toto : [rettyp] := *) + let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in + (* split rettyp in a list without the non rec params and the last -> + e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) + let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in + (* give a type A, this function tries to find the equality on A declared + previously *) + (* nlist = the number of args (A , B , ... ) + eqA = the deBruijn index of the first eq param + ndx = how much to translate due to the 2nd Case + *) + let compute_A_equality rel_list nlist eqA ndx t = + let lifti = ndx in + let rec aux c = + let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in + match kind_of_term c with + | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Var x -> + let eid = id_of_string ("eq_"^(string_of_id x)) in + let () = + try ignore (Environ.lookup_named eid env) + with Not_found -> raise (ParameterWithoutEquality (VarRef x)) + in + mkVar eid, Safe_typing.empty_private_constants + | Cast (x,_,_) -> aux (applist (x,a)) + | App _ -> assert false + | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> + if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants + else begin + try + let eq, eff = + let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in + mkConst c, eff in + let eqa, eff = + let eqa, effs = List.split (List.map aux a) in + Array.of_list eqa, + List.fold_left Safe_typing.concat_private eff (List.rev effs) + in + let args = + Array.append + (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in + if Int.equal (Array.length args) 0 then eq, eff + else mkApp (eq, args), eff + with Not_found -> raise(EqNotFound (ind', fst ind)) + end + | Sort _ -> raise InductiveWithSort + | Prod _ -> raise InductiveWithProduct + | Lambda _-> raise (EqUnknown "abstraction") + | LetIn _ -> raise (EqUnknown "let-in") + | Const kn -> + (match Environ.constant_opt_value_in env kn with + | None -> raise (ParameterWithoutEquality (ConstRef (fst kn))) + | Some c -> aux (applist (c,a))) + | Proj _ -> raise (EqUnknown "projection") + | Construct _ -> raise (EqUnknown "constructor") + | Case _ -> raise (EqUnknown "match") + | CoFix _ -> raise (EqUnknown "cofix") + | Fix _ -> raise (EqUnknown "fix") + | Meta _ -> raise (EqUnknown "meta-variable") + | Evar _ -> raise (EqUnknown "existential variable") + in + aux t + in + (* construct the predicate for the Case part*) + let do_predicate rel_list n = + List.fold_left (fun a b -> mkLambda(Anonymous,b,a)) + (mkLambda (Anonymous, + mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), + (Lazy.force bb))) + (List.rev rettyp_l) in + (* make_one_eq *) + (* do the [| C1 ... => match Y with ... end + ... + Cn => match Y with ... end |] part *) + let ci = make_case_info env (fst ind) MatchStyle in + let constrs n = get_constructors env (make_ind_family (ind, + Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in + let constrsi = constrs (3+nparrec) in + let n = Array.length constrsi in + let ar = Array.make n (Lazy.force ff) in + let eff = ref Safe_typing.empty_private_constants in + for i=0 to n-1 do + let nb_cstr_args = List.length constrsi.(i).cs_args in + let ar2 = Array.make n (Lazy.force ff) in + let constrsj = constrs (3+nparrec+nb_cstr_args) in + for j=0 to n-1 do + if Int.equal i j then + ar2.(j) <- let cc = (match nb_cstr_args with + | 0 -> Lazy.force tt + | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in + for ndx = 0 to nb_cstr_args-1 do + let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in + let eqA, eff' = compute_A_equality rel_list + nparrec + (nparrec+3+2*nb_cstr_args) + (nb_cstr_args+ndx+1) + cc + in + eff := Safe_typing.concat_private eff' !eff; + Array.set eqs ndx + (mkApp (eqA, + [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] + )) + done; + Array.fold_left + (fun a b -> mkApp (andb(),[|b;a|])) + (eqs.(0)) + (Array.sub eqs 1 (nb_cstr_args - 1)) + ) + in + (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc + (constrsj.(j).cs_args) + ) + else ar2.(j) <- (List.fold_left (fun a decl -> + mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) + done; + + ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) + (mkCase (ci,do_predicate rel_list nb_cstr_args, + mkVar (Id.of_string "Y") ,ar2)) + (constrsi.(i).cs_args)) + done; + mkNamedLambda (Id.of_string "X") (mkFullInd ind (nb_ind-1+1)) ( + mkNamedLambda (Id.of_string "Y") (mkFullInd ind (nb_ind-1+2)) ( + mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))), + !eff + in (* build_beq_scheme *) + let names = Array.make nb_ind Anonymous and + types = Array.make nb_ind mkSet and + cores = Array.make nb_ind mkSet in + let eff = ref Safe_typing.empty_private_constants in + let u = Univ.Instance.empty in + for i=0 to (nb_ind-1) do + names.(i) <- Name (Id.of_string (rec_name i)); + types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) + (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb)); + let c, eff' = make_one_eq i in + cores.(i) <- c; + eff := Safe_typing.concat_private eff' !eff + done; + (Array.init nb_ind (fun i -> + let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in + if not (Sorts.List.mem InSet kelim) then + raise (NonSingletonProp (kn,i)); + if mib.mind_finite = Decl_kinds.CoFinite then + raise NoDecidabilityCoInductive; + let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in + create_input fix), + Evd.make_evar_universe_context (Global.env ()) None), + !eff + +let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme + +let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind + +(* This function tryies to get the [inductive] between a constr + the constr should be Ind i or App(Ind i,[|args|]) +*) +let destruct_ind c = + try let u,v = destApp c in + let indc = destInd u in + indc,v + with DestKO -> let indc = destInd c in + indc,[||] + +(* + In the following, avoid is the list of names to avoid. + If the args of the Inductive type are A1 ... An + then avoid should be + [| lb_An ... lb _A1 (resp. bl_An ... bl_A1) + eq_An .... eq_A1 An ... A1 |] +so from Ai we can find the the correct eq_Ai bl_ai or lb_ai +*) +(* used in the leib -> bool side*) +let do_replace_lb mode lb_scheme_key aavoid narg p q = + let avoid = Array.of_list aavoid in + let do_arg v offset = + try + let x = narg*offset in + let s = destVar v in + let n = Array.length avoid in + let rec find i = + if Id.equal avoid.(n-i) s then avoid.(n-i-x) + else (if i + (* if this happen then the args have to be already declared as a + Parameter*) + ( + let mp,dir,lbl = repr_con (fst (destConst v)) in + mkConst (make_con mp dir (mk_label ( + if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) + else ((Label.to_string lbl)^"_lb") + ))) + ) + in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in + let u,v = destruct_ind type_of_pq + in let lb_type_of_p = + try + let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in + Proofview.tclUNIT (mkConst c, eff) + with Not_found -> + (* spiwack: the format of this error message should probably + be improved. *) + let err_msg = + (str "Leibniz->boolean:" ++ + str "You have to declare the" ++ + str "decidability over " ++ + Printer.pr_constr type_of_pq ++ + str " first.") + in + Tacticals.New.tclZEROMSG err_msg + in + lb_type_of_p >>= fun (lb_type_of_p,eff) -> + let lb_args = Array.append (Array.append + (Array.map (fun x -> x) v) + (Array.map (fun x -> do_arg x 1) v)) + (Array.map (fun x -> do_arg x 2) v) + in let app = if Array.equal eq_constr lb_args [||] + then lb_type_of_p else mkApp (lb_type_of_p,lb_args) + in + Tacticals.New.tclTHENLIST [ + Proofview.tclEFFECTS eff; + Equality.replace p q ; apply app ; Auto.default_auto] + end } + +(* used in the bool -> leib side *) +let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = + let avoid = Array.of_list aavoid in + let do_arg v offset = + try + let x = narg*offset in + let s = destVar v in + let n = Array.length avoid in + let rec find i = + if Id.equal avoid.(n-i) s then avoid.(n-i-x) + else (if i + (* if this happen then the args have to be already declared as a + Parameter*) + ( + let mp,dir,lbl = repr_con (fst (destConst v)) in + mkConst (make_con mp dir (mk_label ( + if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) + else ((Label.to_string lbl)^"_bl") + ))) + ) + in + + let rec aux l1 l2 = + match (l1,l2) with + | (t1::q1,t2::q2) -> + Proofview.Goal.enter { enter = begin fun gl -> + let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in + if eq_constr t1 t2 then aux q1 q2 + else ( + let u,v = try destruct_ind tt1 + (* trick so that the good sequence is returned*) + with e when CErrors.noncritical e -> indu,[||] + in if eq_ind (fst u) ind + then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ] + else ( + let bl_t1, eff = + try + let c, eff = find_scheme bl_scheme_key (out_punivs u) (*FIXME*) in + mkConst c, eff + with Not_found -> + (* spiwack: the format of this error message should probably + be improved. *) + let err_msg = string_of_ppcmds + (str "boolean->Leibniz:" ++ + str "You have to declare the" ++ + str "decidability over " ++ + Printer.pr_constr tt1 ++ + str " first.") + in + error err_msg + in let bl_args = + Array.append (Array.append + (Array.map (fun x -> x) v) + (Array.map (fun x -> do_arg x 1) v)) + (Array.map (fun x -> do_arg x 2) v ) + in + let app = if Array.equal eq_constr bl_args [||] + then bl_t1 else mkApp (bl_t1,bl_args) + in + Tacticals.New.tclTHENLIST [ + Proofview.tclEFFECTS eff; + Equality.replace_by t1 t2 + (Tacticals.New.tclTHEN (apply app) (Auto.default_auto)) ; + aux q1 q2 ] + ) + ) + end } + | ([],[]) -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") + in + begin try Proofview.tclUNIT (destApp lft) + with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") + end >>= fun (ind1,ca1) -> + begin try Proofview.tclUNIT (destApp rgt) + with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") + end >>= fun (ind2,ca2) -> + begin try Proofview.tclUNIT (out_punivs (destInd ind1)) + with DestKO -> + begin try Proofview.tclUNIT (fst (fst (destConstruct ind1))) + with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") + end + end >>= fun (sp1,i1) -> + begin try Proofview.tclUNIT (out_punivs (destInd ind2)) + with DestKO -> + begin try Proofview.tclUNIT (fst (fst (destConstruct ind2))) + with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") + end + end >>= fun (sp2,i2) -> + if not (eq_mind sp1 sp2) || not (Int.equal i1 i2) + then Tacticals.New.tclZEROMSG (str "Eq should be on the same type") + else aux (Array.to_list ca1) (Array.to_list ca2) + +(* + create, from a list of ids [i1,i2,...,in] the list + [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] +*) +let list_id l = List.fold_left ( fun a decl -> let s' = + match RelDecl.get_name decl with + Name s -> Id.to_string s + | Anonymous -> "A" in + (Id.of_string s',Id.of_string ("eq_"^s'), + Id.of_string (s'^"_bl"), + Id.of_string (s'^"_lb")) + ::a + ) [] l +(* + build the right eq_I A B.. N eq_A .. eq_N +*) +let eqI ind l = + let list_id = list_id l in + let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@ + (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) + and e, eff = + try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff + with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" + (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed."); + in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff + +(**********************************************************************) +(* Boolean->Leibniz *) + +open Namegen + +let compute_bl_goal ind lnamesparrec nparrec = + let eqI, eff = eqI ind lnamesparrec in + let list_id = list_id lnamesparrec in + let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let create_input c = + let x = next_ident_away (Id.of_string "x") avoid and + y = next_ident_away (Id.of_string "y") avoid in + let bl_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(mkVar seq,[|mkVar x;mkVar y|]);(Lazy.force tt)|])) + ( mkApp(Lazy.force eq,[|mkVar s;mkVar x;mkVar y|])) + )) + ) list_id in + let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> + mkNamedProd sbl b a + ) c (List.rev list_id) (List.rev bl_typ) in + let eqs_typ = List.map (fun (s,_,_,_) -> + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(Lazy.force bb))) + ) list_id in + let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> + mkNamedProd seq b a + ) bl_input (List.rev list_id) (List.rev eqs_typ) in + List.fold_left (fun a decl -> mkNamedProd + (match RelDecl.get_name decl with Name s -> s | Anonymous -> next_ident_away (Id.of_string "A") avoid) + (RelDecl.get_type decl) a) eq_input lnamesparrec + in + let n = next_ident_away (Id.of_string "x") avoid and + m = next_ident_away (Id.of_string "y") avoid in + let u = Univ.Instance.empty in + create_input ( + mkNamedProd n (mkFullInd (ind,u) nparrec) ( + mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) ( + mkArrow + (mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(eqI,[|mkVar n;mkVar m|]);(Lazy.force tt)|])) + (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) + ))), eff + +let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let avoid = ref [] in + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) @ + ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @ + ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) + in + let fresh_id s gl = + Tacmach.New.of_old begin fun gsig -> + let fresh = fresh_id (!avoid) s gsig in + avoid := fresh::(!avoid); fresh + end gl + in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in + let freshn = fresh_id (Id.of_string "x") gl in + let freshm = fresh_id (Id.of_string "y") gl in + let freshz = fresh_id (Id.of_string "Z") gl in + (* try with *) + Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; + intro_using freshn ; + induct_on (mkVar freshn); + intro_using freshm; + destruct_on (mkVar freshm); + intro_using freshz; + intros; + Tacticals.New.tclTRY ( + Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) + ); + simpl_in_hyp (freshz,Locus.InHyp); +(* +repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). +*) + Tacticals.New.tclREPEAT ( + Tacticals.New.tclTHENLIST [ + Simple.apply_in freshz (andb_prop()); + Proofview.Goal.nf_enter { enter = begin fun gl -> + let fresht = fresh_id (Id.of_string "Z") gl in + destruct_on_as (mkVar freshz) + (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht); + dl,IntroNaming (IntroIdentifier freshz)]]) + end } + ]); +(* + Ci a1 ... an = Ci b1 ... bn + replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto +*) + Proofview.Goal.nf_enter { enter = begin fun gls -> + let gl = Proofview.Goal.concl gls in + match (kind_of_term gl) with + | App (c,ca) -> ( + match (kind_of_term c) with + | Ind (indeq, u) -> + if eq_gr (IndRef indeq) Coqlib.glob_eq + then + Tacticals.New.tclTHEN + (do_replace_bl mode bl_scheme_key ind + (!avoid) + nparrec (ca.(2)) + (ca.(1))) + Auto.default_auto + else + Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") + ) + | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + end } + + ] + end } + +let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") + +let side_effect_of_mode = function + | Declare.UserAutomaticRequest -> false + | Declare.InternalTacticRequest -> true + | Declare.UserIndividualRequest -> false + +let make_bl_scheme mode mind = + let mib = Global.lookup_mind mind in + if not (Int.equal (Array.length mib.mind_packets) 1) then + user_err + (str "Automatic building of boolean->Leibniz lemmas not supported"); + let ind = (mind,0) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + let lnonparrec,lnamesparrec = (* TODO subst *) + context_chop (nparams-nparrec) mib.mind_params_ctxt in + let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + in + ([|ans|], ctx), eff + +let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme + +let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind + +(**********************************************************************) +(* Leibniz->Boolean *) + +let compute_lb_goal ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in + let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let eqI, eff = eqI ind lnamesparrec in + let create_input c = + let x = next_ident_away (Id.of_string "x") avoid and + y = next_ident_away (Id.of_string "y") avoid in + let lb_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + )) + ) list_id in + let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b -> + mkNamedProd slb b a + ) c (List.rev list_id) (List.rev lb_typ) in + let eqs_typ = List.map (fun (s,_,_,_) -> + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) + ) list_id in + let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> + mkNamedProd seq b a + ) lb_input (List.rev list_id) (List.rev eqs_typ) in + List.fold_left (fun a decl -> mkNamedProd + (match (RelDecl.get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec + in + let n = next_ident_away (Id.of_string "x") avoid and + m = next_ident_away (Id.of_string "y") avoid in + let u = Univ.Instance.empty in + create_input ( + mkNamedProd n (mkFullInd (ind,u) nparrec) ( + mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) ( + mkArrow + (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|])) + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) + ))), eff + +let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let avoid = ref [] in + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) @ + ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ + ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in + let fresh_id s gl = + Tacmach.New.of_old begin fun gsig -> + let fresh = fresh_id (!avoid) s gsig in + avoid := fresh::(!avoid); fresh + end gl + in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in + let freshn = fresh_id (Id.of_string "x") gl in + let freshm = fresh_id (Id.of_string "y") gl in + let freshz = fresh_id (Id.of_string "Z") gl in + (* try with *) + Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; + intro_using freshn ; + induct_on (mkVar freshn); + intro_using freshm; + destruct_on (mkVar freshm); + intro_using freshz; + intros; + Tacticals.New.tclTRY ( + Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) + ); + Equality.inj None false None (mkVar freshz,NoBindings); + intros; simpl_in_concl; + Auto.default_auto; + Tacticals.New.tclREPEAT ( + Tacticals.New.tclTHENLIST [apply (andb_true_intro()); + simplest_split ;Auto.default_auto ] + ); + Proofview.Goal.nf_enter { enter = begin fun gls -> + let gl = Proofview.Goal.concl gls in + (* assume the goal to be eq (eq_type ...) = true *) + match (kind_of_term gl) with + | App(c,ca) -> (match (kind_of_term ca.(1)) with + | App(c',ca') -> + let n = Array.length ca' in + do_replace_lb mode lb_scheme_key + (!avoid) + nparrec + ca'.(n-2) ca'.(n-1) + | _ -> + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") + ) + | _ -> + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") + end } + ] + end } + +let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") + +let make_lb_scheme mode mind = + let mib = Global.lookup_mind mind in + if not (Int.equal (Array.length mib.mind_packets) 1) then + user_err + (str "Automatic building of Leibniz->boolean lemmas not supported"); + let ind = (mind,0) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + in + ([|ans|], ctx), eff + +let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme + +let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind + +(**********************************************************************) +(* Decidable equality *) + +let check_not_is_defined () = + try ignore (Coqlib.build_coq_not ()) + with e when CErrors.noncritical e -> raise (UndefinedCst "not") + +(* {n=m}+{n<>m} part *) +let compute_dec_goal ind lnamesparrec nparrec = + check_not_is_defined (); + let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in + let list_id = list_id lnamesparrec in + let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let create_input c = + let x = next_ident_away (Id.of_string "x") avoid and + y = next_ident_away (Id.of_string "y") avoid in + let lb_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + )) + ) list_id in + let bl_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + )) + ) list_id in + + let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b -> + mkNamedProd slb b a + ) c (List.rev list_id) (List.rev lb_typ) in + let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> + mkNamedProd sbl b a + ) lb_input (List.rev list_id) (List.rev bl_typ) in + + let eqs_typ = List.map (fun (s,_,_,_) -> + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) + ) list_id in + let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> + mkNamedProd seq b a + ) bl_input (List.rev list_id) (List.rev eqs_typ) in + List.fold_left (fun a decl -> mkNamedProd + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec + in + let n = next_ident_away (Id.of_string "x") avoid and + m = next_ident_away (Id.of_string "y") avoid in + let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in + create_input ( + mkNamedProd n (mkFullInd ind (2*nparrec)) ( + mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( + mkApp(sumbool(),[|eqnm;mkApp (Coqlib.build_coq_not(),[|eqnm|])|]) + ) + ) + ) + +let compute_dec_tact ind lnamesparrec nparrec = + let eq = Lazy.force eq and tt = Lazy.force tt + and ff = Lazy.force ff and bb = Lazy.force bb in + let list_id = list_id lnamesparrec in + let eqI, eff = eqI ind lnamesparrec in + let avoid = ref [] in + let eqtrue x = mkApp(eq,[|bb;x;tt|]) in + let eqfalse x = mkApp(eq,[|bb;x;ff|]) in + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) @ + ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ + ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @ + ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in + let fresh_id s gl = + Tacmach.New.of_old begin fun gsig -> + let fresh = fresh_id (!avoid) s gsig in + avoid := fresh::(!avoid); fresh + end gl + in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in + let freshn = fresh_id (Id.of_string "x") gl in + let freshm = fresh_id (Id.of_string "y") gl in + let freshH = fresh_id (Id.of_string "H") gl in + let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in + let arfresh = Array.of_list fresh_first_intros in + let xargs = Array.sub arfresh 0 (2*nparrec) in + begin try + let c, eff = find_scheme bl_scheme_kind ind in + Proofview.tclUNIT (mkConst c,eff) with + Not_found -> + Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.") + end >>= fun (blI,eff') -> + begin try + let c, eff = find_scheme lb_scheme_kind ind in + Proofview.tclUNIT (mkConst c,eff) with + Not_found -> + Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") + end >>= fun (lbI,eff'') -> + let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in + Tacticals.New.tclTHENLIST [ + Proofview.tclEFFECTS eff; + intros_using fresh_first_intros; + intros_using [freshn;freshm]; + (*we do this so we don't have to prove the same goal twice *) + assert_by (Name freshH) ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + ) + (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto); + + Proofview.Goal.nf_enter { enter = begin fun gl -> + let freshH2 = fresh_id (Id.of_string "H") gl in + Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [ + (* left *) + Tacticals.New.tclTHENLIST [ + simplest_left; + apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)); + Auto.default_auto + ] + ; + + (*right *) + Proofview.Goal.nf_enter { enter = begin fun gl -> + let freshH3 = fresh_id (Id.of_string "H") gl in + Tacticals.New.tclTHENLIST [ + simplest_right ; + unfold_constr (Lazy.force Coqlib.coq_not_ref); + intro; + Equality.subst_all (); + assert_by (Name freshH3) + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) + (Tacticals.New.tclTHENLIST [ + apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)); + Auto.default_auto + ]); + Equality.general_rewrite_bindings_in true + Locus.AllOccurrences true false + (List.hd !avoid) + ((mkVar (List.hd (List.tl !avoid))), + NoBindings + ) + true; + Equality.discr_tac false None + ] + end } + ] + end } + ] + end } + +let make_eq_decidability mode mind = + let mib = Global.lookup_mind mind in + if not (Int.equal (Array.length mib.mind_packets) 1) then + raise DecidabilityMutualNotSupported; + let ind = (mind,0) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + let u = Univ.Instance.empty in + let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx + (compute_dec_goal (ind,u) lnamesparrec nparrec) + (compute_dec_tact ind lnamesparrec nparrec) + in + ([|ans|], ctx), Safe_typing.empty_private_constants + +let eq_dec_scheme_kind = + declare_mutual_scheme_object "_eq_dec" make_eq_decidability + +(* The eq_dec_scheme proofs depend on the equality and discr tactics + but the inj tactics, that comes with discr, depends on the + eq_dec_scheme... *) + +let _ = Equality.set_eq_dec_scheme_kind eq_dec_scheme_kind -- cgit v1.2.3 From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- ide/coqOps.ml | 30 ++++++++++++++----------- ide/ideutils.ml | 2 +- ide/minilib.ml | 6 +++-- ide/minilib.mli | 3 ++- lib/pp.ml | 2 ++ lib/pp.mli | 3 +++ library/summary.ml | 6 +++-- proofs/proof_global.ml | 4 ++-- proofs/proof_using.ml | 2 +- stm/asyncTaskQueue.ml | 25 ++++++++++----------- stm/stm.ml | 58 ++++++++++++++++++++++++------------------------- vernac/auto_ind_decl.ml | 4 ++-- vernac/vernacentries.ml | 4 ++-- 13 files changed, 81 insertions(+), 68 deletions(-) (limited to 'vernac/auto_ind_decl.ml') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index cee243f91..1b4c5d3be 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -128,6 +128,9 @@ end = struct end open SentenceId +let log_pp msg : unit task = + Coq.lift (fun () -> Minilib.log_pp msg) + let log msg : unit task = Coq.lift (fun () -> Minilib.log msg) @@ -308,7 +311,7 @@ object(self) method private print_stack = Minilib.log "document:"; - Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer))) + Minilib.log_pp (Doc.print document (dbg_to_string buffer)) method private enter_focus start stop = let at id id' _ = Stateid.equal id' id in @@ -379,8 +382,7 @@ object(self) Coq.bind (Coq.seq action query) next method private mark_as_needed sentence = - Minilib.log("Marking " ^ - Pp.string_of_ppcmds (dbg_to_string buffer false None sentence)); + Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in let to_process = Tags.Script.to_process in @@ -437,9 +439,11 @@ object(self) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log s state_id = - Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string - (Option.default Stateid.dummy state_id)) in + let log_pp s state_id = + Minilib.log_pp Pp.(seq + [str "Feedback "; s; str " on "; + str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in + let log s state_id = log_pp (Pp.str s) state_id in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> log "AddedAxiom" id; @@ -469,24 +473,24 @@ object(self) (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let msg = Pp.string_of_ppcmds msg in - log "ErrorMsg" id; + log_pp Pp.(str "ErrorMsg" ++ msg) id; remove_flag sentence `PROCESSING; - add_flag sentence (`ERROR (loc, msg)); + let rmsg = Pp.string_of_ppcmds msg in + add_flag sentence (`ERROR (loc, rmsg)); self#mark_as_needed sentence; - self#attach_tooltip sentence loc msg; + self#attach_tooltip sentence loc rmsg; if not (Loc.is_ghost loc) then self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | Message(Warning, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let rmsg = Pp.string_of_ppcmds msg in - log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id; + log_pp Pp.(str "WarningMsg" ++ msg) id; + let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip sentence loc rmsg; self#position_warning_tag_at_sentence sentence loc; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log ("Msg: " ^ Pp.string_of_ppcmds msg) id; + log_pp Pp.(str "Msg" ++ msg) id; messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 101f1a5ee..da867e689 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -337,7 +337,7 @@ let default_logger level message = | Feedback.Warning -> `WARNING | Feedback.Error -> `ERROR in - Minilib.log ~level (Pp.string_of_ppcmds message) + Minilib.log_pp ~level message (** {6 File operations} *) diff --git a/ide/minilib.ml b/ide/minilib.ml index d11e8c56b..2c24e46f8 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -30,7 +30,7 @@ let debug = ref false print in the response buffer. *) -let log ?(level = `DEBUG) msg = +let log_pp ?(level = `DEBUG) msg = let prefix = match level with | `DEBUG -> "DEBUG" | `INFO -> "INFO" @@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg = | `FATAL -> "FATAL" in if !debug then begin - try Printf.eprintf "[%s] %s\n%!" prefix msg + try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg with _ -> () end +let log ?level str = log_pp ?level (Pp.str str) + let coqify d = Filename.concat d "coq" let coqide_config_home () = diff --git a/ide/minilib.mli b/ide/minilib.mli index b7672c900..4517a2374 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,8 @@ type level = [ (** debug printing *) val debug : bool ref -val log : ?level:level -> string -> unit +val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log : ?level:level -> string -> unit val coqide_config_home : unit -> string val coqide_config_dirs : unit -> string list diff --git a/lib/pp.ml b/lib/pp.ml index 7b21f9bbd..80c599274 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -77,6 +77,8 @@ let app s1 s2 = match s1, s2 with | s, Ppcmd_empty -> s | s1, s2 -> Ppcmd_glue [s1; s2] +let seq s = Ppcmd_glue s + let (++) = app (* formatting commands *) diff --git a/lib/pp.mli b/lib/pp.mli index 2c45ce0a7..4b7ac5c1a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -68,6 +68,9 @@ val comment : string list -> std_ppcmds val app : std_ppcmds -> std_ppcmds -> std_ppcmds (** Concatenation. *) +val seq : std_ppcmds list -> std_ppcmds +(** Multi-Concatenation. *) + val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds (** Infix alias for [app]. *) diff --git a/library/summary.ml b/library/summary.ml index 6efa07f38..2ec4760d6 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -107,8 +107,10 @@ let unfreeze_summaries fs = try fold id decl state with e when CErrors.noncritical e -> let e = CErrors.push e in - Printf.eprintf "Error unfrezing summay %s\n%s\n%!" - (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e)); + Feedback.msg_error + Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + str (name_of_summary id); + CErrors.iprint e]); iraise e in (** We rely on the order of the frozen list, and the order of folding *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 120cde5e5..ca7330fdb 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -195,9 +195,9 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - CErrors.error (Pp.string_of_ppcmds + CErrors.user_err (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).")) + str"Use \"Abort All\" first or complete proof(s).") end let discard_gen id = diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a125fb10d..f51586c73 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = prerr_endline (string_of_ppcmds x) in + let print x = Feedback.msg_error x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 28548ecee..125491988 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,9 +10,9 @@ open CErrors open Pp open Util -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type 'a worker_status = [ `Fresh | `Old of 'a ] @@ -147,23 +147,23 @@ module Make(T : Task) = struct let stop_waiting = ref false in let expiration_date = ref (ref false) in let pick_task () = - prerr_endline "waiting for a task"; + stm_prerr_endline "waiting for a task"; let pick age (t, c) = not !c && T.task_match age t in let task, task_expiration = TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in expiration_date := task_expiration; last_task := Some task; - prerr_endline ("got task: "^T.name_of_task task); + stm_prerr_endline ("got task: " ^ T.name_of_task task); task in let add_tasks l = List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in let get_exec_token () = ignore(CoqworkmgrApi.get 1); got_token := true; - prerr_endline ("got execution token") in + stm_prerr_endline ("got execution token") in let kill proc = Worker.kill proc; - prerr_endline ("Worker exited: " ^ + stm_prerr_endline ("Worker exited: " ^ match Worker.wait proc with | Unix.WEXITED 0x400 -> "exit code unavailable" | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i @@ -196,7 +196,7 @@ module Make(T : Task) = struct report_status ~id "Idle"; let task = pick_task () in match T.request_of_task !worker_age task with - | None -> prerr_endline ("Task expired: " ^ T.name_of_task task) + | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task) | Some req -> try get_exec_token (); @@ -222,8 +222,7 @@ module Make(T : Task) = struct raise e (* we pass the exception to the external handler *) | MarshalError s -> T.on_marshal_error s task; raise Die | e -> - pr_err ("Uncaught exception in worker manager: "^ - string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]); flush_all (); raise Die done with | (Die | TQueue.BeingDestroyed) -> @@ -261,7 +260,7 @@ module Make(T : Task) = struct let broadcast { queue } = TQueue.broadcast queue let enqueue_task { queue; active } (t, _ as item) = - prerr_endline ("Enqueue task "^T.name_of_task t); + stm_prerr_endline ("Enqueue task "^T.name_of_task t); TQueue.push queue item let cancel_worker { active } n = Pool.cancel n active @@ -329,11 +328,11 @@ module Make(T : Task) = struct CEphemeron.clear () with | MarshalError s -> - pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 + stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2 | End_of_file -> - prerr_endline "connection lost"; flush_all (); exit 2 + stm_prerr_endline "connection lost"; flush_all (); exit 2 | e -> - pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]); flush_all (); exit 1 done diff --git a/stm/stm.ml b/stm/stm.ml index 75872d633..ee142b293 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr -let prerr_endline s = if false then begin pr_err (s ()) end else () -let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else () +let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () open Vernacexpr open CErrors @@ -540,7 +540,7 @@ end = struct (* {{{ *) let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in checkout branch; - prerr_endline (fun () -> "mode:" ^ mode); + stm_prerr_endline (fun () -> "mode:" ^ mode); Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; @@ -852,7 +852,7 @@ end = struct (* {{{ *) if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); try - prerr_endline (fun () -> "defining "^str_id^" (cache="^ + stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); let good_id = match safe_id with None -> !cur_id | Some id -> id in fix_exn_ref := exn_on id ~valid:good_id; @@ -860,7 +860,7 @@ end = struct (* {{{ *) fix_exn_ref := (fun x -> x); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; - prerr_endline (fun () -> "setting cur id to "^str_id); + stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); @@ -994,11 +994,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) else match cmd with | VernacShow ShowScript -> ShowScript.show_script () | expr -> - prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in @@ -1431,8 +1431,8 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - prerr_endline (fun () -> "failed with the following exception:"); - prerr_endline (fun () -> string_of_ppcmds e_msg); + stm_prerr_endline (fun () -> "failed with the following exception:"); + stm_prerr_endline (fun () -> string_of_ppcmds e_msg); let e_safe_states = List.filter State.is_cached_and_valid my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } @@ -1697,7 +1697,7 @@ end = struct (* {{{ *) | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in - prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); + stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); reqs let reset_task_queue () = TaskQueue.clear (Option.get !queue) @@ -1781,7 +1781,7 @@ end = struct (* {{{ *) `Stay ((),[]) let on_marshal_error err { t_name } = - pr_err ("Fatal marshal error: " ^ t_name ); + stm_pr_err ("Fatal marshal error: " ^ t_name ); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death = function @@ -1880,7 +1880,7 @@ end = struct (* {{{ *) let open Notations in try let pt, uc = Future.join f in - prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ str"uc=" ++ Evd.pr_evar_universe_context uc))); @@ -1925,7 +1925,7 @@ end = struct (* {{{ *) let use_response _ _ _ = `End let on_marshal_error _ _ = - pr_err ("Fatal marshal error in query"); + stm_pr_err ("Fatal marshal error in query"); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death _ = () @@ -2000,7 +2000,7 @@ let warn_deprecated_nested_proofs = "stop working in a future Coq version")) let collect_proof keep cur hd brkind id = - prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); + stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in let name = function | [] -> no_name @@ -2100,7 +2100,7 @@ let string_of_reason = function | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section" | `Unknown -> "unsupported case" -let log_string s = prerr_debug (fun () -> "STM: " ^ s) +let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s) let log_processing_async id name = log_string Printf.(sprintf "%s: proof %s: asynch" (Stateid.to_string id) name ) @@ -2187,16 +2187,16 @@ let known_state ?(redefine_qed=false) ~cache id = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> - prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin Hooks.(call state_computed id ~in_cache:true); - prerr_endline (fun () -> "reached (cache)"); + stm_prerr_endline (fun () -> "reached (cache)"); State.install_cached id end else let step, cache_step, feedback_processed = @@ -2348,7 +2348,7 @@ let known_state ?(redefine_qed=false) ~cache id = else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; - prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in + stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id end (* }}} *) @@ -2363,7 +2363,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline (fun () -> "Initializing workers"); + stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] @@ -2415,9 +2415,9 @@ let rec join_admitted_proofs id = let join () = finish (); wait (); - prerr_endline (fun () -> "Joining the environment"); + stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); - prerr_endline (fun () -> "Joining Admitted proofs"); + stm_prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); VCS.print () @@ -2491,7 +2491,7 @@ let handle_failure (e, info) vcs tty = anomaly(str"error with no safe_id attached:" ++ spc() ++ CErrors.iprint_no_report (e, info)) | Some (safe_id, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; if tty && interactive () = `Yes then begin (* We stay on a valid state *) @@ -2514,13 +2514,13 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty ({ verbose; loc; expr } as x) c = - prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); + stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); let vcs = VCS.backup () in try let head = VCS.current_branch () in VCS.checkout head; let rc = begin - prerr_endline (fun () -> + stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) @@ -2558,7 +2558,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> - prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok @@ -2708,7 +2708,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; - prerr_endline (fun () -> "processed }}}"); + stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc with e -> @@ -2894,7 +2894,7 @@ let edit_at id = anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ CErrors.print_no_report e) | Some (_, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); iraise (e, info) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 594f2e944..6d71601cc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = string_of_ppcmds + let err_msg = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr tt1 ++ str " first.") in - error err_msg + user_err err_msg in let bl_args = Array.append (Array.append (Array.map (fun x -> x) v) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 09c43f93e..999fe297e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -39,7 +39,7 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false -let prerr_endline x = +let vernac_prerr_endline x = if debug then prerr_endline (x ()) else () (* Misc *) @@ -1933,7 +1933,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* The below vernac are candidates for removal from the main type and to be put into a new doc_command datatype: *) -- cgit v1.2.3