diff options
Diffstat (limited to 'parsing')
| -rwxr-xr-x | parsing/ast.ml | 23 | ||||
| -rwxr-xr-x | parsing/ast.mli | 2 | ||||
| -rw-r--r-- | parsing/coqast.ml | 16 | ||||
| -rw-r--r-- | parsing/coqast.mli | 3 | ||||
| -rw-r--r-- | parsing/esyntax.ml | 6 | ||||
| -rw-r--r-- | parsing/g_rsyntax.ml | 2 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 4 | ||||
| -rw-r--r-- | parsing/printer.ml | 10 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 8 | ||||
| -rw-r--r-- | parsing/termast.ml | 2 |
10 files changed, 51 insertions, 25 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml index 83cd633c1b..e366600c83 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -28,6 +28,7 @@ let loc = function | Id (loc,_) -> loc | Str (loc,_) -> loc | Path (loc,_) -> loc + | ConPath (loc,_) -> loc | Dynamic (loc,_) -> loc (* patterns of ast *) @@ -58,6 +59,7 @@ let nvar s = Nvar(dummy_loc,s) let num n = Num(dummy_loc,n) let string s = Str(dummy_loc,s) let path sl = Path(dummy_loc,sl) +let conpath sl = ConPath(dummy_loc,sl) let dynamic d = Dynamic(dummy_loc,d) let rec set_loc loc = function @@ -70,11 +72,11 @@ let rec set_loc loc = function | Str(_,s) -> Str(loc,s) | Num(_,s) -> Num(loc,s) | Path(_,sl) -> Path(loc,sl) + | ConPath(_,sl) -> ConPath(loc,sl) | Dynamic(_,d) -> Dynamic(loc,d) let path_section loc sp = Coqast.Path(loc, sp) - -let section_path sp = sp +let conpath_section loc sp = Coqast.ConPath(loc, sp) (* ast destructors *) let num_of_ast = function @@ -129,19 +131,23 @@ let string_of_dirpath = function let pr_id id = str (string_of_id id) -let print_kn kn = - let (mp,dp,l) = repr_kn kn in +let print_kn_or_con repr kn = + let (mp,dp,l) = repr kn in let dpl = repr_dirpath dp in str (string_of_mp mp) ++ str "." ++ prlist_with_sep (fun _ -> str".") pr_id dpl ++ str (string_of_label l) +let print_kn = print_kn_or_con repr_kn +let print_con = print_kn_or_con repr_con + (* Pretty-printing *) let rec print_ast ast = match ast with | Num(_,n) -> int n | Str(_,s) -> qs s | Path(_,sl) -> print_kn sl + | ConPath(_,sl) -> print_con sl | Id (_,s) -> str "{" ++ str s ++ str "}" | Nvar(_,s) -> pr_id s | Nmeta(_,s) -> str s @@ -208,6 +214,7 @@ let check_cast loc a k = | (Tid, Id _) -> () | (Tvar, Nvar _) -> () | (Tpath, Path _) -> () + | (Tpath, ConPath _) -> () | (Tstr, Str _) -> () | (Tnum, Num _) -> () | (Tlist, _) -> grammar_type_error (loc,"Ast.cast_val") @@ -291,6 +298,7 @@ let rec alpha alp a1 a2 = | (Str(_,s1),Str(_,s2)) -> s1=s2 | (Num(_,n1),Num(_,n2)) -> n1=n2 | (Path(_,sl1),Path(_,sl2)) -> sl1=sl2 + | (ConPath(_,sl1),ConPath(_,sl2)) -> sl1=sl2 | ((Smetalam _ | Nmeta _ | Dynamic _), _) -> false | (_, (Smetalam _ | Nmeta _ | Dynamic _)) -> false | _ -> false @@ -356,6 +364,7 @@ let rec amatch alp sigma spat ast = | (Pmeta(pv,Tnum), Num _) -> bind_env_ast sigma pv ast | (Pmeta(pv,Tstr), Str _) -> bind_env_ast sigma pv ast | (Pmeta(pv,Tpath), Path _) -> bind_env_ast sigma pv ast + | (Pmeta(pv,Tpath), ConPath _) -> bind_env_ast sigma pv ast | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch") | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) -> amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b @@ -472,7 +481,7 @@ let rec pat_of_ast env ast = (Pnode(op,pargs), env') (* Compatibility with new parsing mode *) | Nvar(loc,id) when (string_of_id id).[0] = '$' -> make_astvar env loc (string_of_id id) Tany - | (Path _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env) + | (Path _|ConPath _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env) | Dynamic(loc,_) -> invalid_arg_loc(loc,"pat_of_ast: dynamic") @@ -546,7 +555,7 @@ let rec val_of_ast env = function | Smetalam(loc,s,a) -> let _ = type_of_meta env loc s in (* ids are coerced to id lists *) Pmeta_slam(s, val_of_ast env a) - | (Path _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast) + | (Path _|ConPath _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast) | Slam(_,os,b) -> Pslam(os, val_of_ast env b) | Node(loc,op,_) when isMeta op -> user_err_loc(loc,"Ast.val_of_ast", @@ -577,7 +586,7 @@ let rec occur_var_ast s = function | Node(loc,op,args) -> List.exists (occur_var_ast s) args | Smetalam _ | Nmeta _ -> anomaly "occur_var: metas should not occur here" | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body - | Id _ | Str _ | Num _ | Path _ -> false + | Id _ | Str _ | Num _ | Path _ | ConPath _ -> false | Dynamic _ -> (* Hum... what to do here *) false diff --git a/parsing/ast.mli b/parsing/ast.mli index e6049f40ee..28e8e132f2 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -35,7 +35,7 @@ val dynamic : Dyn.t -> Coqast.t val set_loc : loc -> Coqast.t -> Coqast.t val path_section : loc -> kernel_name -> Coqast.t -val section_path : kernel_name -> kernel_name +val conpath_section : loc -> constant -> Coqast.t (* ast destructors *) val num_of_ast : Coqast.t -> int diff --git a/parsing/coqast.ml b/parsing/coqast.ml index 71dfd9547f..52681fe342 100644 --- a/parsing/coqast.ml +++ b/parsing/coqast.ml @@ -24,6 +24,7 @@ type t = | Str of loc * string | Id of loc * string | Path of loc * kernel_name + | ConPath of loc * constant | Dynamic of loc * Dyn.t type the_coq_ast = t @@ -62,8 +63,9 @@ module Hast = Hashcons.Make( type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string) - * (identifier -> identifier) * (kernel_name -> kernel_name)) - let hash_sub (hast,(hloc,hstr,hid,hsp)) = function + * (identifier -> identifier) * (kernel_name -> kernel_name) + * (constant -> constant)) + let hash_sub (hast,(hloc,hstr,hid,hsp,hcon)) = function | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al) | Nmeta(l,s) -> Nmeta(hloc l, hstr s) | Nvar(l,s) -> Nvar(hloc l, hid s) @@ -74,6 +76,7 @@ module Hast = Hashcons.Make( | Id(l,s) -> Id(hloc l, hstr s) | Str(l,s) -> Str(hloc l, hstr s) | Path(l,d) -> Path(hloc l, hsp d) + | ConPath(l,d) -> ConPath(hloc l, hcon d) | Dynamic(l,d) -> Dynamic(hloc l, d) let equal a1 a2 = match (a1,a2) with @@ -89,13 +92,14 @@ module Hast = Hashcons.Make( | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2 | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2 | (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2) + | (ConPath(l1,d1), ConPath(l2,d2)) -> (l1==l2 & d1==d2) | _ -> false let hash = Hashtbl.hash end) -let hcons_ast (hstr,hid,hpath) = +let hcons_ast (hstr,hid,hpath,hconpath) = let hloc = Hashcons.simple_hcons Hloc.f () in - let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in + let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath,hconpath) in (hast,hloc) let rec subst_ast subst ast = match ast with @@ -115,6 +119,10 @@ let rec subst_ast subst ast = match ast with let kn' = Names.subst_kn subst kn in if kn' == kn then ast else Path(loc,kn') + | ConPath (loc,kn) -> + let kn' = Names.subst_con subst kn in + if kn' == kn then ast else + ConPath(loc,kn') | Nmeta _ | Nvar _ -> ast | Num _ diff --git a/parsing/coqast.mli b/parsing/coqast.mli index 219e04f03d..fcb029319c 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -26,6 +26,7 @@ type t = | Str of loc * string | Id of loc * string | Path of loc * kernel_name + | ConPath of loc * constant | Dynamic of loc * Dyn.t (* returns the list of metas occuring in the ast *) @@ -38,7 +39,7 @@ val subst_meta : (int * t) list -> t -> t (* hash-consing function *) val hcons_ast: (string -> string) * (Names.identifier -> Names.identifier) - * (kernel_name -> kernel_name) + * (kernel_name -> kernel_name) * (constant -> constant) -> (t -> t) * (loc -> loc) val subst_ast: Names.substitution -> t -> t diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 77e5a75263..464c1fffd9 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -41,7 +41,7 @@ type key = let warning_verbose = ref true let ast_keys = function - | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl)]) ::_) -> + | Node(_,"APPLIST", Node(_,"CONST", [ConPath (_,sl)]) ::_) -> [Cst sl; Nod "APPLIST"; All] | Node(_,"APPLIST", Node(_,"SECVAR", [Nvar (_,s)]) ::_) -> [SecVar s; Nod "APPLIST"; All] @@ -57,7 +57,7 @@ let spat_key astp = match astp with | Pnode("APPLIST", Pcons(Pnode("CONST", - Pcons(Pquote(Path (_,sl)),_)), _)) + Pcons(Pquote(ConPath (_,sl)),_)), _)) -> Cst sl | Pnode("APPLIST", Pcons(Pnode("SECVAR", @@ -165,7 +165,7 @@ let _ = declare_primitive_printer "token" token_printer (* A printer for the tokens. *) let token_printer stdpr = function - | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast + | (Id _ | Num _ | Str _ | Path _ | ConPath _ as ast) -> print_ast ast | a -> stdpr a (* Unused ?? diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 8f5aad33be..72f54721aa 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -175,7 +175,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] (* TODO: temporary hack *) -let make_path dir id = Libnames.encode_kn dir (id_of_string id) +let make_path dir id = Libnames.encode_con dir (id_of_string id) let glob_R = ConstRef (make_path rdefinitions "R") let glob_R1 = ConstRef (make_path rdefinitions "R1") diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f84aa664b8..e308230782 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -363,7 +363,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = | (_,"VARIABLE") -> Some (print_section_variable (basename sp)) | (_,"CONSTANT") -> - Some (print_constant with_values sep kn) + Some (print_constant with_values sep (constant_of_kn kn)) | (_,"INDUCTIVE") -> Some (print_inductive kn) | (_,"MODULE") -> @@ -552,7 +552,7 @@ let print_local_context () = | (oname,Lib.Leaf lobj)::rest -> (match object_tag lobj with | "CONSTANT" -> - let kn = snd oname in + let kn = constant_of_kn (snd oname) in let {const_body=val_0;const_type=typ} = Global.lookup_constant kn in (print_last_const rest ++ diff --git a/parsing/printer.ml b/parsing/printer.ml index 06a1cc8128..757b61aa1d 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -46,7 +46,7 @@ let dfltpr ast = (str"#GENTERM " ++ print_ast ast);; let global_const_name kn = try pr_global Idset.empty (ConstRef kn) with Not_found -> (* May happen in debug *) - (str ("CONST("^(string_of_kn kn)^")")) + (str ("CONST("^(string_of_con kn)^")")) let global_var_name id = try pr_global Idset.empty (VarRef id) @@ -67,14 +67,14 @@ let global_constr_name ((kn,tyi),i) = let globpr gt = match gt with | Nvar(_,s) -> (pr_id s) | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev))) - | Node(_,"CONST",[Path(_,sl)]) -> - global_const_name (section_path sl) + | Node(_,"CONST",[ConPath(_,sl)]) -> + global_const_name sl | Node(_,"SECVAR",[Nvar(_,s)]) -> global_var_name s | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) -> - global_ind_name (section_path sl, tyi) + global_ind_name (sl, tyi) | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) -> - global_constr_name ((section_path sl, tyi), i) + global_constr_name ((sl, tyi), i) | Dynamic(_,d) -> if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>") else dfltpr gt diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index ec1e6410e8..e1bb51dd79 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -85,6 +85,14 @@ let rec mlexpr_of_ast = function let e = expr_list_of_var_list e in <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$) (Names.id_of_string $str:Names.string_of_id a$)) >> + | Coqast.ConPath (loc, kn) -> + let l,a = Libnames.decode_con kn in + let mlexpr_of_modid id = + <:expr< Names.id_of_string $str:string_of_id id$ >> in + let e = List.map mlexpr_of_modid (repr_dirpath l) in + let e = expr_list_of_var_list e in + <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$) + (Names.id_of_string $str:Names.string_of_id a$)) >> | Coqast.Dynamic (_, _) -> failwith "Q_Coqast: dynamic: not implemented" diff --git a/parsing/termast.ml b/parsing/termast.ml index 021025f74a..efa6c92068 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -119,7 +119,7 @@ let ast_body_of_binder bl t = bl t let ast_of_constant_ref sp = - ope("CONST", [path_section dummy_loc sp]) + ope("CONST", [conpath_section dummy_loc sp]) let ast_of_existential_ref ev = (* |