diff options
Diffstat (limited to 'plugins')
93 files changed, 568 insertions, 4740 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index ee7341a4a2..f1095fc9f1 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Omega ROmega. +Require Import Bool PArith DecidableClass Omega Lia. Ltac bool := repeat match goal with @@ -84,9 +84,9 @@ Ltac case_decide := match goal with let H := fresh "H" in define (@decide P D) b H; destruct b; try_decide | [ |- context [Pos.compare ?x ?y] ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia | [ X : context [Pos.compare ?x ?y] |- _ ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia end. Section Definitions. @@ -325,13 +325,13 @@ Qed. Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p. Proof. -intros k l p H; revert l; induction H; constructor; eauto; zify; romega. +intros k l p H; revert l; induction H; constructor; eauto; lia. Qed. Lemma linear_valid_incl : forall k p, linear k p -> valid k p. Proof. intros k p H; induction H; constructor; auto. -eapply valid_le_compat; eauto; zify; romega. +eapply valid_le_compat; eauto; lia. Qed. End Validity. @@ -417,13 +417,13 @@ Qed. Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z <= Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (Pos.max ?x ?y < ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | _ => zify; omega end. Hint Resolve Pos.le_max_r Pos.le_max_l. @@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. now rewrite <- (Pos.max_id i); intuition. destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. - + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega. - + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } @@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. -eapply (valid_le_compat i); [now auto|zify; romega]. +eapply (valid_le_compat i); [now auto|lia]. Qed. Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p. diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 3bd7cd622c..d82e8ae8ad 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. +Require Import Bool DecidableClass Algebra Ring PArith Omega. Section Bool. diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/plugin_base.dune new file mode 100644 index 0000000000..6a024358c3 --- /dev/null +++ b/plugins/btauto/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name btauto_plugin) + (public_name coq.plugins.btauto) + (synopsis "Coq's btauto plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index c2bc8c079c..b0f97c59b8 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -224,7 +224,7 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let concl = EConstr.Unsafe.to_constr concl in @@ -240,7 +240,7 @@ module Btauto = struct end let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index ce620d5312..f26ec0f401 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -26,6 +26,10 @@ let init_size=5 let cc_verbose=ref false +let print_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t + let debug x = if !cc_verbose then Feedback.msg_debug (x ()) @@ -483,10 +487,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/plugin_base.dune new file mode 100644 index 0000000000..2a92996d2a --- /dev/null +++ b/plugins/cc/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name cc_plugin) + (public_name coq.plugins.cc) + (synopsis "Coq's congruence closure plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune new file mode 100644 index 0000000000..ba9cd595ce --- /dev/null +++ b/plugins/derive/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name derive_plugin) + (public_name coq.plugins.derive) + (synopsis "Coq's derive plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 4ede11b5c9..5d3115d8d7 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -710,10 +710,10 @@ let structure_for_compute env sg c = init false false ~compute:true; let ast, mlt = Extraction.extract_constr env sg c in let ast = Mlutil.normalize ast in - let refs = ref Refset.empty in - let add_ref r = refs := Refset.add r !refs in + let refs = ref GlobRef.Set.empty in + let add_ref r = refs := GlobRef.Set.add r !refs in let () = ast_iter_references add_ref add_ref add_ref ast in - let refs = Refset.elements !refs in + let refs = GlobRef.Set.elements !refs in let struc = optimize_struct (refs,[]) (mono_environment refs []) in (flatten_structure struc), ast, mlt diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/plugin_base.dune new file mode 100644 index 0000000000..037b0d5053 --- /dev/null +++ b/plugins/extraction/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name extraction_plugin) + (public_name coq.plugins.extraction) + (synopsis "Coq's extraction plugin") + (libraries num coq.plugins.ltac)) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index c3f4cfe654..e05e82af6f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -30,8 +30,8 @@ let capitalize = String.capitalize (** Sets and maps for [global_reference] that use the "user" [kernel_name] instead of the canonical one *) -module Refmap' = Refmap_env -module Refset' = Refset_env +module Refmap' = GlobRef.Map_env +module Refset' = GlobRef.Set_env (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) @@ -213,12 +213,12 @@ let is_recursor = function (* NB: here, working modulo name equivalence is ok *) -let projs = ref (Refmap.empty : (inductive*int) Refmap.t) -let init_projs () = projs := Refmap.empty -let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs -let is_projection r = Refmap.mem r !projs -let projection_arity r = snd (Refmap.find r !projs) -let projection_info r = Refmap.find r !projs +let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t) +let init_projs () = projs := GlobRef.Map.empty +let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs +let is_projection r = GlobRef.Map.mem r !projs +let projection_arity r = snd (GlobRef.Map.find r !projs) +let projection_info r = GlobRef.Map.find r !projs (*s Table of used axioms *) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 85f4939560..286021d68e 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -38,7 +38,7 @@ let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else Globnames.RefOrdered.compare id1 id2 + else GlobRef.Ordered.compare id1 id2 module OrderedInstance= struct diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune new file mode 100644 index 0000000000..bcbb99d9fc --- /dev/null +++ b/plugins/firstorder/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name ground_plugin) + (public_name coq.plugins.ground) + (synopsis "Coq's first order logic solver plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b13580bc03..3ae777cc9a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -34,7 +34,7 @@ type lseqtac= GlobRef.t -> seqtac type 'a with_backtracking = tactic -> 'a let wrap n b continue seq = - Proofview.Goal.nf_enter begin fun gls -> + Proofview.Goal.enter begin fun gls -> Control.check_for_interrupt (); let nc = Proofview.Goal.hyps gls in let env=pf_env gls in diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 2a527da9be..5958fe8203 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -62,7 +62,7 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - let c = Globnames.RefOrdered.compare id1 id2 in + let c = GlobRef.Ordered.compare id1 id2 in if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in diff --git a/plugins/fourier/plugin_base.dune b/plugins/fourier/plugin_base.dune new file mode 100644 index 0000000000..8cc76f6f9e --- /dev/null +++ b/plugins/fourier/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name fourier_plugin) + (public_name coq.plugins.fourier) + (synopsis "Coq's fourier plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 5fc4293cbb..fd2d90e9cf 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1469,7 +1469,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((CAst.make @@ relnames.(i)), None), + ((CAst.make @@ relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1499,14 +1499,14 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = @@ -1521,7 +1521,7 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 489a40ed09..e114a0119e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -98,7 +98,7 @@ let functional_induction with_clean c princl pat = List.map2 (fun c pat -> ((None, - Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), + Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), (None,pat), None)) (args@c_list) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 439274240f..ad11f853ca 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -351,7 +351,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i Locusops.onConcl); observe_tac ("toto ") tclIDTAC; - (* introducing the the result of the graph and the equality hypothesis *) + (* introducing the result of the graph and the equality hypothesis *) observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); (* replacing [res] with its value *) observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune new file mode 100644 index 0000000000..002eb28eea --- /dev/null +++ b/plugins/funind/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name recdef_plugin) + (public_name coq.plugins.recdef) + (synopsis "Coq's functional induction plugin") + (libraries coq.plugins.extraction)) diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 84f13d2131..b0277e9cc2 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -94,12 +94,12 @@ let let_evar name typ = in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) + (Tactics.pose_tac (Name.Name id) evar) end let hget_evar n = let open EConstr in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dbbdbfa396..f4555509cc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -52,8 +52,11 @@ let () = (* Rewriting orientation *) -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" +let _ = + Mltop.declare_cache_obj + (fun () -> Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" let pr_orient _prc _prlc _prt = function | true -> Pp.mt () @@ -196,9 +199,9 @@ let pr_gen_place pr_id = function ConclLocation () -> Pp.mt () | HypLocation (id,InHyp) -> str "in " ++ pr_id id | HypLocation (id,InHypTypeOnly) -> - str "in (Type of " ++ pr_id id ++ str ")" + str "in (type of " ++ pr_id id ++ str ")" | HypLocation (id,InHypValueOnly) -> - str "in (Value of " ++ pr_id id ++ str ")" + str "in (value of " ++ pr_id id ++ str ")" let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print @@ -217,6 +220,14 @@ let interp_place ist gl p = let subst_place subst pl = pl +let warn_deprecated_instantiate_syntax = + CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" + (fun (v,v',id) -> + let s = Id.to_string id in + Pp.strbrk + ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") + ) + ARGUMENT EXTEND hloc PRINTED BY pr_place INTERPRETED BY interp_place @@ -231,8 +242,14 @@ ARGUMENT EXTEND hloc | [ "in" ident(id) ] -> [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] + [ warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> + [ warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) ] +| [ "in" "(" "type" "of" ident(id) ")" ] -> + [ HypLocation ((CAst.make id),InHypTypeOnly) ] +| [ "in" "(" "value" "of" ident(id) ")" ] -> [ HypLocation ((CAst.make id),InHypValueOnly) ] END @@ -294,78 +311,3 @@ let pr_lpar_id_colon _ _ _ _ = mt () ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon | [ local_test_lpar_id_colon(x) ] -> [ () ] END - -(* spiwack: the print functions are incomplete, but I don't know what they are - used for *) -let pr_r_int31_field i31f = - str "int31 " ++ - match i31f with - | Retroknowledge.Int31Bits -> str "bits" - | Retroknowledge.Int31Type -> str "type" - | Retroknowledge.Int31Twice -> str "twice" - | Retroknowledge.Int31TwicePlusOne -> str "twice plus one" - | Retroknowledge.Int31Phi -> str "phi" - | Retroknowledge.Int31PhiInv -> str "phi inv" - | Retroknowledge.Int31Plus -> str "plus" - | Retroknowledge.Int31Times -> str "times" - | Retroknowledge.Int31Constructor -> assert false - | Retroknowledge.Int31PlusC -> str "plusc" - | Retroknowledge.Int31PlusCarryC -> str "pluscarryc" - | Retroknowledge.Int31Minus -> str "minus" - | Retroknowledge.Int31MinusC -> str "minusc" - | Retroknowledge.Int31MinusCarryC -> str "minuscarryc" - | Retroknowledge.Int31TimesC -> str "timesc" - | Retroknowledge.Int31Div21 -> str "div21" - | Retroknowledge.Int31Div -> str "div" - | Retroknowledge.Int31Diveucl -> str "diveucl" - | Retroknowledge.Int31AddMulDiv -> str "addmuldiv" - | Retroknowledge.Int31Compare -> str "compare" - | Retroknowledge.Int31Head0 -> str "head0" - | Retroknowledge.Int31Tail0 -> str "tail0" - | Retroknowledge.Int31Lor -> str "lor" - | Retroknowledge.Int31Land -> str "land" - | Retroknowledge.Int31Lxor -> str "lxor" - -let pr_retroknowledge_field f = - match f with - (* | Retroknowledge.KEq -> str "equality" - | Retroknowledge.KNat natf -> pr_r_nat_field () () () natf - | Retroknowledge.KN nf -> pr_r_n_field () () () nf *) - | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ - spc () ++ str "in " ++ qs group - -VERNAC ARGUMENT EXTEND retroknowledge_int31 -PRINTED BY pr_r_int31_field -| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ] -| [ "int31" "type" ] -> [ Retroknowledge.Int31Type ] -| [ "int31" "twice" ] -> [ Retroknowledge.Int31Twice ] -| [ "int31" "twice" "plus" "one" ] -> [ Retroknowledge.Int31TwicePlusOne ] -| [ "int31" "phi" ] -> [ Retroknowledge.Int31Phi ] -| [ "int31" "phi" "inv" ] -> [ Retroknowledge.Int31PhiInv ] -| [ "int31" "plus" ] -> [ Retroknowledge.Int31Plus ] -| [ "int31" "plusc" ] -> [ Retroknowledge.Int31PlusC ] -| [ "int31" "pluscarryc" ] -> [ Retroknowledge.Int31PlusCarryC ] -| [ "int31" "minus" ] -> [ Retroknowledge.Int31Minus ] -| [ "int31" "minusc" ] -> [ Retroknowledge.Int31MinusC ] -| [ "int31" "minuscarryc" ] -> [ Retroknowledge.Int31MinusCarryC ] -| [ "int31" "times" ] -> [ Retroknowledge.Int31Times ] -| [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ] -| [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ] -| [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] -| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ] -| [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] -| [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] -| [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] -| [ "int31" "tail0" ] -> [ Retroknowledge.Int31Tail0 ] -| [ "int31" "lor" ] -> [ Retroknowledge.Int31Lor ] -| [ "int31" "land" ] -> [ Retroknowledge.Int31Land ] -| [ "int31" "lxor" ] -> [ Retroknowledge.Int31Lxor ] -END - -VERNAC ARGUMENT EXTEND retroknowledge_field -PRINTED BY pr_retroknowledge_field -(*| [ "equality" ] -> [ Retroknowledge.KEq ] -| [ retroknowledge_nat(n)] -> [ Retroknowledge.KNat n ] -| [ retroknowledge_binary_n (n)] -> [ Retroknowledge.KN n ]*) -| [ retroknowledge_int31 (i) "in" string(g)] -> [ Retroknowledge.KInt31(g,i) ] -END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e477b12cd3..fa70235975 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -72,11 +72,6 @@ val test_lpar_id_colon : unit Pcoq.Entry.t val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type -(** Spiwack: Primitive for retroknowledge registration *) - -val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t -val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type - val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index dc027c4041..ba3fa6fa0d 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -26,6 +26,7 @@ open Termops open Equality open Namegen open Tactypes +open Tactics open Proofview.Notations open Vernacinterp @@ -545,22 +546,6 @@ END (**********************************************************************) -(*spiwack : Vernac commands for retroknowledge *) - -VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF - | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> - [ let env = Global.env () in - let evd = Evd.from_env env in - let tc,_ctx = Constrintern.interp_constr env evd c in - let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in - let tc = EConstr.to_constr evd tc in - let tb = EConstr.to_constr evd tb in - Global.register f tc tb ] -END - - - -(**********************************************************************) (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs @@ -796,9 +781,9 @@ END (**********************************************************************) TACTIC EXTEND transparent_abstract -| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl -> +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] -| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl -> +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index c13bd69daf..929390b1c4 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -314,22 +314,23 @@ GEXTEND Gram range_selector_or_nth: [ [ n = natural ; "-" ; m = natural; l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - SelectList ((n, m) :: Option.default [] l) + Goal_select.SelectList ((n, m) :: Option.default [] l) | n = natural; l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> + let open Goal_select in Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] ; selector_body: [ [ l = range_selector_or_nth -> l - | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ] + | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ] ; selector: [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] ; toplevel_selector: [ [ sel = selector_body; ":" -> sel - | "!"; ":" -> SelectAlreadyFocused - | IDENT "all"; ":" -> SelectAll ] ] + | "!"; ":" -> Goal_select.SelectAlreadyFocused + | IDENT "all"; ":" -> Goal_select.SelectAll ] ] ; tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g @@ -346,7 +347,7 @@ GEXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - Vernacexpr.HintsExtern (n,c, in_tac tac) ] ] + Hints.HintsExtern (n,c, in_tac tac) ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> @@ -373,6 +374,7 @@ let _ = declare_int_option { } let vernac_solve n info tcom b = + let open Goal_select in let status = Proof_global.with_current_proof (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in @@ -432,7 +434,7 @@ VERNAC tactic_mode EXTEND VernacSolve VtLater ] -> [ let t = rm_abstract t in - vernac_solve SelectAll n t def + vernac_solve Goal_select.SelectAll n t def ] END diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 2e1ce814aa..571595be70 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -21,6 +21,8 @@ open Constrexpr open Libnames open Tok open Tactypes +open Tactics +open Inv open Locus open Decl_kinds diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune new file mode 100644 index 0000000000..5611f5ba16 --- /dev/null +++ b/plugins/ltac/plugin_base.dune @@ -0,0 +1,13 @@ +(library + (name ltac_plugin) + (public_name coq.plugins.ltac) + (synopsis "Coq's LTAC tactic language") + (modules :standard \ tauto) + (libraries coq.stm)) + +(library + (name tauto_plugin) + (public_name coq.plugins.tauto) + (synopsis "Coq's tauto tactic") + (modules tauto) + (libraries coq.plugins.ltac)) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4357689ee2..b219ee25ca 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -28,6 +28,7 @@ open Printer open Tacexpr open Tacarg +open Tactics module Tag = struct @@ -271,6 +272,8 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence pr prods with Not_found -> + (* FIXME: This key, moreover printed with a low-level printer, + has no meaning user-side *) KerName.print key let pr_alias_gen pr_gen lev key l = @@ -507,7 +510,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_destruction_arg prc prlc (clear_flag,h) = pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h - let pr_inversion_kind = function + let pr_inversion_kind = let open Inv in function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" @@ -516,7 +519,7 @@ let string_of_genarg_arg (ArgumentType arg) = if Int.equal i j then int i else int i ++ str "-" ++ int j -let pr_goal_selector toplevel = function +let pr_goal_selector toplevel = let open Goal_select in function | SelectAlreadyFocused -> str "!:" | SelectNth i -> int i ++ str ":" | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9f8cd2fc4e..5b8bd6d01a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -520,11 +520,6 @@ let rewrite_db = "rewrite" let conv_transparent_state = (Id.Pred.empty, Cpred.full) -let _ = - Hints.add_hints_init - (fun () -> - Hints.create_hint_db false rewrite_db conv_transparent_state true) - let rewrite_transparent_state () = Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 0bb9ccb1d8..1f2c722b34 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -144,7 +144,7 @@ let add ~deprecation kn b t = mactab := KNmap.add kn entry !mactab let replace kn path t = - let (path, _, _) = KerName.repr path in + let path = KerName.modpath path in let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 7143f51853..d5d36c97fa 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -41,7 +41,7 @@ val register_alias : alias -> alias_tactic -> unit (** Register a tactic alias. *) val interp_alias : alias -> alias_tactic -(** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +(** Recover the body of an alias. Raises an anomaly if it does not exist. *) val check_alias : alias -> bool (** Returns [true] if an alias is defined, false otherwise. *) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 59b748e25e..11d13d3a2f 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -37,16 +37,24 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use type goal_selector = Goal_select.t = | SelectAlreadyFocused + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectNth of int + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectList of (int * int) list + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectId of Id.t + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectAll -[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] + [@ocaml.deprecated "Use constructors in [Goal_select]"] +[@@ocaml.deprecated "Use [Goal_select.t]"] type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a + [@ocaml.deprecated "Use constructors in [Tactics]"] | ElimOnIdent of lident + [@ocaml.deprecated "Use constructors in [Tactics]"] | ElimOnAnonHyp of int + [@ocaml.deprecated "Use constructors in [Tactics]"] [@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = @@ -55,8 +63,11 @@ type 'a destruction_arg = type inversion_kind = Inv.inversion_kind = | SimpleInversion + [@ocaml.deprecated "Use constructors in [Inv]"] | FullInversion + [@ocaml.deprecated "Use constructors in [Inv]"] | FullInversionClear + [@ocaml.deprecated "Use constructors in [Inv]"] [@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 3a0badb28f..6b131edaac 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -37,16 +37,24 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use type goal_selector = Goal_select.t = | SelectAlreadyFocused + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectNth of int + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectList of (int * int) list + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectId of Id.t + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectAll + [@ocaml.deprecated "Use constructors in [Goal_select]"] [@@ocaml.deprecated "Use Vernacexpr.goal_selector"] type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a + [@ocaml.deprecated "Use constructors in [Tactics]"] | ElimOnIdent of lident + [@ocaml.deprecated "Use constructors in [Tactics]"] | ElimOnAnonHyp of int + [@ocaml.deprecated "Use constructors in [Tactics]"] [@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = @@ -55,8 +63,11 @@ type 'a destruction_arg = type inversion_kind = Inv.inversion_kind = | SimpleInversion + [@ocaml.deprecated "Use constructors in [Inv]"] | FullInversion + [@ocaml.deprecated "Use constructors in [Inv]"] | FullInversionClear + [@ocaml.deprecated "Use constructors in [Inv]"] [@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 1444800624..5501cf92a5 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -29,6 +29,7 @@ open Stdarg open Tacarg open Namegen open Tactypes +open Tactics open Locus (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a0446bd6a0..9f34df4608 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -37,6 +37,7 @@ open Tacarg open Printer open Pretyping open Tactypes +open Tactics open Locus open Tacintern open Taccoerce @@ -1297,7 +1298,7 @@ and tactic_of_value ist vle = match appl with UnnamedAppl -> "An unnamed user-defined tactic" | GlbAppl apps -> - let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in match nms with [] -> assert false | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) @@ -1468,7 +1469,7 @@ and interp_genarg ist x : Val.t Ftactic.t = independently of goals. *) and interp_genarg_constr_list ist x = - Ftactic.nf_enter begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in @@ -1600,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1615,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1664,16 +1665,18 @@ and interp_atomic ist tac : unit Proofview.tactic = (* We try to fully-typecheck the term *) let flags = open_constr_use_classes_flags () in let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in - let let_tac b na c cl eqpat = - let id = Option.default (make IntroAnonymous) eqpat in - let with_eq = if b then None else Some (true,id) in - Tactics.letin_tac with_eq na c None cl - in let na = interp_name ist env sigma na in + let let_tac = + if b then Tactics.pose_tac na c_interp + else + let id = Option.default (make IntroAnonymous) eqpat in + let with_eq = Some (true, id) in + Tactics.letin_tac with_eq na c_interp None Locusops.nowhere + in Tacticals.New.tclWITHHOLES ev (name_atomic ~env (TacLetTac(ev,na,c_interp,clp,b,eqpat)) - (let_tac b na c_interp clp eqpat)) sigma + let_tac) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = @@ -1693,7 +1696,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l = @@ -1720,7 +1723,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Conversion *) | TacReduce (r,cl) -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) @@ -2029,7 +2032,7 @@ let _ = let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in (EConstr.of_constr c, sigma) in - Pretyping.register_constr_interp0 wit_tactic eval + GlobEnv.register_constr_interp0 wit_tactic eval let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index dd799dc131..4626378db6 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -15,6 +15,7 @@ open Genarg open Stdarg open Tacarg open Tactypes +open Tactics open Globnames open Genredexpr open Patternops diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 105b5c59ae..6bab8d0353 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,7 +12,6 @@ open Util open Names open Pp open Tacexpr -open Termops let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -51,14 +50,14 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) let db_pr_goal gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let penv = print_named_context env in - let pc = print_constr_env env (Tacmach.New.project gl) concl in + let penv = Termops.Internal.print_named_context env in + let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) end @@ -243,7 +242,7 @@ let db_constr debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the pattern rule *) @@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido = is_debug debug >>= fun db -> if db then msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env sigma c) + str " has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the matched conclusion *) @@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints a success message when the goal has been matched *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f22147f8b0..e0a369ca5f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1456,7 +1456,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1709,7 +1709,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec dumpexpr prover tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -1787,7 +1787,7 @@ let micromega_order_changer cert env ff = let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -1817,7 +1817,7 @@ let micromega_genr prover tac = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/plugin_base.dune new file mode 100644 index 0000000000..0ae0e6855d --- /dev/null +++ b/plugins/micromega/plugin_base.dune @@ -0,0 +1,7 @@ +(library + (name micromega_plugin) + (public_name coq.plugins.micromega) + ; be careful not to link the executable to the plugin! + (modules (:standard \ csdpcert)) + (synopsis "Coq's micromega plugin") + (libraries num coq.plugins.ltac)) diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/plugin_base.dune new file mode 100644 index 0000000000..9da5b39972 --- /dev/null +++ b/plugins/nsatz/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name nsatz_plugin) + (public_name coq.plugins.nsatz) + (synopsis "Coq's nsatz solver plugin") + (libraries num coq.plugins.ltac)) diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 59fd9b8017..094adfda7a 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -85,6 +85,7 @@ Ltac zify_binop t thm a b:= Ltac zify_op_1 := match goal with + | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b @@ -114,6 +115,7 @@ Ltac hide_Z_of_nat t := Ltac zify_nat_rel := match goal with (* I: equalities *) + | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) @@ -223,6 +225,7 @@ Ltac hide_Zpos t := Ltac zify_positive_rel := match goal with (* I: equalities *) + | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq positive ?a ?b) => apply Pos2Z.inj | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) @@ -348,6 +351,7 @@ Ltac hide_Z_of_N t := Ltac zify_N_rel := match goal with (* I: equalities *) + | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index e14c4e2ec1..abae6940fa 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -588,7 +588,7 @@ let abstract_path sigma typ path t = let focused_simpl path = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + 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_no_check newc DEFAULTcast end @@ -656,7 +656,7 @@ let new_hole env sigma c = let clever_rewrite_base_poly typ p result theorem = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + 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 @@ -708,7 +708,7 @@ let refine_app gl t = let clever_rewrite p vpath t = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + 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 @@ -1763,7 +1763,7 @@ let onClearedName id tac = (* so renaming may be necessary *) tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let id = fresh_id Id.Set.empty id gl in tclTHEN (introduction id) (tac id) end) @@ -1771,7 +1771,7 @@ let onClearedName id tac = let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter begin fun gl -> + (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.empty (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] @@ -1956,7 +1956,7 @@ let destructure_goal = try let dec = decidability t in tclTHEN - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) end) intro diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/plugin_base.dune new file mode 100644 index 0000000000..f512501c78 --- /dev/null +++ b/plugins/omega/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name omega_plugin) + (public_name coq.plugins.omega) + (synopsis "Coq's omega plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v deleted file mode 100644 index 2d3d9170c1..0000000000 --- a/plugins/quote/Quote.v +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -Declare ML Module "quote_plugin". - -(*********************************************************************** - The "abstract" type index is defined to represent variables. - - index : Set - index_eq : index -> bool - index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m - index_lt : index -> bool - varmap : Type -> Type. - varmap_find : (A:Type)A -> index -> (varmap A) -> A. - - The first arg. of varmap_find is the default value to take - if the object is not found in the varmap. - - index_lt defines a total well-founded order, but we don't prove that. - -***********************************************************************) - -Set Implicit Arguments. - -Section variables_map. - -Variable A : Type. - -Inductive varmap : Type := - | Empty_vm : varmap - | Node_vm : A -> varmap -> varmap -> varmap. - -Inductive index : Set := - | Left_idx : index -> index - | Right_idx : index -> index - | End_idx : index. - -Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A := - match i, v with - | End_idx, Node_vm x _ _ => x - | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2 - | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1 - | _, _ => default_value - end. - -Fixpoint index_eq (n m:index) {struct m} : bool := - match n, m with - | End_idx, End_idx => true - | Left_idx n', Left_idx m' => index_eq n' m' - | Right_idx n', Right_idx m' => index_eq n' m' - | _, _ => false - end. - -Fixpoint index_lt (n m:index) {struct m} : bool := - match n, m with - | End_idx, Left_idx _ => true - | End_idx, Right_idx _ => true - | Left_idx n', Right_idx m' => true - | Right_idx n', Right_idx m' => index_lt n' m' - | Left_idx n', Left_idx m' => index_lt n' m' - | _, _ => false - end. - -Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. - simple induction n; simple induction m; simpl; intros. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - reflexivity. -Qed. - -End variables_map. - -Unset Implicit Arguments. diff --git a/plugins/quote/g_quote.mlg b/plugins/quote/g_quote.mlg deleted file mode 100644 index 749903c3ad..0000000000 --- a/plugins/quote/g_quote.mlg +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -{ - -open Ltac_plugin -open Names -open Tacexpr -open Geninterp -open Quote -open Stdarg -open Tacarg - -} - -DECLARE PLUGIN "quote_plugin" - -{ - -let cont = Id.of_string "cont" -let x = Id.of_string "x" - -let make_cont (k : Val.t) (c : EConstr.t) = - let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in - let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in - Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) - -} - -TACTIC EXTEND quote -| [ "quote" ident(f) ] -> { quote f [] } -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } -| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - { gen_quote (make_cont k) c f [] } -| [ "quote" ident(f) "[" ne_ident_list(lc) "]" - "in" constr(c) "using" tactic(k) ] -> - { gen_quote (make_cont k) c f lc } -END diff --git a/plugins/quote/plugin_base.dune b/plugins/quote/plugin_base.dune new file mode 100644 index 0000000000..323906acb2 --- /dev/null +++ b/plugins/quote/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name quote_plugin) + (public_name coq.plugins.quote) + (synopsis "Coq's quote plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml deleted file mode 100644 index 7464b42dc5..0000000000 --- a/plugins/quote/quote.ml +++ /dev/null @@ -1,540 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -(* The `Quote' tactic *) - -(* The basic idea is to automatize the inversion of interpretation functions - in 2-level approach - - Examples are given in \texttt{theories/DEMOS/DemoQuote.v} - - Suppose you have a langage \texttt{L} of 'abstract terms' - and a type \texttt{A} of 'concrete terms' - and a function \texttt{f : L -> (varmap A L) -> A}. - - Then, the tactic \texttt{quote f} will replace an - expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)} - such that \texttt{e} and \texttt{(f vm t)} are convertible. - - The problem is then inverting the function \texttt{f}. - - The tactic works when: - - \begin{itemize} - \item L is a simple inductive datatype. The constructors of L may - have one of the three following forms: - - \begin{enumerate} - \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L| - \item variable leaf like: \verb|Cvar : index -> L| - \item constant leaf like \verb|Cconst : A -> L| - \end{enumerate} - - The definition of \texttt{L} must contain at most one variable - leaf and at most one constant leaf. - - When there are both a variable leaf and a constant leaf, there is - an ambiguity on inversion. The term t can be either the - interpretation of \texttt{(Cconst t)} or the interpretation of - (\texttt{Cvar}~$i$) in a variable map containing the binding $i - \rightarrow$~\texttt{t}. How to discriminate between these - choices? - - To solve the dilemma, one gives to \texttt{quote} a list of - \emph{constant constructors}: a term will be considered as a - constant if it is either a constant constructor or the - application of a constant constructor to constants. For example - the list \verb+[S, O]+ defines the closed natural - numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is - not. - - The definition of constants vary for each application of the - tactic, so it can even be different for two applications of - \texttt{quote} with the same function. - - \item \texttt{f} is a quite simple fixpoint on - \texttt{L}. In particular, \texttt{f} must verify: - -\begin{verbatim} - (f (Cvar i)) = (varmap_find vm default_value i) -\end{verbatim} -\begin{verbatim} - (f (Cconst c)) = c -\end{verbatim} - - where \texttt{index} and \texttt{varmap\_find} are those defined - the \texttt{Quote} module. \emph{The tactic won't work with - user's own variables map!!} It is mandatory to use the - variable map defined in module \texttt{Quote}. - - \end{itemize} - - The method to proceed is then clear: - - \begin{itemize} - \item Start with an empty hashtable of "registed leafs" - that maps constr to integers and a "variable counter" equal to 0. - \item Try to match the term with every right hand side of the - definition of \texttt{f}. - - If there is one match, returns the correponding left hand - side and call yourself recursively to get the arguments of this - left hand side. - - If there is no match, we are at a leaf. That is the - interpretation of either a variable or a constant. - - If it is a constant, return \texttt{Cconst} applied to that - constant. - - If not, it is a variable. Look in the hashtable - if this leaf has been already encountered. If not, increment - the variable counter and add an entry to the hashtable; then - return \texttt{(Cvar !variables\_counter)} - \end{itemize} -*) - - -(*i*) -open CErrors -open Util -open Names -open Constr -open EConstr -open Pattern -open Patternops -open Constr_matching -open Tacmach -open Proofview.Notations -(*i*) - -(*s First, we need to access some Coq constants - We do that lazily, because this code can be linked before - the constants are loaded in the environment *) - -let constant dir s = - EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Quote" ("quote"::dir) s - -let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") -let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") -let coq_varmap_find = lazy (constant ["Quote"] "varmap_find") -let coq_Right_idx = lazy (constant ["Quote"] "Right_idx") -let coq_Left_idx = lazy (constant ["Quote"] "Left_idx") -let coq_End_idx = lazy (constant ["Quote"] "End_idx") - -(*s Then comes the stuff to decompose the body of interpetation function - and pre-compute the inversion data. - -For a function like: - -\begin{verbatim} - Fixpoint interp (vm:varmap Prop) (f:form) := - match f with - | f_and f1 f1 f2 => (interp f1) /\ (interp f2) - | f_or f1 f1 f2 => (interp f1) \/ (interp f2) - | f_var i => varmap_find Prop default_v i vm - | f_const c => c - end. -\end{verbatim} - -With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the -corresponding scheme will be: - -\begin{verbatim} - {normal_lhs_rhs = - [ "(f_and ?1 ?2)", "?1 /\ ?2"; - "(f_or ?1 ?2)", " ?1 \/ ?2";]; - return_type = "Prop"; - constants = Some [C1,...Cn]; - variable_lhs = Some "(f_var ?1)"; - constant_lhs = Some "(f_const ?1)" - } -\end{verbatim} - -If there is no constructor for variables in the type \texttt{form}, -then [variable_lhs] is [None]. Idem for constants and -[constant_lhs]. Both cannot be equal to [None]. - -The metas in the RHS must correspond to those in the LHS (one cannot -exchange ?1 and ?2 in the example above) - -*) - -module ConstrSet = Set.Make(Constr) - -type inversion_scheme = { - normal_lhs_rhs : (constr * constr_pattern) list; - variable_lhs : constr option; - return_type : constr; - constants : ConstrSet.t; - constant_lhs : constr option } - -(*s [compute_ivs gl f cs] computes the inversion scheme associated to - [f:constr] with constants list [cs:constr list] in the context of - goal [gl]. This function uses the auxiliary functions - [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) - -let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") - -let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) - -(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... - ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive - type [typ] *) - -let coerce_meta_out id = - let s = Id.to_string id in - int_of_string (String.sub s 1 (String.length s - 1)) -let coerce_meta_in n = - Id.of_string ("M" ^ string_of_int n) - -let compute_lhs sigma typ i nargsi = - match EConstr.kind sigma typ with - | Ind((sp,0),u) -> - let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkConstructU (((sp,0),i+1),u), argsi) - | _ -> i_can't_do_that () - -(*s This function builds the pattern from the RHS. Recursive calls are - replaced by meta-variables ?i corresponding to those in the LHS *) - -let compute_rhs env sigma bodyi index_of_f = - let rec aux c = - match EConstr.kind sigma c with - | App (j, args) when isRel sigma j && Int.equal (destRel sigma j) index_of_f (* recursive call *) -> - let i = destRel sigma (Array.last args) in - PMeta (Some (coerce_meta_in i)) - | App (f,args) -> - PApp (pattern_of_constr env sigma (EConstr.to_constr sigma f), Array.map aux args) - | Cast (c,_,_) -> aux c - | _ -> pattern_of_constr env sigma (EConstr.to_constr sigma c) - in - aux bodyi - -(*s Now the function [compute_ivs] itself *) - -let compute_ivs f cs gl = - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in - let u = EInstance.kind sigma u in - let body = Environ.constant_value_in (Global.env()) (cst, u) in - let body = EConstr.of_constr body in - match decomp_term sigma body with - | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> - let (args3, body3) = decompose_lam sigma body2 in - let nargs3 = List.length args3 in - let is_conv = Reductionops.is_conv env sigma in - begin match decomp_term sigma body3 with - | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) - let n_lhs_rhs = ref [] - and v_lhs = ref (None : constr option) - and c_lhs = ref (None : constr option) in - Array.iteri - (fun i ci -> - let argsi, bodyi = decompose_lam sigma ci in - let nargsi = List.length argsi in - (* REL (narg3 + nargsi + 1) is f *) - (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *) - (* REL 1 to REL nargsi are argsi (reverse order) *) - (* First we test if the RHS is the RHS for constants *) - if isRel sigma bodyi && Int.equal (destRel sigma bodyi) 1 then - c_lhs := Some (compute_lhs sigma (snd (List.hd args3)) - i nargsi) - (* Then we test if the RHS is the RHS for variables *) - else begin match decompose_app sigma bodyi with - | vmf, [_; _; a3; a4 ] - when isRel sigma a3 && isRel sigma a4 && is_conv vmf - (Lazy.force coq_varmap_find) -> - v_lhs := Some (compute_lhs sigma - (snd (List.hd args3)) - i nargsi) - (* Third case: this is a normal LHS-RHS *) - | _ -> - n_lhs_rhs := - (compute_lhs sigma (snd (List.hd args3)) i nargsi, - compute_rhs env sigma bodyi (nargs3 + nargsi + 1)) - :: !n_lhs_rhs - end) - lci; - - if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that (); - - (* The Cases predicate is a lambda; we assume no dependency *) - let p = match EConstr.kind sigma p with - | Lambda (_,_,p) -> Termops.pop p - | _ -> p - in - - { normal_lhs_rhs = List.rev !n_lhs_rhs; - variable_lhs = !v_lhs; - return_type = p; - constants = List.fold_right ConstrSet.add cs ConstrSet.empty; - constant_lhs = !c_lhs } - - | _ -> i_can't_do_that () - end - |_ -> i_can't_do_that () - -(* TODO for that function: -\begin{itemize} -\item handle the case where the return type is an argument of the - function -\item handle the case of simple mutual inductive (for example terms - and lists of terms) formulas with the corresponding mutual - recursvive interpretation functions. -\end{itemize} -*) - -(*s Stuff to build variables map, currently implemented as complete -binary search trees (see file \texttt{Quote.v}) *) - -(* First the function to distinghish between constants (closed terms) - and variables (open terms) *) - -let rec closed_under sigma cset t = - (ConstrSet.mem (EConstr.Unsafe.to_constr t) cset) || - (match EConstr.kind sigma t with - | Cast(c,_,_) -> closed_under sigma cset c - | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l - | _ -> false) - -(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete - binary search tree containing the [ci], that is: - -\begin{verbatim} - c1 - / \ - c2 c3 - / \ - c4 c5 -\end{verbatim} - -The second argument is a constr (the common type of the [ci]) -*) - -let btree_of_array a ty = - let size_of_a = Array.length a in - let semi_size_of_a = size_of_a lsr 1 in - let node = Lazy.force coq_Node_vm - and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in - let rec aux n = - if n > size_of_a - then empty - else if n > semi_size_of_a - then mkApp (node, [| ty; a.(n-1); empty; empty |]) - else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |]) - in - aux 1 - -(*s [btree_of_array] and [path_of_int] verify the following invariant:\\ - {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)] - = [a.(n)]\\ - [n] must be [> 0] *) - -let path_of_int n = - (* returns the list of digits of n in reverse order with - initial 1 removed *) - let rec digits_of_int n = - if Int.equal n 1 then [] - else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) - in - List.fold_right - (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx - else Lazy.force coq_Left_idx), - [| c |])) - (List.rev (digits_of_int n)) - (Lazy.force coq_End_idx) - -(*s The tactic works with a list of subterms sharing the same - variables map. We need to sort terms in order to avoid than - strange things happen during replacement of terms by their - 'abstract' counterparties. *) - -(* [subterm t t'] tests if constr [t'] occurs in [t] *) -(* This function does not descend under binders (lambda and Cases) *) - -let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') || - (match EConstr.kind (project gl) t with - | App (f,args) -> Array.exists (fun t -> subterm gl t t') args - | Cast(t,_,_) -> (subterm gl t t') - | _ -> false) - -(*s We want to sort the list according to reverse subterm order. *) -(* Since it's a partial order the algoritm of Sort.list won't work !! *) - -let rec sort_subterm gl l = - let sigma = project gl in - let rec insert c = function - | [] -> [c] - | (h::t as l) when EConstr.eq_constr sigma c h -> l (* Avoid doing the same work twice *) - | h::t -> if subterm gl c h then c::h::t else h::(insert c t) - in - match l with - | [] -> [] - | h::t -> insert h (sort_subterm gl t) - -module Constrhash = Hashtbl.Make(Constr) - -let subst_meta subst c = - let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in - EConstr.of_constr (Termops.subst_meta subst (EConstr.Unsafe.to_constr c)) - -(*s Now we are able to do the inversion itself. - We destructurate the term and use an imperative hashtable - to store leafs that are already encountered. - The type of arguments is:\\ - [ivs : inversion_scheme]\\ - [lc: constr list]\\ - [gl: goal sigma]\\ *) -let quote_terms env sigma ivs lc = - Coqlib.check_required_library ["Coq";"quote";"Quote"]; - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - let rec auxl l = - match l with - | (lhs, rhs)::tail -> - begin try - let s1 = Id.Map.bindings (matches env sigma rhs c) in - let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 - in - subst_meta s2 lhs - with PatternMatchingFailure -> auxl tail - end - | [] -> - begin match ivs.variable_lhs with - | None -> - begin match ivs.constant_lhs with - | Some c_lhs -> subst_meta [1, c] c_lhs - | None -> anomaly (Pp.str "invalid inversion scheme for quote.") - end - | Some var_lhs -> - begin match ivs.constant_lhs with - | Some c_lhs when closed_under sigma ivs.constants c -> - subst_meta [1, c] c_lhs - | _ -> - begin - try Constrhash.find varhash (EConstr.Unsafe.to_constr c) - with Not_found -> - let newvar = - subst_meta [1, (path_of_int !counter)] - var_lhs in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash (EConstr.Unsafe.to_constr c) newvar; - newvar - end - end - end - end - in - auxl ivs.normal_lhs_rhs - in - let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) - ivs.return_type )) - -(*s actually we could "quote" a list of terms instead of a single - term. Ring for example needs that, but Ring doesn't use Quote - yet. *) - -let pf_constrs_of_globals l = - let rec aux l acc = - match l with - [] -> Proofview.tclUNIT (List.rev acc) - | hd :: tl -> - Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc) - in aux l [] - -let quote f lid = - Proofview.Goal.enter begin fun gl -> - let fg = Tacmach.New.pf_global f gl in - let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Tacticals.New.pf_constr_of_global fg >>= fun f -> - pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in - let concl = Proofview.Goal.concl gl in - let quoted_terms = quote_terms env sigma ivs [concl] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast - end - end - -let gen_quote cont c f lid = - Proofview.Goal.enter begin fun gl -> - let fg = Tacmach.New.pf_global f gl in - let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Tacticals.New.pf_constr_of_global fg >>= fun f -> - pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let cl = List.map (EConstr.to_constr sigma) cl in - let ivs = compute_ivs f cl gl in - let quoted_terms = quote_terms env sigma ivs [c] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) - | Some _ -> cont (mkApp (f, [| vm; p |])) - end - end - -(*i - -Just testing ... - -#use "include.ml";; -open Quote;; - -let r = glob_constr_of_string;; - -let ivs = { - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") -};; - -let t1 = r "True/\(True /\ ~False)";; -let t2 = r "True/\~~False";; - -quote_term ivs () t1;; -quote_term ivs () t2;; - -let ivs2 = - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1" - r "True", r "f_true"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") - -i*) diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack deleted file mode 100644 index 2e9be09d8d..0000000000 --- a/plugins/quote/quote_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Quote -G_quote diff --git a/plugins/romega/README b/plugins/romega/README deleted file mode 100644 index 86c9e58afd..0000000000 --- a/plugins/romega/README +++ /dev/null @@ -1,6 +0,0 @@ -This work was done for the RNRT Project Calife. -As such it is distributed under the LGPL licence. - -Report bugs to : - pierre.cregut@francetelecom.com - diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v deleted file mode 100644 index 657aae90e8..0000000000 --- a/plugins/romega/ROmega.v +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - -Require Import ReflOmegaCore. -Require Export Setoid. -Require Export PreOmega. -Require Export ZArith_base. -Require Import OmegaPlugin. -Declare ML Module "romega_plugin". diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v deleted file mode 100644 index 51b99b9935..0000000000 --- a/plugins/romega/ReflOmegaCore.v +++ /dev/null @@ -1,1872 +0,0 @@ -(* -*- coding: utf-8 -*- *) -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence du projet : LGPL version 2.1 - - *************************************************************************) - -Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. -Delimit Scope Int_scope with I. - -(** * Abstract Integers. *) - -Module Type Int. - - Parameter t : Set. - - Bind Scope Int_scope with t. - - Parameter Inline zero : t. - Parameter Inline one : t. - Parameter Inline plus : t -> t -> t. - Parameter Inline opp : t -> t. - Parameter Inline minus : t -> t -> t. - Parameter Inline mult : t -> t -> t. - - Notation "0" := zero : Int_scope. - Notation "1" := one : Int_scope. - Infix "+" := plus : Int_scope. - Infix "-" := minus : Int_scope. - Infix "*" := mult : Int_scope. - Notation "- x" := (opp x) : Int_scope. - - Open Scope Int_scope. - - (** First, Int is a ring: *) - Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t). - - (** Int should also be ordered: *) - - Parameter Inline le : t -> t -> Prop. - Parameter Inline lt : t -> t -> Prop. - Parameter Inline ge : t -> t -> Prop. - Parameter Inline gt : t -> t -> Prop. - Notation "x <= y" := (le x y): Int_scope. - Notation "x < y" := (lt x y) : Int_scope. - Notation "x >= y" := (ge x y) : Int_scope. - Notation "x > y" := (gt x y): Int_scope. - Axiom le_lt_iff : forall i j, (i<=j) <-> ~(j<i). - Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i). - Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i). - - (** Basic properties of this order *) - Axiom lt_trans : forall i j k, i<j -> j<k -> i<k. - Axiom lt_not_eq : forall i j, i<j -> i<>j. - - (** Compatibilities *) - Axiom lt_0_1 : 0<1. - Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l. - Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i). - Axiom mult_lt_compat_l : - forall i j k, 0 < k -> i < j -> k*i<k*j. - - (** We should have a way to decide the equality and the order*) - Parameter compare : t -> t -> comparison. - Infix "?=" := compare (at level 70, no associativity) : Int_scope. - Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j. - Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j. - Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j. - - (** Up to here, these requirements could be fulfilled - by any totally ordered ring. Let's now be int-specific: *) - Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1). - - (** Btw, lt_0_1 could be deduced from this last axiom *) - - (** Now we also require a division function. - It is deliberately underspecified, since that's enough - for the proofs below. But the most appropriate variant - (and the one needed to stay in sync with the omega engine) - is "Floor" (the historical version of Coq's [Z.div]). *) - - Parameter diveucl : t -> t -> t * t. - Notation "i / j" := (fst (diveucl i j)). - Notation "i 'mod' j" := (snd (diveucl i j)). - Axiom diveucl_spec : - forall i j, j<>0 -> i = j * (i/j) + (i mod j). - -End Int. - - - -(** Of course, Z is a model for our abstract int *) - -Module Z_as_Int <: Int. - - Open Scope Z_scope. - - Definition t := Z. - Definition zero := 0. - Definition one := 1. - Definition plus := Z.add. - Definition opp := Z.opp. - Definition minus := Z.sub. - Definition mult := Z.mul. - - Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t). - Proof. - constructor. - exact Z.add_0_l. - exact Z.add_comm. - exact Z.add_assoc. - exact Z.mul_1_l. - exact Z.mul_comm. - exact Z.mul_assoc. - exact Z.mul_add_distr_r. - unfold minus, Z.sub; auto. - exact Z.add_opp_diag_r. - Qed. - - Definition le := Z.le. - Definition lt := Z.lt. - Definition ge := Z.ge. - Definition gt := Z.gt. - Definition le_lt_iff := Z.le_ngt. - Definition ge_le_iff := Z.ge_le_iff. - Definition gt_lt_iff := Z.gt_lt_iff. - - Definition lt_trans := Z.lt_trans. - Definition lt_not_eq := Z.lt_neq. - - Definition lt_0_1 := Z.lt_0_1. - Definition plus_le_compat := Z.add_le_mono. - Definition mult_lt_compat_l := Zmult_lt_compat_l. - Lemma opp_le_compat i j : i<=j -> (-j)<=(-i). - Proof. apply -> Z.opp_le_mono. Qed. - - Definition compare := Z.compare. - Definition compare_Eq := Z.compare_eq_iff. - Lemma compare_Lt i j : compare i j = Lt <-> i<j. - Proof. reflexivity. Qed. - Lemma compare_Gt i j : compare i j = Gt <-> i>j. - Proof. reflexivity. Qed. - - Definition le_lt_int := Z.lt_le_pred. - - Definition diveucl := Z.div_eucl. - Definition diveucl_spec := Z.div_mod. - -End Z_as_Int. - - -(** * Properties of abstract integers *) - -Module IntProperties (I:Int). - Import I. - Local Notation int := I.t. - - (** Primo, some consequences of being a ring theory... *) - - Definition two := 1+1. - Notation "2" := two : Int_scope. - - (** Aliases for properties packed in the ring record. *) - - Definition plus_assoc := ring.(Radd_assoc). - Definition plus_comm := ring.(Radd_comm). - Definition plus_0_l := ring.(Radd_0_l). - Definition mult_assoc := ring.(Rmul_assoc). - Definition mult_comm := ring.(Rmul_comm). - Definition mult_1_l := ring.(Rmul_1_l). - Definition mult_plus_distr_r := ring.(Rdistr_l). - Definition opp_def := ring.(Ropp_def). - Definition minus_def := ring.(Rsub_def). - - Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l - mult_plus_distr_r opp_def minus_def. - - (** More facts about [plus] *) - - Lemma plus_0_r : forall x, x+0 = x. - Proof. intros; rewrite plus_comm; apply plus_0_l. Qed. - - Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z). - Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed. - - Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z. - Proof. - intros. - rewrite <- (plus_0_r y), <- (plus_0_r z), <-(opp_def x). - now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute. - Qed. - - (** More facts about [mult] *) - - Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z. - Proof. - intros. - rewrite (mult_comm x (y+z)), (mult_comm x y), (mult_comm x z). - apply mult_plus_distr_r. - Qed. - - Lemma mult_0_l x : 0*x = 0. - Proof. - assert (H := mult_plus_distr_r 0 1 x). - rewrite plus_0_l, mult_1_l, plus_comm in H. - apply plus_reg_l with x. - now rewrite <- H, plus_0_r. - Qed. - - Lemma mult_0_r x : x*0 = 0. - Proof. - rewrite mult_comm. apply mult_0_l. - Qed. - - Lemma mult_1_r x : x*1 = x. - Proof. - rewrite mult_comm. apply mult_1_l. - Qed. - - (** More facts about [opp] *) - - Definition plus_opp_r := opp_def. - - Lemma plus_opp_l : forall x, -x + x = 0. - Proof. intros; now rewrite plus_comm, opp_def. Qed. - - Lemma mult_opp_comm : forall x y, - x * y = x * - y. - Proof. - intros. - apply plus_reg_l with (x*y). - rewrite <- mult_plus_distr_l, <- mult_plus_distr_r. - now rewrite opp_def, opp_def, mult_0_l, mult_comm, mult_0_l. - Qed. - - Lemma opp_eq_mult_neg_1 : forall x, -x = x * -(1). - Proof. - intros; now rewrite mult_comm, mult_opp_comm, mult_1_l. - Qed. - - Lemma opp_involutive : forall x, -(-x) = x. - Proof. - intros. - apply plus_reg_l with (-x). - now rewrite opp_def, plus_comm, opp_def. - Qed. - - Lemma opp_plus_distr : forall x y, -(x+y) = -x + -y. - Proof. - intros. - apply plus_reg_l with (x+y). - rewrite opp_def. - rewrite plus_permute. - do 2 rewrite plus_assoc. - now rewrite (plus_comm (-x)), opp_def, plus_0_l, opp_def. - Qed. - - Lemma opp_mult_distr_r : forall x y, -(x*y) = x * -y. - Proof. - intros. - rewrite <- mult_opp_comm. - apply plus_reg_l with (x*y). - now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l. - Qed. - - Lemma egal_left n m : 0 = n+-m <-> n = m. - Proof. - split; intros. - - apply plus_reg_l with (-m). - rewrite plus_comm, <- H. symmetry. apply plus_opp_l. - - symmetry. subst; apply opp_def. - Qed. - - (** Specialized distributivities *) - - Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int. - Hint Rewrite <- plus_assoc : int. - - Hint Rewrite plus_0_l plus_0_r mult_0_l mult_0_r mult_1_l mult_1_r : int. - - Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 : - v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2) = - (v * c1 + l1) * k1 + (v * c2 + l2) * k2. - Proof. - autorewrite with int; f_equal; now rewrite plus_permute. - Qed. - - Lemma OMEGA11 v1 c1 l1 l2 k1 : - v1 * (c1 * k1) + (l1 * k1 + l2) = (v1 * c1 + l1) * k1 + l2. - Proof. - now autorewrite with int. - Qed. - - Lemma OMEGA12 v2 c2 l1 l2 k2 : - v2 * (c2 * k2) + (l1 + l2 * k2) = l1 + (v2 * c2 + l2) * k2. - Proof. - autorewrite with int; now rewrite plus_permute. - Qed. - - Lemma sum1 a b c d : 0 = a -> 0 = b -> 0 = a * c + b * d. - Proof. - intros; subst. now autorewrite with int. - Qed. - - - (** Secondo, some results about order (and equality) *) - - Lemma lt_irrefl : forall n, ~ n<n. - Proof. - intros n H. - elim (lt_not_eq _ _ H); auto. - Qed. - - Lemma lt_antisym : forall n m, n<m -> m<n -> False. - Proof. - intros; elim (lt_irrefl _ (lt_trans _ _ _ H H0)); auto. - Qed. - - Lemma lt_le_weak : forall n m, n<m -> n<=m. - Proof. - intros; rewrite le_lt_iff; intro H'; eapply lt_antisym; eauto. - Qed. - - Lemma le_refl : forall n, n<=n. - Proof. - intros; rewrite le_lt_iff; apply lt_irrefl; auto. - Qed. - - Lemma le_antisym : forall n m, n<=m -> m<=n -> n=m. - Proof. - intros n m; do 2 rewrite le_lt_iff; intros. - rewrite <- compare_Lt in H0. - rewrite <- gt_lt_iff, <- compare_Gt in H. - rewrite <- compare_Eq. - destruct compare; intuition. - Qed. - - Lemma lt_eq_lt_dec : forall n m, { n<m }+{ n=m }+{ m<n }. - Proof. - intros. - generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m). - destruct compare; [ left; right | left; left | right ]; intuition. - rewrite gt_lt_iff in H1; intuition. - Qed. - - Lemma lt_dec : forall n m: int, { n<m } + { ~n<m }. - Proof. - intros. - generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m). - destruct compare; [ right | left | right ]; intuition discriminate. - Qed. - - Lemma lt_le_iff : forall n m, (n<m) <-> ~(m<=n). - Proof. - intros. - rewrite le_lt_iff. - destruct (lt_dec n m); intuition. - Qed. - - Lemma le_dec : forall n m: int, { n<=m } + { ~n<=m }. - Proof. - intros; destruct (lt_dec m n); [right|left]; rewrite le_lt_iff; intuition. - Qed. - - Lemma le_lt_dec : forall n m, { n<=m } + { m<n }. - Proof. - intros; destruct (le_dec n m); [left|right]; auto; now rewrite lt_le_iff. - Qed. - - - Definition beq i j := match compare i j with Eq => true | _ => false end. - - Infix "=?" := beq : Int_scope. - - Lemma beq_iff i j : (i =? j) = true <-> i=j. - Proof. - unfold beq. rewrite <- (compare_Eq i j). now destruct compare. - Qed. - - Lemma beq_reflect i j : reflect (i=j) (i =? j). - Proof. - apply iff_reflect. symmetry. apply beq_iff. - Qed. - - Lemma eq_dec : forall n m:int, { n=m } + { n<>m }. - Proof. - intros n m; generalize (beq_iff n m); destruct beq; [left|right]; intuition. - Qed. - - Definition blt i j := match compare i j with Lt => true | _ => false end. - - Infix "<?" := blt : Int_scope. - - Lemma blt_iff i j : (i <? j) = true <-> i<j. - Proof. - unfold blt. rewrite <- (compare_Lt i j). now destruct compare. - Qed. - - Lemma blt_reflect i j : reflect (i<j) (i <? j). - Proof. - apply iff_reflect. symmetry. apply blt_iff. - Qed. - - Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }. - Proof. - intros n m Hnm. - destruct (eq_dec n m) as [H'|H']. - - right; intuition. - - left; rewrite lt_le_iff. - contradict H'. - now apply le_antisym. - Qed. - - Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m. - Proof. - intros n m H. now destruct (le_is_lt_or_eq _ _ H). - Qed. - - Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p. - Proof. - intros n m p; rewrite 3 le_lt_iff; intros A B C. - destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto. - generalize (lt_trans _ _ _ H C); intuition. - Qed. - - Lemma not_eq (a b:int) : ~ a <> b <-> a = b. - Proof. - destruct (eq_dec a b); intuition. - Qed. - - (** Order and operations *) - - Lemma le_0_neg n : n <= 0 <-> 0 <= -n. - Proof. - rewrite <- (mult_0_l (-(1))) at 2. - rewrite <- opp_eq_mult_neg_1. - split; intros. - - now apply opp_le_compat. - - rewrite <-(opp_involutive 0), <-(opp_involutive n). - now apply opp_le_compat. - Qed. - - Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m. - Proof. - intros. - replace n with ((n+p)+-p). - replace m with ((m+p)+-p). - apply plus_le_compat; auto. - apply le_refl. - now rewrite <- plus_assoc, opp_def, plus_0_r. - now rewrite <- plus_assoc, opp_def, plus_0_r. - Qed. - - Lemma plus_le_lt_compat : forall n m p q, n<=m -> p<q -> n+p<m+q. - Proof. - intros. - apply le_neq_lt. - apply plus_le_compat; auto. - apply lt_le_weak; auto. - rewrite lt_le_iff in H0. - contradict H0. - apply plus_le_reg_r with m. - rewrite (plus_comm q m), <-H0, (plus_comm p m). - apply plus_le_compat; auto. - apply le_refl; auto. - Qed. - - Lemma plus_lt_compat : forall n m p q, n<m -> p<q -> n+p<m+q. - Proof. - intros. - apply plus_le_lt_compat; auto. - apply lt_le_weak; auto. - Qed. - - Lemma opp_lt_compat : forall n m, n<m -> -m < -n. - Proof. - intros n m; do 2 rewrite lt_le_iff; intros H; contradict H. - rewrite <-(opp_involutive m), <-(opp_involutive n). - apply opp_le_compat; auto. - Qed. - - Lemma lt_0_neg n : n < 0 <-> 0 < -n. - Proof. - rewrite <- (mult_0_l (-(1))) at 2. - rewrite <- opp_eq_mult_neg_1. - split; intros. - - now apply opp_lt_compat. - - rewrite <-(opp_involutive 0), <-(opp_involutive n). - now apply opp_lt_compat. - Qed. - - Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m. - Proof. - intros. - rewrite <- (mult_0_l n), mult_comm. - apply mult_lt_compat_l; auto. - Qed. - - Lemma mult_integral_r n m : 0 < n -> n * m = 0 -> m = 0. - Proof. - intros Hn H. - destruct (lt_eq_lt_dec 0 m) as [[Hm| <- ]|Hm]; auto; exfalso. - - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite H. - exact (lt_irrefl 0). - - rewrite lt_0_neg in Hm. - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite <- opp_mult_distr_r, opp_eq_mult_neg_1, H, mult_0_l. - exact (lt_irrefl 0). - Qed. - - Lemma mult_integral n m : n * m = 0 -> n = 0 \/ m = 0. - Proof. - intros H. - destruct (lt_eq_lt_dec 0 n) as [[Hn|Hn]|Hn]. - - right; apply (mult_integral_r n m); trivial. - - now left. - - right; apply (mult_integral_r (-n) m). - + now apply lt_0_neg. - + rewrite mult_comm, <- opp_mult_distr_r, mult_comm, H. - now rewrite opp_eq_mult_neg_1, mult_0_l. - Qed. - - Lemma mult_le_compat_l i j k : - 0<=k -> i<=j -> k*i <= k*j. - Proof. - intros Hk Hij. - apply le_is_lt_or_eq in Hk. apply le_is_lt_or_eq in Hij. - destruct Hk as [Hk | <-], Hij as [Hij | <-]; - rewrite ? mult_0_l; try apply le_refl. - now apply lt_le_weak, mult_lt_compat_l. - Qed. - - Lemma mult_le_compat i j k l : - i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l. - Proof. - intros Hij Hkl Hi Hk. - apply le_trans with (i*l). - - now apply mult_le_compat_l. - - rewrite (mult_comm i), (mult_comm j). - apply mult_le_compat_l; trivial. - now apply le_trans with k. - Qed. - - Lemma sum5 a b c d : 0 <> c -> 0 <> a -> 0 = b -> 0 <> a * c + b * d. - Proof. - intros Hc Ha <-. autorewrite with int. contradict Hc. - symmetry in Hc. destruct (mult_integral _ _ Hc); congruence. - Qed. - - Lemma le_left n m : n <= m <-> 0 <= m + - n. - Proof. - split; intros. - - rewrite <- (opp_def m). - apply plus_le_compat. - apply le_refl. - apply opp_le_compat; auto. - - apply plus_le_reg_r with (-n). - now rewrite plus_opp_r. - Qed. - - Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0. - Proof. - intros. - assert (y=-x). - subst x; symmetry; apply opp_involutive. - clear H1; subst y. - destruct (eq_dec 0 x) as [H'|H']; auto. - assert (H'':=le_neq_lt _ _ H H'). - generalize (plus_le_lt_compat _ _ _ _ H0 H''). - rewrite plus_opp_l, plus_0_l. - intros. - elim (lt_not_eq _ _ H1); auto. - Qed. - - Lemma sum2 a b c d : - 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d. - Proof. - intros Hd <- Hb. autorewrite with int. - rewrite <- (mult_0_l 0). - apply mult_le_compat; auto; apply le_refl. - Qed. - - Lemma sum3 a b c d : - 0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d. - Proof. - intros. - rewrite <- (plus_0_l 0). - apply plus_le_compat; auto. - rewrite <- (mult_0_l 0). - apply mult_le_compat; auto; apply le_refl. - rewrite <- (mult_0_l 0). - apply mult_le_compat; auto; apply le_refl. - Qed. - - (** Lemmas specific to integers (they use [le_lt_int]) *) - - Lemma lt_left n m : n < m <-> 0 <= m + -n + -(1). - Proof. - rewrite <- plus_assoc, (plus_comm (-n)), plus_assoc. - rewrite <- le_left. - apply le_lt_int. - Qed. - - Lemma OMEGA4 x y z : 0 < x -> x < y -> z * y + x <> 0. - Proof. - intros H H0 H'. - assert (0 < y) by now apply lt_trans with x. - destruct (lt_eq_lt_dec z 0) as [[G|G]|G]. - - - generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0). - rewrite H'. - rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r. - apply le_lt_iff. - rewrite mult_comm. rewrite <- (mult_0_r y). - apply mult_le_compat_l; auto using lt_le_weak. - apply le_0_neg. rewrite opp_plus_distr. - apply le_lt_int. now apply lt_0_neg. - - - apply (lt_not_eq 0 (z*y+x)); auto. - subst. now autorewrite with int. - - - apply (lt_not_eq 0 (z*y+x)); auto. - rewrite <- (plus_0_l 0). - auto using plus_lt_compat, mult_lt_0_compat. - Qed. - - Lemma OMEGA19 x : x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1). - Proof. - intros. - do 2 rewrite <- le_lt_int. - rewrite <- opp_eq_mult_neg_1. - destruct (lt_eq_lt_dec 0 x) as [[H'|H']|H']. - auto. - congruence. - right. - rewrite <-(mult_0_l (-(1))), <-(opp_eq_mult_neg_1 0). - apply opp_lt_compat; auto. - Qed. - - Lemma mult_le_approx n m p : - 0 < n -> p < n -> 0 <= m * n + p -> 0 <= m. - Proof. - do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H. - apply lt_0_neg, le_lt_int, le_left in Hm. - rewrite lt_0_neg. - rewrite opp_plus_distr, mult_comm, opp_mult_distr_r. - rewrite le_lt_int. apply lt_left. - rewrite le_lt_int. - apply le_trans with (n+-(1)); [ now apply le_lt_int | ]. - apply plus_le_compat; [ | apply le_refl ]. - rewrite <- (mult_1_r n) at 1. - apply mult_le_compat_l; auto using lt_le_weak. - Qed. - - (** Some decidabilities *) - - Lemma dec_eq : forall i j:int, decidable (i=j). - Proof. - red; intros; destruct (eq_dec i j); auto. - Qed. - - Lemma dec_ne : forall i j:int, decidable (i<>j). - Proof. - red; intros; destruct (eq_dec i j); auto. - Qed. - - Lemma dec_le : forall i j:int, decidable (i<=j). - Proof. - red; intros; destruct (le_dec i j); auto. - Qed. - - Lemma dec_lt : forall i j:int, decidable (i<j). - Proof. - red; intros; destruct (lt_dec i j); auto. - Qed. - - Lemma dec_ge : forall i j:int, decidable (i>=j). - Proof. - red; intros; rewrite ge_le_iff; destruct (le_dec j i); auto. - Qed. - - Lemma dec_gt : forall i j:int, decidable (i>j). - Proof. - red; intros; rewrite gt_lt_iff; destruct (lt_dec j i); auto. - Qed. - -End IntProperties. - - -(** * The Coq side of the romega tactic *) - -Module IntOmega (I:Int). -Import I. -Module IP:=IntProperties(I). -Import IP. -Local Notation int := I.t. - -(* ** Definition of reified integer expressions - - Terms are either: - - integers [Tint] - - variables [Tvar] - - operation over integers (addition, product, opposite, subtraction) - - Opposite and subtraction are translated in additions and products. - Note that we'll only deal with products for which at least one side - is [Tint]. *) - -Inductive term : Set := - | Tint : int -> term - | Tplus : term -> term -> term - | Tmult : term -> term -> term - | Tminus : term -> term -> term - | Topp : term -> term - | Tvar : N -> term. - -Bind Scope romega_scope with term. -Delimit Scope romega_scope with term. -Arguments Tint _%I. -Arguments Tplus (_ _)%term. -Arguments Tmult (_ _)%term. -Arguments Tminus (_ _)%term. -Arguments Topp _%term. - -Infix "+" := Tplus : romega_scope. -Infix "*" := Tmult : romega_scope. -Infix "-" := Tminus : romega_scope. -Notation "- x" := (Topp x) : romega_scope. -Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope. - -(* ** Definition of reified goals - - Very restricted definition of handled predicates that should be extended - to cover a wider set of operations. - Taking care of negations and disequations require solving more than a - goal in parallel. This is a major improvement over previous versions. *) - -Inductive proposition : Set := - (** First, basic equations, disequations, inequations *) - | EqTerm : term -> term -> proposition - | NeqTerm : term -> term -> proposition - | LeqTerm : term -> term -> proposition - | GeqTerm : term -> term -> proposition - | GtTerm : term -> term -> proposition - | LtTerm : term -> term -> proposition - (** Then, the supported logical connectors *) - | TrueTerm : proposition - | FalseTerm : proposition - | Tnot : proposition -> proposition - | Tor : proposition -> proposition -> proposition - | Tand : proposition -> proposition -> proposition - | Timp : proposition -> proposition -> proposition - (** Everything else is left as a propositional atom (and ignored). *) - | Tprop : nat -> proposition. - -(** Definition of goals as a list of hypothesis *) -Notation hyps := (list proposition). - -(** Definition of lists of subgoals (set of open goals) *) -Notation lhyps := (list hyps). - -(** A single goal packed in a subgoal list *) -Notation singleton := (fun a : hyps => a :: nil). - -(** An absurd goal *) -Definition absurd := FalseTerm :: nil. - -(** ** Decidable equality on terms *) - -Fixpoint eq_term (t1 t2 : term) {struct t2} : bool := - match t1, t2 with - | Tint i1, Tint i2 => i1 =? i2 - | (t11 + t12), (t21 + t22) => eq_term t11 t21 && eq_term t12 t22 - | (t11 * t12), (t21 * t22) => eq_term t11 t21 && eq_term t12 t22 - | (t11 - t12), (t21 - t22) => eq_term t11 t21 && eq_term t12 t22 - | (- t1), (- t2) => eq_term t1 t2 - | [v1], [v2] => N.eqb v1 v2 - | _, _ => false - end%term. - -Infix "=?" := eq_term : romega_scope. - -Theorem eq_term_iff (t t' : term) : - (t =? t')%term = true <-> t = t'. -Proof. - revert t'. induction t; destruct t'; simpl in *; - rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2; - intuition congruence. -Qed. - -Theorem eq_term_reflect (t t' : term) : reflect (t=t') (t =? t')%term. -Proof. - apply iff_reflect. symmetry. apply eq_term_iff. -Qed. - -(** ** Interpretations of terms (as integers). *) - -Fixpoint Nnth {A} (n:N)(l:list A)(default:A) := - match n, l with - | _, nil => default - | 0%N, x::_ => x - | _, _::l => Nnth (N.pred n) l default - end. - -Fixpoint interp_term (env : list int) (t : term) : int := - match t with - | Tint x => x - | (t1 + t2)%term => interp_term env t1 + interp_term env t2 - | (t1 * t2)%term => interp_term env t1 * interp_term env t2 - | (t1 - t2)%term => interp_term env t1 - interp_term env t2 - | (- t)%term => - interp_term env t - | [n]%term => Nnth n env 0 - end. - -(** ** Interpretation of predicats (as Coq propositions) *) - -Fixpoint interp_prop (envp : list Prop) (env : list int) - (p : proposition) : Prop := - match p with - | EqTerm t1 t2 => interp_term env t1 = interp_term env t2 - | NeqTerm t1 t2 => (interp_term env t1) <> (interp_term env t2) - | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2 - | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2 - | GtTerm t1 t2 => interp_term env t1 > interp_term env t2 - | LtTerm t1 t2 => interp_term env t1 < interp_term env t2 - | TrueTerm => True - | FalseTerm => False - | Tnot p' => ~ interp_prop envp env p' - | Tor p1 p2 => interp_prop envp env p1 \/ interp_prop envp env p2 - | Tand p1 p2 => interp_prop envp env p1 /\ interp_prop envp env p2 - | Timp p1 p2 => interp_prop envp env p1 -> interp_prop envp env p2 - | Tprop n => nth n envp True - end. - -(** ** Intepretation of hypothesis lists (as Coq conjunctions) *) - -Fixpoint interp_hyps (envp : list Prop) (env : list int) (l : hyps) - : Prop := - match l with - | nil => True - | p' :: l' => interp_prop envp env p' /\ interp_hyps envp env l' - end. - -(** ** Interpretation of conclusion + hypotheses - - Here we use Coq implications : it's less easy to manipulate, - but handy to relate to the Coq original goal (cf. the use of - [generalize], and lighter (no repetition of types in intermediate - conjunctions). *) - -Fixpoint interp_goal_concl (c : proposition) (envp : list Prop) - (env : list int) (l : hyps) : Prop := - match l with - | nil => interp_prop envp env c - | p' :: l' => - interp_prop envp env p' -> interp_goal_concl c envp env l' - end. - -Notation interp_goal := (interp_goal_concl FalseTerm). - -(** Equivalence between these two interpretations. *) - -Theorem goal_to_hyps : - forall (envp : list Prop) (env : list int) (l : hyps), - (interp_hyps envp env l -> False) -> interp_goal envp env l. -Proof. - induction l; simpl; auto. -Qed. - -Theorem hyps_to_goal : - forall (envp : list Prop) (env : list int) (l : hyps), - interp_goal envp env l -> interp_hyps envp env l -> False. -Proof. - induction l; simpl; auto. - intros H (H1,H2). auto. -Qed. - -(** ** Interpretations of list of goals - - Here again, two flavours... *) - -Fixpoint interp_list_hyps (envp : list Prop) (env : list int) - (l : lhyps) : Prop := - match l with - | nil => False - | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l' - end. - -Fixpoint interp_list_goal (envp : list Prop) (env : list int) - (l : lhyps) : Prop := - match l with - | nil => True - | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l' - end. - -(** Equivalence between the two flavours. *) - -Theorem list_goal_to_hyps : - forall (envp : list Prop) (env : list int) (l : lhyps), - (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. -Proof. - induction l; simpl; intuition. now apply goal_to_hyps. -Qed. - -Theorem list_hyps_to_goal : - forall (envp : list Prop) (env : list int) (l : lhyps), - interp_list_goal envp env l -> interp_list_hyps envp env l -> False. -Proof. - induction l; simpl; intuition. eapply hyps_to_goal; eauto. -Qed. - -(** ** Stabiliy and validity of operations *) - -(** An operation on terms is stable if the interpretation is unchanged. *) - -Definition term_stable (f : term -> term) := - forall (e : list int) (t : term), interp_term e t = interp_term e (f t). - -(** An operation on one hypothesis is valid if this hypothesis implies - the result of this operation. *) - -Definition valid1 (f : proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 : proposition), - interp_prop ep e p1 -> interp_prop ep e (f p1). - -Definition valid2 (f : proposition -> proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 p2 : proposition), - interp_prop ep e p1 -> - interp_prop ep e p2 -> interp_prop ep e (f p1 p2). - -(** Same for lists of hypotheses, and for list of goals *) - -Definition valid_hyps (f : hyps -> hyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_hyps ep e lp -> interp_hyps ep e (f lp). - -Definition valid_list_hyps (f : hyps -> lhyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_hyps ep e lp -> interp_list_hyps ep e (f lp). - -Definition valid_list_goal (f : hyps -> lhyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_list_goal ep e (f lp) -> interp_goal ep e lp. - -(** Some results about these validities. *) - -Theorem valid_goal : - forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), - valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. -Proof. - intros; simpl; apply goal_to_hyps; intro H1; - apply (hyps_to_goal ep env (a l) H0); apply H; assumption. -Qed. - -Theorem goal_valid : - forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. -Proof. - unfold valid_list_goal; intros f H ep e lp H1; apply goal_to_hyps; - intro H2; apply list_hyps_to_goal with (1 := H1); - apply (H ep e lp); assumption. -Qed. - -Theorem append_valid : - forall (ep : list Prop) (e : list int) (l1 l2 : lhyps), - interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 -> - interp_list_hyps ep e (l1 ++ l2). -Proof. - induction l1; simpl in *. - - now intros l2 [H| H]. - - intros l2 [[H| H]| H]. - + auto. - + right; apply IHl1; now left. - + right; apply IHl1; now right. -Qed. - -(** ** Valid operations on hypotheses *) - -(** Extract an hypothesis from the list *) - -Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. - -Theorem nth_valid : - forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), - interp_hyps ep e l -> interp_prop ep e (nth_hyps i l). -Proof. - unfold nth_hyps. induction i; destruct l; simpl in *; try easy. - intros (H1,H2). now apply IHi. -Qed. - -(** Apply a valid operation on two hypotheses from the list, and - store the result in the list. *) - -Definition apply_oper_2 (i j : nat) - (f : proposition -> proposition -> proposition) (l : hyps) := - f (nth_hyps i l) (nth_hyps j l) :: l. - -Theorem apply_oper_2_valid : - forall (i j : nat) (f : proposition -> proposition -> proposition), - valid2 f -> valid_hyps (apply_oper_2 i j f). -Proof. - intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl; - intros lp Hlp; split. - - apply Hf; apply nth_valid; assumption. - - assumption. -Qed. - -(** In-place modification of an hypothesis by application of - a valid operation. *) - -Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) - (l : hyps) {struct i} : hyps := - match l with - | nil => nil - | p :: l' => - match i with - | O => f p :: l' - | S j => p :: apply_oper_1 j f l' - end - end. - -Theorem apply_oper_1_valid : - forall (i : nat) (f : proposition -> proposition), - valid1 f -> valid_hyps (apply_oper_1 i f). -Proof. - unfold valid_hyps. - induction i; intros f Hf ep e [ | p lp]; simpl; intuition. -Qed. - -(** ** A tactic for proving stability *) - -Ltac loop t := - match t with - (* Global *) - | (?X1 = ?X2) => loop X1 || loop X2 - | (_ -> ?X1) => loop X1 - (* Interpretations *) - | (interp_hyps _ _ ?X1) => loop X1 - | (interp_list_hyps _ _ ?X1) => loop X1 - | (interp_prop _ _ ?X1) => loop X1 - | (interp_term _ ?X1) => loop X1 - (* Propositions *) - | (EqTerm ?X1 ?X2) => loop X1 || loop X2 - | (LeqTerm ?X1 ?X2) => loop X1 || loop X2 - (* Terms *) - | (?X1 + ?X2)%term => loop X1 || loop X2 - | (?X1 - ?X2)%term => loop X1 || loop X2 - | (?X1 * ?X2)%term => loop X1 || loop X2 - | (- ?X1)%term => loop X1 - | (Tint ?X1) => loop X1 - (* Eliminations *) - | (if ?X1 =? ?X2 then _ else _) => - let H := fresh "H" in - case (beq_reflect X1 X2); intro H; - try (rewrite H in *; clear H); simpl; auto; Simplify - | (if ?X1 <? ?X2 then _ else _) => - case (blt_reflect X1 X2); intro; simpl; auto; Simplify - | (if (?X1 =? ?X2)%term then _ else _) => - let H := fresh "H" in - case (eq_term_reflect X1 X2); intro H; - try (rewrite H in *; clear H); simpl; auto; Simplify - | (if _ && _ then _ else _) => rewrite andb_if; Simplify - | (if negb _ then _ else _) => rewrite negb_if; Simplify - | match N.compare ?X1 ?X2 with _ => _ end => - destruct (N.compare_spec X1 X2); Simplify - | match ?X1 with _ => _ end => destruct X1; auto; Simplify - | _ => fail - end - -with Simplify := match goal with - | |- ?X1 => try loop X1 - | _ => idtac - end. - -(** ** Operations on equation bodies *) - -(** The operations below handle in priority _normalized_ terms, i.e. - terms of the form: - [([v1]*Tint k1 + ([v2]*Tint k2 + (... + Tint cst)))] - with [v1>v2>...] and all [ki<>0]. - See [normalize] below for a way to put terms in this form. - - These operations also produce a correct (but suboptimal) - result in case of non-normalized input terms, but this situation - should normally not happen when running [romega]. - - /!\ Do not modify this section (especially [fusion] and [normalize]) - without tweaking the corresponding functions in [refl_omega.ml]. -*) - -(** Multiplication and sum by two constants. Invariant: [k1<>0]. *) - -Fixpoint scalar_mult_add (t : term) (k1 k2 : int) : term := - match t with - | v1 * Tint x1 + l1 => - v1 * Tint (x1 * k1) + scalar_mult_add l1 k1 k2 - | Tint x => Tint (k1 * x + k2) - | _ => t * Tint k1 + Tint k2 (* shouldn't happen *) - end%term. - -Theorem scalar_mult_add_stable e t k1 k2 : - interp_term e (scalar_mult_add t k1 k2) = - interp_term e (t * Tint k1 + Tint k2). -Proof. - induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm. - rewrite IHt2. simpl. apply OMEGA11. -Qed. - -(** Multiplication by a (non-nul) constant. *) - -Definition scalar_mult (t : term) (k : int) := scalar_mult_add t k 0. - -Theorem scalar_mult_stable e t k : - interp_term e (scalar_mult t k) = - interp_term e (t * Tint k). -Proof. - unfold scalar_mult. rewrite scalar_mult_add_stable. simpl. - apply plus_0_r. -Qed. - -(** Adding a constant - - Instead of using [scalar_norm_add t 1 k], the following - definition spares some computations. - *) - -Fixpoint scalar_add (t : term) (k : int) : term := - match t with - | m + l => m + scalar_add l k - | Tint x => Tint (x + k) - | _ => t + Tint k - end%term. - -Theorem scalar_add_stable e t k : - interp_term e (scalar_add t k) = interp_term e (t + Tint k). -Proof. - induction t; simpl; Simplify; simpl; auto. - rewrite IHt2. simpl. apply plus_assoc. -Qed. - -(** Division by a constant - - All the non-constant coefficients should be exactly dividable *) - -Fixpoint scalar_div (t : term) (k : int) : option (term * int) := - match t with - | v * Tint x + l => - let (q,r) := diveucl x k in - if (r =? 0)%I then - match scalar_div l k with - | None => None - | Some (u,c) => Some (v * Tint q + u, c) - end - else None - | Tint x => - let (q,r) := diveucl x k in - Some (Tint q, r) - | _ => None - end%term. - -Lemma scalar_div_stable e t k u c : k<>0 -> - scalar_div t k = Some (u,c) -> - interp_term e (u * Tint k + Tint c) = interp_term e t. -Proof. - revert u c. - induction t; simpl; Simplify; try easy. - - intros u c Hk. assert (H := diveucl_spec t0 k Hk). - simpl in H. - destruct diveucl as (q,r). simpl in H. rewrite H. - injection 1 as <- <-. simpl. f_equal. apply mult_comm. - - intros u c Hk. - destruct t1; simpl; Simplify; try easy. - destruct t1_2; simpl; Simplify; try easy. - assert (H := diveucl_spec t0 k Hk). - simpl in H. - destruct diveucl as (q,r). simpl in H. rewrite H. - case beq_reflect; [intros -> | easy]. - destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy]. - injection 1 as <- ->. simpl. - rewrite <- (IHt2 u' c Hk); simpl; auto. - rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11. -Qed. - - -(** Fusion of two equations. - - From two normalized equations, this fusion will produce - a normalized output corresponding to the coefficiented sum. - Invariant: [k1<>0] and [k2<>0]. -*) - -Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term := - match t1 with - | [v1] * Tint x1 + l1 => - (fix fusion_t1 t2 : term := - match t2 with - | [v2] * Tint x2 + l2 => - match N.compare v1 v2 with - | Eq => - let k := (k1 * x1 + k2 * x2)%I in - if (k =? 0)%I then fusion l1 l2 k1 k2 - else [v1] * Tint k + fusion l1 l2 k1 k2 - | Lt => [v2] * Tint (k2 * x2) + fusion_t1 l2 - | Gt => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2 - end - | Tint x2 => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2 - | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *) - end) t2 - | Tint x1 => scalar_mult_add t2 k2 (k1 * x1) - | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *) - end%term. - -Theorem fusion_stable e t1 t2 k1 k2 : - interp_term e (fusion t1 t2 k1 k2) = - interp_term e (t1 * Tint k1 + t2 * Tint k2). -Proof. - revert t2; induction t1; simpl; Simplify; simpl; auto. - - intros; rewrite scalar_mult_add_stable. simpl. - rewrite plus_comm. f_equal. apply mult_comm. - - intros. Simplify. induction t2; simpl; Simplify; simpl; auto. - + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11. - + rewrite IHt1_2. simpl. subst n0. - rewrite (mult_comm k1), (mult_comm k2) in H0. - rewrite <- OMEGA10, H0. now autorewrite with int. - + rewrite IHt1_2. simpl. subst n0. - rewrite (mult_comm k1), (mult_comm k2); apply OMEGA10. - + rewrite IHt2_2. simpl. rewrite (mult_comm k2); apply OMEGA12. - + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11. -Qed. - -(** Term normalization. - - Precondition: all [Tmult] should be on at least one [Tint]. - Postcondition: a normalized equivalent term (see below). -*) - -Fixpoint normalize t := - match t with - | Tint n => Tint n - | [n]%term => ([n] * Tint 1 + Tint 0)%term - | (t + t')%term => fusion (normalize t) (normalize t') 1 1 - | (- t)%term => scalar_mult (normalize t) (-(1)) - | (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1)) - | (Tint k * t)%term | (t * Tint k)%term => - if k =? 0 then Tint 0 else scalar_mult (normalize t) k - | (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *) - end. - -Theorem normalize_stable : term_stable normalize. -Proof. - intros e t. - induction t; simpl; Simplify; simpl; - rewrite ?scalar_mult_stable; simpl in *; rewrite <- ?IHt1; - rewrite ?fusion_stable; simpl; autorewrite with int; auto. - - now f_equal. - - rewrite mult_comm. now f_equal. - - rewrite <- opp_eq_mult_neg_1, <-minus_def. now f_equal. - - rewrite <- opp_eq_mult_neg_1. now f_equal. -Qed. - -(** ** Normalization of a proposition. - - The only basic facts left after normalization are - [0 = ...] or [0 <> ...] or [0 <= ...]. - When a fact is in negative position, we factorize a [Tnot] - out of it, and normalize the reversed fact inside. - - /!\ Here again, do not change this code without corresponding - modifications in [refl_omega.ml]. -*) - -Fixpoint normalize_prop (negated:bool)(p:proposition) := - match p with - | EqTerm t1 t2 => - if negated then Tnot (NeqTerm (Tint 0) (normalize (t1-t2))) - else EqTerm (Tint 0) (normalize (t1-t2)) - | NeqTerm t1 t2 => - if negated then Tnot (EqTerm (Tint 0) (normalize (t1-t2))) - else NeqTerm (Tint 0) (normalize (t1-t2)) - | LeqTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1))))) - else LeqTerm (Tint 0) (normalize (t2-t1)) - | GeqTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1))))) - else LeqTerm (Tint 0) (normalize (t1-t2)) - | LtTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2))) - else LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1)))) - | GtTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1))) - else LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1)))) - | Tnot p => Tnot (normalize_prop (negb negated) p) - | Tor p p' => Tor (normalize_prop negated p) (normalize_prop negated p') - | Tand p p' => Tand (normalize_prop negated p) (normalize_prop negated p') - | Timp p p' => Timp (normalize_prop (negb negated) p) - (normalize_prop negated p') - | Tprop _ | TrueTerm | FalseTerm => p - end. - -Definition normalize_hyps := List.map (normalize_prop false). - -Local Ltac simp := cbn -[normalize]. - -Theorem normalize_prop_valid b e ep p : - interp_prop e ep (normalize_prop b p) <-> interp_prop e ep p. -Proof. - revert b. - induction p; intros; simp; try tauto. - - destruct b; simp; - rewrite <- ?normalize_stable; simpl; rewrite ?minus_def. - + rewrite not_eq. apply egal_left. - + apply egal_left. - - destruct b; simp; - rewrite <- ?normalize_stable; simpl; rewrite ?minus_def; - apply not_iff_compat, egal_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + symmetry. rewrite le_lt_iff. apply not_iff_compat, lt_left. - + now rewrite <- le_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + symmetry. rewrite ge_le_iff, le_lt_iff. - apply not_iff_compat, lt_left. - + rewrite ge_le_iff. now rewrite <- le_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + rewrite gt_lt_iff, lt_le_iff. apply not_iff_compat. - now rewrite <- le_left. - + symmetry. rewrite gt_lt_iff. apply lt_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + rewrite lt_le_iff. apply not_iff_compat. - now rewrite <- le_left. - + symmetry. apply lt_left. - - now rewrite IHp. - - now rewrite IHp1, IHp2. - - now rewrite IHp1, IHp2. - - now rewrite IHp1, IHp2. -Qed. - -Theorem normalize_hyps_valid : valid_hyps normalize_hyps. -Proof. - intros e ep l. induction l; simpl; intuition. - now rewrite normalize_prop_valid. -Qed. - -Theorem normalize_hyps_goal (ep : list Prop) (env : list int) (l : hyps) : - interp_goal ep env (normalize_hyps l) -> interp_goal ep env l. -Proof. - intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. -Qed. - -(** ** A simple decidability checker - - For us, everything is considered decidable except - propositional atoms [Tprop _]. *) - -Fixpoint decidability (p : proposition) : bool := - match p with - | Tnot t => decidability t - | Tand t1 t2 => decidability t1 && decidability t2 - | Timp t1 t2 => decidability t1 && decidability t2 - | Tor t1 t2 => decidability t1 && decidability t2 - | Tprop _ => false - | _ => true - end. - -Theorem decidable_correct : - forall (ep : list Prop) (e : list int) (p : proposition), - decidability p = true -> decidable (interp_prop ep e p). -Proof. - induction p; simpl; intros Hp; try destruct (andb_prop _ _ Hp). - - apply dec_eq. - - apply dec_ne. - - apply dec_le. - - apply dec_ge. - - apply dec_gt. - - apply dec_lt. - - left; auto. - - right; unfold not; auto. - - apply dec_not; auto. - - apply dec_or; auto. - - apply dec_and; auto. - - apply dec_imp; auto. - - discriminate. -Qed. - -(** ** Omega steps - - The following inductive type describes steps as they can be - found in the trace coming from the decision procedure Omega. - We consider here only normalized equations [0=...], disequations - [0<>...] or inequations [0<=...]. - - First, the final steps leading to a contradiction: - - [O_BAD_CONSTANT i] : hypothesis i has a constant body - and this constant is not compatible with the kind of i. - - [O_NOT_EXACT_DIVIDE i k] : - equation i can be factorized as some [k*t+c] with [0<c<k]. - - Now, the intermediate steps leading to a new hypothesis: - - [O_DIVIDE i k cont] : - the body of hypothesis i could be factorized as [k*t+c] - with either [k<>0] and [c=0] for a (dis)equation, or - [0<k] and [c<k] for an inequation. We change in-place the - body of i for [t]. - - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose - kind depends on the kind of hypotheses [i1] and [i2], and - whose body is [k1*body(i1) + k2*body(i2)]. Depending of the - situation, [k1] or [k2] might have to be positive or non-nul. - - [O_MERGE_EQ i j cont] : - inequations i and j have opposite bodies, we add an equation - with one these bodies. - - [O_SPLIT_INEQ i cont1 cont2] : - disequation i is split into a disjonction of inequations. -*) - -Definition idx := nat. (** Index of an hypothesis in the list *) - -Inductive t_omega : Set := - | O_BAD_CONSTANT : idx -> t_omega - | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega - - | O_DIVIDE : idx -> int -> t_omega -> t_omega - | O_SUM : int -> idx -> int -> idx -> t_omega -> t_omega - | O_MERGE_EQ : idx -> idx -> t_omega -> t_omega - | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega. - -(** ** Actual resolution steps of an omega normalized goal *) - -(** First, the final steps, leading to a contradiction *) - -(** [O_BAD_CONSTANT] *) - -Definition bad_constant (i : nat) (h : hyps) := - match nth_hyps i h with - | EqTerm (Tint Nul) (Tint n) => if n =? Nul then h else absurd - | NeqTerm (Tint Nul) (Tint n) => if n =? Nul then absurd else h - | LeqTerm (Tint Nul) (Tint n) => if n <? Nul then absurd else h - | _ => h - end. - -Theorem bad_constant_valid i : valid_hyps (bad_constant i). -Proof. - unfold valid_hyps, bad_constant; intros ep e lp H. - generalize (nth_valid ep e i lp H); Simplify. - rewrite le_lt_iff. intuition. -Qed. - -(** [O_NOT_EXACT_DIVIDE] *) - -Definition not_exact_divide (i : nat) (k : int) (l : hyps) := - match nth_hyps i l with - | EqTerm (Tint Nul) b => - match scalar_div b k with - | Some (body,c) => - if (Nul =? 0) && (0 <? c) && (c <? k) then absurd - else l - | None => l - end - | _ => l - end. - -Theorem not_exact_divide_valid i k : - valid_hyps (not_exact_divide i k). -Proof. - unfold valid_hyps, not_exact_divide; intros. - generalize (nth_valid ep e i lp). - destruct (nth_hyps i lp); simpl; auto. - destruct t0; auto. - destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto. - Simplify. - assert (k <> 0). - { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } - apply (scalar_div_stable e) in E; auto. simpl in E. - intros H'; rewrite <- H' in E; auto. - exfalso. revert E. now apply OMEGA4. -Qed. - -(** Now, the steps generating a new equation. *) - -(** [O_DIVIDE] *) - -Definition divide (k : int) (prop : proposition) := - match prop with - | EqTerm (Tint o) b => - match scalar_div b k with - | Some (body,c) => - if (o =? 0) && (c =? 0) && negb (k =? 0) - then EqTerm (Tint 0) body - else TrueTerm - | None => TrueTerm - end - | NeqTerm (Tint o) b => - match scalar_div b k with - | Some (body,c) => - if (o =? 0) && (c =? 0) && negb (k =? 0) - then NeqTerm (Tint 0) body - else TrueTerm - | None => TrueTerm - end - | LeqTerm (Tint o) b => - match scalar_div b k with - | Some (body,c) => - if (o =? 0) && (0 <? k) && (c <? k) - then LeqTerm (Tint 0) body - else prop - | None => prop - end - | _ => TrueTerm - end. - -Theorem divide_valid k : valid1 (divide k). -Proof. - unfold valid1, divide; intros ep e p; - destruct p; simpl; auto; - destruct t0; simpl; auto; - destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto. - - apply (scalar_div_stable e) in E; auto. simpl in E. - intros H'; rewrite <- H' in E. rewrite plus_0_r in E. - apply mult_integral in E. intuition. - - apply (scalar_div_stable e) in E; auto. simpl in E. - intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E. - - assert (k <> 0). - { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } - apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E. - intro H'. now apply mult_le_approx with (3 := H'). -Qed. - -(** [O_SUM]. Invariant: [k1] and [k2] non-nul. *) - -Definition sum (k1 k2 : int) (prop1 prop2 : proposition) := - match prop1 with - | EqTerm (Tint o) b1 => - match prop2 with - | EqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) - then EqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | LeqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && (0 <? k2) - then LeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | NeqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && negb (k2 =? 0) - then NeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | _ => TrueTerm - end - | LeqTerm (Tint o) b1 => - if (o =? 0) && (0 <? k1) - then match prop2 with - | EqTerm (Tint o') b2 => - if o' =? 0 then - LeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | LeqTerm (Tint o') b2 => - if (o' =? 0) && (0 <? k2) - then LeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | _ => TrueTerm - end - else TrueTerm - | NeqTerm (Tint o) b1 => - match prop2 with - | EqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && negb (k1 =? 0) - then NeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | _ => TrueTerm - end - | _ => TrueTerm - end. - -Theorem sum_valid : - forall (k1 k2 : int), valid2 (sum k1 k2). -Proof. - unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum; - Simplify; simpl; rewrite ?fusion_stable; - simpl; intros; auto. - - apply sum1; auto. - - rewrite plus_comm. apply sum5; auto. - - apply sum2; auto using lt_le_weak. - - apply sum5; auto. - - rewrite plus_comm. apply sum2; auto using lt_le_weak. - - apply sum3; auto using lt_le_weak. -Qed. - -(** [MERGE_EQ] *) - -Definition merge_eq (prop1 prop2 : proposition) := - match prop1 with - | LeqTerm (Tint o) b1 => - match prop2 with - | LeqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && - (b1 =? scalar_mult b2 (-(1)))%term - then EqTerm (Tint 0) b1 - else TrueTerm - | _ => TrueTerm - end - | _ => TrueTerm - end. - -Theorem merge_eq_valid : valid2 merge_eq. -Proof. - unfold valid2, merge_eq; intros ep e p1 p2; Simplify; simpl; auto. - rewrite scalar_mult_stable. simpl. - intros; symmetry ; apply OMEGA8 with (2 := H0). - - assumption. - - elim opp_eq_mult_neg_1; trivial. -Qed. - -(** [O_SPLIT_INEQ] (only step to produce two subgoals). *) - -Definition split_ineq (i : nat) (f1 f2 : hyps -> lhyps) (l : hyps) := - match nth_hyps i l with - | NeqTerm (Tint o) b1 => - if o =? 0 then - f1 (LeqTerm (Tint 0) (scalar_add b1 (-(1))) :: l) ++ - f2 (LeqTerm (Tint 0) (scalar_mult_add b1 (-(1)) (-(1))) :: l) - else l :: nil - | _ => l :: nil - end. - -Theorem split_ineq_valid : - forall (i : nat) (f1 f2 : hyps -> lhyps), - valid_list_hyps f1 -> - valid_list_hyps f2 -> valid_list_hyps (split_ineq i f1 f2). -Proof. - unfold valid_list_hyps, split_ineq; intros i f1 f2 H1 H2 ep e lp H; - generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); - simpl; auto; intros t1 t2; case t1; simpl; - auto; intros z; simpl; auto; intro H3. - Simplify. - apply append_valid; elim (OMEGA19 (interp_term e t2)). - - intro H4; left; apply H1; simpl; rewrite scalar_add_stable; - simpl; auto. - - intro H4; right; apply H2; simpl; rewrite scalar_mult_add_stable; - simpl; auto. - - generalize H3; unfold not; intros E1 E2; apply E1; - symmetry ; trivial. -Qed. - -(** ** Replaying the resolution trace *) - -Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps := - match t with - | O_BAD_CONSTANT i => singleton (bad_constant i l) - | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l) - | O_DIVIDE i k cont => - execute_omega cont (apply_oper_1 i (divide k) l) - | O_SUM k1 i1 k2 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l) - | O_MERGE_EQ i1 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 merge_eq l) - | O_SPLIT_INEQ i cont1 cont2 => - split_ineq i (execute_omega cont1) (execute_omega cont2) l - end. - -Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr). -Proof. - simple induction tr; unfold valid_list_hyps, valid_hyps; simpl. - - intros; left; now apply bad_constant_valid. - - intros; left; now apply not_exact_divide_valid. - - intros m k t' Ht' ep e lp H; apply Ht'; - apply - (apply_oper_1_valid m (divide k) - (divide_valid k) ep e lp H). - - intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht'; - apply - (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e - lp H). - - intros i1 i2 t' Ht' ep e lp H; apply Ht'; - apply - (apply_oper_2_valid i1 i2 merge_eq merge_eq_valid ep e - lp H). - - intros i k1 H1 k2 H2 ep e lp H; - apply - (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e - lp H). -Qed. - - -(** ** Rules for decomposing the hypothesis - - This type allows navigation in the logical constructors that - form the predicats of the hypothesis in order to decompose them. - This allows in particular to extract one hypothesis from a conjunction. - NB: negations are now silently traversed. *) - -Inductive direction : Set := - | D_left : direction - | D_right : direction. - -(** This type allows extracting useful components from hypothesis, either - hypothesis generated by splitting a disjonction, or equations. - The last constructor indicates how to solve the obtained system - via the use of the trace type of Omega [t_omega] *) - -Inductive e_step : Set := - | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step - | E_EXTRACT : nat -> list direction -> e_step -> e_step - | E_SOLVE : t_omega -> e_step. - -(** Selection of a basic fact inside an hypothesis. *) - -Fixpoint extract_hyp_pos (s : list direction) (p : proposition) : - proposition := - match p, s with - | Tand x y, D_left :: l => extract_hyp_pos l x - | Tand x y, D_right :: l => extract_hyp_pos l y - | Tnot x, _ => extract_hyp_neg s x - | _, _ => p - end - - with extract_hyp_neg (s : list direction) (p : proposition) : - proposition := - match p, s with - | Tor x y, D_left :: l => extract_hyp_neg l x - | Tor x y, D_right :: l => extract_hyp_neg l y - | Timp x y, D_left :: l => - if decidability x then extract_hyp_pos l x else Tnot p - | Timp x y, D_right :: l => extract_hyp_neg l y - | Tnot x, _ => if decidability x then extract_hyp_pos s x else Tnot p - | _, _ => Tnot p - end. - -Theorem extract_valid : - forall s : list direction, valid1 (extract_hyp_pos s). -Proof. - assert (forall p s ep e, - (interp_prop ep e p -> - interp_prop ep e (extract_hyp_pos s p)) /\ - (interp_prop ep e (Tnot p) -> - interp_prop ep e (extract_hyp_neg s p))). - { induction p; destruct s; simpl; auto; split; try destruct d; try easy; - intros; (apply IHp || apply IHp1 || apply IHp2 || idtac); simpl; try tauto; - destruct decidability eqn:D; auto; - apply (decidable_correct ep e) in D; unfold decidable in D; - (apply IHp || apply IHp1); tauto. } - red. intros. now apply H. -Qed. - -(** Attempt to shorten error messages if romega goes rogue... - NB: [interp_list_goal _ _ BUG = False /\ True]. *) -Definition BUG : lhyps := nil :: nil. - -(** Split and extract in hypotheses *) - -Fixpoint decompose_solve (s : e_step) (h : hyps) : lhyps := - match s with - | E_SPLIT i dl s1 s2 => - match extract_hyp_pos dl (nth_hyps i h) with - | Tor x y => decompose_solve s1 (x :: h) ++ decompose_solve s2 (y :: h) - | Tnot (Tand x y) => - if decidability x - then - decompose_solve s1 (Tnot x :: h) ++ - decompose_solve s2 (Tnot y :: h) - else BUG - | Timp x y => - if decidability x then - decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h) - else BUG - | _ => BUG - end - | E_EXTRACT i dl s1 => - decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h) - | E_SOLVE t => execute_omega t h - end. - -Theorem decompose_solve_valid (s : e_step) : - valid_list_goal (decompose_solve s). -Proof. - apply goal_valid. red. induction s; simpl; intros ep e lp H. - - assert (H' : interp_prop ep e (extract_hyp_pos l (nth_hyps n lp))). - { now apply extract_valid, nth_valid. } - destruct extract_hyp_pos; simpl in *; auto. - + destruct p; simpl; auto. - destruct decidability eqn:D; [ | simpl; auto]. - apply (decidable_correct ep e) in D. - apply append_valid. simpl in *. destruct D. - * right. apply IHs2. simpl; auto. - * left. apply IHs1. simpl; auto. - + apply append_valid. destruct H'. - * left. apply IHs1. simpl; auto. - * right. apply IHs2. simpl; auto. - + destruct decidability eqn:D; [ | simpl; auto]. - apply (decidable_correct ep e) in D. - apply append_valid. destruct D. - * right. apply IHs2. simpl; auto. - * left. apply IHs1. simpl; auto. - - apply IHs; simpl; split; auto. - now apply extract_valid, nth_valid. - - now apply omega_valid. -Qed. - -(** Reduction of subgoal list by discarding the contradictory subgoals. *) - -Definition valid_lhyps (f : lhyps -> lhyps) := - forall (ep : list Prop) (e : list int) (lp : lhyps), - interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp). - -Fixpoint reduce_lhyps (lp : lhyps) : lhyps := - match lp with - | nil => nil - | (FalseTerm :: nil) :: lp' => reduce_lhyps lp' - | x :: lp' => BUG - end. - -Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. -Proof. - unfold valid_lhyps; intros ep e lp; elim lp. - - simpl; auto. - - intros a l HR; elim a. - + simpl; tauto. - + intros a1 l1; case l1; case a1; simpl; tauto. -Qed. - -Theorem do_reduce_lhyps : - forall (envp : list Prop) (env : list int) (l : lhyps), - interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l. -Proof. - intros envp env l H; apply list_goal_to_hyps; intro H1; - apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid; - assumption. -Qed. - -(** Pushing the conclusion into the hypotheses. *) - -Definition concl_to_hyp (p : proposition) := - if decidability p then Tnot p else TrueTerm. - -Definition do_concl_to_hyp : - forall (envp : list Prop) (env : list int) (c : proposition) (l : hyps), - interp_goal envp env (concl_to_hyp c :: l) -> - interp_goal_concl c envp env l. -Proof. - induction l; simpl. - - unfold concl_to_hyp; simpl. - destruct decidability eqn:D; [ | simpl; tauto ]. - apply (decidable_correct envp env) in D. unfold decidable in D. - simpl. tauto. - - simpl in *; tauto. -Qed. - -(** The omega tactic : all steps together *) - -Definition omega_tactic (t1 : e_step) (c : proposition) (l : hyps) := - reduce_lhyps (decompose_solve t1 (normalize_hyps (concl_to_hyp c :: l))). - -Theorem do_omega : - forall (t : e_step) (envp : list Prop) - (env : list int) (c : proposition) (l : hyps), - interp_list_goal envp env (omega_tactic t c l) -> - interp_goal_concl c envp env l. -Proof. - unfold omega_tactic; intros t ep e c l H. - apply do_concl_to_hyp. - apply normalize_hyps_goal. - apply (decompose_solve_valid t). - now apply do_reduce_lhyps. -Qed. - -End IntOmega. - -(** For now, the above modular construction is instanciated on Z, - in order to retrieve the initial ROmega. *) - -Module ZOmega := IntOmega(Z_as_Int). diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml deleted file mode 100644 index 949cba2dbe..0000000000 --- a/plugins/romega/const_omega.ml +++ /dev/null @@ -1,332 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - -open Names - -let module_refl_name = "ReflOmegaCore" -let module_refl_path = ["Coq"; "romega"; module_refl_name] - -type result = - | Kvar of string - | Kapp of string * EConstr.t list - | Kimp of EConstr.t * EConstr.t - | Kufo - -let meaningful_submodule = [ "Z"; "N"; "Pos" ] - -let string_of_global r = - let dp = Nametab.dirpath_of_global r in - let prefix = match Names.DirPath.repr dp with - | [] -> "" - | m::_ -> - let s = Names.Id.to_string m in - if Util.String.List.mem s meaningful_submodule then s^"." else "" - in - prefix^(Names.Id.to_string (Nametab.basename_of_global r)) - -let destructurate sigma t = - let c, args = EConstr.decompose_app sigma t in - let open Constr in - match EConstr.kind sigma c, args with - | Const (sp,_), args -> - Kapp (string_of_global (Globnames.ConstRef sp), args) - | Construct (csp,_) , args -> - Kapp (string_of_global (Globnames.ConstructRef csp), args) - | Ind (isp,_), args -> - Kapp (string_of_global (Globnames.IndRef isp), args) - | Var id, [] -> Kvar(Names.Id.to_string id) - | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | _ -> Kufo - -exception DestConstApp - -let dest_const_apply sigma t = - let open Constr in - let f,args = EConstr.decompose_app sigma t in - let ref = - match EConstr.kind sigma f with - | Const (sp,_) -> Globnames.ConstRef sp - | Construct (csp,_) -> Globnames.ConstructRef csp - | Ind (isp,_) -> Globnames.IndRef isp - | _ -> raise DestConstApp - in Nametab.basename_of_global ref, args - -let logic_dir = ["Coq";"Logic";"Decidable"] - -let coq_modules = - Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules - @ [["Coq"; "Lists"; "List"]] - @ [module_refl_path] - @ [module_refl_path@["ZOmega"]] - -let bin_module = [["Coq";"Numbers";"BinNums"]] -let z_module = [["Coq";"ZArith";"BinInt"]] - -let init_constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x -let constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" coq_modules x -let z_constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" z_module x -let bin_constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" bin_module x - -(* Logic *) -let coq_refl_equal = lazy(init_constant "eq_refl") -let coq_and = lazy(init_constant "and") -let coq_not = lazy(init_constant "not") -let coq_or = lazy(init_constant "or") -let coq_True = lazy(init_constant "True") -let coq_False = lazy(init_constant "False") -let coq_I = lazy(init_constant "I") - -(* ReflOmegaCore/ZOmega *) - -let coq_t_int = lazy (constant "Tint") -let coq_t_plus = lazy (constant "Tplus") -let coq_t_mult = lazy (constant "Tmult") -let coq_t_opp = lazy (constant "Topp") -let coq_t_minus = lazy (constant "Tminus") -let coq_t_var = lazy (constant "Tvar") - -let coq_proposition = lazy (constant "proposition") -let coq_p_eq = lazy (constant "EqTerm") -let coq_p_leq = lazy (constant "LeqTerm") -let coq_p_geq = lazy (constant "GeqTerm") -let coq_p_lt = lazy (constant "LtTerm") -let coq_p_gt = lazy (constant "GtTerm") -let coq_p_neq = lazy (constant "NeqTerm") -let coq_p_true = lazy (constant "TrueTerm") -let coq_p_false = lazy (constant "FalseTerm") -let coq_p_not = lazy (constant "Tnot") -let coq_p_or = lazy (constant "Tor") -let coq_p_and = lazy (constant "Tand") -let coq_p_imp = lazy (constant "Timp") -let coq_p_prop = lazy (constant "Tprop") - -let coq_s_bad_constant = lazy (constant "O_BAD_CONSTANT") -let coq_s_divide = lazy (constant "O_DIVIDE") -let coq_s_not_exact_divide = lazy (constant "O_NOT_EXACT_DIVIDE") -let coq_s_sum = lazy (constant "O_SUM") -let coq_s_merge_eq = lazy (constant "O_MERGE_EQ") -let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ") - -(* construction for the [extract_hyp] tactic *) -let coq_direction = lazy (constant "direction") -let coq_d_left = lazy (constant "D_left") -let coq_d_right = lazy (constant "D_right") - -let coq_e_split = lazy (constant "E_SPLIT") -let coq_e_extract = lazy (constant "E_EXTRACT") -let coq_e_solve = lazy (constant "E_SOLVE") - -let coq_interp_sequent = lazy (constant "interp_goal_concl") -let coq_do_omega = lazy (constant "do_omega") - -(* Nat *) - -let coq_S = lazy(init_constant "S") -let coq_O = lazy(init_constant "O") - -let rec mk_nat = function - | 0 -> Lazy.force coq_O - | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) - -(* Lists *) - -let mkListConst c = - let r = - Coqlib.coq_reference "" ["Init";"Datatypes"] c - in - let inst = - if Global.is_polymorphic r then - fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|]) - else - fun _ -> EConstr.EInstance.empty - in - fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u) - -let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = EConstr.mkApp (mkListConst "nil" univ, [|typ|]) - -let mk_list univ typ l = - let rec loop = function - | [] -> coq_nil univ typ - | (step :: l) -> - EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in - loop l - -let mk_plist = - let type1lev = UnivGen.new_univ_level () in - fun l -> mk_list type1lev EConstr.mkProp l - -let mk_list = mk_list Univ.Level.set - -type parse_term = - | Tplus of EConstr.t * EConstr.t - | Tmult of EConstr.t * EConstr.t - | Tminus of EConstr.t * EConstr.t - | Topp of EConstr.t - | Tsucc of EConstr.t - | Tnum of Bigint.bigint - | Tother - -type parse_rel = - | Req of EConstr.t * EConstr.t - | Rne of EConstr.t * EConstr.t - | Rlt of EConstr.t * EConstr.t - | Rle of EConstr.t * EConstr.t - | Rgt of EConstr.t * EConstr.t - | Rge of EConstr.t * EConstr.t - | Rtrue - | Rfalse - | Rnot of EConstr.t - | Ror of EConstr.t * EConstr.t - | Rand of EConstr.t * EConstr.t - | Rimp of EConstr.t * EConstr.t - | Riff of EConstr.t * EConstr.t - | Rother - -let parse_logic_rel sigma c = match destructurate sigma c with - | Kapp("True",[]) -> Rtrue - | Kapp("False",[]) -> Rfalse - | Kapp("not",[t]) -> Rnot t - | Kapp("or",[t1;t2]) -> Ror (t1,t2) - | Kapp("and",[t1;t2]) -> Rand (t1,t2) - | Kimp(t1,t2) -> Rimp (t1,t2) - | Kapp("iff",[t1;t2]) -> Riff (t1,t2) - | _ -> Rother - -(* Binary numbers *) - -let coq_Z = lazy (bin_constant "Z") -let coq_xH = lazy (bin_constant "xH") -let coq_xO = lazy (bin_constant "xO") -let coq_xI = lazy (bin_constant "xI") -let coq_Z0 = lazy (bin_constant "Z0") -let coq_Zpos = lazy (bin_constant "Zpos") -let coq_Zneg = lazy (bin_constant "Zneg") -let coq_N0 = lazy (bin_constant "N0") -let coq_Npos = lazy (bin_constant "Npos") - -let rec mk_positive n = - if Bigint.equal n Bigint.one then Lazy.force coq_xH - else - let (q,r) = Bigint.euclid n Bigint.two in - EConstr.mkApp - ((if Bigint.equal r Bigint.zero - then Lazy.force coq_xO else Lazy.force coq_xI), - [| mk_positive q |]) - -let mk_N = function - | 0 -> Lazy.force coq_N0 - | n -> EConstr.mkApp (Lazy.force coq_Npos, - [| mk_positive (Bigint.of_int n) |]) - -module type Int = sig - val typ : EConstr.t Lazy.t - val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool - val plus : EConstr.t Lazy.t - val mult : EConstr.t Lazy.t - val opp : EConstr.t Lazy.t - val minus : EConstr.t Lazy.t - - val mk : Bigint.bigint -> EConstr.t - val parse_term : Evd.evar_map -> EConstr.t -> parse_term - val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel - (* check whether t is built only with numbers and + * - *) - val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option -end - -module Z : Int = struct - -let typ = coq_Z -let plus = lazy (z_constant "Z.add") -let mult = lazy (z_constant "Z.mul") -let opp = lazy (z_constant "Z.opp") -let minus = lazy (z_constant "Z.sub") - -let recognize_pos sigma t = - let rec loop t = - let f,l = dest_const_apply sigma t in - match Id.to_string f,l with - | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) - | "xO",[t] -> Bigint.mult Bigint.two (loop t) - | "xH",[] -> Bigint.one - | _ -> raise DestConstApp - in - try Some (loop t) with DestConstApp -> None - -let recognize_Z sigma t = - try - let f,l = dest_const_apply sigma t in - match Id.to_string f,l with - | "Zpos",[t] -> recognize_pos sigma t - | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma t) - | "Z0",[] -> Some Bigint.zero - | _ -> None - with DestConstApp -> None - -let mk_Z n = - if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 - else if Bigint.is_strictly_pos n then - EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) - else - EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) - -let mk = mk_Z - -let parse_term sigma t = - match destructurate sigma t with - | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) - | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) - | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) - | Kapp("Z.opp",[t]) -> Topp t - | Kapp("Z.succ",[t]) -> Tsucc t - | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (match recognize_Z sigma t with Some t -> Tnum t | None -> Tother) - | _ -> Tother - -let is_int_typ gl t = - Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z) - -let parse_rel gl t = - let sigma = Proofview.Goal.sigma gl in - match destructurate sigma t with - | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2) - | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) - | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) - | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) - | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) - | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) - | _ -> parse_logic_rel sigma t - -let rec get_scalar sigma t = - match destructurate sigma t with - | Kapp("Z.add", [t1;t2]) -> - Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2) - | Kapp ("Z.sub",[t1;t2]) -> - Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2) - | Kapp ("Z.mul",[t1;t2]) -> - Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2) - | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t) - | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t) - | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t - | _ -> None - -end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli deleted file mode 100644 index 64668df007..0000000000 --- a/plugins/romega/const_omega.mli +++ /dev/null @@ -1,124 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - - -(** Coq objects used in romega *) - -(* from Logic *) -val coq_refl_equal : EConstr.t lazy_t -val coq_and : EConstr.t lazy_t -val coq_not : EConstr.t lazy_t -val coq_or : EConstr.t lazy_t -val coq_True : EConstr.t lazy_t -val coq_False : EConstr.t lazy_t -val coq_I : EConstr.t lazy_t - -(* from ReflOmegaCore/ZOmega *) - -val coq_t_int : EConstr.t lazy_t -val coq_t_plus : EConstr.t lazy_t -val coq_t_mult : EConstr.t lazy_t -val coq_t_opp : EConstr.t lazy_t -val coq_t_minus : EConstr.t lazy_t -val coq_t_var : EConstr.t lazy_t - -val coq_proposition : EConstr.t lazy_t -val coq_p_eq : EConstr.t lazy_t -val coq_p_leq : EConstr.t lazy_t -val coq_p_geq : EConstr.t lazy_t -val coq_p_lt : EConstr.t lazy_t -val coq_p_gt : EConstr.t lazy_t -val coq_p_neq : EConstr.t lazy_t -val coq_p_true : EConstr.t lazy_t -val coq_p_false : EConstr.t lazy_t -val coq_p_not : EConstr.t lazy_t -val coq_p_or : EConstr.t lazy_t -val coq_p_and : EConstr.t lazy_t -val coq_p_imp : EConstr.t lazy_t -val coq_p_prop : EConstr.t lazy_t - -val coq_s_bad_constant : EConstr.t lazy_t -val coq_s_divide : EConstr.t lazy_t -val coq_s_not_exact_divide : EConstr.t lazy_t -val coq_s_sum : EConstr.t lazy_t -val coq_s_merge_eq : EConstr.t lazy_t -val coq_s_split_ineq : EConstr.t lazy_t - -val coq_direction : EConstr.t lazy_t -val coq_d_left : EConstr.t lazy_t -val coq_d_right : EConstr.t lazy_t - -val coq_e_split : EConstr.t lazy_t -val coq_e_extract : EConstr.t lazy_t -val coq_e_solve : EConstr.t lazy_t - -val coq_interp_sequent : EConstr.t lazy_t -val coq_do_omega : EConstr.t lazy_t - -val mk_nat : int -> EConstr.t -val mk_N : int -> EConstr.t - -(** Precondition: the type of the list is in Set *) -val mk_list : EConstr.t -> EConstr.t list -> EConstr.t -val mk_plist : EConstr.types list -> EConstr.types - -(** Analyzing a coq term *) - -(* The generic result shape of the analysis of a term. - One-level depth, except when a number is found *) -type parse_term = - Tplus of EConstr.t * EConstr.t - | Tmult of EConstr.t * EConstr.t - | Tminus of EConstr.t * EConstr.t - | Topp of EConstr.t - | Tsucc of EConstr.t - | Tnum of Bigint.bigint - | Tother - -(* The generic result shape of the analysis of a relation. - One-level depth. *) -type parse_rel = - Req of EConstr.t * EConstr.t - | Rne of EConstr.t * EConstr.t - | Rlt of EConstr.t * EConstr.t - | Rle of EConstr.t * EConstr.t - | Rgt of EConstr.t * EConstr.t - | Rge of EConstr.t * EConstr.t - | Rtrue - | Rfalse - | Rnot of EConstr.t - | Ror of EConstr.t * EConstr.t - | Rand of EConstr.t * EConstr.t - | Rimp of EConstr.t * EConstr.t - | Riff of EConstr.t * EConstr.t - | Rother - -(* A module factorizing what we should now about the number representation *) -module type Int = - sig - (* the coq type of the numbers *) - val typ : EConstr.t Lazy.t - (* Is a constr expands to the type of these numbers *) - val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool - (* the operations on the numbers *) - val plus : EConstr.t Lazy.t - val mult : EConstr.t Lazy.t - val opp : EConstr.t Lazy.t - val minus : EConstr.t Lazy.t - (* building a coq number *) - val mk : Bigint.bigint -> EConstr.t - (* parsing a term (one level, except if a number is found) *) - val parse_term : Evd.evar_map -> EConstr.t -> parse_term - (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel - (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option - end - -(* Currently, we only use Z numbers *) -module Z : Int diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg deleted file mode 100644 index c1ce30027e..0000000000 --- a/plugins/romega/g_romega.mlg +++ /dev/null @@ -1,55 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - - -DECLARE PLUGIN "romega_plugin" - -{ - -open Ltac_plugin -open Names -open Refl_omega -open Stdarg - -let eval_tactic name = - let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in - let tac = Tacenv.interp_ltac kn in - Tacinterp.eval_tactic tac - -let romega_tactic unsafe l = - let tacs = List.map - (function - | "nat" -> eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs))) - (Tacticals.New.tclTHEN - (* because of the contradiction process in (r)omega, - we'd better leave as little as possible in the conclusion, - for an easier decidability argument. *) - (Tactics.intros) - (total_reflexive_omega_tactic unsafe)) - -} - -TACTIC EXTEND romega -| [ "romega" ] -> { romega_tactic false [] } -| [ "unsafe_romega" ] -> { romega_tactic true [] } -END - -TACTIC EXTEND romega' -| [ "romega" "with" ne_ident_list(l) ] -> - { romega_tactic false (List.map Names.Id.to_string l) } -| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } -END diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml deleted file mode 100644 index e603480656..0000000000 --- a/plugins/romega/refl_omega.ml +++ /dev/null @@ -1,1071 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - -open Pp -open Util -open Constr -open Const_omega -module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) -open OmegaSolver - -module Id = Names.Id -module IntSet = Int.Set -module IntHtbl = Hashtbl.Make(Int) - -(* \section{Useful functions and flags} *) -(* Especially useful debugging functions *) -let debug = ref false - -let show_goal = Tacticals.New.tclIDTAC - -let pp i = print_int i; print_newline (); flush stdout - -(* More readable than the prefix notation *) -let (>>) = Tacticals.New.tclTHEN - -(* \section{Types} - \subsection{How to walk in a term} - To represent how to get to a proposition. Only choice points are - kept (branch to choose in a disjunction and identifier of the disjunctive - connector) *) -type direction = Left of int | Right of int - -(* Step to find a proposition (operators are at most binary). A list is - a path *) -type occ_step = O_left | O_right | O_mono -type occ_path = occ_step list - -(* chemin identifiant une proposition sous forme du nom de l'hypothèse et - d'une liste de pas à partir de la racine de l'hypothèse *) -type occurrence = {o_hyp : Id.t; o_path : occ_path} - -type atom_index = int - -(* \subsection{reifiable formulas} *) -type oformula = - (* integer *) - | Oint of Bigint.bigint - (* recognized binary and unary operations *) - | Oplus of oformula * oformula - | Omult of oformula * oformula (* Invariant : one side is [Oint] *) - | Ominus of oformula * oformula - | Oopp of oformula - (* an atom in the environment *) - | Oatom of atom_index - -(* Operators for comparison recognized by Omega *) -type comparaison = Eq | Leq | Geq | Gt | Lt | Neq - -(* Representation of reified predicats (fragment of propositional calculus, - no quantifier here). *) -(* Note : in [Pprop p], the non-reified constr [p] should be closed - (it could contains some [Term.Var] but no [Term.Rel]). So no need to - lift when breaking or creating arrows. *) -type oproposition = - Pequa of EConstr.t * oequation (* constr = copy of the Coq formula *) - | Ptrue - | Pfalse - | Pnot of oproposition - | Por of int * oproposition * oproposition - | Pand of int * oproposition * oproposition - | Pimp of int * oproposition * oproposition - | Pprop of EConstr.t - -(* The equations *) -and oequation = { - e_comp: comparaison; (* comparaison *) - e_left: oformula; (* formule brute gauche *) - e_right: oformula; (* formule brute droite *) - e_origin: occurrence; (* l'hypothèse dont vient le terme *) - e_negated: bool; (* vrai si apparait en position nié - après normalisation *) - e_depends: direction list; (* liste des points de disjonction dont - dépend l'accès à l'équation avec la - direction (branche) pour y accéder *) - e_omega: OmegaSolver.afine (* normalized formula *) - } - -(* \subsection{Proof context} - This environment codes - \begin{itemize} - \item the terms and propositions that are given as - parameters of the reified proof (and are represented as variables in the - reified goals) - \item translation functions linking the decision procedure and the Coq proof - \end{itemize} *) - -type environment = { - (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : EConstr.t list; - (* La meme chose pour les propositions *) - mutable props : EConstr.t list; - (* Traduction des indices utilisés ici en les indices finaux utilisés par - * la tactique Omega après dénombrement des variables utiles *) - real_indices : int IntHtbl.t; - mutable cnt_connectors : int; - equations : oequation IntHtbl.t; - constructors : occurrence IntHtbl.t -} - -(* \subsection{Solution tree} - Définition d'une solution trouvée par Omega sous la forme d'un identifiant, - d'un ensemble d'équation dont dépend la solution et d'une trace *) - -type solution = { - s_index : int; - s_equa_deps : IntSet.t; - s_trace : OmegaSolver.action list } - -(* Arbre de solution résolvant complètement un ensemble de systèmes *) -type solution_tree = - Leaf of solution - (* un noeud interne représente un point de branchement correspondant à - l'élimination d'un connecteur générant plusieurs buts - (typ. disjonction). Le premier argument - est l'identifiant du connecteur *) - | Tree of int * solution_tree * solution_tree - -(* Représentation de l'environnement extrait du but initial sous forme de - chemins pour extraire des equations ou d'hypothèses *) - -type context_content = - CCHyp of occurrence - | CCEqua of int - -(** Some dedicated equality tests *) - -let occ_step_eq s1 s2 = match s1, s2 with -| O_left, O_left | O_right, O_right | O_mono, O_mono -> true -| _ -> false - -let rec oform_eq f f' = match f,f' with - | Oint i, Oint i' -> Bigint.equal i i' - | Oplus (f1,f2), Oplus (f1',f2') - | Omult (f1,f2), Omult (f1',f2') - | Ominus (f1,f2), Ominus (f1',f2') -> oform_eq f1 f1' && oform_eq f2 f2' - | Oopp f, Oopp f' -> oform_eq f f' - | Oatom a, Oatom a' -> Int.equal a a' - | _ -> false - -let dir_eq d d' = match d, d' with - | Left i, Left i' | Right i, Right i' -> Int.equal i i' - | _ -> false - -(* \section{Specific utility functions to handle base types} *) -(* Nom arbitraire de l'hypothèse codant la négation du but final *) -let id_concl = Id.of_string "__goal__" - -(* Initialisation de l'environnement de réification de la tactique *) -let new_environment () = { - terms = []; props = []; cnt_connectors = 0; - real_indices = IntHtbl.create 7; - equations = IntHtbl.create 7; - constructors = IntHtbl.create 7; -} - -(* Génération d'un nom d'équation *) -let new_connector_id env = - env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors - -(* Calcul de la branche complémentaire *) -let barre = function Left x -> Right x | Right x -> Left x - -(* Identifiant associé à une branche *) -let indice = function Left x | Right x -> x - -(* Affichage de l'environnement de réification (termes et propositions) *) -let print_env_reification env = - let rec loop c i = function - [] -> str " ===============================\n\n" - | t :: l -> - let sigma, env = Pfedit.get_current_context () in - let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ - loop c (succ i) l - in - let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in - let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in - Feedback.msg_debug (prop_info ++ fnl () ++ term_info) - -(* \subsection{Gestion des environnements de variable pour Omega} *) -(* generation d'identifiant d'equation pour Omega *) - -let new_omega_eq, rst_omega_eq = - let cpt = ref (-1) in - (function () -> incr cpt; !cpt), - (function () -> cpt:=(-1)) - -(* generation d'identifiant de variable pour Omega *) - -let new_omega_var, rst_omega_var, set_omega_maxvar = - let cpt = ref (-1) in - (function () -> incr cpt; !cpt), - (function () -> cpt:=(-1)), - (function n -> cpt:=n) - -(* Affichage des variables d'un système *) - -let display_omega_var i = Printf.sprintf "OV%d" i - -(* \subsection{Gestion des environnements de variable pour la réflexion} - Gestion des environnements de traduction entre termes des constructions - non réifiés et variables des termes reifies. Attention il s'agit de - l'environnement initial contenant tout. Il faudra le réduire après - calcul des variables utiles. *) - -let add_reified_atom sigma t env = - try List.index0 (EConstr.eq_constr sigma) t env.terms - with Not_found -> - let i = List.length env.terms in - env.terms <- env.terms @ [t]; i - -let get_reified_atom env = - try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom" - -(** When the omega resolution has created a variable [v], we re-sync - the environment with this new variable. To be done in the right order. *) - -let set_reified_atom v t env = - assert (Int.equal v (List.length env.terms)); - env.terms <- env.terms @ [t] - -(* \subsection{Gestion de l'environnement de proposition pour Omega} *) -(* ajout d'une proposition *) -let add_prop sigma env t = - try List.index0 (EConstr.eq_constr sigma) t env.props - with Not_found -> - let i = List.length env.props in env.props <- env.props @ [t]; i - -(* accès a une proposition *) -let get_prop v env = - try List.nth v env with Invalid_argument _ -> failwith "get_prop" - -(* \subsection{Gestion du nommage des équations} *) -(* Ajout d'une equation dans l'environnement de reification *) -let add_equation env e = - let id = e.e_omega.id in - if IntHtbl.mem env.equations id then () else IntHtbl.add env.equations id e - -(* accès a une equation *) -let get_equation env id = - try IntHtbl.find env.equations id - with Not_found as e -> - Printf.printf "Omega Equation %d non trouvée\n" id; raise e - -(* Affichage des termes réifiés *) -let rec oprint ch = function - | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n) - | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2 - | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2 - | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2 - | Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1 - | Oatom n -> Printf.fprintf ch "V%02d" n - -let print_comp = function - | Eq -> "=" | Leq -> "<=" | Geq -> ">=" - | Gt -> ">" | Lt -> "<" | Neq -> "!=" - -let rec pprint ch = function - Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 }) -> - Printf.fprintf ch "%a %s %a" oprint t1 (print_comp comp) oprint t2 - | Ptrue -> Printf.fprintf ch "TT" - | Pfalse -> Printf.fprintf ch "FF" - | Pnot t -> Printf.fprintf ch "not(%a)" pprint t - | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2 - | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2 - | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2 - | Pprop c -> Printf.fprintf ch "Prop" - -(* \subsection{Omega vers Oformula} *) - -let oformula_of_omega af = - let rec loop = function - | ({v=v; c=n}::r) -> Oplus(Omult(Oatom v,Oint n),loop r) - | [] -> Oint af.constant - in - loop af.body - -let app f v = EConstr.mkApp(Lazy.force f,v) - -(* \subsection{Oformula vers COQ reel} *) - -let coq_of_formula env t = - let rec loop = function - | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |] - | Oopp t -> app Z.opp [| loop t |] - | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |] - | Oint v -> Z.mk v - | Oatom var -> - (* attention ne traite pas les nouvelles variables si on ne les - * met pas dans env.term *) - get_reified_atom env var - | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in - loop t - -(* \subsection{Oformula vers COQ reifié} *) - -let reified_of_atom env i = - try IntHtbl.find env.real_indices i - with Not_found -> - Printf.printf "Atome %d non trouvé\n" i; - IntHtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; - raise Not_found - -let reified_binop = function - | Oplus _ -> app coq_t_plus - | Ominus _ -> app coq_t_minus - | Omult _ -> app coq_t_mult - | _ -> assert false - -let rec reified_of_formula env t = match t with - | Oplus (t1,t2) | Omult (t1,t2) | Ominus (t1,t2) -> - reified_binop t [| reified_of_formula env t1; reified_of_formula env t2 |] - | Oopp t -> app coq_t_opp [| reified_of_formula env t |] - | Oint v -> app coq_t_int [| Z.mk v |] - | Oatom i -> app coq_t_var [| mk_N (reified_of_atom env i) |] - -let reified_of_formula env f = - try reified_of_formula env f - with reraise -> oprint stderr f; raise reraise - -let reified_cmp = function - | Eq -> app coq_p_eq - | Leq -> app coq_p_leq - | Geq -> app coq_p_geq - | Gt -> app coq_p_gt - | Lt -> app coq_p_lt - | Neq -> app coq_p_neq - -let reified_conn = function - | Por _ -> app coq_p_or - | Pand _ -> app coq_p_and - | Pimp _ -> app coq_p_imp - | _ -> assert false - -let rec reified_of_oprop sigma env t = match t with - | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) -> - reified_cmp cmp [| reified_of_formula env t1; reified_of_formula env t2 |] - | Ptrue -> Lazy.force coq_p_true - | Pfalse -> Lazy.force coq_p_false - | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |] - | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) -> - reified_conn t - [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |] - | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |] - -let reified_of_proposition sigma env f = - try reified_of_oprop sigma env f - with reraise -> pprint stderr f; raise reraise - -let reified_of_eq env (l,r) = - app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |] - -(* \section{Opérations sur les équations} -Ces fonctions préparent les traces utilisées par la tactique réfléchie -pour faire des opérations de normalisation sur les équations. *) - -(* \subsection{Extractions des variables d'une équation} *) -(* Extraction des variables d'une équation. *) -(* Chaque fonction retourne une liste triée sans redondance *) - -let (@@) = IntSet.union - -let rec vars_of_formula = function - | Oint _ -> IntSet.empty - | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) - | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) - | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) - | Oopp e -> vars_of_formula e - | Oatom i -> IntSet.singleton i - -let rec vars_of_equations = function - | [] -> IntSet.empty - | e::l -> - (vars_of_formula e.e_left) @@ - (vars_of_formula e.e_right) @@ - (vars_of_equations l) - -let rec vars_of_prop = function - | Pequa(_,e) -> vars_of_equations [e] - | Pnot p -> vars_of_prop p - | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pprop _ | Ptrue | Pfalse -> IntSet.empty - -(* Normalized formulas : - - - sorted list of monomials, largest index first, - with non-null coefficients - - a constant coefficient - - /!\ Keep in sync with the corresponding functions in ReflOmegaCore ! -*) - -type nformula = - { coefs : (atom_index * Bigint.bigint) list; - cst : Bigint.bigint } - -let scale n { coefs; cst } = - { coefs = List.map (fun (v,k) -> (v,k*n)) coefs; - cst = cst*n } - -let shuffle nf1 nf2 = - let rec merge l1 l2 = match l1,l2 with - | [],_ -> l2 - | _,[] -> l1 - | (v1,k1)::r1,(v2,k2)::r2 -> - if Int.equal v1 v2 then - let k = k1+k2 in - if Bigint.equal k Bigint.zero then merge r1 r2 - else (v1,k) :: merge r1 r2 - else if v1 > v2 then (v1,k1) :: merge r1 l2 - else (v2,k2) :: merge l1 r2 - in - { coefs = merge nf1.coefs nf2.coefs; - cst = nf1.cst + nf2.cst } - -let rec normalize = function - | Oplus(t1,t2) -> shuffle (normalize t1) (normalize t2) - | Ominus(t1,t2) -> normalize (Oplus (t1, Oopp(t2))) - | Oopp(t) -> scale negone (normalize t) - | Omult(t,Oint n) | Omult (Oint n, t) -> - if Bigint.equal n Bigint.zero then { coefs = []; cst = zero } - else scale n (normalize t) - | Omult _ -> assert false (* invariant on Omult *) - | Oint n -> { coefs = []; cst = n } - | Oatom v -> { coefs = [v,Bigint.one]; cst=Bigint.zero} - -(* From normalized formulas to omega representations *) - -let omega_of_nformula env kind nf = - { id = new_omega_eq (); - kind; - constant=nf.cst; - body = List.map (fun (v,c) -> { v; c }) nf.coefs } - - -let negate_oper = function - Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq - -let normalize_equation env (negated,depends,origin,path) oper t1 t2 = - let mk_step t kind = - let equa = omega_of_nformula env kind (normalize t) in - { e_comp = oper; e_left = t1; e_right = t2; - e_negated = negated; e_depends = depends; - e_origin = { o_hyp = origin; o_path = List.rev path }; - e_omega = equa } - in - try match (if negated then (negate_oper oper) else oper) with - | Eq -> mk_step (Oplus (t1,Oopp t2)) EQUA - | Neq -> mk_step (Oplus (t1,Oopp t2)) DISE - | Leq -> mk_step (Oplus (t2,Oopp t1)) INEQ - | Geq -> mk_step (Oplus (t1,Oopp t2)) INEQ - | Lt -> mk_step (Oplus (Oplus(t2,Oint negone),Oopp t1)) INEQ - | Gt -> mk_step (Oplus (Oplus(t1,Oint negone),Oopp t2)) INEQ - with e when Logic.catchable_exception e -> raise e - -(* \section{Compilation des hypothèses} *) - -let mkPor i x y = Por (i,x,y) -let mkPand i x y = Pand (i,x,y) -let mkPimp i x y = Pimp (i,x,y) - -let rec oformula_of_constr sigma env t = - match Z.parse_term sigma t with - | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2 - | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2 - | Tmult (t1,t2) -> - (match Z.get_scalar sigma t1 with - | Some n -> Omult (Oint n,oformula_of_constr sigma env t2) - | None -> - match Z.get_scalar sigma t2 with - | Some n -> Omult (oformula_of_constr sigma env t1, Oint n) - | None -> Oatom (add_reified_atom sigma t env)) - | Topp t -> Oopp(oformula_of_constr sigma env t) - | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one) - | Tnum n -> Oint n - | Tother -> Oatom (add_reified_atom sigma t env) - -and binop sigma env c t1 t2 = - let t1' = oformula_of_constr sigma env t1 in - let t2' = oformula_of_constr sigma env t2 in - c t1' t2' - -and binprop sigma env (neg2,depends,origin,path) - add_to_depends neg1 gl c t1 t2 = - let i = new_connector_id env in - let depends1 = if add_to_depends then Left i::depends else depends in - let depends2 = if add_to_depends then Right i::depends else depends in - if add_to_depends then - IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; - let t1' = - oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in - let t2' = - oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in - (* On numérote le connecteur dans l'environnement. *) - c i t1' t2' - -and mk_equation sigma env ctxt c connector t1 t2 = - let t1' = oformula_of_constr sigma env t1 in - let t2' = oformula_of_constr sigma env t2 in - (* On ajoute l'equation dans l'environnement. *) - let omega = normalize_equation env ctxt connector t1' t2' in - add_equation env omega; - Pequa (c,omega) - -and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c = - match Z.parse_rel gl c with - | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2 - | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2 - | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2 - | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2 - | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2 - | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2 - | Rtrue -> Ptrue - | Rfalse -> Pfalse - | Rnot t -> - let ctxt' = (not negated, depends, origin,(O_mono::path)) in - Pnot (oproposition_of_constr sigma env ctxt' gl t) - | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2 - | Rand (t1,t2) -> binprop sigma env ctxt negated negated gl mkPand t1 t2 - | Rimp (t1,t2) -> - binprop sigma env ctxt (not negated) (not negated) gl mkPimp t1 t2 - | Riff (t1,t2) -> - (* No lifting here, since Omega only works on closed propositions. *) - binprop sigma env ctxt negated negated gl mkPand - (EConstr.mkArrow t1 t2) (EConstr.mkArrow t2 t1) - | _ -> Pprop c - -(* Destructuration des hypothèses et de la conclusion *) - -let display_gl env t_concl t_lhyps = - Printf.printf "REIFED PROBLEM\n\n"; - Printf.printf " CONCL: %a\n" pprint t_concl; - List.iter - (fun (i,_,t) -> Printf.printf " %s: %a\n" (Id.to_string i) pprint t) - t_lhyps; - print_env_reification env - -type defined = Defined | Assumed - -let reify_hyp sigma env gl i = - let open Context.Named.Declaration in - let ctxt = (false,[],i,[]) in - match Tacmach.New.pf_get_hyp i gl with - | LocalDef (_,d,t) when Z.is_int_typ gl t -> - let dummy = Lazy.force coq_True in - let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in - i,Defined,p - | LocalDef (_,_,t) | LocalAssum (_,t) -> - let p = oproposition_of_constr sigma env ctxt gl t in - i,Assumed,p - -let reify_gl env gl = - let sigma = Proofview.Goal.sigma gl in - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_ids_of_hyps gl in - let ctxt_concl = (true,[],id_concl,[O_mono]) in - let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in - let t_lhyps = List.map (reify_hyp sigma env gl) hyps in - let () = if !debug then display_gl env t_concl t_lhyps in - t_concl, t_lhyps - -let rec destruct_pos_hyp eqns = function - | Pequa (_,e) -> [e :: eqns] - | Ptrue | Pfalse | Pprop _ -> [eqns] - | Pnot t -> destruct_neg_hyp eqns t - | Por (_,t1,t2) -> - let s1 = destruct_pos_hyp eqns t1 in - let s2 = destruct_pos_hyp eqns t2 in - s1 @ s2 - | Pand(_,t1,t2) -> - List.map_append - (fun le1 -> destruct_pos_hyp le1 t2) - (destruct_pos_hyp eqns t1) - | Pimp(_,t1,t2) -> - let s1 = destruct_neg_hyp eqns t1 in - let s2 = destruct_pos_hyp eqns t2 in - s1 @ s2 - -and destruct_neg_hyp eqns = function - | Pequa (_,e) -> [e :: eqns] - | Ptrue | Pfalse | Pprop _ -> [eqns] - | Pnot t -> destruct_pos_hyp eqns t - | Pand (_,t1,t2) -> - let s1 = destruct_neg_hyp eqns t1 in - let s2 = destruct_neg_hyp eqns t2 in - s1 @ s2 - | Por(_,t1,t2) -> - List.map_append - (fun le1 -> destruct_neg_hyp le1 t2) - (destruct_neg_hyp eqns t1) - | Pimp(_,t1,t2) -> - List.map_append - (fun le1 -> destruct_neg_hyp le1 t2) - (destruct_pos_hyp eqns t1) - -let rec destructurate_hyps = function - | [] -> [[]] - | (i,_,t) :: l -> - let l_syst1 = destruct_pos_hyp [] t in - let l_syst2 = destructurate_hyps l in - List.cartesian (@) l_syst1 l_syst2 - -(* \subsection{Affichage d'un système d'équation} *) - -(* Affichage des dépendances de système *) -let display_depend = function - Left i -> Printf.printf " L%d" i - | Right i -> Printf.printf " R%d" i - -let display_systems syst_list = - let display_omega om_e = - Printf.printf " E%d : %a %s 0\n" - om_e.id - (fun _ -> display_eq display_omega_var) - (om_e.body, om_e.constant) - (operator_of_eq om_e.kind) in - - let display_equation oformula_eq = - pprint stdout (Pequa (Lazy.force coq_I,oformula_eq)); print_newline (); - display_omega oformula_eq.e_omega; - Printf.printf " Depends on:"; - List.iter display_depend oformula_eq.e_depends; - Printf.printf "\n Path: %s" - (String.concat "" - (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M") - oformula_eq.e_origin.o_path)); - Printf.printf "\n Origin: %s (negated : %s)\n\n" - (Id.to_string oformula_eq.e_origin.o_hyp) - (if oformula_eq.e_negated then "yes" else "no") in - - let display_system syst = - Printf.printf "=SYSTEM===================================\n"; - List.iter display_equation syst in - List.iter display_system syst_list - -(* Extraction des prédicats utilisées dans une trace. Permet ensuite le - calcul des hypothèses *) - -let rec hyps_used_in_trace = function - | [] -> IntSet.empty - | act :: l -> - match act with - | HYP e -> IntSet.add e.id (hyps_used_in_trace l) - | SPLIT_INEQ (_,(_,act1),(_,act2)) -> - hyps_used_in_trace act1 @@ hyps_used_in_trace act2 - | _ -> hyps_used_in_trace l - -(** Retreive variables declared as extra equations during resolution - and declare them into the environment. - We should consider these variables in their introduction order, - otherwise really bad things will happen. *) - -let state_cmp x y = Int.compare x.st_var y.st_var - -module StateSet = - Set.Make (struct type t = state_action let compare = state_cmp end) - -let rec stated_in_trace = function - | [] -> StateSet.empty - | [SPLIT_INEQ (_,(_,t1),(_,t2))] -> - StateSet.union (stated_in_trace t1) (stated_in_trace t2) - | STATE action :: l -> StateSet.add action (stated_in_trace l) - | _ :: l -> stated_in_trace l - -let rec stated_in_tree = function - | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) - | Leaf s -> stated_in_trace s.s_trace - -let mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|] - -let digest_stated_equations env tree = - let do_equation st (vars,gens,eqns,ids) = - (** We turn the definition of [v] - - into a reified formula : *) - let v_def = oformula_of_omega st.st_def in - (** - into a concrete Coq formula - (this uses only older vars already in env) : *) - let coq_v = coq_of_formula env v_def in - (** We then update the environment *) - set_reified_atom st.st_var coq_v env; - (** The term we'll introduce *) - let term_to_generalize = mk_refl coq_v in - (** Its representation as equation (but not reified yet, - we lack the proper env to do that). *) - let term_to_reify = (v_def,Oatom st.st_var) in - (st.st_var::vars, - term_to_generalize::gens, - term_to_reify::eqns, - CCEqua st.st_def.id :: ids) - in - let (vars,gens,eqns,ids) = - StateSet.fold do_equation (stated_in_tree tree) ([],[],[],[]) - in - (List.rev vars, List.rev gens, List.rev eqns, List.rev ids) - -(* Calcule la liste des éclatements à réaliser sur les hypothèses - nécessaires pour extraire une liste d'équations donnée *) - -(* PL: experimentally, the result order of the following function seems - _very_ crucial for efficiency. No idea why. Do not remove the List.rev - or modify the current semantics of Util.List.union (some elements of first - arg, then second arg), unless you know what you're doing. *) - -let rec get_eclatement env = function - | [] -> [] - | i :: r -> - let l = try (get_equation env i).e_depends with Not_found -> [] in - List.union dir_eq (List.rev l) (get_eclatement env r) - -let select_smaller l = - let comp (_,x) (_,y) = Int.compare (List.length x) (List.length y) in - try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller" - -let filter_compatible_systems required systems = - let rec select = function - | [] -> [] - | (x::l) -> - if List.mem_f dir_eq x required then select l - else if List.mem_f dir_eq (barre x) required then raise Exit - else x :: select l - in - List.map_filter - (function (sol, splits) -> - try Some (sol, select splits) with Exit -> None) - systems - -let rec equas_of_solution_tree = function - | Tree(_,t1,t2) -> - (equas_of_solution_tree t1)@@(equas_of_solution_tree t2) - | Leaf s -> s.s_equa_deps - -(** [maximize_prop] pushes useless props in a new Pprop atom. - The reified formulas get shorter, but be careful with decidabilities. - For instance, anything that contains a Pprop is considered to be - undecidable in [ReflOmegaCore], whereas a Pfalse for instance at - the same spot will lead to a decidable formula. - In particular, do not use this function on the conclusion. - Even in hypotheses, we could probably build pathological examples - that romega won't handle correctly, but they should be pretty rare. -*) - -let maximize_prop equas c = - let rec loop c = match c with - | Pequa(t,e) -> if IntSet.mem e.e_omega.id equas then c else Pprop t - | Pnot t -> - (match loop t with - | Pprop p -> Pprop (app coq_not [|p|]) - | t' -> Pnot t') - | Por(i,t1,t2) -> - (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (app coq_or [|p1;p2|]) - | t1', t2' -> Por(i,t1',t2')) - | Pand(i,t1,t2) -> - (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (app coq_and [|p1;p2|]) - | t1', t2' -> Pand(i,t1',t2')) - | Pimp(i,t1,t2) -> - (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (EConstr.mkArrow p1 p2) (* no lift (closed) *) - | t1', t2' -> Pimp(i,t1',t2')) - | Ptrue -> Pprop (app coq_True [||]) - | Pfalse -> Pprop (app coq_False [||]) - | Pprop _ -> c - in loop c - -let rec display_solution_tree ch = function - Leaf t -> - output_string ch - (Printf.sprintf "%d[%s]" - t.s_index - (String.concat " " (List.map string_of_int - (IntSet.elements t.s_equa_deps)))) - | Tree(i,t1,t2) -> - Printf.fprintf ch "S%d(%a,%a)" i - display_solution_tree t1 display_solution_tree t2 - -let rec solve_with_constraints all_solutions path = - let rec build_tree sol buf = function - [] -> Leaf sol - | (Left i :: remainder) -> - Tree(i, - build_tree sol (Left i :: buf) remainder, - solve_with_constraints all_solutions (List.rev(Right i :: buf))) - | (Right i :: remainder) -> - Tree(i, - solve_with_constraints all_solutions (List.rev (Left i :: buf)), - build_tree sol (Right i :: buf) remainder) in - let weighted = filter_compatible_systems path all_solutions in - let (winner_sol,winner_deps) = - try select_smaller weighted - with reraise -> - Printf.printf "%d - %d\n" - (List.length weighted) (List.length all_solutions); - List.iter display_depend path; raise reraise - in - build_tree winner_sol (List.rev path) winner_deps - -let find_path {o_hyp=id;o_path=p} env = - let rec loop_path = function - ([],l) -> Some l - | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2) - | _ -> None in - let rec loop_id i = function - CCHyp{o_hyp=id';o_path=p'} :: l when Id.equal id id' -> - begin match loop_path (p',p) with - Some r -> i,r - | None -> loop_id (succ i) l - end - | _ :: l -> loop_id (succ i) l - | [] -> failwith "find_path" in - loop_id 0 env - -let mk_direction_list l = - let trans = function - | O_left -> Some (Lazy.force coq_d_left) - | O_right -> Some (Lazy.force coq_d_right) - | O_mono -> None (* No more [D_mono] constructor now *) - in - mk_list (Lazy.force coq_direction) (List.map_filter trans l) - - -(* \section{Rejouer l'historique} *) - -let hyp_idx env_hyp i = - let rec loop count = function - | [] -> failwith (Printf.sprintf "get_hyp %d" i) - | CCEqua i' :: _ when Int.equal i i' -> mk_nat count - | _ :: l -> loop (succ count) l - in loop 0 env_hyp - - -(* We now expand NEGATE_CONTRADICT and CONTRADICTION into - a O_SUM followed by a O_BAD_CONSTANT *) - -let sum_bad inv i1 i2 = - let open EConstr in - mkApp (Lazy.force coq_s_sum, - [| Z.mk Bigint.one; i1; - Z.mk (if inv then negone else Bigint.one); i2; - mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|]) - -let rec reify_trace env env_hyp = - let open EConstr in - function - | CONSTANT_NOT_NUL(e,_) :: [] - | CONSTANT_NEG(e,_) :: [] - | CONSTANT_NUL e :: [] -> - mkApp (Lazy.force coq_s_bad_constant,[| hyp_idx env_hyp e |]) - | NEGATE_CONTRADICT(e1,e2,direct) :: [] -> - sum_bad direct (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id) - | CONTRADICTION (e1,e2) :: [] -> - sum_bad false (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id) - | NOT_EXACT_DIVIDE (e1,k) :: [] -> - mkApp (Lazy.force coq_s_not_exact_divide, - [| hyp_idx env_hyp e1.id; Z.mk k |]) - | DIVIDE_AND_APPROX (e1,_,k,_) :: l - | EXACT_DIVIDE (e1,k) :: l -> - mkApp (Lazy.force coq_s_divide, - [| hyp_idx env_hyp e1.id; Z.mk k; - reify_trace env env_hyp l |]) - | MERGE_EQ(e3,e1,e2) :: l -> - mkApp (Lazy.force coq_s_merge_eq, - [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2; - reify_trace env (CCEqua e3:: env_hyp) l |]) - | SUM(e3,(k1,e1),(k2,e2)) :: l -> - mkApp (Lazy.force coq_s_sum, - [| Z.mk k1; hyp_idx env_hyp e1.id; - Z.mk k2; hyp_idx env_hyp e2.id; - reify_trace env (CCEqua e3 :: env_hyp) l |]) - | STATE {st_new_eq; st_def; st_orig; st_coef } :: l -> - (* we now produce a [O_SUM] here *) - mkApp (Lazy.force coq_s_sum, - [| Z.mk Bigint.one; hyp_idx env_hyp st_orig.id; - Z.mk st_coef; hyp_idx env_hyp st_def.id; - reify_trace env (CCEqua st_new_eq.id :: env_hyp) l |]) - | HYP _ :: l -> reify_trace env env_hyp l - | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ -> - let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in - let r2 = reify_trace env (CCEqua e2 :: env_hyp) l2 in - mkApp (Lazy.force coq_s_split_ineq, - [| hyp_idx env_hyp e.id; r1 ; r2 |]) - | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> reify_trace env env_hyp l - | WEAKEN _ :: l -> failwith "not_treated" - | _ -> failwith "bad history" - -let rec decompose_tree env ctxt = function - Tree(i,left,right) -> - let org = - try IntHtbl.find env.constructors i - with Not_found -> - failwith (Printf.sprintf "Cannot find constructor %d" i) in - let (index,path) = find_path org ctxt in - let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in - let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in - app coq_e_split - [| mk_nat index; - mk_direction_list path; - decompose_tree env (left_hyp::ctxt) left; - decompose_tree env (right_hyp::ctxt) right |] - | Leaf s -> - decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps) -and decompose_tree_hyps trace env ctxt = function - [] -> app coq_e_solve [| reify_trace env ctxt trace |] - | (i::l) -> - let equation = - try IntHtbl.find env.equations i - with Not_found -> - failwith (Printf.sprintf "Cannot find equation %d" i) in - let (index,path) = find_path equation.e_origin ctxt in - let cont = - decompose_tree_hyps trace env - (CCEqua equation.e_omega.id :: ctxt) l in - app coq_e_extract [|mk_nat index; mk_direction_list path; cont |] - -let solve_system env index list_eq = - let system = List.map (fun eq -> eq.e_omega) list_eq in - let trace = - OmegaSolver.simplify_strong - (new_omega_eq,new_omega_var,display_omega_var) - system - in - (* Hypotheses used for this solution *) - let vars = hyps_used_in_trace trace in - let splits = get_eclatement env (IntSet.elements vars) in - if !debug then - begin - Printf.printf "SYSTEME %d\n" index; - display_action display_omega_var trace; - print_string "\n Depend :"; - IntSet.iter (fun i -> Printf.printf " %d" i) vars; - print_string "\n Split points :"; - List.iter display_depend splits; - Printf.printf "\n------------------------------------\n" - end; - {s_index = index; s_trace = trace; s_equa_deps = vars}, splits - -(* \section{La fonction principale} *) - (* Cette fonction construit la -trace pour la procédure de décision réflexive. A partir des résultats -de l'extraction des systèmes, elle lance la résolution par Omega, puis -l'extraction d'un ensemble minimal de solutions permettant la -résolution globale du système et enfin construit la trace qui permet -de faire rejouer cette solution par la tactique réflexive. *) - -let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = - if !debug then Printf.printf "\n====================================\n"; - let all_solutions = List.mapi (solve_system env) systems_list in - let solution_tree = solve_with_constraints all_solutions [] in - if !debug then begin - display_solution_tree stdout solution_tree; - print_newline() - end; - (** Collect all hypotheses and variables used in the solution tree *) - let useful_equa_ids = equas_of_solution_tree solution_tree in - let useful_hypnames, useful_vars = - IntSet.fold - (fun i (hyps,vars) -> - let e = get_equation env i in - Id.Set.add e.e_origin.o_hyp hyps, - vars_of_equations [e] @@ vars) - useful_equa_ids - (Id.Set.empty, vars_of_prop reified_concl) - in - let useful_hypnames = - Id.Set.elements (Id.Set.remove id_concl useful_hypnames) - in - - (** Parts coming from equations introduced by omega: *) - let stated_vars, l_generalize_arg, to_reify_stated, hyp_stated_vars = - digest_stated_equations env solution_tree - in - (** The final variables are either coming from: - - useful hypotheses (and conclusion) - - equations introduced during resolution *) - let all_vars_env = (IntSet.elements useful_vars) @ stated_vars - in - (** We prepare the renumbering from all variables to useful ones. - Since [all_var_env] is sorted, this renumbering will preserve - order: this way, the equations in ReflOmegaCore will have - the same normal forms as here. *) - let reduced_term_env = - let rec loop i = function - | [] -> [] - | var :: l -> - let t = get_reified_atom env var in - IntHtbl.add env.real_indices var i; t :: loop (succ i) l - in - mk_list (Lazy.force Z.typ) (loop 0 all_vars_env) - in - (** The environment [env] (and especially [env.real_indices]) is now - ready for the coming reifications: *) - let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in - let reified_concl = reified_of_proposition sigma env reified_concl in - let l_reified_terms = - List.map - (fun id -> - match Id.Map.find id reified_hyps with - | Defined,p -> - reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id) - | Assumed,p -> - reified_of_proposition sigma env (maximize_prop useful_equa_ids p), - EConstr.mkVar id - | exception Not_found -> assert false) - useful_hypnames - in - let l_reified_terms, l_reified_hypnames = List.split l_reified_terms in - let env_props_reified = mk_plist env.props in - let reified_goal = - mk_list (Lazy.force coq_proposition) - (l_reified_stated @ l_reified_terms) in - let reified = - app coq_interp_sequent - [| reified_concl;env_props_reified;reduced_term_env;reified_goal|] - in - let mk_occ id = {o_hyp=id;o_path=[]} in - let initial_context = - List.map (fun id -> CCHyp (mk_occ id)) useful_hypnames in - let context = - CCHyp (mk_occ id_concl) :: hyp_stated_vars @ initial_context in - let decompose_tactic = decompose_tree env context solution_tree in - - Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check reified DEFAULTcast >> - Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> - show_goal >> - (if unsafe then - (* Trust the produced term. Faster, but might fail later at Qed. - Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast - else - Tactics.normalise_vm_in_concl) >> - Tactics.apply (Lazy.force coq_I) - -let total_reflexive_omega_tactic unsafe = - Proofview.Goal.nf_enter begin fun gl -> - Coqlib.check_required_library ["Coq";"romega";"ROmega"]; - rst_omega_eq (); - rst_omega_var (); - try - let env = new_environment () in - let (concl,hyps) = reify_gl env gl in - (* Register all atom indexes created during reification as omega vars *) - set_omega_maxvar (pred (List.length env.terms)); - let full_reified_goal = (id_concl,Assumed,Pnot concl) :: hyps in - let systems_list = destructurate_hyps full_reified_goal in - let hyps = - List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps - in - if !debug then display_systems systems_list; - let sigma = Proofview.Goal.sigma gl in - resolution unsafe sigma env (concl,hyps) systems_list - with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") - end - diff --git a/plugins/romega/romega_plugin.mlpack b/plugins/romega/romega_plugin.mlpack deleted file mode 100644 index 38d0e94111..0000000000 --- a/plugins/romega/romega_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Const_omega -Refl_omega -G_romega diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune new file mode 100644 index 0000000000..233845ae0f --- /dev/null +++ b/plugins/rtauto/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name rtauto_plugin) + (public_name coq.plugins.rtauto) + (synopsis "Coq's rtauto plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index d9e32dbbf8..ce115f564f 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -19,6 +19,7 @@ Section MakeFieldPol. (* Field elements : R *) Variable R:Type. +Declare Scope R_scope. Bind Scope R_scope with R. Delimit Scope R_scope with ring. Local Open Scope R_scope. @@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth. (* Coefficients : C *) Variable C: Type. +Declare Scope C_scope. Bind Scope C_scope with C. Delimit Scope C_scope with coef. @@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N). (* Polynomial expressions : (PExpr C) *) +Declare Scope PE_scope. Bind Scope PE_scope with PExpr. Delimit Scope PE_scope with poly. diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 523c7b02eb..1ca6227f25 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. - Local Open Scope ZMORPHISM. + Declare Scope ZMORPHISM. + Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index a9b4d9d6f4..920b13ef49 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -12,7 +12,6 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Require Import Quote. Declare ML Module "newring_plugin". Require Export Ring_theory. Require Export Ring_tac. diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index e8efb362e2..26fef99bb2 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -15,7 +15,6 @@ Require Import Ring_polynom. Require Import BinList. Require Export ListTactics. Require Import InitialRing. -Require Import Quote. Declare ML Module "newring_plugin". diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a736eec5e7..b05e1e85b7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -99,7 +99,7 @@ let protect_tac_in map id = let rec closed_under sigma cset t = try let (gr, _) = Termops.global_of_constr sigma t in - Refset_env.mem gr cset + GlobRef.Set_env.mem gr cset with Not_found -> match EConstr.kind sigma t with | Cast(c,_,_) -> closed_under sigma cset c @@ -111,7 +111,7 @@ let closed_term args _ = match args with let t = Option.get (Value.to_constr t) in let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in Proofview.tclEVARMAP >>= fun sigma -> - let cs = List.fold_right Refset_env.add l Refset_env.empty in + let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) | _ -> assert false diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune new file mode 100644 index 0000000000..101246e28f --- /dev/null +++ b/plugins/setoid_ring/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name newring_plugin) + (public_name coq.plugins.setoid_ring) + (synopsis "Coq's setoid ring plugin") + (libraries coq.plugins.quote)) diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune new file mode 100644 index 0000000000..de9053f1a0 --- /dev/null +++ b/plugins/ssr/plugin_base.dune @@ -0,0 +1,6 @@ +(library + (name ssreflect_plugin) + (public_name coq.plugins.ssreflect) + (synopsis "Coq's ssreflect plugin") + (modules_without_implementation ssrast) + (libraries coq.plugins.ssrmatching)) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 54f3f9c718..f2f236f448 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -469,7 +469,7 @@ let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac (* term mkApp (t', args) is convertible to t. *) (* This makes a useful shorthand for local definitions in proofs, *) (* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *) -(* and, in context of the the 4CT library, pose mid := maps id means *) +(* and, in context of the 4CT library, pose mid := maps id means *) (* pose mid := fun d : detaSet => @maps d d (@id (datum d)) *) (* Note that this facility does not extend to set, which tries *) (* instead to fill holes by matching a goal subterm. *) @@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;; (** Basic tactics *) -let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl -> +let rec fst_prod red tac = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in match EConstr.kind (Proofview.Goal.sigma gl) concl with | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b4144aa45e..460bdc6d23 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,6 +86,7 @@ Export SsrSyntax. (* recognize the expansion of the boolean if; using the default printer *) (* avoids a spurrious trailing %GEN_IF. *) +Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. Notation "'if' c 'then' v1 'else' v2" := @@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (* Force boolean interpretation of simple if expressions. *) +Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. Notation "'if' c 'return' t 'then' v1 'else' v2" := @@ -125,6 +127,7 @@ Open Scope boolean_if_scope. (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) (* Lists library) should be loaded before ssreflect so that their notations *) (* do not mask all ssreflect forms. *) +Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index fbe3b000fb..602fcfcab5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -293,7 +293,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let c, cl, ucst = match_pat env p occ h cl in let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in - let gl = try pf_unify_HO gl inf_t c with _ -> error gl c inf_t in + let gl = try pf_unify_HO gl inf_t c + with exn when CErrors.noncritical exn -> error gl c inf_t in cl, gl, post with | NoMatch | NoProgress -> @@ -302,7 +303,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let e = EConstr.of_constr e in let n, e, _, _ucst = pf_abs_evars gl (fst p, e) in let e, _, _, gl = pf_saturate ~beta:true gl e n in - let gl = try pf_unify_HO gl inf_t e with _ -> error gl e inf_t in + let gl = try pf_unify_HO gl inf_t e + with exn when CErrors.noncritical exn -> error gl e inf_t in cl, gl, post in let rec match_all concl gl patterns = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 23cbf49c05..f23433f2f4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -115,7 +115,8 @@ let newssrcongrtac arg ist 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 = - match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with + match try Some (pf_unify_HO gl_c (pf_concl gl) c) + with exn when CErrors.noncritical exn -> None with | Some gl_c -> tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) (t_ok (proj gl_c)) gl diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b2d5143e36..99ff943e61 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -216,6 +216,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. @@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y) Notation "@^~ x" := (fun f => f x) (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index e367cd32d6..f67cf20e49 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) (** Defined identifier *) - -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let ssrposetac (id, (_, t)) gl = let ist, t = diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 46fde41150..1dbacf0ff7 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -379,8 +379,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = let ctx, last = EConstr.decompose_prod_assum sigma concl in let args = match EConstr.kind_of_type sigma last with | Term.AtomicType (hd, args) -> - assert(Ssrcommon.is_protect hd env sigma); - args + if Ssrcommon.is_protect hd env sigma then args + else Ssrcommon.errorstrm + (Pp.str "Too many names in intro pattern") | _ -> assert false in let case = args.(Array.length args-1) in if not(EConstr.Vars.closed0 sigma case) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 8b9c94f2db..e4a0910673 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -342,7 +342,7 @@ let interp_index ist gl idx = open Pltac -ARGUMENT EXTEND ssrindex TYPED AS ssrindex PRINTED BY pr_ssrindex +ARGUMENT EXTEND ssrindex PRINTED BY pr_ssrindex INTERPRETED BY interp_index | [ int_or_var(i) ] -> [ mk_index ~loc i ] END @@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg END let vmexacttac pf = - Goal.nf_enter begin fun gl -> + Goal.enter begin fun gl -> exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 83581f3416..f12f9fac0f 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Locusops open Ssrast open Ssrcommon @@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq = let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let hidetacs clseq idhide cl0 = if not (hidden_clseq clseq) then [] else diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune new file mode 100644 index 0000000000..06f67c3774 --- /dev/null +++ b/plugins/ssrmatching/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name ssrmatching_plugin) + (public_name coq.plugins.ssrmatching) + (synopsis "Coq ssrmatching plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 30a998c6ce..aadb4fe5f6 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -291,7 +291,10 @@ let unif_EQ_args env sigma pa a = prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a ;; -let unif_HO env ise p c = Evarconv.the_conv_x env p c ise +let unif_HO env ise p c = + try Evarconv.the_conv_x env p c ise + with Evarconv.UnableToUnify(ise, err) -> + raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) let unif_HO_args env ise0 pa i ca = let n = Array.length pa in @@ -1363,7 +1366,7 @@ let ssrpatterntac _ist arg gl = let concl0 = pf_concl gl in let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = - fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in + fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 829ee05e11..9a53e1dd1a 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0). Reserved Notation "( a 'in' b 'in' c )" (at level 0). Reserved Notation "( a 'as' b 'in' c )" (at level 0). +Declare Scope ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + (* Notation to define shortcuts for the "X in t" part of a pattern. *) Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. -Delimit Scope ssrpatternscope with pattern. (* Some shortcuts for recurrent "X in t" parts. *) Notation RHS := (X in _ = X)%pattern. diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 47a59ba631..53153198f9 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -83,8 +83,18 @@ let make_ascii_string n = let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "char_scope" - (ascii_path,ascii_module) - interp_ascii_string - ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + let sc = "char_scope" in + register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_interp_info = Uid sc; + pt_required = (ascii_path,ascii_module); + pt_refs = [static_glob_Ascii]; + pt_in_match = true } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 new file mode 100644 index 0000000000..55f61a58f9 --- /dev/null +++ b/plugins/syntax/g_numeral.ml4 @@ -0,0 +1,38 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +DECLARE PLUGIN "numeral_notation_plugin" + +open Notation +open Numeral +open Pp +open Names +open Vernacinterp +open Ltac_plugin +open Stdarg +open Pcoq.Prim + +let pr_numnot_option _ _ _ = function + | Nop -> mt () + | Warning n -> str "(warning after " ++ str n ++ str ")" + | Abstract n -> str "(abstract after " ++ str n ++ str ")" + +ARGUMENT EXTEND numnotoption + PRINTED BY pr_numnot_option +| [ ] -> [ Nop ] +| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ] +| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ] +END + +VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF + | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ] +END diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index f10f98e23b..e34a401c2c 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -96,10 +96,19 @@ let uninterp_int31 (AnyGlobConstr i) = with Non_closed -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + (* Actually declares the interpreter for int31 *) -let _ = Notation.declare_numeral_interpreter int31_scope - (int31_path, int31_module) - interp_int31 - ([DAst.make (GRef (int31_construct, None))], - uninterp_int31, - true) + +let _ = + register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = int31_scope; + pt_interp_info = Uid int31_scope; + pt_required = (int31_path,int31_module); + pt_refs = [int31_construct]; + pt_in_match = true } diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml deleted file mode 100644 index 0e202be47f..0000000000 --- a/plugins/syntax/n_syntax.ml +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Pp -open CErrors -open Names -open Bigint -open Positive_syntax_plugin.Positive_syntax - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "n_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(**********************************************************************) -(* Parsing N via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -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) - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let n_kn = make_kn (make_dir binnums) (Id.of_string "N") -let glob_n = IndRef (n_kn,0) -let path_of_N0 = ((n_kn,0),1) -let path_of_Npos = ((n_kn,0),2) -let glob_N0 = ConstructRef path_of_N0 -let glob_Npos = ConstructRef path_of_Npos - -let n_path = make_path binnums "N" - -let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ - if not (Bigint.equal n zero) then - GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) - else - GRef(glob_N0, None) - -let error_negative ?loc = - user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") - -let n_of_int ?loc n = - if is_pos_or_zero n then n_of_binnat ?loc true n - else error_negative ?loc - -(**********************************************************************) -(* Printing N via scopes *) -(**********************************************************************) - -let bignat_of_n n = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a - | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero - | _ -> raise Non_closed_number - ) n - -let uninterp_n (AnyGlobConstr p) = - try Some (bignat_of_n p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for N *) - -let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnums) - n_of_int - ([DAst.make @@ GRef (glob_N0, None); - DAst.make @@ GRef (glob_Npos, None)], - uninterp_n, - true) diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack deleted file mode 100644 index 4c56645f07..0000000000 --- a/plugins/syntax/n_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -N_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml deleted file mode 100644 index e158e0b516..0000000000 --- a/plugins/syntax/nat_syntax.ml +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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 = "nat_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* This file defines the printer for natural numbers in [nat] *) - -(*i*) -open Pp -open CErrors -open Names -open Glob_term -open Bigint -open Coqlib -(*i*) - -(**********************************************************************) -(* Parsing via scopes *) -(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) - -let threshold = of_int 5000 - -let warn_large_nat = - CWarnings.create ~name:"large-nat" ~category:"numbers" - (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in nat (observed threshold " ++ - strbrk "may vary from 5000 to 70000 depending on your system " ++ - strbrk "limits and on the command executed).") - -let nat_of_int ?loc n = - if is_pos_or_zero n then begin - if less_than threshold n then warn_large_nat (); - let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in - let rec mk_nat acc n = - if n <> zero then - mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) - else - acc - in - mk_nat ref_O n - end - else - user_err ?loc ~hdr:"nat_of_int" - (str "Cannot interpret a negative number as a number of type nat") - -(************************************************************************) -(* Printing via scopes *) - -exception Non_closed_number - -let rec int_of_nat x = DAst.with_val (function - | GApp (r, [a]) -> - begin match DAst.get r with - | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a) - | _ -> raise Non_closed_number - end - | GRef (z,_) when GlobRef.equal z glob_O -> zero - | _ -> raise Non_closed_number - ) x - -let uninterp_nat (AnyGlobConstr p) = - try - Some (int_of_nat p) - with - Non_closed_number -> None - -(************************************************************************) -(* Declare the primitive parsers and printers *) - -let _ = - Notation.declare_numeral_interpreter "nat_scope" - (nat_path,datatypes_module_name) - nat_of_int - ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack deleted file mode 100644 index 39bdd62f47..0000000000 --- a/plugins/syntax/nat_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Nat_syntax diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml new file mode 100644 index 0000000000..10a0af0b8f --- /dev/null +++ b/plugins/syntax/numeral.ml @@ -0,0 +1,142 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +open Pp +open Util +open Names +open Libnames +open Globnames +open Constrexpr +open Constrexpr_ops +open Notation + +(** * Numeral notation *) + +let warn_abstract_large_num_no_op = + CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" + (fun f -> + strbrk "The 'abstract after' directive has no effect when " ++ + strbrk "the parsing function (" ++ + Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ + strbrk "option type.") + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + +let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" +let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" +let q_int = qualid_of_string "Coq.Init.Decimal.int" +let q_uint = qualid_of_string "Coq.Init.Decimal.uint" +let q_option = qualid_of_string "Coq.Init.Datatypes.option" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + +let locate_ind q = + try unsafe_locate_ind q + with Not_found -> Nametab.error_global_not_found q + +let locate_z () = + try + Some { z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_positive } + with Not_found -> None + +let locate_int () = + { uint = locate_ind q_uint; + int = locate_ind q_int } + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty loadZ = + CErrors.user_err + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let type_error_of g ty loadZ = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ + str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let vernac_numeral_notation local ty f g scope opts = + let int_ty = locate_int () in + let z_pos_ty = locate_z () in + let tyc = Smartlocate.global_inductive_with_alias 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 + let app x y = mkAppC (x,[y]) in + let cref q = mkRefC q in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + in + let cZ = cref q_z in + let cint = cref q_int in + let cuint = cref q_uint in + let coption = cref q_option in + let opt r = app coption r in + let constructors = get_constructors tyc in + (* Check the type of f *) + let to_kind = + if has_type f (arrow cint cty) then Int int_ty, Direct + else if has_type f (arrow cint (opt cty)) then Int int_ty, Option + else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct + else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type f (arrow cZ cty) then Z z_pos_ty, Direct + else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option + else type_error_to f ty false + | None -> type_error_to f ty true + in + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty cint) then Int int_ty, Direct + else if has_type g (arrow cty (opt cint)) then Int int_ty, Option + else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct + else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type g (arrow cty cZ) then Z z_pos_ty, Direct + else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option + else type_error_of g ty false + | None -> type_error_of g ty true + in + let o = { to_kind; to_ty; of_kind; of_ty; + num_ty = ty; + warning = opts } + in + (match opts, to_kind with + | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty + | _ -> ()); + let i = + { pt_local = local; + pt_scope = scope; + pt_interp_info = NumeralNotation o; + pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_refs = constructors; + pt_in_match = true } + in + enable_prim_token_interpretation i diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli new file mode 100644 index 0000000000..f96b8321f8 --- /dev/null +++ b/plugins/syntax/numeral.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +open Libnames +open Vernacexpr +open Notation + +(** * Numeral notation *) + +val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack new file mode 100644 index 0000000000..f4d9cae3ff --- /dev/null +++ b/plugins/syntax/numeral_notation_plugin.mlpack @@ -0,0 +1,2 @@ +Numeral +G_numeral diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune new file mode 100644 index 0000000000..bfdd480fe9 --- /dev/null +++ b/plugins/syntax/plugin_base.dune @@ -0,0 +1,35 @@ +(library + (name numeral_notation_plugin) + (public_name coq.plugins.numeral_notation) + (synopsis "Coq numeral notation plugin") + (modules g_numeral numeral) + (libraries coq.plugins.ltac)) + +(library + (name r_syntax_plugin) + (public_name coq.plugins.r_syntax) + (synopsis "Coq syntax plugin: reals") + (modules r_syntax) + (libraries coq.vernac)) + +(library + (name ascii_syntax_plugin) + (public_name coq.plugins.ascii_syntax) + (synopsis "Coq syntax plugin: ASCII") + (modules ascii_syntax) + (libraries coq.vernac)) + +(library + (name string_syntax_plugin) + (public_name coq.plugins.string_syntax) + (synopsis "Coq syntax plugin: strings") + (modules string_syntax) + (libraries coq.plugins.ascii_syntax)) + +(library + (name int31_syntax_plugin) + (public_name coq.plugins.int31_syntax) + (synopsis "Coq syntax plugin: int31") + (modules int31_syntax) + (libraries coq.vernac)) + diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml deleted file mode 100644 index 0c82e47445..0000000000 --- a/plugins/syntax/positive_syntax.ml +++ /dev/null @@ -1,101 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Names -open Bigint - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "positive_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -exception Non_closed_number - -(**********************************************************************) -(* Parsing positive via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -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) - -let positive_path = make_path binnums "positive" - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") -let glob_positive = IndRef (positive_kn,0) -let path_of_xI = ((positive_kn,0),1) -let path_of_xO = ((positive_kn,0),2) -let path_of_xH = ((positive_kn,0),3) -let glob_xI = ConstructRef path_of_xI -let glob_xO = ConstructRef path_of_xO -let glob_xH = ConstructRef path_of_xH - -let pos_of_bignat ?loc x = - let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in - let rec pos_of x = - match div2_with_rest x with - | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -let interp_positive ?loc n = - if is_strictly_pos n then pos_of_bignat ?loc n - else error_non_positive ?loc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let rec bignat_of_pos x = DAst.with_val (function - | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one - | _ -> raise Non_closed_number - ) x - -let uninterp_positive (AnyGlobConstr p) = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,binnums) - interp_positive - ([DAst.make @@ GRef (glob_xI, None); - DAst.make @@ GRef (glob_xO, None); - DAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack deleted file mode 100644 index ac8f3c425c..0000000000 --- a/plugins/syntax/positive_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Positive_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 94aa143350..49497aef54 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -131,9 +131,19 @@ let uninterp_r (AnyGlobConstr p) = with Non_closed_number -> None -let _ = Notation.declare_numeral_interpreter "R_scope" - (r_path,["Coq";"Reals";"Rdefinitions"]) - r_of_int - ([DAst.make @@ GRef (glob_IZR, None)], - uninterp_r, - false) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let r_scope = "R_scope" + +let _ = + register_bignumeral_interpretation r_scope (r_of_int,uninterp_r); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = r_scope; + pt_interp_info = Uid r_scope; + pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); + pt_refs = [glob_IZR]; + pt_in_match = false } diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index c22869f4d6..7478c1e978 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,10 +64,18 @@ let uninterp_string (AnyGlobConstr r) = with Non_closed_string -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([DAst.make @@ GRef (static_glob_String,None); - DAst.make @@ GRef (static_glob_EmptyString,None)], - uninterp_string, true) + let sc = "string_scope" in + register_string_interpretation sc (interp_string,uninterp_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_interp_info = Uid sc; + pt_required = (string_path,["Coq";"Strings";"String"]); + pt_refs = [static_glob_String; static_glob_EmptyString]; + pt_in_match = true } diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml deleted file mode 100644 index 2534162e36..0000000000 --- a/plugins/syntax/z_syntax.ml +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - -open Names -open Bigint -open Positive_syntax_plugin.Positive_syntax - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "z_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(**********************************************************************) -(* Parsing Z via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -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) - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let z_path = make_path binnums "Z" -let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") -let glob_z = IndRef (z_kn,0) -let path_of_ZERO = ((z_kn,0),1) -let path_of_POS = ((z_kn,0),2) -let path_of_NEG = ((z_kn,0),3) -let glob_ZERO = ConstructRef path_of_ZERO -let glob_POS = ConstructRef path_of_POS -let glob_NEG = ConstructRef path_of_NEG - -let z_of_int ?loc n = - if not (Bigint.equal n zero) then - let sgn, n = - if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) - else - DAst.make ?loc @@ GRef(glob_ZERO, None) - -(**********************************************************************) -(* Printing Z via scopes *) -(**********************************************************************) - -let bigint_of_z z = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a - | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero - | _ -> raise Non_closed_number - ) z - -let uninterp_z (AnyGlobConstr p) = - try - Some (bigint_of_z p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for Z *) - -let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binnums) - z_of_int - ([DAst.make @@ GRef (glob_ZERO, None); - DAst.make @@ GRef (glob_POS, None); - DAst.make @@ GRef (glob_NEG, None)], - uninterp_z, - true) diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack deleted file mode 100644 index 411260c04c..0000000000 --- a/plugins/syntax/z_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Z_syntax diff --git a/plugins/xml/README b/plugins/xml/README deleted file mode 100644 index 3128189929..0000000000 --- a/plugins/xml/README +++ /dev/null @@ -1,4 +0,0 @@ -The xml export plugin for Coq has been removed from the sources. -A backward compatible plug-in will be provided as a third-party plugin. -For more informations, contact -Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>. |