From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 18 Aug 2007 20:34:57 +0000 Subject: Imported Upstream version 8.1.pl1+dfsg --- tools/coqdep.ml | 38 +++++++++++++++++++++++++++----------- tools/coqdoc/output.ml | 15 +++++++-------- tools/coqdoc/pretty.mll | 20 +++++++++++++------- tools/coqwc.mll | 8 +++++--- 4 files changed, 52 insertions(+), 29 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 3647152a..89f39b22 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 9276 2006-10-25 13:00:22Z barras $ *) +(* $Id: coqdep.ml 9808 2007-04-29 07:15:18Z herbelin $ *) open Printf open Coqdep_lexer @@ -24,6 +24,8 @@ let option_i = ref false let option_sort = ref false let option_slash = ref false +let directories_added = ref false + let suffixe = ref ".vo" let suffixe_spec = ref ".vi" @@ -42,7 +44,7 @@ let file_concat l = (* Files specified on the command line *) let mlAccu = ref ([] : (string * string * dir) list) and mliAccu = ref ([] : (string * string * dir) list) -and vAccu = ref ([] : string list) +and vAccu = ref ([] : (string * string) list) (* Queue operations *) let addQueue q v = q := v :: !q @@ -97,6 +99,16 @@ let safe_assoc verbose file k = List.assoc k !vKnown +let absolute_dir dir = + let current = Sys.getcwd () in + Sys.chdir dir; + let dir' = Sys.getcwd () in + Sys.chdir current; + dir' + +let absolute_file_name basename odir = + let dir = match odir with Some dir -> dir | None -> "." in + absolute_dir dir / basename let file_name = function | (s,None) -> file_concat s @@ -152,9 +164,11 @@ let cut_prefix p s = let ls = String.length s in if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s -let canonize f = match Sys.os_type with - | "Win32" when not !option_slash -> cut_prefix ".\\" f - | _ -> cut_prefix "./" f +let canonize f = + let f' = absolute_dir (Filename.dirname f) / Filename.basename f in + match List.filter (fun (_,full) -> f' = full) !vAccu with + | (f,_) :: _ -> f + | _ -> f let sort () = let seen = Hashtbl.create 97 in @@ -181,7 +195,7 @@ let sort () = printf "%s%s " file !suffixe end in - List.iter loop !vAccu + List.iter (fun (name,_) -> loop name) !vAccu let traite_fichier_Coq verbose f = try @@ -352,7 +366,7 @@ let mL_dependencies () = let coq_dependencies () = List.iter - (fun name -> + (fun (name,_) -> printf "%s%s: %s.v" name !suffixe name; traite_fichier_Coq true (name ^ ".v"); printf "\n"; @@ -366,7 +380,7 @@ let coq_dependencies () = let declare_dependencies () = List.iter - (fun name -> + (fun (name,_) -> traite_Declare (name^".v"); flush stdout) (List.rev !vAccu) @@ -410,7 +424,7 @@ let all_subdirs root_dir log_dir = let usage () = eprintf - "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] + ]\n"; + "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] + ]\n"; flush stderr; exit 1 @@ -471,7 +485,8 @@ let coqdep () = addQueue mliAccu (basename,".mli",dirname) else if Filename.check_suffix name ".v" then let basename = Filename.chop_suffix name ".v" in - addQueue vAccu (file_name ([basename], dirname)) + let name = file_name ([basename],dirname) in + addQueue vAccu (name, absolute_file_name basename dirname) | _ -> () in let add_known phys_dir log_dir f = @@ -496,6 +511,7 @@ let coqdep () = (fun n -> safe_addQueue clash_v vKnown (n,file)) paths | _ -> () in let add_directory (phys_dir, log_dir) = + directories_added := true; match try (stat phys_dir).st_kind with _ -> S_BLK with | S_DIR -> (let dir = opendir phys_dir in @@ -526,7 +542,7 @@ let coqdep () = | f :: ll -> treat None f; parse ll | [] -> () in - add_directory (".", []); + if not !directories_added then add_directory (".", []); parse (List.tl (Array.to_list Sys.argv)); List.iter (fun (s,_) -> add_coqlib_directory s) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 84e03d92..28a0cd6d 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: output.ml 9976 2007-07-12 11:58:30Z msozeau $ i*) open Cdglobals open Index @@ -40,15 +40,14 @@ let is_keyword = "Module"; "Module Type"; "Declare Module"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; + "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Unset"; "Variable"; "Variables"; "Notation"; - (*i (* correctness *) - "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if"; - "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant"; - "while"; i*) - (*i (* coq terms *) - "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*) + (* Program *) + "Program Definition"; "Program Fixpoint"; "Program Lemma"; + "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; + (*i (* coq terms *) *) + "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":=" ] (*s Current Coq module *) diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index bdb58f86..c63a6a9b 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 9204 2006-10-04 13:05:58Z notin $ i*) +(*i $Id: pretty.mll 10017 2007-07-18 13:23:55Z notin $ i*) (*s Utility functions for the scanners *) @@ -212,6 +212,8 @@ let def_token = | "Scheme" | "Inductive" | "CoInductive" + | "Program" space+ "Definition" + | "Program" space+ "Fixpoint" let decl_token = "Hypothesis" @@ -455,11 +457,11 @@ and doc = parse start_inline_coq (); escaped_coq lexbuf; end_inline_coq (); doc lexbuf } | "[[" '\n' space* - { formatted := true; start_code (); + { formatted := true; line_break (); start_inline_coq (); indentation (count_spaces (lexeme lexbuf)); - without_gallina coq lexbuf; - end_code (); formatted := false; - doc lexbuf } + let eol = body_bol lexbuf in + end_inline_coq (); formatted := false; + if eol then doc_bol lexbuf else doc lexbuf} | '*'* "*)" space* '\n' { true } | '*'* "*)" @@ -570,6 +572,8 @@ and body_bol = parse and body = parse | '\n' {line_break(); body_bol lexbuf} + | '\n'+ space* "]]" + { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true } | eof { false } | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true } | '.' space+ { char '.'; char ' '; false } @@ -577,12 +581,14 @@ and body = parse if eol then body_bol lexbuf else body lexbuf } | identifier { let s = lexeme lexbuf in - ident s (lexeme_start lexbuf); body lexbuf } + ident s (lexeme_start lexbuf); + body lexbuf } | token { let s = lexeme lexbuf in symbol s; body lexbuf } | _ { let c = lexeme_char lexbuf 0 in - char c; body lexbuf } + char c; + body lexbuf } and skip_hide = parse | eof | end_hide { () } diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 26b64095..0ce172ea 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -9,7 +9,7 @@ (* coqwc - counts the lines of spec, proof and comments in Coq sources * Copyright (C) 2003 Jean-Christophe Filliātre *) -(*i $Id: coqwc.mll 7095 2005-05-31 15:05:23Z filliatr $ i*) +(*i $Id: coqwc.mll 9976 2007-07-12 11:58:30Z msozeau $ i*) (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. It assumes the files to be lexically well-formed. *) @@ -97,7 +97,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036" let stars = "(*" '*'* "*)" let dot = '.' (' ' | '\t' | '\n' | '\r' | eof) let proof_start = - "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" + "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next" let proof_end = ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.' @@ -114,8 +114,10 @@ rule spec = parse { seen_spec := true; spec_to_dot lexbuf; proof lexbuf } | proof_start '\n' { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf } - | "Definition" space + | "Program"? "Definition" space { seen_spec := true; definition lexbuf } + | "Program"? "Fixpoint" space + { seen_spec := true; definition lexbuf } | character | _ { seen_spec := true; spec lexbuf } | eof { () } -- cgit v1.2.3