From ec0ad20de8daf2ad9f3237de92a745247db845f5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Mar 2017 16:13:24 +0100 Subject: remove legacy syntax plugins subsumed by Numeral Notation --- plugins/syntax/n_syntax.ml | 88 ---------------------- plugins/syntax/n_syntax_plugin.mlpack | 1 - plugins/syntax/nat_syntax.ml | 95 ------------------------ plugins/syntax/nat_syntax_plugin.mlpack | 1 - plugins/syntax/positive_syntax.ml | 107 --------------------------- plugins/syntax/positive_syntax_plugin.mlpack | 1 - plugins/syntax/z_syntax.ml | 84 --------------------- plugins/syntax/z_syntax_plugin.mlpack | 1 - 8 files changed, 378 deletions(-) delete mode 100644 plugins/syntax/n_syntax.ml delete mode 100644 plugins/syntax/n_syntax_plugin.mlpack delete mode 100644 plugins/syntax/nat_syntax.ml delete mode 100644 plugins/syntax/nat_syntax_plugin.mlpack delete mode 100644 plugins/syntax/positive_syntax.ml delete mode 100644 plugins/syntax/positive_syntax_plugin.mlpack delete mode 100644 plugins/syntax/z_syntax.ml delete mode 100644 plugins/syntax/z_syntax_plugin.mlpack (limited to 'plugins') diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml deleted file mode 100644 index 29b88b1cb3..0000000000 --- a/plugins/syntax/n_syntax.ml +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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 *) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "N_scope" in - register_bignumeral_interpretation scope (n_of_int,uninterp_n); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (n_path,binnums); - pt_refs = [glob_N0; glob_Npos]; - pt_in_match = 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 85cb49586d..0000000000 --- a/plugins/syntax/nat_syntax.ml +++ /dev/null @@ -1,95 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* > *) - -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 *) - -open Notation - -let nat_scope = "nat_scope" - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - register_bignumeral_interpretation nat_scope (nat_of_int,uninterp_nat); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = nat_scope; - pt_uid = nat_scope; - pt_required = (nat_path,datatypes_module_name); - pt_refs = [glob_S; glob_O]; - pt_in_match = 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/positive_syntax.ml b/plugins/syntax/positive_syntax.ml deleted file mode 100644 index 6fce4de9ef..0000000000 --- a/plugins/syntax/positive_syntax.ml +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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 *) -(************************************************************************) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "positive_scope" in - register_bignumeral_interpretation scope (interp_positive,uninterp_positive); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (positive_path,binnums); - pt_refs = [glob_xI; glob_xO; glob_xH]; - pt_in_match = 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/z_syntax.ml b/plugins/syntax/z_syntax.ml deleted file mode 100644 index 72e1321eab..0000000000 --- a/plugins/syntax/z_syntax.ml +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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 *) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "Z_scope" in - register_bignumeral_interpretation scope (z_of_int,uninterp_z); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (z_path,binnums); - pt_refs = [glob_ZERO; glob_POS; glob_NEG]; - pt_in_match = 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 -- cgit v1.2.3