From b3a30395c85a34a6162fe884c7a06b1079e698c2 Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 26 Apr 2000 16:56:26 +0000 Subject: suppression doublon git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@375 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Arith/g_natsyntax.ml | 78 ---------------------- theories/Zarith/g_zsyntax.ml | 150 ------------------------------------------ 2 files changed, 228 deletions(-) delete mode 100644 theories/Arith/g_natsyntax.ml delete mode 100644 theories/Zarith/g_zsyntax.ml (limited to 'theories') diff --git a/theories/Arith/g_natsyntax.ml b/theories/Arith/g_natsyntax.ml deleted file mode 100644 index ff5c5b948..000000000 --- a/theories/Arith/g_natsyntax.ml +++ /dev/null @@ -1,78 +0,0 @@ - -(* $Id;$ *) - -(* This file to allow writing (3) for (S (S (S O))) - and still write (S y) for (S y) *) - -open Util -open Pcoq -open Pp -open Names -open Coqast -open Ast - -exception Non_closed_number - -let get_nat_sign loc = - let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in - (ast_of_id "O", ast_of_id "S", ast_of_id "My_special_variable") - -(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) -let nat_of_int n dloc = - let (astO,astS,_) = get_nat_sign dloc in - let rec mk_nat n = - if n <= 0 then - astO - else - Node(dloc,"APPLIST", [astS; mk_nat (n-1)]) - in - mk_nat n - -let nat_of_string s dloc = nat_of_int (int_of_string s) dloc - -let rec int_of_nat_rec astS astO p = - match p with - | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) -> - (int_of_nat_rec astS astO a)+1 - | a when alpha_eq(a,astO) -> 1 - (***** YES, 1, non 0 ... to print the successor of p *) - | _ -> raise Non_closed_number - -let int_of_nat p = - let (astO,astS,_) = get_nat_sign dummy_loc in - try - Some (int_of_nat_rec astS astO p) - with - Non_closed_number -> None - -let replace_S p = - let (_,astS,astmyvar) = get_nat_sign dummy_loc in - let rec aux p = - match p with - | Node (l,"APPLIST", [b; a]) when b = astS -> - Node (l, "APPLIST", [astmyvar; (aux a)]) - | _ -> p - in - ope("APPLIST", [astmyvar; (aux p)]) - -(* Declare the primitive printer *) - -(* Prints not p, but the SUCCESSOR of p !!!!! *) -let nat_printer std_pr p = - match (int_of_nat p) with - | Some i -> [< 'sTR (string_of_int i) >] - | None -> std_pr (replace_S p) - -let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer) - -(* Declare the primitive parser *) -open Pcoq - -let number = - match create_entry (get_univ "nat") "number" ETast with - | Ast n -> n - | _ -> anomaly "G_natsyntax : create_entry number failed" - -let _ = - Gram.extend number None - [None, None, [[Gramext.Stoken ("INT", "")], Gramext.action nat_of_string]] diff --git a/theories/Zarith/g_zsyntax.ml b/theories/Zarith/g_zsyntax.ml deleted file mode 100644 index 85ebb140a..000000000 --- a/theories/Zarith/g_zsyntax.ml +++ /dev/null @@ -1,150 +0,0 @@ - -(* $Id$ *) - -open Coqast -open Pcoq -open Util -open Pp -open Names -open Ast - -let get_z_sign loc = - let ast_of_id id = Astterm.globalize_command (Nvar(loc,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"), - (ast_of_id "My_special_variable0", ast_of_id "My_special_variable1")) - -let int_array_of_string s = - let a = Array.create (String.length s) 0 in - for i = 0 to String.length s - 1 do - a.(i) <- int_of_string (String.sub s i 1) - done; - a - -let string_of_int_array s = - String.concat "" (Array.to_list (Array.map string_of_int s)) - -let is_nonzero a = - let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b - -let div2_with_rest n = - let len = Array.length n in - let q = Array.create len 0 in - for i = 0 to len - 2 do - q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- 5 * (n.(i) mod 2) - done; - q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2; - q, n.(len - 1) mod 2 - -let add_1 n = - let m = Array.copy n - and i = ref (Array.length n - 1) in - m.(!i) <- m.(!i) + 1; - while m.(!i) = 10 && !i > 0 do - m.(!i) <- 0; decr i; m.(!i) <- m.(!i) + 1 - done; - if !i = 0 && m.(0) = 10 then - begin m.(0) <- 0; Array.concat [[| 1 |]; m] end - else m - -let rec mult_2 n = - let m = Array.copy n in - m.(Array.length n - 1) <- 2 * m.(Array.length n - 1); - for i = Array.length n - 2 downto 0 do - m.(i) <- 2 * m.(i); - if m.(i + 1) >= 10 then - begin m.(i + 1) <- m.(i + 1) - 10; m.(i) <- m.(i) + 1 end - done; - if m.(0) >= 10 then - begin m.(0) <- m.(0) - 10; Array.concat [[| 1 |]; m] end - else m - -let pos_of_int_array astxI astxO astxH x = - let rec pos_of x = - match div2_with_rest x with - | (q, 1) -> - if is_nonzero q then ope("APPLIST", [astxI; pos_of q]) - else astxH - | (q, 0) -> ope("APPLIST", [astxO; pos_of q]) - | _ -> anomaly "n mod 2 is neither 1 nor 0. Do you bielive that ?" - in - pos_of x - -let z_of_string pos_or_neg s dloc = - let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG),_) = get_z_sign dloc in - let v = int_array_of_string s in - if is_nonzero v then - if pos_or_neg then - ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v]) - else - ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v]) - else - astZERO - -exception Non_closed_number - -let rec int_array_of_pos c1 c2 c3 p = - match p with - | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) -> - mult_2 (int_array_of_pos c1 c2 c3 a) - | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) -> - add_1 (mult_2 (int_array_of_pos c1 c2 c3 a)) - | a when alpha_eq(a,c3) -> [| 1 |] - | _ -> raise Non_closed_number - -let int_array_option_of_pos astxI astxO astxH p = - try Some (int_array_of_pos astxO astxI astxH p) - with Non_closed_number -> None - -let inside_printer posneg std_pr p = - let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in - match (int_array_option_of_pos astxI astxO astxH p) with - | Some n -> - if posneg - then [< 'sTR (string_of_int_array n) >] - else [< 'sTR "(-"; 'sTR (string_of_int_array n); 'sTR ")" >] - | None -> - let c = if posneg then myvar0 else myvar1 in - std_pr (ope("ZEXPR",[ope("APPLIST",[c; p])])) - -let outside_printer posneg std_pr p = - let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in - match (int_array_option_of_pos astxI astxO astxH p) with - | Some n -> - if posneg - then [< 'sTR "`"; 'sTR (string_of_int_array n); 'sTR "`">] - else [< 'sTR "`-"; 'sTR (string_of_int_array n); 'sTR "`" >] - | None -> - let c = if posneg then myvar0 else myvar1 in - [< 'sTR "("; std_pr (ope("APPLIST",[c; p])); 'sTR ")" >] - -(* Declare pretty-printers for integers *) -let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true)) -let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false)) -let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true)) -let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false)) - -(* Declare the primitive parser *) -open Pcoq - -let number = - match create_entry (get_univ "znatural") "number" ETast with - | Ast n -> n - | _ -> anomaly "G_zsyntax.number" - -let negnumber = - match create_entry (get_univ "znatural") "negnumber" ETast with - | Ast n -> n - | _ -> anomaly "G_zsyntax.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)]] -- cgit v1.2.3