mise au point lexer / debugage PP

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@205 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 87 insertions, 29 deletions

diff --git a/parsing/.cvsignore b/parsing/.cvsignore
index 87551eece..7d96a5222 100644
--- a/parsing/.cvsignore
+++ b/parsing/.cvsignore
@@ -1,2 +1,4 @@
 lexer.ml
 *.ppo
+pcoq.ml
+extend.ml
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 7babfe020..5799e3515 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -494,6 +494,9 @@ let constr_of_com sigma env com =
 let constr_of_com_sort sigma sign com =
   constr_of_com1 true sigma sign com
 
+let constr_of_com_pattern sigma sign com =
+  constr_of_com1 true sigma sign com
+
 let fconstr_of_com1 is_ass sigma env com = 
   fconstr_of_com_env1 is_ass sigma env com
 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 8f844e600..d762faba1 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -46,6 +46,7 @@ val constr_of_com_casted : 'a evar_map -> env -> Coqast.t -> constr ->
 val constr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
 val constr_of_com : 'a evar_map -> env -> Coqast.t -> constr
 val constr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
+val constr_of_com_pattern : 'a evar_map -> env -> Coqast.t -> constr
 
 val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
 val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index da7383d63..71edadb8f 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -63,7 +63,7 @@ let find_syntax_entry whatfor gt =
   let gt_keys = ast_keys gt in
   let entries =
     List.flatten
-      (List.map (fun k -> Gmap.find (whatfor,k) !from_key_table) gt_keys)
+      (List.map (fun k -> Gmapl.find (whatfor,k) !from_key_table) gt_keys)
   in 
   first_match (fun se -> se.syn_astpat) [] gt entries
 
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index 682d060ab..5b0474156 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -8,7 +8,7 @@ open Pcoq
 open Coqast
 open Ast
 
-open Vernac
+open Pcoq.Vernac
 
 GEXTEND Gram
   vernac:
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 469e61393..982e29436 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -5,7 +5,6 @@ exception BadToken of string
 
 val add_keyword : string -> unit
 val is_keyword : string -> bool
-val find_keyword : string -> string
 
 val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
 
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index adafc2c84..680835499 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -13,13 +13,53 @@ exception BadToken of string
 
 exception Error of error * int * int
 
-type frozen_t = string list
+(* token trees *)
 
