diff options
| -rw-r--r-- | .depend | 12 | ||||
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | parsing/g_natsyntax.ml | 81 | ||||
| -rw-r--r-- | parsing/g_natsyntax.mli | 4 | ||||
| -rw-r--r-- | parsing/g_zsyntax.ml | 157 | ||||
| -rw-r--r-- | parsing/g_zsyntax.mli | 4 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 3 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 (renamed from toplevel/mltop.ml) | 7 |
8 files changed, 275 insertions, 5 deletions
@@ -432,6 +432,18 @@ parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi +parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ + parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi +parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ + parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi \ + lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi +parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ + parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ + lib/util.cmi +parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ + parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \ + lib/util.cmx parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi parsing/pretty.cmo: pretyping/classops.cmi kernel/constant.cmi \ @@ -85,6 +85,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/extend.cmo parsing/termast.cmo \ parsing/esyntax.cmo parsing/printer.cmo parsing/pretty.cmo \ parsing/astterm.cmo parsing/egrammar.cmo +ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo PROOFS=proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ @@ -107,7 +108,7 @@ CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ $(PROOFS) $(TACTICS) $(TOPLEVEL) -CMX=$(CMO:.cmo=.cmx) +CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) ########################################################################### # Main targets @@ -255,6 +256,15 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma beforedepend:: $(GRAMMARCMO) +# toplevel/mltop.ml4 (ifdef Opt) + +CAMLP4IFDEF=camlp4o pa_ifdef.cmo + +toplevel/mltop.cmo: toplevel/mltop.ml4 + $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -DByte -impl" -impl $< +toplevel/mltop.cmx: toplevel/mltop.ml4 + $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< + ########################################################################### # Default rules ########################################################################### diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml new file mode 100644 index 000000000..1c5b64623 --- /dev/null +++ b/parsing/g_natsyntax.ml @@ -0,0 +1,81 @@ + +(* $Id$ *) + +(* This file to allow writing (3) for (S (S (S O))) + and still write (S y) for (S y) *) + +open Pcoq +open Pp +open Util +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 *) + +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/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli new file mode 100644 index 000000000..61f305ad9 --- /dev/null +++ b/parsing/g_natsyntax.mli @@ -0,0 +1,4 @@ + +(* $Id$ *) + +(* Nice syntax for naturals. *) diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml new file mode 100644 index 000000000..8128cb3d9 --- /dev/null +++ b/parsing/g_zsyntax.ml @@ -0,0 +1,157 @@ + +(* $Id$ *) + +open Coqast +open Pcoq +open Pp +open Util +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)]] + diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli new file mode 100644 index 000000000..310d09a12 --- /dev/null +++ b/parsing/g_zsyntax.mli @@ -0,0 +1,4 @@ + +(* $Id$ *) + +(* Nice syntax for integers. *) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 6a244b988..bde07410a 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -17,8 +17,7 @@ let ocamlobjs = ["unix.cma"] let dynobjs = ["dynlink.cma"] let camlp4objs = ["gramlib.cma"] let configobjs = ["coq_config.cmo"] -let launchobjs = ["usage.cmo"] -let libobjs = ocamlobjs @ camlp4objs @ configobjs @ launchobjs +let libobjs = ocamlobjs @ camlp4objs @ configobjs let spaces = Str.regexp "[ \t\n]+" let split_cmo l = Str.split spaces l diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml4 index b38fa5756..5329becae 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml4 @@ -84,7 +84,8 @@ let dir_ml_load s = errorlabstrm "Mltop.load_object" [< 'sTR"File not found on loadpath : "; 'sTR s >] | WithoutTop -> - if is_in_path !coq_mlpath_copy s then + ifdef Byte then + (if is_in_path !coq_mlpath_copy s then let gname = where_in_path !coq_mlpath_copy s in try Dynlink.loadfile gname; @@ -97,7 +98,9 @@ let dir_ml_load s = errorlabstrm "Mltop.load_object" [< 'sTR (Dynlink.error_message a) >] else errorlabstrm "Mltop.load_object" - [< 'sTR"File not found on loadpath : "; 'sTR s >] + [< 'sTR"File not found on loadpath : "; 'sTR s >]) + else + () | Native -> errorlabstrm "Mltop.no_load_object" [< 'sTR"Loading of ML object file forbidden in a native Coq" >] |