diff options
Diffstat (limited to 'parsing/coqast.ml')
| -rw-r--r-- | parsing/coqast.ml | 31 |
1 files changed, 29 insertions, 2 deletions
diff --git a/parsing/coqast.ml b/parsing/coqast.ml index 9b65bdfb1..e9b9e3c14 100644 --- a/parsing/coqast.ml +++ b/parsing/coqast.ml @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames (*i*) type loc = int * int @@ -23,7 +24,7 @@ type t = | Num of loc * int | Str of loc * string | Id of loc * string - | Path of loc * section_path + | Path of loc * kernel_name | Dynamic of loc * Dyn.t type the_coq_ast = t @@ -62,7 +63,7 @@ module Hast = Hashcons.Make( type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string) - * (identifier -> identifier) * (section_path -> section_path)) + * (identifier -> identifier) * (kernel_name -> kernel_name)) let hash_sub (hast,(hloc,hstr,hid,hsp)) = function | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al) | Nmeta(l,s) -> Nmeta(hloc l, hstr s) @@ -98,6 +99,32 @@ let hcons_ast (hstr,hid,hpath) = let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in (hast,hloc) +let rec subst_ast subst ast = match ast with + | Node (l,s,astl) -> + let astl' = Util.list_smartmap (subst_ast subst) astl in + if astl' == astl then ast else + Node (l,s,astl') + | Slam (l,ido,ast1) -> + let ast1' = subst_ast subst ast1 in + if ast1' == ast1 then ast else + Slam (l,ido,ast1') + | Smetalam (l,s,ast1) -> + let ast1' = subst_ast subst ast1 in + if ast1' == ast1 then ast else + Smetalam (l,s,ast1') + | Path (loc,kn) -> + let kn' = Names.subst_kn subst kn in + if kn' == kn then ast else + Path(loc,kn') + | Nmeta _ + | Nvar _ -> ast + | Num _ + | Str _ + | Id _ + | Dynamic _ -> ast + + + (* type 'vernac_ast raw_typed_ast = | PureAstNode of t |