diff options
Diffstat (limited to 'plugins')
45 files changed, 366 insertions, 3086 deletions
diff --git a/plugins/btauto/dune b/plugins/btauto/dune index d2f5b65980..f7b3477460 100644 --- a/plugins/btauto/dune +++ b/plugins/btauto/dune @@ -1,7 +1,7 @@ (library (name btauto_plugin) - (public_name coq.plugins.btauto) + (public_name coq-core.plugins.btauto) (synopsis "Coq's btauto plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_btauto)) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 129b220680..6617f4726e 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -19,20 +19,12 @@ open Sorts open Constr open Context open Vars -open Goptions open Tacmach open Util let init_size=5 -let cc_verbose= - declare_bool_option_and_ref - ~depr:false - ~key:["Congruence";"Verbose"] - ~value:false - -let debug x = - if cc_verbose () then Feedback.msg_debug (x ()) +let debug_congruence = CDebug.create ~name:"congruence" () (* Signature table *) @@ -576,7 +568,7 @@ let add_inst state (inst,int_subst) = Control.check_for_interrupt (); if state.rew_depth > 0 then if is_redundant state inst.qe_hyp_id int_subst then - debug (fun () -> str "discarding redundant (dis)equality") + debug_congruence (fun () -> str "discarding redundant (dis)equality") else begin Identhash.add state.q_history inst.qe_hyp_id int_subst; @@ -591,7 +583,7 @@ let add_inst state (inst,int_subst) = state.rew_depth<-pred state.rew_depth; if inst.qe_pol then begin - debug (fun () -> + debug_congruence (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]")); @@ -599,7 +591,7 @@ let add_inst state (inst,int_subst) = end else begin - debug (fun () -> + debug_congruence (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]")); @@ -630,7 +622,7 @@ let join_path uf i j= min_path (down_path uf i [],down_path uf j []) let union state i1 i2 eq= - debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ + debug_congruence (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str "."); let r1= get_representative state.uf i1 and r2= get_representative state.uf i2 in @@ -670,7 +662,7 @@ let union state i1 i2 eq= | _,_ -> () let merge eq state = (* merge and no-merge *) - debug + debug_congruence (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++ str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str "."); let uf=state.uf in @@ -683,7 +675,7 @@ let merge eq state = (* merge and no-merge *) union state j i (swap eq) let update t state = (* update 1 and 2 *) - debug + debug_congruence (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let (i,j) as sign = signature state.uf t in let (u,v) = subterms state.uf t in @@ -745,7 +737,7 @@ let process_constructor_mark t i rep pac state = end let process_mark t m state = - debug + debug_congruence (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let i=find state.uf t in let rep=get_representative state.uf i in @@ -766,7 +758,7 @@ let check_disequalities state = if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis) else (str "No", check_aux q) in - let _ = debug + let _ = debug_congruence (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++ pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in ans @@ -953,7 +945,7 @@ let find_instances state = let pb_stack= init_pb_stack state in let res =ref [] in let _ = - debug (fun () -> str "Running E-matching algorithm ... "); + debug_congruence (fun () -> str "Running E-matching algorithm ... "); try while true do Control.check_for_interrupt (); @@ -964,7 +956,7 @@ let find_instances state = !res let rec execute first_run state = - debug (fun () -> str "Executing ... "); + debug_congruence (fun () -> str "Executing ... "); try while Control.check_for_interrupt (); @@ -974,7 +966,7 @@ let rec execute first_run state = None -> if not(Int.Set.is_empty state.pa_classes) then begin - debug (fun () -> str "First run was incomplete, completing ... "); + debug_congruence (fun () -> str "First run was incomplete, completing ... "); complete state; execute false state end @@ -989,12 +981,12 @@ let rec execute first_run state = end else begin - debug (fun () -> str "Out of instances ... "); + debug_congruence (fun () -> str "Out of instances ... "); None end else begin - debug (fun () -> str "Out of depth ... "); + debug_congruence (fun () -> str "Out of depth ... "); None end | Some dis -> Some diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 3270f74479..047756deef 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -121,7 +121,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.t) -> unit +val debug_congruence : CDebug.t val forest : state -> forest diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 53d8c5bdd9..e7e0822916 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -95,13 +95,13 @@ let pinject p c n a = p_rule=Inject(p,c,n,a)} let rec equal_proof env sigma uf i j= - debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj)) and edge_proof env sigma uf ((i,j),eq)= - debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let pi=equal_proof env sigma uf i eq.lhs in let pj=psym (equal_proof env sigma uf j eq.rhs) in let pij= @@ -117,7 +117,7 @@ and edge_proof env sigma uf ((i,j),eq)= ptrans (ptrans pi pij) pj and constr_proof env sigma uf i ipac= - debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); + debug_congruence (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); let t=find_oldest_pac uf i ipac in let eq_it=equal_proof env sigma uf i t in if ipac.args=[] then @@ -130,20 +130,20 @@ and constr_proof env sigma uf i ipac= ptrans eq_it (pcongr p (prefl targ)) and path_proof env sigma uf i l= - debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ + debug_congruence (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}"); match l with | [] -> prefl (term uf i) | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x) and congr_proof env sigma uf i j= - debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2) and ind_proof env sigma uf i ipac j jpac= - debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let p=equal_proof env sigma uf i j and p1=constr_proof env sigma uf i ipac and p2=constr_proof env sigma uf j jpac in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 72f77508d8..341fde7b77 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -420,16 +420,16 @@ let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in Coqlib.(check_required_library logic_module_name); - let _ = debug (fun () -> Pp.str "Reading goal ...") in + let _ = debug_congruence (fun () -> Pp.str "Reading goal ...") in let state = make_prb gl depth additionnal_terms in - let _ = debug (fun () -> Pp.str "Problem built, solving ...") in + let _ = debug_congruence (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in - let _ = debug (fun () -> Pp.str "Computation completed.") in + let _ = debug_congruence (fun () -> Pp.str "Computation completed.") in let uf=forest state in match sol with None -> Tacticals.New.tclFAIL 0 (str "congruence failed") | Some reason -> - debug (fun () -> Pp.str "Goal solved, generating proof ..."); + debug_congruence (fun () -> Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in diff --git a/plugins/cc/dune b/plugins/cc/dune index f7fa3adb56..ee28148c5a 100644 --- a/plugins/cc/dune +++ b/plugins/cc/dune @@ -1,7 +1,7 @@ (library (name cc_plugin) - (public_name coq.plugins.cc) + (public_name coq-core.plugins.cc) (synopsis "Coq's congruence closure plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_congruence)) diff --git a/plugins/derive/dune b/plugins/derive/dune index 1931339471..d382031a58 100644 --- a/plugins/derive/dune +++ b/plugins/derive/dune @@ -1,7 +1,7 @@ (library (name derive_plugin) - (public_name coq.plugins.derive) + (public_name coq-core.plugins.derive) (synopsis "Coq's derive plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_derive)) diff --git a/plugins/extraction/dune b/plugins/extraction/dune index d9d675fe6a..7f2582f84e 100644 --- a/plugins/extraction/dune +++ b/plugins/extraction/dune @@ -1,7 +1,7 @@ (library (name extraction_plugin) - (public_name coq.plugins.extraction) + (public_name coq-core.plugins.extraction) (synopsis "Coq's extraction plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_extraction)) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0cad192332..30f90dd1fc 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -22,7 +22,6 @@ open Reductionops open Inductive open Termops open Inductiveops -open Recordops open Namegen open Miniml open Table @@ -428,6 +427,7 @@ and extract_really_ind env kn mib = (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in + let ndecls = List.length mib.mind_params_ctxt in let npar = mib.mind_nparams in let epar = push_rel_context mib.mind_params_ctxt env in let sg = Evd.from_env env in @@ -463,17 +463,17 @@ and extract_really_ind env kn mib = if not p.ip_logical then let types = arities_of_constructors env ((kn,i),u) in for j = 0 to Array.length types - 1 do - let t = snd (decompose_prod_n npar types.(j)) in + let t = snd (decompose_prod_n_assum ndecls types.(j)) in let prods,head = dest_prod epar t in let nprods = List.length prods in let args = match Constr.kind head with | App (f,args) -> args (* [Constr.kind f = Ind ip] *) | _ -> [||] in - let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in - let db = db_from_ind dbmap npar in + let dbmap = parse_ind_args p.ip_sign args (nprods + ndecls) in + let db = db_from_ind dbmap ndecls in p.ip_types.(j) <- - extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1) + extract_type_cons epar sg db dbmap (EConstr.of_constr t) (ndecls+1) done done; (* Third pass: we determine special cases. *) @@ -531,7 +531,7 @@ and extract_really_ind env kn mib = let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in - List.iter (Option.iter check_proj) (lookup_projections ip) + List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip) with Not_found -> () end; Record field_glob @@ -1129,7 +1129,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_typ (get_body c) | Some p -> let body = fake_match_projection env p in @@ -1142,7 +1142,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_def (get_body c) | Some p -> let body = fake_match_projection env p in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index da4a50b674..cfdaac710b 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -217,13 +217,13 @@ module Mlenv = struct (* Adding a type with no [Tvar], hence no generalization needed. *) - let push_type {env=e;free=f} t = - { env = (0,t) :: e; free = find_free f t} + let push_type mle t = + { env = (0,t) :: mle.env; free = find_free mle.free t} (* Adding a type with no [Tvar] nor [Tmeta]. *) - let push_std_type {env=e;free=f} t = - { env = (0,t) :: e; free = f} + let push_std_type mle t = + { env = (0,t) :: mle.env; free = mle.free} end diff --git a/plugins/firstorder/dune b/plugins/firstorder/dune index 1b05452d8f..0299ca802f 100644 --- a/plugins/firstorder/dune +++ b/plugins/firstorder/dune @@ -1,7 +1,7 @@ (library (name ground_plugin) - (public_name coq.plugins.firstorder) + (public_name coq-core.plugins.firstorder) (synopsis "Coq's first order logic solver plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ground)) diff --git a/plugins/funind/dune b/plugins/funind/dune index e594ffbd02..42377f37f4 100644 --- a/plugins/funind/dune +++ b/plugins/funind/dune @@ -1,7 +1,7 @@ (library (name recdef_plugin) - (public_name coq.plugins.funind) + (public_name coq-core.plugins.funind) (synopsis "Coq's functional induction plugin") - (libraries coq.plugins.extraction)) + (libraries coq-core.plugins.extraction)) (coq.pp (modules g_indfun)) diff --git a/plugins/ltac/dune b/plugins/ltac/dune index 6558ecbfe8..9ec2b10873 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -1,15 +1,15 @@ (library (name ltac_plugin) - (public_name coq.plugins.ltac) + (public_name coq-core.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) - (libraries coq.stm)) + (libraries coq-core.stm)) (library (name tauto_plugin) - (public_name coq.plugins.tauto) + (public_name coq-core.plugins.tauto) (synopsis "Coq's tauto tactic") (modules tauto) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6d0e0c36b3..1640bff43b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -251,10 +251,10 @@ end) = struct (** Folding/unfolding of the tactic constants. *) - let unfold_impl sigma t = + let unfold_impl n sigma t = match EConstr.kind sigma t with | App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) -> - mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b) + mkProd (make_annot n Sorts.Relevant, a, lift 1 b) | _ -> assert false let unfold_all sigma t = @@ -273,16 +273,16 @@ end) = struct | _ -> assert false) | _ -> assert false - let arrow_morphism env evd ta tb a b = + let arrow_morphism env evd n ta tb a b = let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in - if ap && bp then app_poly env evd impl [| a; b |], unfold_impl + if ap && bp then app_poly env evd impl [| a; b |], unfold_impl n else if ap then (* Domain in Prop, CoDomain in Type *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (make_annot n Sorts.Relevant, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n let rec decomp_pointwise sigma n c = if Int.equal n 0 then c @@ -373,11 +373,6 @@ end) = struct end -(* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) -(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) - - let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in let evd', t = Typing.type_of env (goalevars evars) c in @@ -1079,7 +1074,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in - let (evars', mor), unfold = arr env evars tx tb x b in + let (evars', mor), unfold = arr env evars n.binder_name tx tb x b in let state, res = aux { state ; env ; unfresh ; term1 = mor ; ty1 = ty ; cstr = (prop,cstr) ; evars = evars' } in @@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) - (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 5e88bf7c79..f2f5fc16a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -91,6 +91,13 @@ let to_int v = Some (out_gen (topwit wit_int) v) else None +let of_ident id = in_gen (topwit wit_ident) id + +let to_ident v = + if has_type v (topwit wit_ident) then + Some (out_gen (topwit wit_ident) v) + else None + let to_list v = prj Val.typ_list v let to_option v = prj Val.typ_opt v diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 8ca2510459..c748fb3d1a 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -39,6 +39,8 @@ sig val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option + val of_ident : Id.t -> t + val to_ident : t -> Id.t option val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f2241e78d2..da95869abb 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v) - | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) + | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> let alias = Tacenv.interp_alias s in @@ -2148,7 +2148,8 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval lfun poly env sigma ty tac = + let eval ?loc ~poly env sigma tycon tac = + let lfun = GlobEnv.lfun env in let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = eval_tactic_ist ist tac in @@ -2156,8 +2157,13 @@ let _ = poly seems like enough to get reasonable behavior in practice *) let name = Id.of_string "ltac_gen" in - let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in - (EConstr.of_constr c, sigma) + let sigma, ty = match tycon with + | Some ty -> sigma, ty + | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) + in + let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in + let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in + (j, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval diff --git a/plugins/micromega/dune b/plugins/micromega/dune index 204125ab56..41f894bce3 100644 --- a/plugins/micromega/dune +++ b/plugins/micromega/dune @@ -1,24 +1,24 @@ (library (name micromega_plugin) - (public_name coq.plugins.micromega) + (public_name coq-core.plugins.micromega) ; be careful not to link the executable to the plugin! (modules (:standard \ csdpcert g_zify zify)) (synopsis "Coq's micromega plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (executable (name csdpcert) (public_name csdpcert) - (package coq) + (package coq-core) (modules csdpcert) (flags :standard -open Micromega_plugin) - (libraries coq.plugins.micromega)) + (libraries coq-core.plugins.micromega)) (library (name zify_plugin) - (public_name coq.plugins.zify) + (public_name coq-core.plugins.zify) (modules g_zify zify) (synopsis "Coq's zify plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_micromega g_zify)) diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index d1403558ad..800dc6cee2 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -14,7 +14,7 @@ open Pp open Lazy module NamedDecl = Context.Named.Declaration -let debug = false +let debug_zify = CDebug.create ~name:"zify" () (* The following [constr] are necessary for constructing the proof terms *) @@ -66,14 +66,36 @@ let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2) let get_type_of env evd e = Tacred.cbv_beta env evd (Retyping.get_type_of env evd e) +(* arguments are dealt with in a second step *) + let rec find_option pred l = match l with | [] -> raise Not_found | e :: l -> ( match pred e with Some r -> r | None -> find_option pred l ) -(** [HConstr] is a map indexed by EConstr.t. - It should only be used using closed terms. - *) +module ConstrMap = struct + open Names.GlobRef + + type 'a t = 'a list Map.t + + let add gr e m = + Map.update gr (function None -> Some [e] | Some l -> Some (e :: l)) m + + let empty = Map.empty + + let find evd h m = + match Map.find (fst (EConstr.destRef evd h)) m with + | e :: _ -> e + | [] -> assert false + + let find_all evd h m = Map.find (fst (EConstr.destRef evd h)) m + + let fold f m acc = + Map.fold + (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) + m acc +end + module HConstr = struct module M = Map.Make (struct type t = EConstr.t @@ -81,20 +103,11 @@ module HConstr = struct let compare c c' = Constr.compare (unsafe_to_constr c) (unsafe_to_constr c') end) - type 'a t = 'a list M.t - - let lfind h m = try M.find h m with Not_found -> [] - - let add h e m = - let l = lfind h m in - M.add h (e :: l) m + type 'a t = 'a M.t + let add h e m = M.add h e m let empty = M.empty - let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found - let find_all = lfind - - let fold f m acc = - M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc + let find = M.find end (** [get_projections_from_constant (evd,c) ] @@ -331,7 +344,7 @@ module type Elt = sig (** name *) val name : string - val table : (term_kind * decl_kind) HConstr.t ref + val table : (term_kind * decl_kind) ConstrMap.t ref val cast : elt decl -> decl_kind val dest : decl_kind -> elt decl option @@ -346,12 +359,12 @@ module type Elt = sig (* val arity : int*) end -let table = Summary.ref ~name:"zify_table" HConstr.empty -let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty -let specs = Summary.ref ~name:"zify_specs" HConstr.empty -let table_cache = ref HConstr.empty -let saturate_cache = ref HConstr.empty -let specs_cache = ref HConstr.empty +let table = Summary.ref ~name:"zify_table" ConstrMap.empty +let saturate = Summary.ref ~name:"zify_saturate" ConstrMap.empty +let specs = Summary.ref ~name:"zify_specs" ConstrMap.empty +let table_cache = ref ConstrMap.empty +let saturate_cache = ref ConstrMap.empty +let specs_cache = ref ConstrMap.empty (** Each type-class gives rise to a different table. They only differ on how projections are extracted. *) @@ -589,8 +602,11 @@ module MakeTable (E : Elt) = struct let register_hint evd t elt = match EConstr.kind evd t with | App (c, _) -> - E.table := HConstr.add c (Application t, E.cast elt) !E.table - | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table + let gr = fst (EConstr.destRef evd c) in + E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table + | _ -> + let gr = fst (EConstr.destRef evd t) in + E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table let register_constr env evd c = let c = EConstr.of_constr c in @@ -637,7 +653,7 @@ module MakeTable (E : Elt) = struct let pp_keys () = let env = Global.env () in let evd = Evd.from_env env in - HConstr.fold + ConstrMap.fold (fun _ (k, d) acc -> match E.dest d with | None -> acc @@ -805,12 +821,11 @@ let pp_prf prf = let interp_prf evd inj source prf = let t, prf' = interp_prf evd inj source prf in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "interp_prf " ++ gl_pr_constr inj.EInjT.inj ++ str " " ++ gl_pr_constr source ++ str " = " ++ gl_pr_constr t ++ str " by " - ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ()); + ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ())); (t, prf') let mkvar evd inj e = @@ -888,13 +903,12 @@ let app_unop evd src unop arg prf = let app_unop evd src unop arg prf = let res = app_unop evd src unop arg prf in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "\napp_unop " ++ pp_prf evd unop.EUnOpT.inj1_t arg prf ++ str " => " - ++ pp_prf evd unop.EUnOpT.inj2_t src res); + ++ pp_prf evd unop.EUnOpT.inj2_t src res)); res let app_binop evd src binop arg1 prf1 arg2 prf2 = @@ -949,9 +963,11 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 = type typed_constr = {constr : EConstr.t; typ : EConstr.t; inj : EInjT.t} let get_injection env evd t = - match snd (HConstr.find t !table_cache) with - | InjTyp i -> i - | _ -> raise Not_found + try + match snd (ConstrMap.find evd t !table_cache) with + | InjTyp i -> i + | _ -> raise Not_found + with DestKO -> raise Not_found (* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *) let arrow = @@ -1066,8 +1082,7 @@ let match_operator env evd hd args (t, d) = let pp_trans_expr env evd e res = let {deriv = inj} = get_injection env evd e.typ in - if debug then - Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res); + debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res)); res let declared_term env evd hd args = @@ -1090,7 +1105,7 @@ let declared_term env evd hd args = | PropUnOp _ -> decomp t 1 | _ -> None ) in - find_option match_operator (HConstr.find_all hd !table) + find_option match_operator (ConstrMap.find_all evd hd !table) let rec trans_expr env evd e = let inj = e.inj in @@ -1102,7 +1117,7 @@ let rec trans_expr env evd e = let k, t = find_option (match_operator env evd c a) - (HConstr.find_all c !table_cache) + (ConstrMap.find_all evd c !table_cache) in let n = Array.length a in match k with @@ -1187,7 +1202,7 @@ let trans_binrel evd src rop a1 prf1 a2 prf2 = let trans_binrel evd src rop a1 prf1 a2 prf2 = let res = trans_binrel evd src rop a1 prf1 a2 prf2 in - if debug then Feedback.msg_debug Pp.(str "\ntrans_binrel " ++ pp_prfp res); + debug_zify (fun () -> Pp.(str "\ntrans_binrel " ++ pp_prfp res)); res let mkprf t p = @@ -1199,11 +1214,10 @@ let mkprf t p = let mkprf t p = let t', p = mkprf t p in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "mkprf " ++ gl_pr_constr t ++ str " <-> " ++ gl_pr_constr t' - ++ str " by " ++ gl_pr_constr p); + ++ str " by " ++ gl_pr_constr p)); (t', p) let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = @@ -1221,7 +1235,7 @@ let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = let prf = trans_bin_prop op_constr op_iff t1 p1 t2 p2 in - if debug then Feedback.msg_debug (pp_prfp prf); + debug_zify (fun () -> pp_prfp prf); prf let trans_un_prop op_constr op_iff p1 prf1 = @@ -1247,7 +1261,7 @@ let rec trans_prop env evd e = let k, t = find_option (match_operator env evd c a) - (HConstr.find_all c !table_cache) + (ConstrMap.find_all evd c !table_cache) in let n = Array.length a in match k with @@ -1266,7 +1280,7 @@ let rec trans_prop env evd e = in trans_binrel evd e rop a.(n - 2) a1 a.(n - 1) a2 | _ -> IProof - with Not_found -> IProof ) + with Not_found | DestKO -> IProof ) let trans_check_prop env evd t = if is_prop env evd t then Some (trans_prop env evd t) else None @@ -1285,8 +1299,7 @@ let trans_hyps env evd l = [] l let trans_hyp h t0 prfp = - if debug then - Feedback.msg_debug Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ()); + debug_zify (fun () -> Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ())); match prfp with | IProof -> Tacticals.New.tclIDTAC (* Should detect before *) | CProof t' -> @@ -1313,8 +1326,7 @@ let trans_hyp h t0 prfp = (tclTHEN (Tactics.clear [h]) (Tactics.rename_hyp [(h', h)]))))) let trans_concl prfp = - if debug then - Feedback.msg_debug Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ()); + debug_zify (fun () -> Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ())); match prfp with | IProof -> Tacticals.New.tclIDTAC | CProof t -> @@ -1365,7 +1377,7 @@ let do_let tac (h : Constr.named_declaration) = find_option (match_operator env evd eq [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|]) - (HConstr.find_all eq !table_cache)); + (ConstrMap.find_all evd eq !table_cache)); tac x (EConstr.of_constr t) (EConstr.of_constr ty) with Not_found -> Tacticals.New.tclIDTAC) @@ -1459,12 +1471,12 @@ let rec spec_of_term env evd (senv : spec_env) t = try (EConstr.mkVar (HConstr.find t' senv'.map), senv') with Not_found -> ( try - match snd (HConstr.find c !specs_cache) with + match snd (ConstrMap.find evd c !specs_cache) with | UnOpSpec s | BinOpSpec s -> let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in register_constr senv' t' thm | _ -> (get_name t' senv', senv') - with Not_found -> (t', senv') ) + with Not_found | DestKO -> (t', senv') ) let interp_pscript s = match s with @@ -1539,7 +1551,8 @@ let get_all_sat env evd c = List.fold_left (fun acc e -> match e with _, Saturate s -> s :: acc | _ -> acc) [] - (HConstr.find_all c !saturate_cache) + ( try ConstrMap.find_all evd c !saturate_cache + with DestKO | Not_found -> [] ) let saturate = Proofview.Goal.enter (fun gl -> diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune index 3b67ab3429..2aaeec2665 100644 --- a/plugins/nsatz/dune +++ b/plugins/nsatz/dune @@ -1,7 +1,7 @@ (library (name nsatz_plugin) - (public_name coq.plugins.nsatz) + (public_name coq-core.plugins.nsatz) (synopsis "Coq's nsatz solver plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_nsatz)) diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 1caa042db6..19bdcbac58 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -1,9 +1,9 @@ (* Printing *) let pr x = - if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else () + if CDebug.(get_flag misc) then (Format.printf "@[%s@]" x; flush(stdout);)else () let prt0 s = () (* print_string s;flush(stdout)*) -let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s) -let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ())) +let sinfo s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str s) +let info s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str (s ())) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml deleted file mode 100644 index 9d92ffde74..0000000000 --- a/plugins/omega/coq_omega.ml +++ /dev/null @@ -1,1939 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - -open CErrors -open Util -open Names -open Constr -open Context -open Nameops -open EConstr -open Tacticals.New -open Tacmach.New -open Tactics -open Libnames -open Nametab -open Contradiction -open Tactypes -open Context.Named.Declaration - -module NamedDecl = Context.Named.Declaration - -module ZOmega = struct - type bigint = Z.t - let equal = Z.equal - let less_than = Z.lt - let add = Z.add - let sub = Z.sub - let mult = Z.mul - let euclid = Z.div_rem - let neg = Z.neg - let zero = Z.zero - let one = Z.one - let to_string = Z.to_string -end - -module OmegaSolver = Omega.MakeOmegaSolver (ZOmega) -open OmegaSolver - -(* Added by JCF, 09/03/98 *) - -let elim_id id = simplest_elim (mkVar id) - -let resolve_id id = apply (mkVar id) - -let display_system_flag = ref false -let display_action_flag = ref false -let old_style_flag = ref false -let letin_flag = ref true - -(* Should we reset all variable labels between two runs of omega ? *) - -let reset_flag = ref true - -(* Coq < 8.5 was not performing such resets, hence omega was slightly - non-deterministic: successive runs of omega on the same problem may - lead to distinct proof-terms. - At the very least, these terms differed on the inner - variable names, but they could even be non-convertible : - the OmegaSolver relies on Hashtbl.iter, it can hence find a different - solution when variable indices differ. *) - -let read f () = !f -let write f x = f:=x - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"System"]; - optread = read display_system_flag; - optwrite = write display_system_flag } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"Action"]; - optread = read display_action_flag; - optwrite = write display_action_flag } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"OldStyle"]; - optread = read old_style_flag; - optwrite = write old_style_flag } - -let () = - declare_bool_option - { optdepr = true; - optkey = ["Stable";"Omega"]; - optread = read reset_flag; - optwrite = write reset_flag } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Omega";"UseLocalDefs"]; - optread = read letin_flag; - optwrite = write letin_flag } - -let intref, reset_all_references = - let refs = ref [] in - (fun n -> let r = ref n in refs := (r,n) :: !refs; r), - (fun () -> List.iter (fun (r,n) -> r:=n) !refs) - -let new_identifier = - let cpt = intref 0 in - (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) - -let new_identifier_var = - let cpt = intref 0 in - (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) - -let new_id = - let cpt = intref 0 in fun () -> incr cpt; !cpt - -let new_var_num = - let cpt = intref 1000 in (fun () -> incr cpt; !cpt) - -let new_var = - let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) - -let display_var i = Printf.sprintf "X%d" i - -let intern_id,unintern_id,reset_intern_tables = - let cpt = ref 0 in - let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in - (fun (name : Id.t) -> - try Hashtbl.find table name with Not_found -> - let idx = !cpt in - Hashtbl.add table name idx; - Hashtbl.add co_table idx name; - incr cpt; idx), - (fun idx -> - try Hashtbl.find co_table idx with Not_found -> - let v = new_var () in - Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), - (fun () -> cpt := 0; Hashtbl.clear table) - -let mk_then tacs = tclTHENLIST tacs - -let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) - -let generalize_tac t = generalize t -let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] -let pf_nf gl c = pf_apply Tacred.simpl gl c - -let rev_assoc k = - let rec loop = function - | [] -> raise Not_found - | (v,k')::_ when Int.equal k k' -> v - | _ :: l -> loop l - in - loop - -let tag_hypothesis, hyp_of_tag, clear_tags = - let l = ref ([]:(Id.t * int) list) in - (fun h id -> l := (h,id):: !l), - (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), - (fun () -> l := []) - -let hide_constr,find_constr,clear_constr_tables,dump_tables = - let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in - (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun sigma h -> - try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"), - (fun () -> l := []), - (fun () -> !l) - -let reset_all () = - if !reset_flag then begin - reset_all_references (); - reset_intern_tables (); - clear_tags (); - clear_constr_tables () - end - -(* Lazy evaluation is used for Coq constants, because this code - is evaluated before the compiled modules are loaded. - To use the constant Zplus, one must type "Lazy.force coq_Zplus" - This is the right way to access to Coq constants in tactics ML code *) - -let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global - |> EConstr.of_constr) - - -(* Zarith *) -let coq_xH = gen_constant "num.pos.xH" -let coq_xO = gen_constant "num.pos.xO" -let coq_xI = gen_constant "num.pos.xI" -let coq_Z0 = gen_constant "num.Z.Z0" -let coq_Zpos = gen_constant "num.Z.Zpos" -let coq_Zneg = gen_constant "num.Z.Zneg" -let coq_Z = gen_constant "num.Z.type" -let coq_comparison = gen_constant "core.comparison.type" -let coq_Gt = gen_constant "core.comparison.Gt" -let coq_Zplus = gen_constant "num.Z.add" -let coq_Zmult = gen_constant "num.Z.mul" -let coq_Zopp = gen_constant "num.Z.opp" -let coq_Zminus = gen_constant "num.Z.sub" -let coq_Zsucc = gen_constant "num.Z.succ" -let coq_Zpred = gen_constant "num.Z.pred" -let coq_Z_of_nat = gen_constant "num.Z.of_nat" -let coq_inj_plus = gen_constant "num.Nat2Z.inj_add" -let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul" -let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub" -let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2" -let coq_inj_S = gen_constant "num.Nat2Z.inj_succ" -let coq_inj_eq = gen_constant "plugins.omega.inj_eq" -let coq_inj_neq = gen_constant "plugins.omega.inj_neq" -let coq_inj_le = gen_constant "plugins.omega.inj_le" -let coq_inj_lt = gen_constant "plugins.omega.inj_lt" -let coq_inj_ge = gen_constant "plugins.omega.inj_ge" -let coq_inj_gt = gen_constant "plugins.omega.inj_gt" -let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse" -let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc" -let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse" -let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute" -let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm" -let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm" -let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx" -let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1" -let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2" -let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3" -let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4" -let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5" -let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6" -let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7" -let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8" -let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9" -let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10" -let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11" -let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12" -let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13" -let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14" -let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15" -let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16" -let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17" -let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18" -let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19" -let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20" -let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0" -let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1" -let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2" -let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3" -let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4" -let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5" -let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6" -let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l" -let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr" -let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r" -let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1" -let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left" -let coq_Zne_left = gen_constant "plugins.omega.Zne_left" -let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left" -let coq_Zge_left = gen_constant "plugins.omega.Zge_left" -let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left" -let coq_Zle_left = gen_constant "plugins.omega.Zle_left" -let coq_new_var = gen_constant "plugins.omega.new_var" -let coq_intro_Z = gen_constant "plugins.omega.intro_Z" - -let coq_dec_eq = gen_constant "num.Z.eq_decidable" -let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne" -let coq_dec_Zle = gen_constant "num.Z.le_decidable" -let coq_dec_Zlt = gen_constant "num.Z.lt_decidable" -let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt" -let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge" - -let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq" -let coq_not_Zne = gen_constant "plugins.omega.not_Zne" -let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt" -let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge" -let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt" -let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le" -let coq_neq = gen_constant "plugins.omega.neq" -let coq_Zne = gen_constant "plugins.omega.Zne" -let coq_Zle = gen_constant "num.Z.le" -let coq_Zlt = gen_constant "num.Z.lt" -let coq_Zge = gen_constant "num.Z.ge" -let coq_Zgt = gen_constant "num.Z.gt" - -(* Peano/Datatypes *) -let coq_nat = gen_constant "num.nat.type" -let coq_O = gen_constant "num.nat.O" -let coq_S = gen_constant "num.nat.S" -let coq_le = gen_constant "num.nat.le" -let coq_lt = gen_constant "num.nat.lt" -let coq_ge = gen_constant "num.nat.ge" -let coq_gt = gen_constant "num.nat.gt" -let coq_plus = gen_constant "num.nat.add" -let coq_minus = gen_constant "num.nat.sub" -let coq_mult = gen_constant "num.nat.mul" -let coq_pred = gen_constant "num.nat.pred" - -(* Compare_dec/Peano_dec/Minus *) -let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus" -let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec" -let coq_dec_eq_nat = gen_constant "num.nat.eq_dec" -let coq_dec_le = gen_constant "num.nat.dec_le" -let coq_dec_lt = gen_constant "num.nat.dec_lt" -let coq_dec_ge = gen_constant "num.nat.dec_ge" -let coq_dec_gt = gen_constant "num.nat.dec_gt" -let coq_not_eq = gen_constant "num.nat.not_eq" -let coq_not_le = gen_constant "num.nat.not_le" -let coq_not_lt = gen_constant "num.nat.not_lt" -let coq_not_ge = gen_constant "num.nat.not_ge" -let coq_not_gt = gen_constant "num.nat.not_gt" - -(* Logic/Decidable *) -let coq_eq_ind_r = gen_constant "core.eq.ind_r" - -let coq_dec_or = gen_constant "core.dec.or" -let coq_dec_and = gen_constant "core.dec.and" -let coq_dec_imp = gen_constant "core.dec.imp" -let coq_dec_iff = gen_constant "core.dec.iff" -let coq_dec_not = gen_constant "core.dec.not" -let coq_dec_False = gen_constant "core.dec.False" -let coq_dec_not_not = gen_constant "core.dec.not_not" -let coq_dec_True = gen_constant "core.dec.True" - -let coq_not_or = gen_constant "core.dec.not_or" -let coq_not_and = gen_constant "core.dec.not_and" -let coq_not_imp = gen_constant "core.dec.not_imp" -let coq_not_iff = gen_constant "core.dec.not_iff" -let coq_not_not = gen_constant "core.dec.dec_not_not" -let coq_imp_simp = gen_constant "core.dec.imp_simp" -let coq_iff = gen_constant "core.iff.type" -let coq_not = gen_constant "core.not.type" -let coq_and = gen_constant "core.and.type" -let coq_or = gen_constant "core.or.type" -let coq_eq = gen_constant "core.eq.type" -let coq_ex = gen_constant "core.ex.type" -let coq_False = gen_constant "core.False.type" -let coq_True = gen_constant "core.True.type" - -(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) - -(* For unfold *) -let evaluable_ref_of_constr s c = - let env = Global.env () in - let evd = Evd.from_env env in - let open Tacred in - match EConstr.kind evd (Lazy.force c) with - | Const (kn,u) when is_evaluable env (EvalConstRef kn) -> - EvalConstRef kn - | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) - -let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) -let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) -let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) -let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) -let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) -let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) - -let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) -let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) -let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) -let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) -let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 -let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) -let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) -let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) -let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) -let mk_not t = mkApp (Lazy.force coq_not, [| t |]) -let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) - -let mk_integer n = - let rec loop n = - if n =? one then Lazy.force coq_xH else - mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI), - [| loop (n/two) |]) - in - if n =? zero then Lazy.force coq_Z0 - else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg), - [| loop (abs n) |]) - -type omega_constant = - | Zplus | Zmult | Zminus | Zsucc | Zopp | Zpred - | Plus | Mult | Minus | Pred | S | O - | Zpos | Zneg | Z0 | Z_of_nat - | Eq | Neq - | Zne | Zle | Zlt | Zge | Zgt - | Z | Nat - | And | Or | False | True | Not | Iff - | Le | Lt | Ge | Gt - | Other of string - -type result = - | Kvar of Id.t - | Kapp of omega_constant * constr list - | Kimp of constr * constr - | Kufo - -(* Nota: Kimp correspond to a binder (Prod), but hopefully we won't - have to bother with term lifting: Kimp will correspond to anonymous - product, for which (Rel 1) doesn't occur in the right term. - Moreover, we'll work on fully introduced goals, hence no Rel's in - the term parts that we manipulate, but rather Var's. - Said otherwise: all constr manipulated here are closed *) - -let destructurate_prop sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let c, args = decompose_app sigma t in - match EConstr.kind sigma c, args with - | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args) - | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args) - | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args) - | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args) - | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args) - | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args) - | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args) - | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args) - | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args) - | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) - | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) - | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) - | Const (sp,_), args -> - Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args) - | Construct (csp,_) , args -> - Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args) - | Ind (isp,_), args -> - Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args) - | Var id,[] -> Kvar id - | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) - | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") - | _ -> Kufo - -let nf = Tacred.simpl - -let destructurate_type env sigma t = - let is_conv = Reductionops.is_conv env sigma in - let c, args = decompose_app sigma (nf env sigma t) in - match EConstr.kind sigma c, args with - | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args) - | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args) - | _ -> Kufo - -let destructurate_term sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let c, args = decompose_app sigma t in - match EConstr.kind sigma c, args with - | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args) - | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args) - | _, [_] when eq_constr c (Lazy.force coq_Zsucc) -> Kapp (Zsucc,args) - | _, [_] when eq_constr c (Lazy.force coq_Zpred) -> Kapp (Zpred,args) - | _, [_] when eq_constr c (Lazy.force coq_Zopp) -> Kapp (Zopp,args) - | _, [_;_] when eq_constr c (Lazy.force coq_plus) -> Kapp (Plus,args) - | _, [_;_] when eq_constr c (Lazy.force coq_mult) -> Kapp (Mult,args) - | _, [_;_] when eq_constr c (Lazy.force coq_minus) -> Kapp (Minus,args) - | _, [_] when eq_constr c (Lazy.force coq_pred) -> Kapp (Pred,args) - | _, [_] when eq_constr c (Lazy.force coq_S) -> Kapp (S,args) - | _, [] when eq_constr c (Lazy.force coq_O) -> Kapp (O,args) - | _, [_] when eq_constr c (Lazy.force coq_Zpos) -> Kapp (Zneg,args) - | _, [_] when eq_constr c (Lazy.force coq_Zneg) -> Kapp (Zpos,args) - | _, [] when eq_constr c (Lazy.force coq_Z0) -> Kapp (Z0,args) - | _, [_] when eq_constr c (Lazy.force coq_Z_of_nat) -> Kapp (Z_of_nat,args) - | Var id,[] -> Kvar id - | _ -> Kufo - -let recognize_number sigma t = - let eq_constr c1 c2 = eq_constr sigma c1 c2 in - let rec loop t = - match decompose_app sigma t with - | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t - | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t - | f, [] when eq_constr f (Lazy.force coq_xH) -> one - | _ -> failwith "not a number" - in - match decompose_app sigma t with - | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t - | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t) - | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero - | _ -> failwith "not a number" - -type constr_path = - | P_APP of int - (* Abstraction and product *) - | P_TYPE - -let context sigma operation path (t : constr) = - let rec loop i p0 t = - match (p0,EConstr.kind sigma t) with - | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) - | ([], _) -> operation i t - | ((P_APP n :: p), App (f,v)) -> - let v' = Array.copy v in - v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v') - | (p, Fix ((_,n as ln),(tys,lna,v))) -> - let l = Array.length v in - let v' = Array.copy v in - v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) - | ((P_TYPE :: p), Prod (n,t,c)) -> - (mkProd (n,loop i p t,c)) - | ((P_TYPE :: p), Lambda (n,t,c)) -> - (mkLambda (n,loop i p t,c)) - | ((P_TYPE :: p), LetIn (n,b,t,c)) -> - (mkLetIn (n,b,loop i p t,c)) - | (p, _) -> - failwith ("abstract_path " ^ string_of_int(List.length p)) - in - loop 1 path t - -let occurrence sigma path (t : constr) = - let rec loop p0 t = match (p0,EConstr.kind sigma t) with - | (p, Cast (c,_,_)) -> loop p c - | ([], _) -> t - | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) - | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n) - | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term - | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term - | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term - | (p, _) -> - failwith ("occurrence " ^ string_of_int(List.length p)) - in - loop path t - -let abstract_path sigma typ path t = - let term_occur = ref (mkRel 0) in - let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in - mkLambda (make_annot (Name (Id.of_string "x")) Sorts.Relevant, typ, abstract), !term_occur - -let focused_simpl path = - let open Tacmach.New in - Proofview.Goal.enter begin fun gl -> - let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl ~check:false newc DEFAULTcast - end - -let focused_simpl path = focused_simpl path - -type oformula = - | Oplus of oformula * oformula - | Otimes of oformula * oformula - | Oatom of Id.t - | Oz of bigint - | Oufo of constr - -let rec oprint = function - | Oplus(t1,t2) -> - print_string "("; oprint t1; print_string "+"; - oprint t2; print_string ")" - | Otimes (t1,t2) -> - print_string "("; oprint t1; print_string "*"; - oprint t2; print_string ")" - | Oatom s -> print_string (Id.to_string s) - | Oz i -> print_string (string_of_bigint i) - | Oufo f -> print_string "?" - -let rec weight = function - | Oatom c -> intern_id c - | Oz _ -> -1 - | Otimes(c,_) -> weight c - | Oplus _ -> failwith "weight" - | Oufo _ -> -1 - -let rec val_of = function - | Oatom c -> mkVar c - | Oz c -> mk_integer c - | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |]) - | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) - | Oufo c -> c - -let compile name kind = - let rec loop accu = function - | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r - | Oz n -> - let id = new_id () in - tag_hypothesis name id; - {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly (Pp.str "compile_equation.") - in - loop [] - -let decompile af = - let rec loop = function - | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r) - | [] -> Oz af.constant - in - loop af.body - -(** Backward compat to emulate the old Refine: normalize the goal conclusion *) -let new_hole env sigma c = - let c = Reductionops.nf_betaiota env sigma c in - Evarutil.new_evar env sigma c - -let clever_rewrite_base_poly typ p result theorem = - let open Tacmach.New in - Proofview.Goal.enter begin fun gl -> - let full = pf_concl gl in - let env = pf_env gl in - let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in - Refine.refine ~typecheck:false begin fun sigma -> - let t = - applist - (mkLambda - (make_annot (Name (Id.of_string "P")) Sorts.Relevant, - mkArrow typ Sorts.Relevant mkProp, - mkLambda - (make_annot (Name (Id.of_string "H")) Sorts.Relevant, - applist (mkRel 1,[result]), - mkApp (Lazy.force coq_eq_ind_r, - [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), - [abstracted]) - in - let argt = mkApp (abstracted, [|result|]) in - let (sigma, hole) = new_hole env sigma argt in - (sigma, applist (t, [hole])) - end - end - -let clever_rewrite_base p result theorem = - clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem - -let clever_rewrite_base_nat p result theorem = - clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem - -let clever_rewrite_gen p result (t,args) = - let theorem = applist(t, args) in - clever_rewrite_base p result theorem - -let clever_rewrite_gen_nat p result (t,args) = - let theorem = applist(t, args) in - clever_rewrite_base_nat p result theorem - -(** Solve using the term the term [t _] *) -let refine_app gl t = - let open Tacmach.New in - Refine.refine ~typecheck:false begin fun sigma -> - let env = pf_env gl in - let ht = match EConstr.kind sigma (pf_get_type_of gl t) with - | Prod (_, t, _) -> t - | _ -> assert false - in - let (sigma, hole) = new_hole env sigma ht in - (sigma, applist (t, [hole])) - end - -let clever_rewrite p vpath t = - let open Tacmach.New in - Proofview.Goal.enter begin fun gl -> - let full = pf_concl gl in - let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in - let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in - let t' = applist(t, (vargs @ [abstracted])) in - refine_app gl t' - end - -(** simpl_coeffs : - The subterm at location [path_init] in the current goal should - look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce - via "simpl" each [ci] and the final constant [k]. - The path [path_k] gives the location of constant [k]. - Earlier, the whole was a mere call to [focused_simpl], - leading to reduction inside the atoms [vi], which is bad, - for instance when the atom is an evaluable definition - (see #4132). *) - -let simpl_coeffs path_init path_k = - Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let rec loop n t = - if Int.equal n 0 then pf_nf gl t - else - (* t should be of the form ((v * c) + ...) *) - match EConstr.kind sigma t with - | App(f,[|t1;t2|]) -> - (match EConstr.kind sigma t1 with - | App (g,[|v;c|]) -> - let c' = pf_nf gl c in - let t2' = loop (pred n) t2 in - mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) - | _ -> assert false) - | _ -> assert false - in - let n = Util.(-) (List.length path_k) (List.length path_init) in - let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) - in - convert_concl ~check:false newc DEFAULTcast - end - -let rec shuffle p (t1,t2) = - match t1,t2 with - | Oplus(l1,r1), Oplus(l2,r2) -> - if weight l1 > weight l2 then - let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in - (clever_rewrite p [[P_APP 1;P_APP 1]; - [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) - :: tac, - Oplus(l1,t')) - else - let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in - (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zplus_permute) - :: tac, - Oplus(l2,t')) - | Oplus(l1,r1), t2 -> - if weight l1 > weight t2 then - let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) - :: tac, - Oplus(l1, t') - else - [clever_rewrite p [[P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zplus_comm)], - Oplus(t2,t1) - | t1,Oplus(l2,r2) -> - if weight l2 > weight t1 then - let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in - clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zplus_permute) - :: tac, - Oplus(l2,t') - else [],Oplus(t1,t2) - | Oz t1,Oz t2 -> - [focused_simpl p], Oz(Z.add t1 t2) - | t1,t2 -> - if weight t1 < weight t2 then - [clever_rewrite p [[P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zplus_comm)], - Oplus(t2,t1) - else [],Oplus(t1,t2) - -let shuffle_mult p_init k1 e1 k2 e2 = - let rec loop p = function - | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> - if Int.equal v1 v2 then - let tac = - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA10) - in - if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then - let tac' = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: - loop p (l1,l2) - else tac :: loop (P_APP 2 :: p) (l1,l2) - else if v1 > v2 then - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2]; - [P_APP 1; P_APP 2]] - (Lazy.force coq_fast_OMEGA11) :: - loop (P_APP 2 :: p) (l1,l2') - else - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) (l1',l2) - | ({c=c1;v=v1}::l1), [] -> - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2]; - [P_APP 1; P_APP 2]] - (Lazy.force coq_fast_OMEGA11) :: - loop (P_APP 2 :: p) (l1,[]) - | [],({c=c2;v=v2}::l2) -> - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) ([],l2) - | [],[] -> [simpl_coeffs p_init p] - in - loop p_init (e1,e2) - -let shuffle_mult_right p_init e1 k2 e2 = - let rec loop p = function - | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') -> - if Int.equal v1 v2 then - let tac = - clever_rewrite p - [[P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 2]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA15) - in - if Z.add c1 (Z.mul k2 c2) =? zero then - let tac' = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) - in - tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: - loop p (l1,l2) - else tac :: loop (P_APP 2 :: p) (l1,l2) - else if v1 > v2 then - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) (l1,l2') - else - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) (l1',l2) - | ({c=c1;v=v1}::l1), [] -> - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) (l1,[]) - | [],({c=c2;v=v2}::l2) -> - clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 2; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1]; - [P_APP 2; P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]] - (Lazy.force coq_fast_OMEGA12) :: - loop (P_APP 2 :: p) ([],l2) - | [],[] -> [simpl_coeffs p_init p] - in - loop p_init (e1,e2) - -let rec shuffle_cancel p = function - | [] -> [focused_simpl p] - | ({c=c1}::l1) -> - let tac = - clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2]; - [P_APP 2; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2; P_APP 1]] - (if c1 >? zero then - (Lazy.force coq_fast_OMEGA13) - else - (Lazy.force coq_fast_OMEGA14)) - in - tac :: shuffle_cancel p l1 - -let rec scalar p n = function - | Oplus(t1,t2) -> - let tac1,t1' = scalar (P_APP 1 :: p) n t1 and - tac2,t2' = scalar (P_APP 2 :: p) n t2 in - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zmult_plus_distr_l) :: - (tac1 @ tac2), Oplus(t1',t2') - | Otimes(t1,Oz x) -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zmult_assoc_reverse); - focused_simpl (P_APP 2 :: p)], - Otimes(t1,Oz (n*x)) - | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") - | (Oatom _ as t) -> [], Otimes(t,Oz n) - | Oz i -> [focused_simpl p],Oz(n*i) - | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) - -let scalar_norm p_init = - let rec loop p = function - | [] -> [simpl_coeffs p_init p] - | (_::l) -> - clever_rewrite p - [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l - in - loop p_init - -let norm_add p_init = - let rec loop p = function - | [] -> [simpl_coeffs p_init p] - | _:: l -> - clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc_reverse) :: - loop (P_APP 2 :: p) l - in - loop p_init - -let scalar_norm_add p_init = - let rec loop p = function - | [] -> [simpl_coeffs p_init p] - | _ :: l -> - clever_rewrite p - [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; - [P_APP 1; P_APP 1; P_APP 1; P_APP 2]; - [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]] - (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l - in - loop p_init - -let rec negate p = function - | Oplus(t1,t2) -> - let tac1,t1' = negate (P_APP 1 :: p) t1 and - tac2,t2' = negate (P_APP 2 :: p) t2 in - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zopp_plus_distr) :: - (tac1 @ tac2), - Oplus(t1',t2') - | Otimes(t1,Oz x) -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zopp_mult_distr_r); - focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) - | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") - | (Oatom _ as t) -> - let r = Otimes(t,Oz(negone)) in - [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r - | Oz i -> [focused_simpl p],Oz(neg i) - | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |])) - -let rec transform sigma p t = - let default isnat t' = - try - let v,th,_ = find_constr sigma t' in - [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - with e when CErrors.noncritical e -> - let v = new_identifier_var () - and th = new_identifier () in - hide_constr t' v th isnat; - [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v - in - try match destructurate_term sigma t with - | Kapp(Zplus,[t1;t2]) -> - let tac1,t1' = transform sigma (P_APP 1 :: p) t1 - and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in - let tac,t' = shuffle p (t1',t2') in - tac1 @ tac2 @ tac, t' - | Kapp(Zminus,[t1;t2]) -> - let tac,t = - transform sigma p - (mkApp (Lazy.force coq_Zplus, - [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - unfold sp_Zminus :: tac,t - | Kapp(Zsucc,[t1]) -> - let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, - [| t1; mk_integer one |])) in - unfold sp_Zsucc :: tac,t - | Kapp(Zpred,[t1]) -> - let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, - [| t1; mk_integer negone |])) in - unfold sp_Zpred :: tac,t - | Kapp(Zmult,[t1;t2]) -> - let tac1,t1' = transform sigma (P_APP 1 :: p) t1 - and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in - begin match t1',t2' with - | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t' - | (Oz n,_) -> - let sym = - clever_rewrite p [[P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zmult_comm) in - let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t' - | _ -> default false t - end - | Kapp((Zpos|Zneg|Z0),_) -> - (try ([],Oz(recognize_number sigma t)) - with e when CErrors.noncritical e -> default false t) - | Kvar s -> [],Oatom s - | Kapp(Zopp,[t]) -> - let tac,t' = transform sigma (P_APP 1 :: p) t in - let tac',t'' = negate p t' in - tac @ tac', t'' - | Kapp(Z_of_nat,[t']) -> default true t' - | _ -> default false t - with e when noncritical e -> default false t - -let shrink_pair p f1 f2 = - match f1,f2 with - | Oatom v,Oatom _ -> - let r = Otimes(Oatom v,Oz two) in - clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r - | Oatom v, Otimes(_,c2) -> - let r = Otimes(Oatom v,Oplus(c2,Oz one)) in - clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zred_factor2), r - | Otimes (v1,c1),Oatom v -> - let r = Otimes(Oatom v,Oplus(c1,Oz one)) in - clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]] - (Lazy.force coq_fast_Zred_factor3), r - | Otimes (Oatom v,c1),Otimes (v2,c2) -> - let r = Otimes(Oatom v,Oplus(c1,c2)) in - clever_rewrite p - [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zred_factor4),r - | t1,t2 -> - begin - oprint t1; print_newline (); oprint t2; print_newline (); - flush stdout; CErrors.user_err Pp.(str "shrink.1") - end - -let reduce_factor p = function - | Oatom v -> - let r = Otimes(Oatom v,Oz one) in - [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r - | Otimes(Oatom v,Oz n) as f -> [],f - | Otimes(Oatom v,c) -> - let rec compute = function - | Oz n -> n - | Oplus(t1,t2) -> Z.add (compute t1) (compute t2) - | _ -> CErrors.user_err Pp.(str "condense.1") - in - [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) - | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1") - -let rec condense p = function - | Oplus(f1,(Oplus(f2,r) as t)) -> - if Int.equal (weight f1) (weight f2) then begin - let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in - let assoc_tac = - clever_rewrite p - [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]] - (Lazy.force coq_fast_Zplus_assoc) in - let tac_list,t' = condense p (Oplus(t,r)) in - (assoc_tac :: shrink_tac :: tac_list), t' - end else begin - let tac,f = reduce_factor (P_APP 1 :: p) f1 in - let tac',t' = condense (P_APP 2 :: p) t in - (tac @ tac'), Oplus(f,t') - end - | Oplus(f1,Oz n) -> - let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n) - | Oplus(f1,f2) -> - if Int.equal (weight f1) (weight f2) then begin - let tac_shrink,t = shrink_pair p f1 f2 in - let tac,t' = condense p t in - tac_shrink :: tac,t' - end else begin - let tac,f = reduce_factor (P_APP 1 :: p) f1 in - let tac',t' = condense (P_APP 2 :: p) f2 in - (tac @ tac'),Oplus(f,t') - end - | Oz _ as t -> [],t - | t -> - let tac,t' = reduce_factor p t in - let final = Oplus(t',Oz zero) in - let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in - tac @ [tac'], final - -let rec clear_zero p = function - | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero -> - let tac = - clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zred_factor5) in - let tac',t = clear_zero p r in - tac :: tac',t - | Oplus(f,r) -> - let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t) - | t -> [],t - -open Proofview -open Proofview.Notations - -let replay_history tactic_normalisation = - let aux = Id.of_string "auxiliary" in - let aux1 = Id.of_string "auxiliary_1" in - let aux2 = Id.of_string "auxiliary_2" in - let izero = mk_integer zero in - let rec loop t : unit Proofview.tactic = - match t with - | HYP e :: l -> - begin - try - tclTHEN - (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) - (loop l) - with Not_found -> loop l end - | NEGATE_CONTRADICT (e2,e1,b) :: l -> - let eq1 = decompile e1 - and eq2 = decompile e2 in - let id1 = hyp_of_tag e1.id - and id2 = hyp_of_tag e2.id in - let k = if b then negone else one in - let p_initial = [P_APP 1;P_TYPE] in - let tac= shuffle_mult_right p_initial e1.body k e2.body in - tclTHENLIST [ - generalize_tac - [mkApp (Lazy.force coq_OMEGA17, [| - val_of eq1; - val_of eq2; - mk_integer k; - mkVar id1; mkVar id2 |])]; - mk_then tac; - intro_using_then aux (fun aux -> - resolve_id aux); - reflexivity - ] - | CONTRADICTION (e1,e2) :: l -> - let eq1 = decompile e1 - and eq2 = decompile e2 in - let p_initial = [P_APP 2;P_TYPE] in - let tac = shuffle_cancel p_initial e1.body in - let solve_le = - let not_sup_sup = mkApp (Lazy.force coq_eq, - [| - Lazy.force coq_comparison; - Lazy.force coq_Gt; - Lazy.force coq_Gt |]) - in - tclTHENS - (tclTHENLIST [ - unfold sp_Zle; - simpl_in_concl; - intro; - (absurd not_sup_sup) ]) - [ assumption ; reflexivity ] - in - let theorem = - mkApp (Lazy.force coq_OMEGA2, [| - val_of eq1; val_of eq2; - mkVar (hyp_of_tag e1.id); - mkVar (hyp_of_tag e2.id) |]) - in - Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le - | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> - let id = hyp_of_tag e1.id in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in - let kk = mk_integer k - and dd = mk_integer d in - let rhs = mk_plus (mk_times eq2 kk) dd in - let state_eg = mk_eq eq1 rhs in - let tac = scalar_norm_add [P_APP 3] e2.body in - tclTHENS - (cut state_eg) - [ tclTHENS - (intro_using_then aux (fun aux -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA1, - [| eq1; rhs; mkVar aux; mkVar id |])]); - (clear [aux;id]); - (intro_mustbe_force id); - (cut (mk_gt kk dd)) ])) - [ tclTHENS - (cut (mk_gt kk izero)) - [ intro_using_then aux1 (fun aux1 -> - intro_using_then aux2 (fun aux2 -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_Zmult_le_approx, - [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); - (clear [aux1;aux2;id]); - (intro_mustbe_force id); - (loop l) ])); - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; - reflexivity ] ]; - tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] - ]; - tclTHEN (mk_then tac) reflexivity ] - - | NOT_EXACT_DIVIDE (e1,k) :: l -> - let c = floor_div e1.constant k in - let d = Z.sub e1.constant (Z.mul c k) in - let e2 = {id=e1.id; kind=EQUA;constant = c; - body = map_eq_linear (fun c -> c / k) e1.body } in - let eq2 = val_of(decompile e2) in - let kk = mk_integer k - and dd = mk_integer d in - let tac = scalar_norm_add [P_APP 2] e2.body in - tclTHENS - (cut (mk_gt dd izero)) - [ tclTHENS (cut (mk_gt kk dd)) - [ intro_using_then aux2 (fun aux2 -> - intro_using_then aux1 (fun aux1 -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA4, - [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); - (clear [aux1;aux2]); - unfold sp_not; - intro_using_then aux (fun aux -> - tclTHENLIST [ - resolve_id aux; - mk_then tac; - assumption - ])])) ; - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ]; - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ] - | EXACT_DIVIDE (e1,k) :: l -> - let id = hyp_of_tag e1.id in - let e2 = map_eq_afine (fun c -> c / k) e1 in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in - let kk = mk_integer k in - let state_eq = mk_eq eq1 (mk_times eq2 kk) in - if e1.kind == DISE then - let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS - (cut state_eq) - [ intro_using_then aux1 (fun aux1 -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA18, - [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); - (clear [aux1;id]); - (intro_mustbe_force id); - (loop l) ]); - tclTHEN (mk_then tac) reflexivity ] - else - let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS (cut state_eq) - [ - tclTHENS - (cut (mk_gt kk izero)) - [ intro_using_then aux2 (fun aux2 -> - intro_using_then aux1 (fun aux1 -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA3, - [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); - (clear [aux1;aux2;id]); - (intro_mustbe_force id); - (loop l) ])); - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ]; - tclTHEN (mk_then tac) reflexivity ] - | (MERGE_EQ(e3,e1,e2)) :: l -> - let id = new_identifier () in - tag_hypothesis id e3; - let id1 = hyp_of_tag e1.id - and id2 = hyp_of_tag e2 in - let eq1 = val_of(decompile e1) - and eq2 = val_of (decompile (negate_eq e1)) in - let tac = - clever_rewrite [P_APP 3] [[P_APP 1]] - (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: - scalar_norm [P_APP 3] e1.body - in - tclTHENS - (cut (mk_eq eq1 (mk_inv eq2))) - [ intro_using_then aux (fun aux -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); - (clear [id1;id2;aux]); - (intro_mustbe_force id); - (loop l) ]); - tclTHEN (mk_then tac) reflexivity] - - | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> - let id = new_identifier () - and id2 = hyp_of_tag orig.id in - tag_hypothesis id e.id; - let eq1 = val_of(decompile def) - and eq2 = val_of(decompile orig) in - let vid = unintern_id v in - let theorem = - mkApp (Lazy.force coq_ex, [| - Lazy.force coq_Z; - mkLambda - (make_annot (Name vid) Sorts.Relevant, - Lazy.force coq_Z, - mk_eq (mkRel 1) eq1) |]) - in - let mm = mk_integer m in - let p_initial = [P_APP 2;P_TYPE] in - let tac = - clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) - [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: - shuffle_mult_right p_initial - orig.body m ({c= negone;v= v}::def.body) in - tclTHENS - (cut theorem) - [ tclTHENLIST [ intro_using_then aux (fun aux -> - (elim_id aux) <*> - (clear [aux])); - intro_using_then vid (fun vid -> - intro_using_then aux (fun aux -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA9, - [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); - mk_then tac; - (clear [aux]); - (intro_mustbe_force id); - (loop l) ]))]; - tclTHEN (exists_tac eq1) reflexivity ] - | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> - let id1 = new_identifier () - and id2 = new_identifier () in - tag_hypothesis id1 e1; tag_hypothesis id2 e2; - let id = hyp_of_tag e.id in - let tac1 = norm_add [P_APP 2;P_TYPE] e.body in - let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in - let eq = val_of(decompile e) in - tclTHENS - (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [tclTHENLIST [ mk_then tac1; (intro_mustbe_force id1); (loop act1) ]; - tclTHENLIST [ mk_then tac2; (intro_mustbe_force id2); (loop act2) ]] - | SUM(e3,(k1,e1),(k2,e2)) :: l -> - let id = new_identifier () in - tag_hypothesis id e3; - let id1 = hyp_of_tag e1.id - and id2 = hyp_of_tag e2.id in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in - if k1 =? one && e2.kind == EQUA then - let tac_thm = - match e1.kind with - | EQUA -> Lazy.force coq_OMEGA5 - | INEQ -> Lazy.force coq_OMEGA6 - | DISE -> Lazy.force coq_OMEGA20 - in - let kk = mk_integer k2 in - let p_initial = - if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in - let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - tclTHENLIST [ - (generalize_tac - [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - mk_then tac; - (intro_mustbe_force id); - (loop l) - ] - else - let kk1 = mk_integer k1 - and kk2 = mk_integer k2 in - let p_initial = [P_APP 2;P_TYPE] in - let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - tclTHENS (cut (mk_gt kk1 izero)) - [tclTHENS - (cut (mk_gt kk2 izero)) - [ intro_using_then aux2 (fun aux2 -> - intro_using_then aux1 (fun aux1 -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_OMEGA7, [| - eq1;eq2;kk1;kk2; - mkVar aux1;mkVar aux2; - mkVar id1;mkVar id2 |])]); - (clear [aux1;aux2]); - mk_then tac; - (intro_mustbe_force id); - (loop l) ])); - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ]; - tclTHENLIST [ - unfold sp_Zgt; - simpl_in_concl; - reflexivity ] ] - | CONSTANT_NOT_NUL(e,k) :: l -> - tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl - | CONSTANT_NUL(e) :: l -> - tclTHEN (resolve_id (hyp_of_tag e)) reflexivity - | CONSTANT_NEG(e,k) :: l -> - tclTHENLIST [ - (generalize_tac [mkVar (hyp_of_tag e)]); - unfold sp_Zle; - simpl_in_concl; - unfold sp_not; - intro_using_then aux (fun aux -> - resolve_id aux <*> reflexivity) - ] - | _ -> Proofview.tclUNIT () - in - loop - -let normalize sigma p_initial t = - let (tac,t') = transform sigma p_initial t in - let (tac',t'') = condense p_initial t' in - let (tac'',t''') = clear_zero p_initial t'' in - tac @ tac' @ tac'' , t''' - -let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = - let p_initial = [P_APP pos ;P_TYPE] in - let (tac,t') = normalize sigma p_initial t in - let shift_left = - tclTHEN - (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) - (tclTRY (clear [id])) - in - if not (List.is_empty tac) then - let id' = new_identifier () in - ((id',(tclTHENLIST [ shift_left; mk_then tac; (intro_mustbe_force id') ])) - :: tactic, - compile id' flag t' :: defs) - else - (tactic,defs) - -let destructure_omega env sigma tac_def (id,c) = - if String.equal (atompart_of_id id) "State" then - tac_def - else - try match destructurate_prop sigma c with - | Kapp(Eq,[typ;t1;t2]) - when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end -> - let t = mk_plus t1 (mk_inv t2) in - normalize_equation sigma - id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def - | Kapp(Zne,[t1;t2]) -> - let t = mk_plus t1 (mk_inv t2) in - normalize_equation sigma - id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def - | Kapp(Zle,[t1;t2]) -> - let t = mk_plus t2 (mk_inv t1) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def - | Kapp(Zlt,[t1;t2]) -> - let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def - | Kapp(Zge,[t1;t2]) -> - let t = mk_plus t1 (mk_inv t2) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def - | Kapp(Zgt,[t1;t2]) -> - let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in - normalize_equation sigma - id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def - | _ -> tac_def - with e when noncritical e -> tac_def - -let reintroduce id = - (* [id] cannot be cleared if dependent: protect it by a try *) - tclTHEN (tclTRY (clear [id])) (intro_using_then id (fun _ -> tclUNIT())) - -let coq_omega = - Proofview.Goal.enter begin fun gl -> - clear_constr_tables (); - let hyps_types = Tacmach.New.pf_hyps_types gl in - let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in - let tactic_normalisation, system = - List.fold_left destructure_omega ([],[]) hyps_types in - let prelude,sys = - List.fold_left - (fun (tac,sys) (t,(v,th,b)) -> - if b then - let id = new_identifier () in - let i = new_id () in - tag_hypothesis id i; - (tclTHENLIST [ - (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); - (intros_mustbe_force [v; id]); - (elim_id id); - (clear [id]); - (intros_mustbe_force [th;id]); - tac ]), - {kind = INEQ; - body = [{v=intern_id v; c=one}]; - constant = zero; id = i} :: sys - else - (tclTHENLIST [ - (simplest_elim (applist (Lazy.force coq_new_var, [t]))); - (intros_mustbe_force [v;th]); - tac ]), - sys) - (Proofview.tclUNIT (),[]) (dump_tables ()) - in - let system = system @ sys in - if !display_system_flag then display_system display_var system; - if !old_style_flag then begin - try - let _ = simplify (new_id,new_var_num,display_var) false system in - Proofview.tclUNIT () - with UNSOLVABLE -> - let _,path = depend [] [] (history ()) in - if !display_action_flag then display_action display_var path; - (tclTHEN prelude (replay_history tactic_normalisation path)) - end else begin - try - let path = simplify_strong (new_id,new_var_num,display_var) system in - if !display_action_flag then display_action display_var path; - tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION as e -> - let _, info = Exninfo.capture e in - tclZEROMSG ~info (Pp.str"Omega can't solve this system") - end - end - -let coq_omega = coq_omega - -let nat_inject = - Proofview.Goal.enter begin fun gl -> - let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in - let rec explore p t : unit Proofview.tactic = - Proofview.tclEVARMAP >>= fun sigma -> - try match destructurate_term sigma t with - | Kapp(Plus,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_plus),[t1;t2])); - (explore (P_APP 1 :: p) t1); - (explore (P_APP 2 :: p) t2) - ] - | Kapp(Mult,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_mult),[t1;t2])); - (explore (P_APP 1 :: p) t1); - (explore (P_APP 2 :: p) t2) - ] - | Kapp(Minus,[t1;t2]) -> - let id = new_identifier () in - tclTHENS - (tclTHEN - (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) - (intro_mustbe_force id)) - [ - tclTHENLIST [ - (clever_rewrite_gen p - (mk_minus (mk_inj t1) (mk_inj t2)) - ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); - (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); - (explore (P_APP 1 :: p) t1); - (explore (P_APP 2 :: p) t2) ]; - (tclTHEN - (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) - (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) - ] - | Kapp(S,[t']) -> - let rec is_number t = - try match destructurate_term sigma t with - Kapp(S,[t]) -> is_number t - | Kapp(O,[]) -> true - | _ -> false - with e when noncritical e -> false - in - let rec loop p t : unit Proofview.tactic = - try match destructurate_term sigma t with - Kapp(S,[t]) -> - (tclTHEN - (clever_rewrite_gen p - (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[t])) - (loop (P_APP 1 :: p) t)) - | _ -> explore p t - with e when noncritical e -> explore p t - in - if is_number t' then focused_simpl p else loop p t - | Kapp(Pred,[t]) -> - let t_minus_one = - mkApp (Lazy.force coq_minus, [| t; - mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in - tclTHEN - (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t])) - (explore p t_minus_one) - | Kapp(O,[]) -> focused_simpl p - | _ -> Proofview.tclUNIT () - with e when noncritical e -> Proofview.tclUNIT () - - and loop = function - | [] -> Proofview.tclUNIT () - | (i,t)::lit -> - Proofview.tclEVARMAP >>= fun sigma -> - begin try match destructurate_prop sigma t with - Kapp(Le,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Lt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Ge,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Gt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Neq,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 1; P_TYPE] t1); - (explore [P_APP 2; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - | Kapp(Eq,[typ;t1;t2]) -> - if is_conv typ (Lazy.force coq_nat) then - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); - (explore [P_APP 2; P_TYPE] t1); - (explore [P_APP 3; P_TYPE] t2); - (reintroduce i); - (loop lit) - ] - else loop lit - | _ -> loop lit - with e when noncritical e -> loop lit end - in - let hyps_types = Tacmach.New.pf_hyps_types gl in - loop (List.rev hyps_types) - end - -let dec_binop = function - | Zne -> coq_dec_Zne - | Zle -> coq_dec_Zle - | Zlt -> coq_dec_Zlt - | Zge -> coq_dec_Zge - | Zgt -> coq_dec_Zgt - | Le -> coq_dec_le - | Lt -> coq_dec_lt - | Ge -> coq_dec_ge - | Gt -> coq_dec_gt - | _ -> raise Not_found - -let not_binop = function - | Zne -> coq_not_Zne - | Zle -> coq_Znot_le_gt - | Zlt -> coq_Znot_lt_ge - | Zge -> coq_Znot_ge_lt - | Zgt -> coq_Znot_gt_le - | Le -> coq_not_le - | Lt -> coq_not_lt - | Ge -> coq_not_ge - | Gt -> coq_not_gt - | _ -> raise Not_found - -(** A decidability check : for some [t], could we build a term - of type [decidable t] (i.e. [t\/~t]) ? Otherwise, we raise - [Undecidable]. Note that a successful check implies that - [t] has type Prop. -*) - -exception Undecidable - -let rec decidability env sigma t = - match destructurate_prop sigma t with - | Kapp(Or,[t1;t2]) -> - mkApp (Lazy.force coq_dec_or, [| t1; t2; - decidability env sigma t1; decidability env sigma t2 |]) - | Kapp(And,[t1;t2]) -> - mkApp (Lazy.force coq_dec_and, [| t1; t2; - decidability env sigma t1; decidability env sigma t2 |]) - | Kapp(Iff,[t1;t2]) -> - mkApp (Lazy.force coq_dec_iff, [| t1; t2; - decidability env sigma t1; decidability env sigma t2 |]) - | Kimp(t1,t2) -> - (* This is the only situation where it's not obvious that [t] - is in Prop. The recursive call on [t2] will ensure that. *) - mkApp (Lazy.force coq_dec_imp, - [| t1; t2; decidability env sigma t1; decidability env sigma t2 |]) - | Kapp(Not,[t1]) -> - mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |]) - | Kapp(Eq,[typ;t1;t2]) -> - begin match destructurate_type env sigma typ with - | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |]) - | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) - | _ -> raise Undecidable - end - | Kapp(op,[t1;t2]) -> - (try mkApp (Lazy.force (dec_binop op), [| t1; t2 |]) - with Not_found -> raise Undecidable) - | Kapp(False,[]) -> Lazy.force coq_dec_False - | Kapp(True,[]) -> Lazy.force coq_dec_True - | _ -> raise Undecidable - -let fresh_id avoid id gl = - fresh_id_in_env avoid id (Proofview.Goal.env gl) - -let onClearedName id tac = - (* We cannot ensure that hyps can be cleared (because of dependencies), *) - (* so renaming may be necessary *) - tclTHEN - (tclTRY (clear [id])) - (Proofview.Goal.enter begin fun gl -> - let id = fresh_id Id.Set.empty id gl in - tclTHEN (introduction id) (tac id) - end) - -let onClearedName2 id tac = - tclTHEN - (tclTRY (clear [id])) - (Proofview.Goal.enter begin fun gl -> - let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in - let id2 = fresh_id (Id.Set.singleton id1) (add_suffix id "_right") gl in - tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] - end) - -let destructure_hyps = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let decidability = decidability env sigma in - let rec loop = function - | [] -> (tclTHEN nat_inject coq_omega) - | LocalDef (i,body,typ) :: lit when !letin_flag -> - Proofview.tclEVARMAP >>= fun sigma -> - begin - try - match destructurate_type env sigma typ with - | Kapp(Nat,_) | Kapp(Z,_) -> - let hid = fresh_id Id.Set.empty (add_suffix i.binder_name "_eqn") gl in - let hty = mk_gen_eq typ (mkVar i.binder_name) body in - tclTHEN - (assert_by (Name hid) hty reflexivity) - (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit)) - | _ -> loop lit - with e when noncritical e -> loop lit - end - | decl :: lit -> (* variable without body (or !letin_flag isn't set) *) - let i = NamedDecl.get_id decl in - Proofview.tclEVARMAP >>= fun sigma -> - begin try match destructurate_prop sigma (NamedDecl.get_type decl) with - | Kapp(False,[]) -> elim_id i - | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit - | Kapp(Or,[t1;t2]) -> - (tclTHENS - (elim_id i) - [ onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t1)::lit))); - onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t2)::lit))) ]) - | Kapp(And,[t1;t2]) -> - tclTHEN - (elim_id i) - (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (make_annot i1 Sorts.Relevant,t1) :: - LocalAssum (make_annot i2 Sorts.Relevant,t2) :: lit))) - | Kapp(Iff,[t1;t2]) -> - tclTHEN - (elim_id i) - (onClearedName2 i (fun i1 i2 -> - loop (LocalAssum (make_annot i1 Sorts.Relevant,mkArrow t1 Sorts.Relevant t2) :: - LocalAssum (make_annot i2 Sorts.Relevant,mkArrow t2 Sorts.Relevant t1) :: lit))) - | Kimp(t1,t2) -> - (* t1 and t2 might be in Type rather than Prop. - For t1, the decidability check will ensure being Prop. *) - if Termops.is_Prop sigma (Retyping.get_type_of env sigma t2) - then - let d1 = decidability t1 in - tclTHENLIST [ - (generalize_tac [mkApp (Lazy.force coq_imp_simp, - [| t1; t2; d1; mkVar i|])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) t2) :: lit)))) - ] - else - loop lit - | Kapp(Not,[t]) -> - begin match destructurate_prop sigma t with - Kapp(Or,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and (mk_not t1) (mk_not t2)) :: lit)))) - ] - | Kapp(And,[t1;t2]) -> - let d1 = decidability t1 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_and, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) (mk_not t2)) :: lit)))) - ] - | Kapp(Iff,[t1;t2]) -> - let d1 = decidability t1 in - let d2 = decidability t2 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_iff, - [| t1; t2; d1; d2; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_and t1 (mk_not t2)) - (mk_and (mk_not t1) t2)) :: lit)))) - ] - | Kimp(t1,t2) -> - (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. - For t1, being decidable implies being Prop. *) - let d1 = decidability t1 in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_imp, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and t1 (mk_not t2)) :: lit)))) - ] - | Kapp(Not,[t]) -> - let d = decidability t in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t) :: lit)))) - ] - | Kapp(op,[t1;t2]) -> - (try - let thm = not_binop op in - tclTHENLIST [ - (generalize_tac - [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); - (onClearedName i (fun _ -> loop lit)) - ] - with Not_found -> loop lit) - | Kapp(Eq,[typ;t1;t2]) -> - if !old_style_flag then begin - match destructurate_type env sigma typ with - | Kapp(Nat,_) -> - tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | Kapp(Z,_) -> - tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | _ -> loop lit - end else begin - match destructurate_type env sigma typ with - | Kapp(Nat,_) -> - (tclTHEN - (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) - (loop lit)) - | Kapp(Z,_) -> - (tclTHEN - (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) - (loop lit)) - | _ -> loop lit - end - | _ -> loop lit - end - | _ -> loop lit - with - | Undecidable -> loop lit - | e when noncritical e -> loop lit - end - in - let hyps = Proofview.Goal.hyps gl in - loop hyps - end - -let destructure_goal = - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let decidability = decidability env sigma in - let rec loop t = - Proofview.tclEVARMAP >>= fun sigma -> - let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in - Proofview.V82.wrap_exceptions prop >>= fun prop -> - match prop with - | Kapp(Not,[t]) -> - (tclTHEN - (tclTHEN (unfold sp_not) intro) - destructure_hyps) - | Kimp(a,b) -> (tclTHEN intro (loop b)) - | Kapp(False,[]) -> destructure_hyps - | _ -> - let goal_tac = - try - let dec = decidability t in - tclTHEN - (Proofview.Goal.enter begin fun gl -> - refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) - end) - intro - with Undecidable -> Tactics.elim_type (Lazy.force coq_False) - | e when Proofview.V82.catchable_exception e -> - let e, info = Exninfo.capture e in - Proofview.tclZERO ~info e - in - tclTHEN goal_tac destructure_hyps - in - (loop concl) - end - -let destructure_goal = destructure_goal - -let warn_omega_is_deprecated = - let name = "omega-is-deprecated" in - let category = "deprecated" in - CWarnings.create ~name ~category (fun () -> - Pp.str "omega is deprecated since 8.12; use “lia” instead.") - -let omega_solver = - Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *) - warn_omega_is_deprecated (); - Coqlib.check_required_library ["Coq";"omega";"Omega"]; - reset_all (); - destructure_goal diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli deleted file mode 100644 index e723082803..0000000000 --- a/plugins/omega/coq_omega.mli +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -val omega_solver : unit Proofview.tactic diff --git a/plugins/omega/dune b/plugins/omega/dune index 0db71ed6fb..e69de29bb2 100644 --- a/plugins/omega/dune +++ b/plugins/omega/dune @@ -1,7 +0,0 @@ -(library - (name omega_plugin) - (public_name coq.plugins.omega) - (synopsis "Coq's omega plugin") - (libraries coq.plugins.ltac)) - -(coq.pp (modules g_omega)) diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg deleted file mode 100644 index 888a62b2bc..0000000000 --- a/plugins/omega/g_omega.mlg +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - - -DECLARE PLUGIN "omega_plugin" - -{ - -open Ltac_plugin - -} - -TACTIC EXTEND omega -| [ "omega" ] -> { Coq_omega.omega_solver } -END diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml deleted file mode 100644 index 24cd342e42..0000000000 --- a/plugins/omega/omega.ml +++ /dev/null @@ -1,708 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(* 13/10/2002 : modified to cope with an external numbering of equations *) -(* and hypothesis. Its use for Omega is not more complex and it makes *) -(* things much simpler for the reflexive version where we should limit *) -(* the number of source of numbering. *) -(**************************************************************************) - -module type INT = sig - type bigint - val equal : bigint -> bigint -> bool - val less_than : bigint -> bigint -> bool - val add : bigint -> bigint -> bigint - val sub : bigint -> bigint -> bigint - val mult : bigint -> bigint -> bigint - val euclid : bigint -> bigint -> bigint * bigint - val neg : bigint -> bigint - val zero : bigint - val one : bigint - val to_string : bigint -> string -end - -let debug = ref false - -module MakeOmegaSolver (I:INT) = struct - -type bigint = I.bigint -let (=?) = I.equal -let (<?) = I.less_than -let (<=?) x y = I.less_than x y || x = y -let (>?) x y = I.less_than y x -let (>=?) x y = I.less_than y x || x = y -let (+) = I.add -let (-) = I.sub -let ( * ) = I.mult -let (/) x y = fst (I.euclid x y) -let (mod) x y = snd (I.euclid x y) -let zero = I.zero -let one = I.one -let two = one + one -let negone = I.neg one -let abs x = if I.less_than x zero then I.neg x else x -let string_of_bigint = I.to_string -let neg = I.neg - -(* To ensure that polymorphic (<) is not used mistakenly on big integers *) -(* Warning: do not use (=) either on big int *) -let (<) = ((<) : int -> int -> bool) -let (>) = ((>) : int -> int -> bool) -let (<=) = ((<=) : int -> int -> bool) -let (>=) = ((>=) : int -> int -> bool) - -let pp i = print_int i; print_newline (); flush stdout - -let push v l = l := v :: !l - -let rec pgcd x y = if y =? zero then x else pgcd y (x mod y) - -let pgcd_l = function - | [] -> failwith "pgcd_l" - | x :: l -> List.fold_left pgcd x l - -let floor_div a b = - match a >=? zero , b >? zero with - | true,true -> a / b - | false,false -> a / b - | true, false -> (a-one) / b - one - | false,true -> (a+one) / b - one - -type coeff = {c: bigint ; v: int} - -type linear = coeff list - -type eqn_kind = EQUA | INEQ | DISE - -type afine = { - (* a number uniquely identifying the equation *) - id: int ; - (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *) - kind: eqn_kind; - (* the variables and their coefficient *) - body: coeff list; - (* a constant *) - constant: bigint } - -type state_action = { - st_new_eq : afine; - st_def : afine; (* /!\ this represents [st_def = st_var] *) - st_orig : afine; - st_coef : bigint; - st_var : int } - -type action = - | DIVIDE_AND_APPROX of afine * afine * bigint * bigint - | NOT_EXACT_DIVIDE of afine * bigint - | FORGET_C of int - | EXACT_DIVIDE of afine * bigint - | SUM of int * (bigint * afine) * (bigint * afine) - | STATE of state_action - | HYP of afine - | FORGET of int * int - | FORGET_I of int * int - | CONTRADICTION of afine * afine - | NEGATE_CONTRADICT of afine * afine * bool - | MERGE_EQ of int * afine * int - | CONSTANT_NOT_NUL of int * bigint - | CONSTANT_NUL of int - | CONSTANT_NEG of int * bigint - | SPLIT_INEQ of afine * (int * action list) * (int * action list) - | WEAKEN of int * bigint - -exception UNSOLVABLE - -exception NO_CONTRADICTION - -let display_eq print_var (l,e) = - let _ = - List.fold_left - (fun not_first f -> - print_string - (if f.c <? zero then "- " else if not_first then "+ " else ""); - let c = abs f.c in - if c =? one then - Printf.printf "%s " (print_var f.v) - else - Printf.printf "%s %s " (string_of_bigint c) (print_var f.v); - true) - false l - in - if e >? zero then - Printf.printf "+ %s " (string_of_bigint e) - else if e <? zero then - Printf.printf "- %s " (string_of_bigint (abs e)) - -let rec trace_length l = - let action_length accu = function - | SPLIT_INEQ (_,(_,l1),(_,l2)) -> - accu + one + trace_length l1 + trace_length l2 - | _ -> accu + one in - List.fold_left action_length zero l - -let operator_of_eq = function - | EQUA -> "=" | DISE -> "!=" | INEQ -> ">=" - -let kind_of = function - | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation" - -let display_system print_var l = - List.iter - (fun { kind=b; body=e; constant=c; id=id} -> - Printf.printf "E%d: " id; - display_eq print_var (e,c); - Printf.printf "%s 0\n" (operator_of_eq b)) - l; - print_string "------------------------\n\n" - -let display_inequations print_var l = - List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l; - print_string "------------------------\n\n" - -let sbi = string_of_bigint - -let rec display_action print_var = function - | act :: l -> begin match act with - | DIVIDE_AND_APPROX (e1,e2,k,d) -> - Printf.printf - "Inequation E%d is divided by %s and the constant coefficient is \ - rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) - | NOT_EXACT_DIVIDE (e,k) -> - Printf.printf - "Constant in equation E%d is not divisible by the pgcd \ - %s of its other coefficients.\n" e.id (sbi k) - | EXACT_DIVIDE (e,k) -> - Printf.printf - "Equation E%d is divided by the pgcd \ - %s of its coefficients.\n" e.id (sbi k) - | WEAKEN (e,k) -> - Printf.printf - "To ensure a solution in the dark shadow \ - the equation E%d is weakened by %s.\n" e (sbi k) - | SUM (e,(c1,e1),(c2,e2)) -> - Printf.printf - "We state %s E%d = %s %s E%d + %s %s E%d.\n" - (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2) - (kind_of e2.kind) e2.id - | STATE { st_new_eq = e } -> - Printf.printf "We define a new equation E%d: " e.id; - display_eq print_var (e.body,e.constant); - print_string (operator_of_eq e.kind); print_string " 0" - | HYP e -> - Printf.printf "We define E%d: " e.id; - display_eq print_var (e.body,e.constant); - print_string (operator_of_eq e.kind); print_string " 0\n" - | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e - | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 - | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2 - | MERGE_EQ (e,e1,e2) -> - Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e - | CONTRADICTION (e1,e2) -> - Printf.printf - "Equations E%d and E%d imply a contradiction on their \ - constant factors.\n" e1.id e2.id - | NEGATE_CONTRADICT(e1,e2,b) -> - Printf.printf - "Equations E%d and E%d state that their body is at the same time \ - equal and different\n" e1.id e2.id - | CONSTANT_NOT_NUL (e,k) -> - Printf.printf "Equation E%d states %s = 0.\n" e (sbi k) - | CONSTANT_NEG(e,k) -> - Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k) - | CONSTANT_NUL e -> - Printf.printf "Inequation E%d states 0 != 0.\n" e - | SPLIT_INEQ (e,(e1,l1),(e2,l2)) -> - Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2; - display_action print_var l1; - print_newline (); - display_action print_var l2; - print_newline () - end; display_action print_var l - | [] -> - flush stdout - -let default_print_var v = Printf.sprintf "X%d" v (* For debugging *) - -(*""*) -let add_event, history, clear_history = - let accu = ref [] in - (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu), - (fun () -> !accu), - (fun () -> accu := []) - -let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v) - -let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) - -let map_eq_linear f = - let rec loop = function - | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l - | [] -> [] - in - loop - -let map_eq_afine f e = - { id = e.id; kind = e.kind; body = map_eq_linear f e.body; - constant = f e.constant } - -let negate_eq = map_eq_afine (fun x -> neg x) - -let rec sum p0 p1 = match (p0,p1) with - | ([], l) -> l | (l, []) -> l - | (((x1::l1) as l1'), ((x2::l2) as l2')) -> - if x1.v = x2.v then - let c = x1.c + x2.c in - if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2 - else if x1.v > x2.v then - x1 :: sum l1 l2' - else - x2 :: sum l1' l2 - -let sum_afine new_eq_id eq1 eq2 = - { kind = eq1.kind; id = new_eq_id (); - body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant } - -exception FACTOR1 - -let rec chop_factor_1 = function - | x :: l -> - if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l') - | [] -> raise FACTOR1 - -exception CHOPVAR - -let rec chop_var v = function - | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l') - | [] -> raise CHOPVAR - -let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) = - if e = [] then begin - match eq_flag with - | EQUA -> - if x =? zero then [] else begin - add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE - end - | DISE -> - if x <> zero then [] else begin - add_event (CONSTANT_NUL id); raise UNSOLVABLE - end - | INEQ -> - if x >=? zero then [] else begin - add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE - end - end else - let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in - if eq_flag=EQUA && x mod gcd <> zero then begin - add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE - end else if eq_flag=DISE && x mod gcd <> zero then begin - add_event (FORGET_C eq.id); [] - end else if gcd <> one then begin - let c = floor_div x gcd in - let d = x - c * gcd in - let new_eq = {id=id; kind=eq_flag; constant=c; - body=map_eq_linear (fun c -> c / gcd) e} in - add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd) - else DIVIDE_AND_APPROX(eq,new_eq,gcd,d)); - [new_eq] - end else [eq] - -let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2 - ({body=e1; constant=c1} as eq1) = - try - let (f,_) = chop_var v e1 in - let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c - else failwith "eliminate_with_in" in - let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in - add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res - with CHOPVAR -> eq1 - -let omega_mod a b = a - b * floor_div (two * a + b) (two * b) -let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = - let e = original.body in - let sigma = new_var_id () in - if e == [] then begin - display_system print_var [original] ; failwith "TL" - end; - let smallest,var = - List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) - (abs (List.hd e).c, (List.hd e).v) (List.tl e) - in - let m = smallest + one in - let new_eq = - { constant = omega_mod original.constant m; - body = {c= neg m;v=sigma} :: - map_eq_linear (fun a -> omega_mod a m) original.body; - id = new_eq_id (); kind = EQUA } in - let definition = - { constant = neg (floor_div (two * original.constant + m) (two * m)); - body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m))) - original.body; - id = new_eq_id (); kind = EQUA } in - add_event (STATE {st_new_eq = new_eq; st_def = definition; - st_orig = original; st_coef = m; st_var = sigma}); - let new_eq = List.hd (normalize new_eq) in - let eliminated_var, def = chop_var var new_eq.body in - let other_equations = - Util.List.map_append - (fun e -> - normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in - let inequations = - Util.List.map_append - (fun e -> - normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in - let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in - let mod_original = map_eq_afine (fun c -> c / m) original' in - add_event (EXACT_DIVIDE (original',m)); - List.hd (normalize mod_original),other_equations,inequations - -let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) = - if !debug then display_system print_var (e::other); - try - let v,def = chop_factor_1 e.body in - (Util.List.map_append - (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other, - Util.List.map_append - (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs) - with FACTOR1 -> - eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs) - -let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) = - let rec fst_eq_1 = function - (eq::l) -> - if List.exists (fun x -> abs x.c =? one) eq.body then eq,l - else let (eq',l') = fst_eq_1 l in (eq',eq::l') - | [] -> raise Not_found in - match sys_eq with - [] -> if !debug then display_system print_var sys_ineq; sys_ineq - | (e1::rest) -> - let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in - if eq.body = [] then - if eq.constant =? zero then begin - add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq) - end else begin - add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE - end - else - banerjee new_ids - (eliminate_one_equation new_ids (eq,other,sys_ineq)) - -type kind = INVERTED | NORMAL - -let redundancy_elimination new_eq_id system = - let normal = function - ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED - | e -> e,NORMAL in - let table = Hashtbl.create 7 in - List.iter - (fun e -> - let ({body=ne} as nx) ,kind = normal e in - if ne = [] then - if nx.constant <? zero then begin - add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE - end else add_event (FORGET_C nx.id) - else - try - let (optnormal,optinvert) = Hashtbl.find table ne in - let final = - if kind = NORMAL then begin - match optnormal with - Some v -> - let kept = - if v.constant <? nx.constant - then begin add_event (FORGET (v.id,nx.id));v end - else begin add_event (FORGET (nx.id,v.id));nx end in - (Some(kept),optinvert) - | None -> Some nx,optinvert - end else begin - match optinvert with - Some v -> - let _kept = - if v.constant >? nx.constant - then begin add_event (FORGET_I (v.id,nx.id));v end - else begin add_event (FORGET_I (nx.id,v.id));nx end in - (optnormal,Some(if v.constant >? nx.constant then v else nx)) - | None -> optnormal,Some nx - end in - begin match final with - (Some high, Some low) -> - if high.constant <? low.constant then begin - add_event(CONTRADICTION (high,negate_eq low)); - raise UNSOLVABLE - end - | _ -> () end; - Hashtbl.remove table ne; - Hashtbl.add table ne final - with Not_found -> - Hashtbl.add table ne - (if kind = NORMAL then (Some nx,None) else (None,Some nx))) - system; - let accu_eq = ref [] in - let accu_ineq = ref [] in - Hashtbl.iter - (fun p0 p1 -> match (p0,p1) with - | (e, (Some x, Some y)) when x.constant =? y.constant -> - let id=new_eq_id () in - add_event (MERGE_EQ(id,x,y.id)); - push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq - | (e, (optnorm,optinvert)) -> - begin match optnorm with - Some x -> push x accu_ineq | _ -> () end; - begin match optinvert with - Some x -> push (negate_eq x) accu_ineq | _ -> () end) - table; - !accu_eq,!accu_ineq - -exception SOLVED_SYSTEM - -let select_variable system = - let table = Hashtbl.create 7 in - let push v c= - try let r = Hashtbl.find table v in r := max !r (abs c) - with Not_found -> Hashtbl.add table v (ref (abs c)) in - List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system; - let vmin,cmin = ref (-1), ref zero in - let var_cpt = ref 0 in - Hashtbl.iter - (fun v ({contents = c}) -> - incr var_cpt; - if c <? !cmin || !vmin = (-1) then begin vmin := v; cmin := c end) - table; - if !var_cpt < 1 then raise SOLVED_SYSTEM; - !vmin - -let classify v system = - List.fold_left - (fun (not_occ,below,over) eq -> - try let f,eq' = chop_var v eq.body in - if f.c >=? zero then (not_occ,((f.c,eq) :: below),over) - else (not_occ,below,((neg f.c,eq) :: over)) - with CHOPVAR -> (eq::not_occ,below,over)) - ([],[],[]) system - -let product new_eq_id dark_shadow low high = - List.fold_left - (fun accu (a,eq1) -> - List.fold_left - (fun accu (b,eq2) -> - let eq = - sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1) - (map_eq_afine (fun c -> c * a) eq2) in - add_event(SUM(eq.id,(b,eq1),(a,eq2))); - match normalize eq with - | [eq] -> - let final_eq = - if dark_shadow then - let delta = (a - one) * (b - one) in - add_event(WEAKEN(eq.id,delta)); - {id = eq.id; kind=INEQ; body = eq.body; - constant = eq.constant - delta} - else eq - in final_eq :: accu - | (e::_) -> failwith "Product dardk" - | [] -> accu) - accu high) - [] low - -let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system = - let v = select_variable system in - let (ineq_out, ineq_low,ineq_high) = classify v system in - let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in - if !debug then display_system print_var expanded; expanded - -let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = - if List.exists (fun e -> e.kind = DISE) system then - failwith "disequation in simplify"; - clear_history (); - List.iter (fun e -> add_event (HYP e)) system; - let system = Util.List.map_append normalize system in - let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in - let system = (eqs @ simp_eq,simp_ineq) in - let rec loop1a system = - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq - and loop1b sys_ineq = - let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in - if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq) - in - let rec loop2 system = - try - let expanded = fourier_motzkin new_ids dark_shadow system in - loop2 (loop1b expanded) - with SOLVED_SYSTEM -> - if !debug then display_system print_var system; system - in - loop2 (loop1a system) - -let rec depend relie_on accu = function - | act :: l -> - begin match act with - | DIVIDE_AND_APPROX (e,_,_,_) -> - if Int.List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | EXACT_DIVIDE (e,_) -> - if Int.List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | WEAKEN (e,_) -> - if Int.List.mem e relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | SUM (e,(_,e1),(_,e2)) -> - if Int.List.mem e relie_on then - depend (e1.id::e2.id::relie_on) (act::accu) l - else - depend relie_on accu l - | STATE {st_new_eq=e;st_orig=o} -> - if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l - else depend relie_on accu l - | HYP e -> - if Int.List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l - | FORGET_C _ -> depend relie_on accu l - | FORGET _ -> depend relie_on accu l - | FORGET_I _ -> depend relie_on accu l - | MERGE_EQ (e,e1,e2) -> - if Int.List.mem e relie_on then - depend (e1.id::e2::relie_on) (act::accu) l - else - depend relie_on accu l - | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l - | CONTRADICTION (e1,e2) -> - depend (e1.id::e2.id::relie_on) (act::accu) l - | CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l - | CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l - | CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l - | NEGATE_CONTRADICT (e1,e2,_) -> - depend (e1.id::e2.id::relie_on) (act::accu) l - | SPLIT_INEQ _ -> failwith "depend" - end - | [] -> relie_on, accu - -let negation (eqs,ineqs) = - let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in - let normal = function - | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED - | e -> e,NORMAL in - let table = Hashtbl.create 7 in - List.iter (fun e -> - let {body=ne;constant=c} ,kind = normal e in - Hashtbl.add table (ne,c) (kind,e)) diseq; - List.iter (fun e -> - assert (e.kind = EQUA); - let {body=ne;constant=c},kind = normal e in - try - let (kind',e') = Hashtbl.find table (ne,c) in - add_event (NEGATE_CONTRADICT (e,e',kind=kind')); - raise UNSOLVABLE - with Not_found -> ()) eqs - -exception FULL_SOLUTION of action list * int list - -let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = - clear_history (); - List.iter (fun e -> add_event (HYP e)) system; - (* Initial simplification phase *) - let rec loop1a system = - negation system; - let sys_ineq = banerjee new_ids system in - loop1b sys_ineq - and loop1b sys_ineq = - let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in - if simp_eq = [] then dise @ simp_ineq - else loop1a (simp_eq,dise @ simp_ineq) - in - let rec loop2 system = - try - let expanded = fourier_motzkin new_ids false system in - loop2 (loop1b expanded) - with SOLVED_SYSTEM -> if !debug then display_system print_var system; system - in - let rec explode_diseq = function - | (de::diseq,ineqs,expl_map) -> - let id1 = new_eq_id () - and id2 = new_eq_id () in - let e1 = - {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in - let e2 = - {id = id2; kind=INEQ; body = map_eq_linear neg de.body; - constant = neg de.constant - one} in - let new_sys = - List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys)) - ineqs @ - List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys)) - ineqs - in - explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map) - | ([],ineqs,expl_map) -> ineqs,expl_map - in - try - let system = Util.List.map_append normalize system in - let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in - let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in - let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in - let system = (eqs @ simp_eq,simp_ineq @ dise) in - let system' = loop1a system in - let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in - let first_segment = history () in - let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in - let all_solutions = - List.map - (fun (decomp,sys) -> - clear_history (); - try let _ = loop2 sys in raise NO_CONTRADICTION - with UNSOLVABLE -> - let relie_on,path = depend [] [] (history ()) in - let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in - let red = List.map (fun (x,_,_) -> x) dc in - (red,relie_on,decomp,path)) - sys_exploded - in - let max_count sys = - let tbl = Hashtbl.create 7 in - let augment x = - try incr (Hashtbl.find tbl x) - with Not_found -> Hashtbl.add tbl x (ref 1) in - let eq = ref (-1) and c = ref 0 in - List.iter (function - | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on)) - | (l,_,_,_) -> List.iter augment l) sys; - Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl; - !eq - in - let rec solve systems = - try - let id = max_count systems in - let rec sign = function - | ((id',_,b)::l) -> if id=id' then b else sign l - | [] -> failwith "solve" in - let s1,s2 = - List.partition (fun (_,_,decomp,_) -> sign decomp) systems in - let remove_int (dep,ro,dc,pa) = - (Util.List.except Int.equal id dep,ro,dc,pa) - in - let s1' = List.map remove_int s1 in - let s2' = List.map remove_int s2 in - let (r1,relie1) = solve s1' - and (r2,relie2) = solve s2' in - let (eq,id1,id2) = Int.List.assoc id explode_map in - [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], - eq.id :: Util.List.union Int.equal relie1 relie2 - with FULL_SOLUTION (x0,x1) -> (x0,x1) - in - let act,relie_on = solve all_solutions in - snd(depend relie_on act first_segment) - with UNSOLVABLE -> snd (depend [] [] (history ())) - -end diff --git a/plugins/omega/omega_plugin.mlpack b/plugins/omega/omega_plugin.mlpack deleted file mode 100644 index df7f1047f2..0000000000 --- a/plugins/omega/omega_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Omega -Coq_omega -G_omega diff --git a/plugins/ring/dune b/plugins/ring/dune index 080d8c672e..40f310831a 100644 --- a/plugins/ring/dune +++ b/plugins/ring/dune @@ -1,7 +1,7 @@ (library (name ring_plugin) - (public_name coq.plugins.ring) + (public_name coq-core.plugins.ring) (synopsis "Coq's ring plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ring)) diff --git a/plugins/rtauto/dune b/plugins/rtauto/dune index 43efa0eca5..a13f063550 100644 --- a/plugins/rtauto/dune +++ b/plugins/rtauto/dune @@ -1,7 +1,7 @@ (library (name rtauto_plugin) - (public_name coq.plugins.rtauto) + (public_name coq-core.plugins.rtauto) (synopsis "Coq's rtauto plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_rtauto)) diff --git a/plugins/ssr/dune b/plugins/ssr/dune index a117d09a16..4c28776bb7 100644 --- a/plugins/ssr/dune +++ b/plugins/ssr/dune @@ -1,9 +1,9 @@ (library (name ssreflect_plugin) - (public_name coq.plugins.ssreflect) + (public_name coq-core.plugins.ssreflect) (synopsis "Coq's ssreflect plugin") (modules_without_implementation ssrast) (flags :standard -open Gramlib) - (libraries coq.plugins.ssrmatching)) + (libraries coq-core.plugins.ssrmatching)) (coq.pp (modules ssrvernac ssrparser)) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 4d57abb465..41fd96ccb5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -252,7 +252,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); + debug_ssr (fun () -> str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c); (sigma, (sigma, c)) @@ -1207,7 +1207,7 @@ let gentac gen = Proofview.V82.tactic begin fun gl -> (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); + debug_ssr (fun () -> str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 582c45cde1..78a59abda9 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -126,17 +126,17 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = fun (oc, orig_clr, occ, c_gen) -> pfLIFT begin fun gl -> let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in - ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); + debug_ssr (fun () -> (Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in - ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); + debug_ssr (fun () -> Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); + debug_ssr (fun () -> Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -212,10 +212,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let renamed_tys = Array.mapi (fun j (ctx, cty) -> let t = Term.it_mkProd_or_LetIn cty ctx in - ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); + debug_ssr (fun () -> Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in - ppdebug(lazy Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); + debug_ssr (fun () -> Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); t) tys in @@ -241,8 +241,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = in let () = let sigma = project gl in - ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); - ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in + debug_ssr (fun () -> Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); + debug_ssr (fun () -> Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in let open EConstr in let inf_deps_r = match kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) @@ -301,7 +301,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = | Some (c, _, _,gl) -> Some(true, gl) | None -> None in first [try_c_last_arg;try_c_last_pattern] in - ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); + debug_ssr (fun () -> Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at @@ -321,7 +321,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); + debug_ssr (fun () -> Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in @@ -337,8 +337,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in head_p @ patterns, Util.List.uniquize clr, gl in - ppdebug(lazy Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns))); - ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); + debug_ssr (fun () -> Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns))); + debug_ssr (fun () -> Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); (* Predicate generation, and (if necessary) tactic to generalize the * equation asked by the user *) let elim_pred, gen_eq_tac, clr, gl = @@ -348,7 +348,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then - let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in + let () = debug_ssr (fun () -> Pp.(str"postponing " ++ pp_pattern env p)) in cl, gl, post @ [h, p, inf_t, occ] else try let c, cl, ucst = match_pat env p occ h cl in @@ -420,8 +420,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = else gl, concl in concl, gen_eq_tac, clr, gl in let gl, pty = pf_e_type_of gl elim_pred in - ppdebug(lazy Pp.(str"elim_pred=" ++ pp_term gl elim_pred)); - ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty)); + debug_ssr (fun () -> Pp.(str"elim_pred=" ++ pp_term gl elim_pred)); + debug_ssr (fun () -> Pp.(str"elim_pred_ty=" ++ pp_term gl pty)); let gl = pf_unify_HO gl pred elim_pred in let elim = fire_subst gl elim in let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 0008d31ffd..92a481dd18 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -76,7 +76,7 @@ let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s) (** The "congr" tactic *) let interp_congrarg_at ist gl n rf ty m = - ppdebug(lazy Pp.(str"===interp_congrarg_at===")); + debug_ssr (fun () -> Pp.(str"===interp_congrarg_at===")); let congrn, _ = mkSsrRRef "nary_congruence" in let args1 = mkRnat n :: mkRHoles n @ [ty] in let args2 = mkRHoles (3 * n) in @@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); + debug_ssr (fun () -> Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -92,8 +92,8 @@ let interp_congrarg_at ist gl n rf ty m = let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = - ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); + debug_ssr (fun () -> (Pp.str"===congr===")); + debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -124,8 +124,8 @@ let newssrcongrtac arg ist = Proofview.Goal.enter_one ~__LOC__ begin fun _g -> (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr -> Proofview.V82.tactic begin fun gl -> - ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); + debug_ssr (fun () -> Pp.(str"===newcongr===")); + debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -385,8 +385,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) | e when CErrors.noncritical e -> raise (PRtype_error None) in - ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); - ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); + debug_ssr (fun () -> Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); + debug_ssr (fun () -> Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try Proofview.V82.of_tactic (refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl with e when CErrors.noncritical e -> @@ -435,12 +435,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr = let sigma0 = Evd.set_universe_context sigma0 ucst in let rdxt = Retyping.get_type_of env (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); + debug_ssr (fun () -> Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); let cvtac, rwtac, sigma0 = if EConstr.Vars.closed0 sigma0 r' then let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); + debug_ssr (fun () -> Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); let open EConstr in match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> @@ -521,7 +521,7 @@ let rwprocess_rule env dir rule = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta env sigma t0 in - ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); + debug_ssr (fun () -> Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> let sigma = Evd.create_evar_defs sigma in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f2c7f495b3..bc46c23761 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -296,8 +296,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave = | Some id -> if pats = [] then Tacticals.New.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); + debug_ssr (fun () -> str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))); + debug_ssr (fun () -> str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct); Tacticals.New.tclTHENS (basecuttac "ssr_have" ct) [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in "ssr_have", @@ -395,7 +395,7 @@ let intro_lock ipats = Array.length args = 3 && is_app_evar sigma args.(2) -> protect_subgoal env sigma hd args | _ -> - ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); + debug_ssr (fun () -> Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); Proofview.tclUNIT () end) @@ -468,13 +468,13 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = | Some l -> [IPatCase(Regular [l;[]])] in let map_redex env evar_map ~before:_ ~after:t = - ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); + debug_ssr (fun () -> Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); let evar_map, ty = Typing.type_of env evar_map t in let new_t = (* pretty-rename the bound variables *) try begin match EConstr.destApp evar_map t with (f, ar) -> let lam = Array.last ar in - ppdebug(lazy Pp.(str"under: mapping:" ++ + debug_ssr(fun () -> Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map lam)); let new_lam = pretty_rename evar_map lam varnames in let new_ar, len1 = Array.copy ar, pred (Array.length ar) in @@ -482,10 +482,10 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = EConstr.mkApp (f, new_ar) end with | DestKO -> - ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp")); + debug_ssr (fun () -> Pp.(str"under: cannot pretty-rename bound variables with destApp")); t in - ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); + debug_ssr (fun () -> Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); evar_map, new_t in let undertacs = diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 1e940b5ad3..f8abed5482 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -324,7 +324,7 @@ end `tac`, where k is the size of `seeds` *) let tclSEED_SUBGOALS seeds tac = tclTHENin tac (fun i n -> - Ssrprinters.ppdebug (lazy Pp.(str"seeding")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"seeding")); (* eg [case: (H _ : nat)] generates 3 goals: - 1 for _ - 2 for the nat constructors *) @@ -416,11 +416,11 @@ let tclMK_ABSTRACT_VARS ids = (* Debugging *) let tclLOG p t = tclUNIT () >>= begin fun () -> - Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "exec: " ++ pr_ipatop p)); tclUNIT () end <*> Goal.enter begin fun g -> - Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str" on state:" ++ spc () ++ isPRINT g ++ str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g))); tclUNIT () @@ -429,7 +429,7 @@ let tclLOG p t = t p >>= fun ret -> Goal.enter begin fun g -> - Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "done: " ++ isPRINT g)); tclUNIT () end >>= fun () -> tclUNIT ret @@ -579,10 +579,10 @@ let tclCompileIPats l = elab l ;; let tclCompileIPats l = - Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats input: " ++ prlist_with_sep spc Ssrprinters.pr_ipat l)); let ops = tclCompileIPats l in - Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats output: " ++ prlist_with_sep spc pr_ipatop ops)); ops @@ -597,11 +597,11 @@ let main ?eqtac ~first_case_is_dispatch iops = end (* }}} *) let tclIPAT_EQ eqtac ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclIPATssr ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclCompileIPats = IpatMachine.tclCompileIPats diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 935cef58b9..ad85f68b03 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -46,6 +46,7 @@ open Ssrtacticals open Ssrbwd open Ssrequality open Ssripats +open Libobject (** Ssreflect load check. *) @@ -79,8 +80,39 @@ let ssrtac_entry name = { mltac_index = 0; } -let register_ssrtac name f = - Tacenv.register_ml_tactic (ssrtac_name name) [|f|] +let cache_tactic_notation (_, (key, body, parule)) = + Tacenv.register_alias key body; + Pptactic.declare_notation_tactic_pprule key parule + +type tactic_grammar_obj = KerName.t * Tacenv.alias_tactic * Pptactic.pp_tactic + +let inSsrGrammar : tactic_grammar_obj -> obj = + declare_object {(default_object "SsrGrammar") with + load_function = (fun _ -> cache_tactic_notation); + cache_function = cache_tactic_notation; + classify_function = (fun x -> Keep x)} + +let path = MPfile (DirPath.make @@ List.map Id.of_string ["ssreflect"; "ssr"; "Coq"]) + +let register_ssrtac name f prods = + let open Pptactic in + Tacenv.register_ml_tactic (ssrtac_name name) [|f|]; + let map id = Reference (Locus.ArgVar (CAst.make id)) in + let get_id = function + | TacTerm s -> None + | TacNonTerm (_, (_, ido)) -> ido in + let ids = List.map_filter get_id prods in + let tac = TacML (CAst.make (ssrtac_entry name, List.map map ids)) in + let key = KerName.make path (Label.make ("ssrparser_" ^ name)) in + let body = Tacenv.{ alias_args = ids; alias_body = tac; alias_deprecation = None } in + let parule = { + pptac_level = 0; + pptac_prods = prods + } in + let obj () = + Lib.add_anonymous_leaf (inSsrGrammar (key, body, parule)) in + Mltop.declare_cache_obj obj __coq_plugin_name; + key let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v @@ -933,7 +965,7 @@ END { let pr_intros sep intrs = - if intrs = [] then mt() else sep () ++ str "=>" ++ pr_ipats intrs + if intrs = [] then mt() else sep () ++ str "=>" ++ sep () ++ pr_ipats intrs let pr_ssrintros _ _ _ = pr_intros mt } @@ -963,15 +995,6 @@ END { -let () = register_ssrtac "tclintros" begin fun args ist -> match args with -| [arg] -> - let arg = cast_arg wit_ssrintrosarg arg in - let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros -| _ -> assert false -end - - (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id @@ -1672,20 +1695,28 @@ let _ = add_internal_name (is_tagged perm_tag) { -type ssrargfmt = ArgSsr of string | ArgSep of string + let ssrtac_expr ?loc key args = + TacAlias (CAst.make ?loc (key, (List.map (fun x -> Tacexpr.TacGeneric (None, x)) args))) -let set_pr_ssrtac name prec afmt = (* FIXME *) () (* - let fmt = List.map (function - | ArgSep s -> Egramml.GramTerminal s - | ArgSsr s -> Egramml.GramTerminal s - | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in - let tacname = ssrtac_name name in () *) +let mk_non_term wit id = + let open Pptactic in + TacNonTerm (None, (Extend.Uentry (Genarg.ArgT.Any (Genarg.get_arg_tag wit)), Some id)) -let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) +let tclintroskey = + let prods = + [ mk_non_term wit_ssrintrosarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [arg] -> + let arg = cast_arg wit_ssrintrosarg arg in + let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros + | _ -> assert false + end in + register_ssrtac "tclintros" tac prods let tclintros_expr ?loc tac ipats = - let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in - ssrtac_expr ?loc "tclintros" args + let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in + ssrtac_expr ?loc tclintroskey args } @@ -1768,18 +1799,20 @@ END { -let () = register_ssrtac "tcldo" begin fun args ist -> match args with -| [arg] -> - let arg = cast_arg wit_ssrdoarg arg in - ssrdotac ist arg -| _ -> assert false -end - -let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] +let tcldokey = + let open Pptactic in + let prods = [ TacTerm "do"; mk_non_term wit_ssrdoarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [arg] -> + let arg = cast_arg wit_ssrdoarg arg in + ssrdotac ist arg + | _ -> assert false + end in + register_ssrtac "tcldo" tac prods let ssrdotac_expr ?loc n m tac clauses = let arg = ((n, m), tac), clauses in - ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)] + ssrtac_expr ?loc tcldokey [in_gen (rawwit wit_ssrdoarg) arg] } @@ -1815,22 +1848,26 @@ END { -let () = register_ssrtac "tclseq" begin fun args ist -> match args with -| [tac; dir; arg] -> - let tac = cast_arg wit_ssrtclarg tac in - let dir = cast_arg wit_ssrseqdir dir in - let arg = cast_arg wit_ssrseqarg arg in - tclSEQAT ist tac dir arg -| _ -> assert false -end - -let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] +let tclseqkey = + let prods = + [ mk_non_term wit_ssrtclarg (Names.Id.of_string "tac") + ; mk_non_term wit_ssrseqdir (Names.Id.of_string "dir") + ; mk_non_term wit_ssrseqarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [tac; dir; arg] -> + let tac = cast_arg wit_ssrtclarg tac in + let dir = cast_arg wit_ssrseqdir dir in + let arg = cast_arg wit_ssrseqarg arg in + tclSEQAT ist tac dir arg + | _ -> assert false + end in + register_ssrtac "tclseq" tac prods let tclseq_expr ?loc tac dir arg = let arg1 = in_gen (rawwit wit_ssrtclarg) tac in let arg2 = in_gen (rawwit wit_ssrseqdir) dir in let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in - ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3]) + ssrtac_expr ?loc tclseqkey [arg1; arg2; arg3] } @@ -2453,8 +2490,9 @@ GRAMMAR EXTEND Gram GLOBAL: ltac_expr; ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> - { ssrtac_expr ~loc "abstract" - [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; + { TacML (CAst.make ~loc ( + ssrtac_entry "abstract", [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)])) + } ]]; END TACTIC EXTEND ssrabstract | [ "abstract" ssrdgens(gens) ] -> { diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 6ed68094dc..434568b554 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -15,7 +15,6 @@ open Names open Printer open Tacmach -open Ssrmatching_plugin open Ssrast let pr_spc () = str " " @@ -121,15 +120,4 @@ and pr_block = function (Prefix id) -> str"^" ++ Id.print id | (SuffixId id) -> str"^~" ++ Id.print id | (SuffixNum n) -> str"^~" ++ int n -(* 0 cost pp function. Active only if Debug Ssreflect is Set *) -let ppdebug_ref = ref (fun _ -> ()) -let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let () = - Goptions.(declare_bool_option - { optkey = ["Debug";"Ssreflect"]; - optdepr = false; - optread = (fun _ -> !ppdebug_ref == ssr_pp); - optwrite = (fun b -> - Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) -let ppdebug s = !ppdebug_ref s +let debug_ssr = CDebug.create ~name:"ssreflect" () diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 21fb28038a..994577a0c9 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -51,5 +51,4 @@ val pr_guarded : val pr_occ : ssrocc -> Pp.t -val ppdebug : Pp.t Lazy.t -> unit - +val debug_ssr : CDebug.t diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 97926753f5..b3a9e71a3f 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -194,17 +194,17 @@ let mkGApp f args = let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> let env = Goal.env goal in let sigma = Goal.sigma goal in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob)); try let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term)); tclUNIT (env,sigma,term) with e -> (* XXX this is another catch all! *) let e, info = Exninfo.capture e in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob)); tclZERO ~info e end @@ -217,7 +217,7 @@ end let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t let tclADD_CLEAR_IF_ID (env, ist, t) x = - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); let hd, args = EConstr.decompose_app ist t in match EConstr.kind ist hd with @@ -269,11 +269,11 @@ let interp_view ~clear_if_id ist v p = let p_id = DAst.make p_id in match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> - Ssrprinters.ppdebug (lazy Pp.(str "specialize")); + Ssrprinters.debug_ssr (fun () -> Pp.(str "specialize")); interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> - Ssrprinters.ppdebug (lazy Pp.(str "view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE @@ -324,7 +324,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let rigid = rigid_of und0 in let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in let p = if simple_types then pf_abs_cterm s0 n p else p in - Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str"view@finalized: " ++ Printer.pr_econstr_env env sigma p)); let sigma = List.fold_left Evd.remove sigma to_prune in Unsafe.tclEVARS sigma <*> @@ -349,26 +349,26 @@ let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 = pose_proof name p <*> conclusion ~to_clear:name) <*> tclUNIT false) | v :: vs -> - Ssrprinters.ppdebug (lazy Pp.(str"piling...")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"piling...")); is_tac_in_term ~extra_scope:"ssripat" v >>= function | `Term v -> - Ssrprinters.ppdebug (lazy Pp.(str"..a term")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..a term")); pile_up_view ~clear_if_id v <*> apply_all_views_aux ~clear_if_id vs finalization conclusion s0 | `Tac tac -> - Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..a tactic")); finalization s0 (fun name p -> (match p with | None -> tclUNIT () | Some p -> pose_proof name p) <*> Tacinterp.eval_tactic tac <*> if vs = [] then begin - Ssrprinters.ppdebug (lazy Pp.(str"..was the last view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..was the last view")); conclusion ~to_clear:name <*> tclUNIT true end else Tactics.clear name <*> tclINDEPENDENTL begin - Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..was NOT the last view")); Ssrcommon.tacSIGMA >>= apply_all_views_aux ~clear_if_id vs finalization conclusion end >>= reduce_or) diff --git a/plugins/ssrmatching/dune b/plugins/ssrmatching/dune index 629d723816..efaa09c939 100644 --- a/plugins/ssrmatching/dune +++ b/plugins/ssrmatching/dune @@ -1,7 +1,7 @@ (library (name ssrmatching_plugin) - (public_name coq.plugins.ssrmatching) + (public_name coq-core.plugins.ssrmatching) (synopsis "Coq ssrmatching plugin") - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules g_ssrmatching)) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7774258fca..805be1fc87 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -22,7 +22,6 @@ open Vars open Libnames open Tactics open Termops -open Recordops open Tacmach open Glob_term open Util @@ -333,7 +332,8 @@ type tpattern = { let all_ok _ _ = true let proj_nparams c = - try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0 + try 1 + Structures.Structure.projection_nparams c + with Not_found -> 0 let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true @@ -429,9 +429,13 @@ let ungen_upat lhs (sigma, uc, t) u = | _ -> KpatRigid in sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t} -let nb_cs_proj_args pc f u = +let nb_cs_proj_args ise pc f u = + let open Structures in + let open ValuePattern in let na k = - List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in + let open CanonicalSolution in + let _, { cvalue_arguments } = find (Global.env()) ise (GlobRef.ConstRef pc, k) in + List.length cvalue_arguments in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be @@ -441,7 +445,7 @@ let nb_cs_proj_args pc f u = | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Names.Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -467,7 +471,7 @@ let splay_app ise = | Cast _ | Evar _ -> loop c [| |] | _ -> c, [| |] -let filter_upat i0 f n u fpats = +let filter_upat ise i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with @@ -479,7 +483,7 @@ let filter_upat i0 f n u fpats = | KpatRigid when isRigid f -> na | KpatFlex -> na | KpatProj pc -> - let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np + let np = na + nb_cs_proj_args ise pc f u in if n < np then -1 else np | _ -> -1 in if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats @@ -568,7 +572,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = let f, a = splay_app ise c in let i0 = ref (-1) in - let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in + let fpats = List.fold_right (filter_upat ise i0 f (Array.length a)) upats [] in while !i0 >= 0 do let i = !i0 in i0 := -1; let one_match (u, np) = diff --git a/plugins/ssrsearch/dune b/plugins/ssrsearch/dune index 2851835eae..a38bec496f 100644 --- a/plugins/ssrsearch/dune +++ b/plugins/ssrsearch/dune @@ -1,7 +1,7 @@ (library (name ssrsearch_plugin) - (public_name coq.plugins.ssrsearch) + (public_name coq-core.plugins.ssrsearch) (synopsis "Deprecated Search command from SSReflect") - (libraries coq.plugins.ssreflect)) + (libraries coq-core.plugins.ssreflect)) (coq.pp (modules g_search)) diff --git a/plugins/syntax/dune b/plugins/syntax/dune index f930fc265a..b00242be1a 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -1,22 +1,15 @@ (library (name number_string_notation_plugin) - (public_name coq.plugins.number_string_notation) + (public_name coq-core.plugins.number_string_notation) (synopsis "Coq number and string notation plugin") (modules g_number_string string_notation number) - (libraries coq.vernac)) - -(library - (name int63_syntax_plugin) - (public_name coq.plugins.int63_syntax) - (synopsis "Coq syntax plugin: int63") - (modules int63_syntax) - (libraries coq.vernac)) + (libraries coq-core.vernac)) (library (name float_syntax_plugin) - (public_name coq.plugins.float_syntax) + (public_name coq-core.plugins.float_syntax) (synopsis "Coq syntax plugin: float") (modules float_syntax) - (libraries coq.vernac)) + (libraries coq-core.vernac)) (coq.pp (modules g_number_string)) diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml deleted file mode 100644 index 110b26581f..0000000000 --- a/plugins/syntax/int63_syntax.ml +++ /dev/null @@ -1,58 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "int63_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* digit-based syntax for int63 *) - -open Names -open Libnames - -(*** Constants for locating int63 constructors ***) - -let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int" -let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.id_int" - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -(* int63 stuff *) -let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"] -let int63_path = make_path int63_module "int" -let int63_scope = "int63_scope" - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -(* Actually declares the interpreter for int63 *) - -let _ = - let open Notation in - at_declare_ml_module - (fun () -> - let id_int63 = Nametab.locate q_id_int63 in - let o = { to_kind = Int63, Direct; - to_ty = id_int63; - to_post = [||]; - of_kind = Int63, Direct; - of_ty = id_int63; - ty_name = q_int63; - warning = Nop } in - enable_prim_token_interpretation - { pt_local = false; - pt_scope = int63_scope; - pt_interp_info = NumberNotation o; - pt_required = (int63_path, int63_module); - pt_refs = []; - pt_in_match = false }) - () diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index 0e7640f430..551e2bac5d 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -106,10 +106,12 @@ let locate_number () = let locate_int63 () = let int63n = "num.int63.type" in - if Coqlib.has_ref int63n + let pos_neg_int63n = "num.int63.pos_neg_int63" in + if Coqlib.has_ref int63n && Coqlib.has_ref pos_neg_int63n then - let q_int63 = qualid_of_ref int63n in - Some (mkRefC q_int63) + let q_pos_neg_int63 = qualid_of_ref pos_neg_int63n in + Some ({pos_neg_int63_ty = unsafe_locate_ind q_pos_neg_int63}, + mkRefC q_pos_neg_int63) else None let has_type env sigma f ty = @@ -121,20 +123,13 @@ let type_error_to f ty = CErrors.user_err (pr_qualid f ++ str " should go from Number.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + fnl () ++ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Number.int or (option Number.int)." ++ fnl () ++ - str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") - -let warn_deprecated_decimal = - CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" - (fun () -> - strbrk "Deprecated Number Notation for Decimal.uint, \ - Decimal.int or Decimal.decimal. Use Number.uint, \ - Number.int or Number.number respectively.") + str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") let error_params ind = CErrors.user_err @@ -381,22 +376,37 @@ let elaborate_to_post_via env sigma ty_name ty_ind l = let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in to_post, pt_refs -let locate_global_inductive allow_params qid = - let locate_param_inductive qid = +type target_type = + | TargetInd of (inductive * GlobRef.t option list) + | TargetPrim of required_module + +let locate_global_inductive_with_params allow_params qid = + if not allow_params then raise Not_found else match Nametab.locate_extended qid with | Globnames.TrueGlobal _ -> raise Not_found | Globnames.SynDef kn -> match Syntax_def.search_syntactic_definition kn with - | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params -> + | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) -> i, List.map (function | Notation_term.NRef (r,None) -> Some r | Notation_term.NHole _ -> None | _ -> raise Not_found) l - | _ -> raise Not_found in - try locate_param_inductive qid + | _ -> raise Not_found + +let locate_global_inductive allow_params qid = + try locate_global_inductive_with_params allow_params qid with Not_found -> Smartlocate.global_inductive_with_alias qid, [] +let locate_global_inductive_or_int63 allow_params qid = + try TargetInd (locate_global_inductive_with_params allow_params qid) + with Not_found -> + let int63n = "num.int63.type" in + if allow_params && Coqlib.has_ref int63n + && GlobRef.equal (Smartlocate.global_with_alias qid) (Coqlib.lib_ref int63n) + then TargetPrim (Nametab.path_of_global (Coqlib.lib_ref int63n), []) + else TargetInd (Smartlocate.global_inductive_with_alias qid, []) + let vernac_number_notation local ty f g opts scope = let rec parse_opts = function | [] -> None, Nop @@ -421,7 +431,7 @@ let vernac_number_notation local ty f g opts scope = let ty_name = ty in let ty, via = match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in - let tyc, params = locate_global_inductive (via = None) ty in + let tyc_params = locate_global_inductive_or_int63 (via = None) ty in let to_ty = Smartlocate.global_with_alias f in let of_ty = Smartlocate.global_with_alias g in let cty = mkRefC ty in @@ -439,23 +449,20 @@ let vernac_number_notation local ty f g opts scope = | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct - | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option + | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 cty) -> Int63 pos_neg_int63_ty, Direct + | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 (opt cty)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_to f ty in (* Check the type of g *) + let cty = match tyc_params with + | TargetPrim _ -> mkRefC (qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int_wrapper") + | TargetInd _ -> cty in let of_kind = match num_ty with | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct @@ -464,30 +471,24 @@ let vernac_number_notation local ty f g opts scope = | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct - | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option + | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty cint63) -> Int63 pos_neg_int63_ty, Direct + | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_of g ty in - (match to_kind, of_kind with - | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ - | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> - warn_deprecated_decimal () - | _ -> ()); - let to_post, pt_refs = match via with - | None -> elaborate_to_post_params env sigma tyc params - | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + let to_post, pt_required, pt_refs = match tyc_params with + | TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"] + | TargetInd (tyc, params) -> + let to_post, pt_refs = + match via with + | None -> elaborate_to_post_params env sigma tyc params + | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = opts } in @@ -498,7 +499,7 @@ let vernac_number_notation local ty f g opts scope = { pt_local = local; pt_scope = scope; pt_interp_info = NumberNotation o; - pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; + pt_required; pt_refs; pt_in_match = true } in |