diff options
Diffstat (limited to 'parsing/g_zsyntax.ml')
| -rw-r--r-- | parsing/g_zsyntax.ml | 176 |
1 files changed, 1 insertions, 175 deletions
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index f78373c28..9f4bba335 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -8,144 +8,16 @@ (* $Id$ *) -open Coqast open Pcoq open Pp open Util open Names -open Ast -open Extend open Topconstr open Libnames open Bigint -(**********************************************************************) -(* V7 parsing via Grammar *) - -let get_z_sign loc = - let mkid id = - mkRefC (Qualid (loc,Libnames.make_short_qualid id)) - in - ((mkid (id_of_string "xI"), - mkid (id_of_string "xO"), - mkid (id_of_string "xH")), - (mkid (id_of_string "ZERO"), - mkid (id_of_string "POS"), - mkid (id_of_string "NEG"))) - -let pos_of_bignat xI xO xH x = - let rec pos_of x = - match div2_with_rest x with - | (q, true) when q <> zero -> mkAppC (xI, [pos_of q]) - | (q, false) -> mkAppC (xO, [pos_of q]) - | (_, true) -> xH - in - pos_of x - -let z_of_string pos_or_neg s dloc = - let ((xI,xO,xH),(aZERO,aPOS,aNEG)) = get_z_sign dloc in - let v = Bigint.of_string s in - if v <> zero then - if pos_or_neg then - mkAppC (aPOS, [pos_of_bignat xI xO xH v]) - else - mkAppC (aNEG, [pos_of_bignat xI xO xH v]) - else - aZERO - -(* Declare the primitive parser with Grammar and without the scope mechanism *) -let zsyntax_create name = - let e = - Pcoq.create_constr_entry (Pcoq.get_univ "znatural") name in - Pcoq.Gram.Unsafe.clear_entry e; - e - -let number = zsyntax_create "number" - -let negnumber = zsyntax_create "negnumber" - -let _ = - Gram.extend number None - [None, None, - [[Gramext.Stoken ("INT", "")], - Gramext.action (z_of_string true)]] - -let _ = - Gram.extend negnumber None - [None, None, - [[Gramext.Stoken ("INT", "")], - Gramext.action (z_of_string false)]] - -(**********************************************************************) -(* Old v7 ast printing *) - -open Coqlib - exception Non_closed_number -let get_z_sign_ast loc = - let ast_of_id id = - Termast.ast_of_ref - (global_of_constr - (gen_constant_in_modules "Z-printer" zarith_base_modules id)) - in - ((ast_of_id "xI", - ast_of_id "xO", - ast_of_id "xH"), - (ast_of_id "ZERO", - ast_of_id "POS", - ast_of_id "NEG")) - -let _ = if !Options.v7 then -let rec bignat_of_pos c1 c2 c3 p = - match p with - | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) -> - mult_2 (bignat_of_pos c1 c2 c3 a) - | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) -> - add_1 (mult_2 (bignat_of_pos c1 c2 c3 a)) - | a when alpha_eq(a,c3) -> Bigint.one - | _ -> raise Non_closed_number -in -let bignat_option_of_pos xI xO xH p = - try - Some (bignat_of_pos xO xI xH p) - with Non_closed_number -> - None -in -let pr_pos a = hov 0 (str "POS" ++ brk (1,1) ++ a) in -let pr_neg a = hov 0 (str "NEG" ++ brk (1,1) ++ a) in - -let inside_printer posneg std_pr p = - let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in - match (bignat_option_of_pos xI xO xH p) with - | Some n -> - if posneg then - (str (Bigint.to_string n)) - else - (str "(-" ++ str (Bigint.to_string n) ++ str ")") - | None -> - let pr = if posneg then pr_pos else pr_neg in - str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")" -in -let outside_printer posneg std_pr p = - let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in - match (bignat_option_of_pos xI xO xH p) with - | Some n -> - if posneg then - (str "`" ++ str (Bigint.to_string n) ++ str "`") - else - (str "`-" ++ str (Bigint.to_string n) ++ str "`") - | None -> - let pr = if posneg then pr_pos else pr_neg in - str "(" ++ pr (std_pr p) ++ str ")" -in -(* For printing with Syntax and without the scope mechanism *) -let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true)) in -let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false)) in -let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))in -let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false)) -in () - (**********************************************************************) (* Parsing positive via scopes *) (**********************************************************************) @@ -235,8 +107,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope" (**********************************************************************) let binnat_module = ["Coq";"NArith";"BinNat"] -let n_path = make_path (make_dir binnat_module) - (id_of_string (if !Options.v7 then "entier" else "N")) +let n_path = make_path (make_dir binnat_module) (id_of_string "N") let glob_n = IndRef (n_path,0) let path_of_N0 = ((n_path,0),1) let path_of_Npos = ((n_path,0),2) @@ -346,48 +217,3 @@ let _ = Notation.declare_numeral_interpreter "Z_scope" RRef (dummy_loc, glob_NEG)], uninterp_z, None) - -(************************************************************************) -(* Old V7 ast Printers *) - -open Esyntax - -let _ = if !Options.v7 then -let bignat_of_pos p = - let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in - let c1 = xO in - let c2 = xI in - let c3 = xH in - let rec transl = function - | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c1) -> mult_2(transl a) - | Node (_,"APPLIST",[b; a]) when alpha_eq(b,c2) -> add_1(mult_2(transl a)) - | a when alpha_eq(a,c3) -> Bigint.one - | _ -> raise Non_closed_number - in transl p -in -let bignat_option_of_pos p = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None -in -let z_printer posneg p = - match bignat_option_of_pos p with - | Some n -> - if posneg then - Some (str (Bigint.to_string n)) - else - Some (str "-" ++ str (Bigint.to_string n)) - | None -> None -in -let z_printer_ZERO _ = - Some (int 0) -in -(* Declare pretty-printers for integers *) -let _ = - declare_primitive_printer "z_printer_POS" "Z_scope" (z_printer true) in -let _ = - declare_primitive_printer "z_printer_NEG" "Z_scope" (z_printer false) in -let _ = - declare_primitive_printer "z_printer_ZERO" "Z_scope" z_printer_ZERO in -() |