added URI concrete syntax

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 49b08a7c5d6b46bb942c01899ecfdf1dde178b61..1b1d690bdff2ca449fa26637d81f5ab4e7d10218 100644 (file)
--- 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 *)