From 66a331a32509281f0c28ced014640e98a49cc0e0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 11 Jan 2005 16:08:24 +0000 Subject: [PATCH] added syntax for URIs --- .../ocaml/cic_disambiguation/cicTextualLexer2.ml | 12 ++++++++---- helm/ocaml/cic_disambiguation/disambiguate.ml | 16 ++++++++++++++-- helm/ocaml/cic_transformations/ast2pres.ml | 12 ++++++++---- helm/ocaml/cic_transformations/cicAstPp.ml | 8 +++++--- 4 files changed, 35 insertions(+), 13 deletions(-) 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 -- 2.39.2