-let kw_table = Hashtbl.create 149
+module Charmap = Map.Make (struct type t = char let compare = compare end)
+
+type ttree = { node : string option; branch : ttree Charmap.t }
+
+let ttree_empty = { node = None; branch = Charmap.empty }
+
+let ttree_add ttree str =
+  let n = String.length str in
+  let rec insert tt i =
+    if i == n then 
+      { node = Some str; branch = tt.branch }
+    else
+      let c = str.[i] in
+      let br =
+        match 
+	  try Some (Charmap.find c tt.branch) with Not_found -> None
+        with
+          | Some tt' ->
+              Charmap.add c (insert tt' (i + 1)) (Charmap.remove c tt.branch)
+          | None ->
+              let tt' = { node = None; branch = Charmap.empty } in
+              Charmap.add c (insert tt' (i + 1)) tt.branch
+      in
+      { node = tt.node; branch = br }
+  in 
+  insert ttree 0
+
+let ttree_find ttree str =
+  let n = String.length str in
+  let rec proc_rec tt i =
+    if i == n then
+      match tt.node with
+	| Some s -> s
+      	| None -> raise Not_found
+    else 
+      proc_rec (Charmap.find str.[i] tt.branch) (i+1)
+  in 
+  proc_rec ttree 0
+
+let kw_table = ref ttree_empty
 
 let init () =
-  Hashtbl.clear kw_table;
-  List.iter (fun kw -> Hashtbl.add kw_table kw ())
+  kw_table := ttree_empty;
+  List.iter 
+    (fun kw -> kw_table := ttree_add !kw_table kw)
     [ "Grammar"; "Syntax"; "Quit"; "Load"; "Compile";
       "of"; "with"; "end"; "as"; "in"; "using";
       "Cases"; "Fixpoint"; "CoFixpoint";
@@ -28,21 +68,19 @@ let init () =
       "Orelse"; "Proof"; "Qed";
       "Prop"; "Set"; "Type" ]  
 
-let add_keyword s = Hashtbl.add kw_table s ()
+let _ = init ()
+
+let add_keyword s = kw_table := ttree_add !kw_table s
 
-let is_keyword s = try Hashtbl.find kw_table s; true with Not_found -> false
+let is_keyword s = 
+  try let _ = ttree_find !kw_table s in true with Not_found -> false
 
-let freeze () = 
-  let l = ref [] in
-  Hashtbl.iter (fun k _ -> l := k :: !l) kw_table;
-  !l
+type frozen_t = ttree
 
-let unfreeze ft =
-  init ();
-  List.iter add_keyword ft
+let freeze () = !kw_table
+
+let unfreeze ft = kw_table := ft
 
-let find_keyword s = if is_keyword s then s else raise Not_found
-      
 let char_for_backslash =
   match Sys.os_type with
   | "Unix" | "Win32" ->
@@ -79,12 +117,13 @@ let comment_start_pos = ref 0
 
 let blank = [' ' '\010' '\013' '\009' '\012']
 let firstchar = 
-  ['$' 'A'-'Z' 'a'-'z' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
    '\'' '0'-'9']
 let symbolchar =
-  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' ';' '=' '?' '@' '^' '|' '~' '#']
+  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' ',' ';' '=' '?' '@' '^'
+   '|' '~' '#']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
 let oct_literal = '0' ['o' 'O'] ['0'-'7']+
@@ -197,8 +236,15 @@ let func cs =
   let ts = Stream.from next_token in
   (ts, find_loc loct)
 
+let is_ident s =
+  String.length s > 0 &&
+  (match s.[0] with
+     | '$' | 'A'..'Z' | 'a'..'z' | '\192'..'\214' | '\216'..'\246' 
+     | '\248'..'\255' -> true
+     | _ -> false)
+
 let add_token = function
-  | ("",kw) -> add_keyword kw
+  | ("",kw) -> if is_ident kw then add_keyword kw
   | _ -> ()
 	 
 let token_text = function
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 20083b8ea..0e062f6c9 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -222,7 +222,7 @@ let print_leaf_entry with_values sep (spopt,lobj) =
 	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") ->
+    | (sp,("CONSTANT"|"PARAMETER")) ->
 	let cb = Global.lookup_constant sp in
 	if kind_of_path sp = CCI then
 	  let val_0 = cb.const_body in
@@ -364,7 +364,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
                if (head_const typ.body) = const then  
                  fn (string_of_id namec) hyps typ.body;
                crible_rec rest
-	   | (sp,"CONSTANT") ->
+	   | (sp,("CONSTANT"|"PARAMETER")) ->
 	       let {const_type=typ} = Global.lookup_constant sp in
                if (head_const typ.body) = const then
                  fn (print_basename sp) hyps typ.body;
@@ -422,8 +422,15 @@ let print_eval red_fun env {uj_val=trm;uj_type=typ} =
 let print_name name = 
   let str = string_of_id name in 
   try 
-    let sp = Nametab.sp_of_id CCI name in  
-    let lobj = Lib.map_leaf (objsp_of sp) in
+    let (sp,lobj) = 
+      let (sp,entry) =
+      	List.find (fun en -> basename (fst en) = name) 
+	  (Lib.contents_after None)
+      in
+      match entry with
+	| Lib.Leaf obj -> (sp,obj)
+	| _ -> raise Not_found
+    in
     print_leaf_entry true " = " (sp,lobj)
   with 
     | Not_found -> 
@@ -477,7 +484,7 @@ let print_local_context () =
   and print_last_const = function
     | (sp,Lib.Leaf lobj)::rest -> 
         (match object_tag lobj with
-           | "CONSTANT" -> 
+           | "CONSTANT" | "PARAMETER" -> 
                let {const_body=val_0;const_type=typ} = 
 		 Global.lookup_constant sp in
                [< print_last_const rest;
diff --git a/parsing/termast.ml b/parsing/termast.ml
index d26363ca3..cdaa2a268 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -852,7 +852,7 @@ let rec ast_of_raw avoid env = function
 	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
 	  (* non dépendant, pour isoler l'implication; peut-être un *)
 	  (* constructeur ARROW serait-il plus justifié ? *) 
-	| BProd -> if n=1 then "PROD" else "PROLIST" 
+	| BProd -> if n=1 then "PROD" else "PRODLIST" 
       in
       ope(tag,[ast_of_raw [] env t;a])
 
@@ -963,7 +963,7 @@ and weak_concrete_name avoid env na c =
     | Anonymous -> (None,avoid)
     | Name id -> (Some id,avoid)
 
-let bdize_no_casts at_top env t =
+let bdize at_top env t =
   try
     let avoid = if at_top then ids_of_env env else [] in
     ast_of_raw avoid env (detype t)
@@ -984,6 +984,6 @@ let rec strong whdfun t =
     | VAR _ as t -> t
     | Rel _ as t -> t
 
-let bdize at_top env t = bdize_no_casts at_top env (strong strip_outer_cast t) 
+let bdize_no_casts at_top env t = bdize at_top env (strong strip_outer_cast t) 
 			   
 let ast_of_rawconstr = ast_of_raw []