From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 11 Jan 2005 16:08:24 +0000 (+0000)
Subject: added syntax for URIs
X-Git-Tag: V_0_1_0~144
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=66a331a32509281f0c28ced014640e98a49cc0e0;p=helm.git

added syntax for URIs
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 8a6faa193..b62230a33 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -33,8 +33,10 @@ let regexp blank = [ ' ' '\t' '\n' ]
 let regexp paren = [ '(' '[' '{' ')' ']' '}' ]
 let regexp implicit = '?'
 let regexp symbol_char =
-  [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' '\\' '(' '[' '{' ')' ']' '}' ]
-
+  [^ 'a' - 'z' 'A' - 'Z' '0' - '9'
+     ' ' '\t' '\n'
+     '\\' '(' '[' '{' ')' ']' '}' '?'
+  ]
 let regexp blanks = blank+
 let regexp num = digit+
 let regexp tex_token = '\\' alpha+
@@ -46,8 +48,10 @@ let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+)
 let regexp meta = implicit num
 let regexp qstring = '"' [^ '"']* '"'
 let regexp uri =
-  (*      schema      *) (*     path     *) (*  ext   *) (*    xpointer     *)
-  ("cic:/" | "theory:/") ident ('/' ident)* ('.' ident)+ ('#' num ('/' num)*)?
+  ("cic:/" | "theory:/")              (* schema *)
+  ident ('/' ident)*                  (* path *)
+  ('.' ident)+                        (* ext *)
+  ("#xpointer(" num ('/' num)+ ")")?    (* xpointer *)
 (* let regexp catchall = .* *)
 
 let keywords = Hashtbl.create 17
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index c384dc59f..2eafc81f3 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -195,15 +195,26 @@ let interpretate ~context ~env ast =
                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
-    | CicAst.Ident (name, subst) ->
+    | CicAst.Ident (name, subst)
+    | CicAst.Uri (name, subst) as ast ->
+        let is_uri = function CicAst.Uri _ -> true | _ -> false in
         (try
+          if is_uri ast then raise Not_found;(* don't search the env for URIs *)
           let index = find_in_environment name context in
           if subst <> None then
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
         with Not_found ->
-          let cic = resolve env (Id name) () in
+          let cic =
+            if is_uri ast then  (* we have the URI, build the term out of it *)
+              try
+                CicUtil.term_of_uri name
+              with UriManager.IllFormedUri _ ->
+                CicTextualParser2.fail loc "Ill formed URI"
+            else
+              resolve env (Id name) ()
+          in
           let mk_subst uris =
             let ids_to_uris =
               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
@@ -371,6 +382,7 @@ let domain_of_term ~context ast =
                   let dom' = aux loc context term in
                   dom' @ dom)
                 [Id name] subst))
+    | CicAst.Uri _ -> []
     | CicAst.Implicit -> []
     | CicAst.Num (num, i) -> [ Num i ]
     | CicAst.Meta (index, local_context) ->
diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 87944aa34..0eba3757f 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -77,8 +77,10 @@ and countterm current_size t =
                let size1 = countvar c var in
                countterm size1 s) current_size l in
           countterm size1 t
-    | A.Ident(s,None) -> current_size + (String.length s)
-    | A.Ident(s,Some l) ->
+    | A.Ident (s,None)
+    | A.Uri (s, None) -> current_size + (String.length s)
+    | A.Ident (s,Some l)
+    | A.Uri (s,Some l) ->
         List.fold_left 
           (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
@@ -278,7 +280,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
           make_defs "let rec" vars in
         Box.V(make_attributes [Some "helm","xref"] [xref],
               definitions@[ast2box ~tail body])
-    | A.Ident (s, subst) ->
+    | A.Ident (s, subst)
+    | A.Uri (s, subst) ->
         let subst =
           let rec make_substs start_txt = 
             function
@@ -423,7 +426,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.Symbol (name,_) -> 
         let attr = make_std_attributes xref in
         P.Mi (attr,name)
-    | A.Ident (name,subst) ->
+    | A.Ident (name,subst)
+    | A.Uri (name,subst) ->
         let attr = make_std_attributes xref in
         let rec make_subst =
           (function 
diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index 4c0412949..bb365d73c 100644
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -62,10 +62,12 @@ let rec pp_term = function
               sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
             definitions))
         (pp_term term)
-  | CicAst.Ident (name, Some [])
-  | CicAst.Ident (name, None) ->
+  | CicAst.Ident (name, Some []) | CicAst.Ident (name, None)
+  | CicAst.Uri (name, Some []) | CicAst.Uri (name, None) ->
       name
-  | CicAst.Ident (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs)
+  | CicAst.Ident (name, Some substs)
+  | CicAst.Uri (name, Some substs) ->
+      sprintf "%s \\subst [%s]" name (pp_substs substs)
   | CicAst.Implicit -> "?"
   | CicAst.Meta (index, substs) ->
       sprintf "%d[%s]" index