diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 18:37:54 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 18:37:54 +0000 |
commit | e88e0b2140bdd2d194a52bc09f8338b5667d0f92 (patch) | |
tree | 67ca22f77ddb98725456e5f9a0b5ad613ae28da5 /library/libnames.ml | |
parent | e4efb857fa9053c41e4c030256bd17de7e24542f (diff) |
Réforme de l'interprétation des termes :
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.ml')
-rw-r--r-- | library/libnames.ml | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 19e7d2833..79acb7231 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -11,6 +11,8 @@ open Pp open Util open Names +open Nameops +open Term type global_reference = | VarRef of variable @@ -30,6 +32,18 @@ let subst_global subst ref = match ref with let kn' = subst_kn subst kn in if kn==kn' then ref else ConstructRef ((kn',i),j) +let reference_of_constr c = match kind_of_term c with + | Const sp -> ConstRef sp + | Ind ind_sp -> IndRef ind_sp + | Construct cstr_cp -> ConstructRef cstr_cp + | Var id -> VarRef id + | _ -> raise Not_found + +let constr_of_reference = function + | VarRef id -> mkVar id + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkConstruct sp + | IndRef sp -> mkInd sp (**********************************************) @@ -205,3 +219,23 @@ type global_dir_reference = let kn' = subst_kernel_name subst kn in if kn==kn' then ref else ModTypeRef kn' *) + +type reference = + | Qualid of qualid located + | Ident of identifier located + +let qualid_of_reference = function + | Qualid (loc,qid) -> loc, qid + | Ident (loc,id) -> loc, make_short_qualid id + +let string_of_reference = function + | Qualid (loc,qid) -> string_of_qualid qid + | Ident (loc,id) -> string_of_id id + +let pr_reference = function + | Qualid (_,qid) -> pr_qualid qid + | Ident (_,id) -> pr_id id + +let loc_of_reference = function + | Qualid (loc,qid) -> loc + | Ident (loc,id) -> loc |