diff options
| -rw-r--r-- | Makefile | 29 | ||||
| -rw-r--r-- | dev/TODO | 11 | ||||
| -rw-r--r-- | lib/options.ml | 2 | ||||
| -rw-r--r-- | lib/options.mli | 2 | ||||
| -rw-r--r-- | lib/system.ml | 9 | ||||
| -rw-r--r-- | lib/system.mli | 3 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pretty.ml | 137 | ||||
| -rw-r--r-- | parsing/printer.ml | 15 | ||||
| -rw-r--r-- | scripts/.cvsignore | 1 | ||||
| -rw-r--r-- | scripts/coqc.ml4 | 156 |
11 files changed, 287 insertions, 82 deletions
@@ -39,6 +39,9 @@ DEPFLAGS=$(LOCALINCLUDES) CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) +CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE) + +COQINCLUDES= ########################################################################### # Objects files @@ -117,8 +120,9 @@ CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) ########################################################################### COQMKTOP=scripts/coqmktop +COQC=scripts/coqc -world: $(COQMKTOP) coqtop.byte coqtop.opt states tools +world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states tools coqtop.opt: $(COQMKTOP) $(CMX) $(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop.opt @@ -131,7 +135,8 @@ coqtop.byte: $(COQMKTOP) $(CMO) Makefile COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo $(COQMKTOP): $(COQMKTOPCMO) - $(OCAMLC) $(BYTEFLAGS) -o $(COQMKTOP) -custom str.cma unix.cma $(COQMKTOPCMO) $(OSDEPLIBS) $(STRLIB) + $(OCAMLC) $(BYTEFLAGS) -o $(COQMKTOP) -custom str.cma unix.cma \ + $(COQMKTOPCMO) $(OSDEPLIBS) $(STRLIB) scripts/tolink.ml: Makefile echo "let lib = \""$(LIB)"\"" > $@ @@ -146,6 +151,17 @@ scripts/tolink.ml: Makefile beforedepend:: scripts/tolink.ml +# coqc + +COQCCMO=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo + +$(COQC): $(COQCCMO) + $(OCAMLC) $(BYTEFLAGS) -o $(COQC) -custom unix.cma $(COQCCMO) \ + $(OSDEPLIBS) + +scripts/coqc.cmo: scripts/coqc.ml4 + $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< + # we provide targets for each subdirectories lib: $(LIB) @@ -179,6 +195,8 @@ tools/coqdep: $(COQDEPCMX) $(OCAMLOPT) $(OPTFLAGS) -o tools/coqdep unix.cmxa $(COQDEPCMX) \ $(OSDEPLIBS) +beforedepend:: tools/coqdep + GALLINACMX=tools/gallina_lexer.cmx tools/gallina.cmx tools/gallina: $(GALLINACMX) @@ -321,8 +339,6 @@ beforedepend:: parsing/pcoq.ml parsing/extend.ml # toplevel/mltop.ml4 (ifdef Byte) -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 @@ -332,7 +348,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4 # Default rules ########################################################################### -.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 .el .elc +.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 .v .vo .el .elc .ml.cmo: $(OCAMLC) $(BYTEFLAGS) -c $< @@ -352,6 +368,9 @@ toplevel/mltop.cmx: toplevel/mltop.ml4 .ml4.cmx: $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< +.v.vo: + $(COQC) $(COQCINCLUDES) $< + .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile echo "(byte-compile-file \"$<\")" >> $*.compile @@ -1,9 +1,10 @@ - o Lib - - écrire une fonction d'export qui supprimme les FrozenState, - vérifie qu'il n'y a pas de section ouverte, et présente les - déclarations dans l'ordre chronologique (y compris dans les - sections fermées ?). A utiliser dans Library pour sauver un module. + o options de la ligne de commande + - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml + + o arguments implicites + - les calculer une fois pour toutes à la déclaration (dans Declare) + et stocker cette information dans le in_variable, in_constant, etc. o configure - il faut tester la version du programme correspondant à $bytecamlc diff --git a/lib/options.ml b/lib/options.ml index 26869e7ad..fdfec98d0 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -15,7 +15,7 @@ let emacs_str s = if !print_emacs then s else "" let silent = ref false let make_silent flag = silent := flag; () let is_silent () = !silent -let verbose () = not !silent +let is_verbose () = not !silent let silently f x = let oldsilent = !silent in diff --git a/lib/options.mli b/lib/options.mli index dc6b5b982..25c194106 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -12,7 +12,7 @@ val emacs_str : string -> string val make_silent : bool -> unit val is_silent : unit -> bool -val verbose : unit -> bool +val is_verbose : unit -> bool val silently : ('a -> 'b) -> 'a -> 'b val set_print_hyps_limit : int -> unit diff --git a/lib/system.ml b/lib/system.ml index 5422bc465..aed203b20 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -101,13 +101,15 @@ let try_remove f = with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ; 'sTR f ; 'sTR" which is corrupted !!" >] +let marshal_out ch v = Marshal.to_channel ch v [Marshal.Closures] +let marshal_in ch = Marshal.from_channel ch + exception Bad_magic_number of string let (raw_extern_intern : int -> string -> (string -> string * out_channel) * (string -> string * in_channel)) = fun magic suffix -> - let extern_state name = let (_,channel) as filec = open_trapping_failure (fun n -> n,open_out_bin n) name suffix in @@ -125,13 +127,12 @@ let (raw_extern_intern : let (extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a)) = fun magic suffix -> - let (raw_extern,raw_intern) = raw_extern_intern magic suffix in let extern_state name val_0 = try let (fname,channel) = raw_extern name in try - output_value channel val_0; + marshal_out channel val_0; close_out channel with e -> begin try_remove fname; raise e end @@ -140,7 +141,7 @@ let (extern_intern : and intern_state name = try let (fname,channel) = raw_intern name in - let v = input_value channel in + let v = marshal_in channel in close_in channel; v with Sys_error s -> error("System error: " ^ s) diff --git a/lib/system.mli b/lib/system.mli index e3fd5978c..3d355e843 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -28,6 +28,9 @@ val find_file_in_path : string -> string and a suffix. The intern functions raise the exception [Bad_magic_number] when the check fails, with the full file name. *) +val marshal_out : out_channel -> 'a -> unit +val marshal_in : in_channel -> 'a + exception Bad_magic_number of string val raw_extern_intern : int -> string -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4fb5380f5..c28cfde12 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -341,6 +341,10 @@ GEXTEND Gram | IDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >> | IDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >> | IDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >> + | IDENT "Write"; IDENT "Module"; id = identarg; "." -> + <:ast< (WriteModule $id) >> + | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg; "." -> + <:ast< (WriteModule $id $s) >> | IDENT "Begin"; IDENT "Silent"; "." -> <:ast< (BeginSilent) >> | IDENT "End"; IDENT "Silent"; "." -> <:ast< (EndSilent) >> | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >> diff --git a/parsing/pretty.ml b/parsing/pretty.ml index e0277761d..8147fd2b8 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -58,7 +58,7 @@ let fprint_recipe = function | None -> [< 'sTR"<uncookable>" >] let print_typed_recipe (val_0,typ) = - [< print_recipe val_0 ; 'fNL ; 'sTR " : "; prtype typ ; 'fNL >] + [< print_recipe val_0; 'fNL; 'sTR " : "; prtype typ; 'fNL >] let print_impl_args = function | [] -> [<>] @@ -215,66 +215,74 @@ let print_extracted_mutual sp = print_mutual fwsp (Global.lookup_mind fwsp) | Some a -> fprterm a -let print_leaf_entry with_values sep (spopt,lobj) = +let print_variable sp = + let (name,typ,_,_) = out_variable sp in + let l = implicits_of_var (kind_of_path sp) name in + [< print_var (string_of_id name) typ; print_impl_args l; 'fNL >] + +let print_constant with_values sep sp = + let cb = Global.lookup_constant sp in + if kind_of_path sp = CCI then + let val_0 = cb.const_body in + let typ = cb.const_type in + let l = constant_implicits sp in + hOV 0 [< (match val_0 with + | None -> + [< 'sTR"*** [ "; + 'sTR (print_basename (ccisp_of sp)); + 'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >] + | _ -> + [< 'sTR(print_basename (ccisp_of sp)) ; + 'sTR sep; 'cUT ; + if with_values then + print_typed_recipe (val_0,typ) + else + [< prtype typ ; 'fNL >] >]); + print_impl_args (list_of_implicits l); 'fNL >] + else + hOV 0 [< 'sTR"Fw constant " ; + 'sTR (print_basename (fwsp_of sp)) ; 'fNL>] + +let print_inductive sp = + let mib = Global.lookup_mind sp in + if kind_of_path sp = CCI then + [< print_mutual sp mib; 'fNL >] + else + hOV 0 [< 'sTR"Fw inductive definition "; + 'sTR (print_basename (fwsp_of sp)); 'fNL >] + +let print_leaf_entry with_values sep (sp,lobj) = let tag = object_tag lobj in - match (spopt,tag) with + match (sp,tag) with | (_,"VARIABLE") -> - let (name,typ,_,_) = out_variable spopt in - let l = implicits_of_var (kind_of_path spopt) name in - [< print_var (string_of_id name) typ; print_impl_args l; 'fNL >] - - | (sp,("CONSTANT"|"PARAMETER")) -> - let cb = Global.lookup_constant sp in - if kind_of_path sp = CCI then - let val_0 = cb.const_body in - let typ = cb.const_type in - let l = constant_implicits sp in - hOV 0 [< (match val_0 with - | None -> - [< 'sTR"*** [ "; - 'sTR (print_basename (ccisp_of sp)); - 'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >] - | _ -> - [< 'sTR(print_basename (ccisp_of sp)) ; - 'sTR sep; 'cUT ; - if with_values then - print_typed_recipe (val_0,typ) - else - [< prtype typ ; 'fNL >] >]); - print_impl_args (list_of_implicits l); 'fNL >] - else - hOV 0 [< 'sTR"Fw constant " ; - 'sTR (print_basename (fwsp_of sp)) ; 'fNL>] - - | (sp,"INDUCTIVE") -> - let mib = Global.lookup_mind sp in - if kind_of_path sp = CCI then - [< print_mutual sp mib; 'fNL >] - else - hOV 0 [< 'sTR"Fw inductive definition " ; - 'sTR (print_basename (fwsp_of sp)) ; 'fNL >] - - | (_,"AUTOHINT") -> [< 'sTR" Add Auto Marker" ; 'fNL >] - - | (_,"GRAMMAR") -> [< 'sTR" Grammar Marker" ; 'fNL >] - - | (sp,"SYNTAXCONSTANT") -> + print_variable sp + | (_,("CONSTANT"|"PARAMETER")) -> + print_constant with_values sep sp + | (_,"INDUCTIVE") -> + print_inductive sp + | (_,"AUTOHINT") -> + [< 'sTR" Add Auto Marker"; 'fNL >] + | (_,"GRAMMAR") -> + [< 'sTR" Grammar Marker"; 'fNL >] + | (_,"SYNTAXCONSTANT") -> let id = basename sp in - [< 'sTR" Syntax Macro " ; + [< 'sTR" Syntax Macro "; print_id id ; 'sTR sep; if with_values then let c = Syntax_def.search_syntactic_definition id in [< prrawterm c >] else [<>]; 'fNL >] - - | (_,"PPSYNTAX") -> [< 'sTR" Syntax Marker" ; 'fNL >] - - | (_,"TOKEN") -> [< 'sTR" Token Marker" ; 'fNL >] - - | (_,"CLASS") -> [< 'sTR" Class Marker" ; 'fNL >] - | (_,"COERCION") -> [< 'sTR" Coercion Marker" ; 'fNL >] - | (sp,s) -> [< 'sTR(string_of_path sp) ; 'sTR" : " ; - 'sTR"Unrecognized object " ; 'sTR s ; 'fNL >] + | (_,"PPSYNTAX") -> + [< 'sTR" Syntax Marker"; 'fNL >] + | (_,"TOKEN") -> + [< 'sTR" Token Marker"; 'fNL >] + | (_,"CLASS") -> + [< 'sTR" Class Marker"; 'fNL >] + | (_,"COERCION") -> + [< 'sTR" Coercion Marker"; 'fNL >] + | (_,s) -> + [< 'sTR(string_of_path sp); 'sTR" : "; + 'sTR"Unrecognized object "; 'sTR s; 'fNL >] let rec print_library_entry with_values ent = let sep = if with_values then " = " else " : " in @@ -282,7 +290,9 @@ let rec print_library_entry with_values ent = | (sp,Lib.Leaf lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >] | (_,Lib.OpenedSection (str,_)) -> - [< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >] + [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >] + | (_,Lib.Module str) -> + [< 'sTR(" >>>>>>> Module " ^ str); 'fNL >] | (_,Lib.FrozenState _) -> [< >] @@ -374,7 +384,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name = crible_rec rest | _ -> crible_rec rest) - | (_, (Lib.OpenedSection _ | Lib.FrozenState _))::rest -> + | (_, (Lib.OpenedSection _ | Lib.FrozenState _ | Lib.Module _))::rest -> crible_rec rest | [] -> () in @@ -429,10 +439,19 @@ let print_name name = with | Not_found -> (try - let (_,typ) = Global.lookup_var name in - [< print_var str typ; - try print_impl_args (implicits_of_var CCI name) - with _ -> [<>] >] + (match Declare.global_reference CCI name with + | VAR _ -> + let (_,typ) = Global.lookup_var name in + [< print_var str typ; + try print_impl_args (implicits_of_var CCI name) + with _ -> [<>] >] + | DOPN(Const sp,_) -> + print_constant true " = " sp + | DOPN(MutInd (sp,_),_) -> + print_inductive sp + | DOPN (MutConstruct((sp,_),_),_) -> + print_inductive sp + | _ -> assert false) with Not_found | Invalid_argument _ -> error (str ^ " not a defined object")) | Invalid_argument _ -> error (str ^ " not a defined object") diff --git a/parsing/printer.ml b/parsing/printer.ml index df0daa130..fcda9fb93 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -33,9 +33,10 @@ let with_implicits f x = Termast.print_implicits := oimpl; raise e let pr_qualified sp id = - if Nametab.sp_of_id (kind_of_path sp) id = sp - then [< 'sTR(string_of_id id) >] - else [< 'sTR(string_of_path sp) >] + if Nametab.sp_of_id (kind_of_path sp) id = sp then + [< 'sTR(string_of_id id) >] + else + [< 'sTR(string_of_path sp) >] let pr_constant sp = pr_qualified sp (basename sp) @@ -205,7 +206,7 @@ let dbenv_it_with f env e = (* Prints a signature, all declarations on the same line if possible *) let pr_sign sign = hV 0 [< (sign_it_with (fun id t sign pps -> - [< pps ; 'wS 2 ; print_decl CCI sign (id,t) >]) + [< pps; 'wS 2; print_decl CCI sign (id,t) >]) sign) [< >] >] (* Prints an env (variables and de Bruijn). Separator: newline *) @@ -213,13 +214,13 @@ let pr_env k env = let sign_env = sign_it_with (fun id t sign pps -> - let pidt = print_decl k sign (id,t) in [< pps ; 'fNL ; pidt >]) + let pidt = print_decl k sign (id,t) in [< pps; 'fNL; pidt >]) (get_globals env) [< >] in let db_env = dbenv_it_with (fun na t env pps -> - let pnat = print_binding k env (na,t) in [< pps ; 'fNL ; pnat >]) + let pnat = print_binding k env (na,t) in [< pps; 'fNL; pnat >]) env [< >] in [< sign_env; db_env >] @@ -251,7 +252,7 @@ let pr_env_limit n env = dbenv_it_with (fun na t env pps -> let pnat = print_binding CCI env (na,t) in - [< pps ; 'fNL ; + [< pps; 'fNL; 'sTR (emacs_str (String.make 1 (Char.chr 253))); pnat >]) env [< >] diff --git a/scripts/.cvsignore b/scripts/.cvsignore index 52ba6cec1..b95eb1ba9 100644 --- a/scripts/.cvsignore +++ b/scripts/.cvsignore @@ -1,2 +1,3 @@ coqmktop tolink.ml +coqc diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 new file mode 100644 index 000000000..a1d64c1d2 --- /dev/null +++ b/scripts/coqc.ml4 @@ -0,0 +1,156 @@ + +(* $Id$ *) + +(* Afin de rendre Coq plus portable, ce programme Caml remplace le script + coqc. + + Ici, on trie la ligne de commande pour en extraire les fichiers à compiler, + puis on les compile un par un en passant le reste de la ligne de commande + à un process "coqtop -batch -load-vernac-source <fichier>". + + On essaye au maximum d'utiliser les modules Sys et Filename pour que la + portabilité soit maximale, mais il reste encore des appels à des fonctions + du module Unix. Ceux-ci sont préfixés par "Unix." +*) + +(* environment *) + +let environment = Unix.environment () + +let bindir = ref Coq_config.bindir + +(* the $COQBIN environment variable has priority over the Coq_config value *) +let _ = + try + let c = Sys.getenv "COQBIN" in + if c <> "" then bindir := c + with Not_found -> () + +let specification = ref false + +let keep = ref false + +(* Verifies that a string do not contains others caracters than letters, + digits, or `_` *) + +let check_module_name s = + let err () = + output_string stderr + "Modules names must only contain letters, digits, or underscores\n"; + output_string stderr + "and must begin with a letter\n"; + exit 1 + in + match String.get s 0 with + | 'a' .. 'z' | 'A' .. 'Z' -> + for i = 1 to (String.length s)-1 do + match String.get s i with + | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> () + | _ -> err () + done + | _ -> err () + + (* compilation of a file [file] with command [command] and args [args] *) + +let compile command args file = + let dirname = Filename.dirname file in + let basename = Filename.basename file in + let modulename = + if Filename.check_suffix basename ".v" then + Filename.chop_suffix basename ".v" + else + basename + in + check_module_name modulename; + let tmpfile = Filename.temp_file "coqc" ".v" in + let args' = + command :: "-batch" :: "-silent" :: args + @ ["-load-vernac-source"; tmpfile] in + let devnull = + ifdef Unix then + Unix.openfile "/dev/null" [] 0o777 + else + Unix.stdin + in + let filevo = Filename.concat dirname (modulename ^ ".vo") in + let oc = open_out tmpfile in + Printf.fprintf oc "Module %s.\n" modulename; + Printf.fprintf oc "Load \"%s\".\n" file; + Printf.fprintf oc "Write Module %s \"%s\".\n" modulename filevo; + flush oc; + close_out oc; + try + let pid = + Unix.create_process_env command + (Array.of_list args') environment devnull Unix.stdout Unix.stderr in + let status = Unix.waitpid [] pid in + if not !keep then Sys.remove tmpfile ; + match status with + | _, Unix.WEXITED 0 -> () + | _, Unix.WEXITED c -> exit c + | _ -> exit 1 + with _ -> + if not !keep then Sys.remove tmpfile; exit 1 + +(* parsing of the command line + * + * special treatment for -bindir and -i. + * other options are passed to coqtop *) + +let usage () = + Usage.print_usage_coqc () ; + flush stderr ; + exit 1 + +let parse_args () = + let rec parse (cfiles,args) = function + | [] -> + List.rev cfiles, List.rev args + | "-i" :: rem -> + specification := true ; parse (cfiles,args) rem + | "-t" :: rem -> + keep := true ; parse (cfiles,args) rem + | "-bindir" :: d :: rem -> + bindir := d ; parse (cfiles,d::"-bindir"::args) rem + | "-bindir" :: [] -> + usage () + | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () + | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate" + |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source" + |"-require"|"-unsafe"|"-quiet"|"-silent"|"-v"|"--version" + |"-load-ml-object"|"-user"|"-init-file" as o) :: rem -> + begin + match rem with + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" + |"-q"|"-opt"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> + parse (cfiles,o::args) rem + | f :: rem -> + if Sys.file_exists f then + parse (f::cfiles,args) rem + else + let fv = f ^ ".v" in + if Sys.file_exists fv then + parse (fv::cfiles,args) rem + else begin + prerr_endline ("coqc: "^f^": no such file or directory") ; + exit 1 + end + in + parse ([],[]) (List.tl (Array.to_list Sys.argv)) + +(* main: we parse the command line, define the command to compile files + * and then call the compilation on each file *) + +let main () = + let cfiles, args = parse_args () in + if cfiles = [] then begin + prerr_endline "coqc: too few arguments" ; + usage () + end; + let coqtopname = Filename.concat !bindir "coqtop.byte" in + List.iter (compile coqtopname args) cfiles + +let _ = Printexc.print main (); exit 0 |