From a4f6e8b443d8a676bd2bfbf7f29369e070298aa0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Jan 2005 10:24:59 +0000 Subject: [PATCH] added URI concrete syntax --- .../cic_disambiguation/cicTextualParser2.ml | 27 +++++++++++++++---- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 49b08a7c5..1b1d690bd 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -79,6 +79,20 @@ let int_opt = function | None -> None | Some lexeme -> Some (int_of_string lexeme) + (** the uri of an inductive type (a ".ind" uri) is not meaningful without an + * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind" + * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive + * type in a block of mutual inductive types. + * + * This function performs the expansion foo.ind -> foo#xpointer..., if needed + *) +let ind_expansion uri = + let len = String.length uri in + if len >= 4 && String.sub uri (len - 4) 4 = ".ind" then + uri ^ "#xpointer(1/1)" + else + uri + EXTEND GLOBAL: term term0 tactic tactical tactical0 command script; int: [ @@ -110,9 +124,8 @@ EXTEND | i = IDENT -> (name_of_string i, None) ] ]; - substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = IDENT; - subst = OPT [ + subst: [ + [ subst = OPT [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) PAREN "["; substs = LIST1 [ @@ -120,8 +133,12 @@ EXTEND ] SEP SYMBOL ";"; PAREN "]" -> substs - ] -> - CicAst.Ident (s, subst) + ] -> subst + ] + ]; + substituted_name: [ (* a subs.name is an explicit substitution subject *) + [ s = IDENT; subst = subst -> CicAst.Ident (s, subst) + | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) -- 2.39.2