diff options
-rw-r--r-- | parsing/.cvsignore | 2 | ||||
-rw-r--r-- | parsing/astterm.ml | 3 | ||||
-rw-r--r-- | parsing/astterm.mli | 1 | ||||
-rw-r--r-- | parsing/esyntax.ml | 2 | ||||
-rw-r--r-- | parsing/extend.ml4 | 2 | ||||
-rw-r--r-- | parsing/lexer.mli | 1 | ||||
-rw-r--r-- | parsing/lexer.mll | 82 | ||||
-rw-r--r-- | parsing/pretty.ml | 17 | ||||
-rw-r--r-- | parsing/termast.ml | 6 |
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 [] |