-requires="http unix pcre zip helm-xml helm-logger helm-urimanager helm-registry"
+requires="http unix pcre zip helm-xml helm-logger helm-ng_kernel helm-registry"
version="0.0.1"
archive(byte)="getter.cma"
archive(native)="getter.cmxa"
+++ /dev/null
-requires="str"
-version="0.0.1"
-archive(byte)="urimanager.cma"
-archive(native)="urimanager.cmxa"
-linkopts=""
registry \
syntax_extensions \
thread \
- urimanager \
logger \
+ ng_kernel \
getter \
library \
- ng_kernel \
content \
grafite \
disambiguation \
- ng_kernel \
ng_refiner \
ng_disambiguation \
ng_cic_content \
type 'term cobj =
id * (* id *)
- UriManager.uri list * (* params *)
'term conjecture list option * (* optional metasenv *)
'term in_object_context_element (* actual object *)
;;
type 'term cobj =
id * (* id *)
- UriManager.uri list * (* params *)
'term conjecture list option * (* optional metasenv *)
'term in_object_context_element (* actual object *)
;;
type term_info =
{ sort: (cic_id, Ast.sort_kind) Hashtbl.t;
- uri: (cic_id, UriManager.uri) Hashtbl.t;
+ uri: (cic_id, NReference.reference) Hashtbl.t;
}
(* persistent state *)
let init () = List.iter (fun f -> f []) !load_patterns32s
let instantiate_appl_pattern
- ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern
+ ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern
=
let lookup name =
try List.assoc name env
assert false
in
let rec aux = function
- | Ast.UriPattern uri -> term_of_uri uri
| Ast.NRefPattern nref -> term_of_nref nref
| Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
val instantiate_appl_pattern:
mk_appl:('term list -> 'term) ->
mk_implicit:(bool -> 'term) ->
- term_of_uri : (UriManager.uri -> 'term) ->
term_of_nref : (NReference.reference -> 'term) ->
(string * 'term) list -> NotationPt.cic_appl_pattern ->
'term
sprintf " in %s%s" ty
(match debug_printing, href_opt with
| true, Some uri ->
- sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> ""))
(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(pp_patterns patterns)
let head_pp =
head ^
(match debug_printing, href with
- | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> "")
in
sprintf "%s \\Rightarrow %s"
env)
let rec pp_cic_appl_pattern = function
- | Ast.UriPattern uri -> UriManager.string_of_uri uri
| Ast.NRefPattern nref -> NReference.string_of_reference nref
| Ast.VarPattern name -> name
| Ast.ImplicitPattern -> "?"
let (x, y) = HExtlib.loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
-type href = UriManager.uri
+type href = NReference.reference
type child_pos = [ `Left | `Right | `Inner ]
| IdentArg of int * string (* eta-depth, name *)
type cic_appl_pattern =
- | UriPattern of UriManager.uri
| NRefPattern of NReference.reference
| VarPattern of string
| ImplicitPattern
let find_appl_pattern_uris ap =
let rec aux acc =
function
- | Ast.UriPattern uri -> `Uri uri :: acc
- | Ast.NRefPattern nref -> `NRef nref :: acc
+ | Ast.NRefPattern nref -> nref :: acc
| Ast.ImplicitPattern
| Ast.VarPattern _ -> acc
| Ast.ApplPattern apl -> List.fold_left aux acc apl
in
let uris = aux [] ap in
- let cmp u1 u2 =
- match u1,u2 with
- `Uri u1, `Uri u2 -> UriManager.compare u1 u2
- | `NRef r1, `NRef r2 -> NReference.compare r1 r2
- | `Uri _,`NRef _ -> -1
- | `NRef _, `Uri _ -> 1
- in
- HExtlib.list_uniq (List.fast_sort cmp uris)
+ HExtlib.list_uniq (List.fast_sort NReference.compare uris)
let rec find_branch =
function
val ungroup: NotationPt.term list -> NotationPt.term list
val find_appl_pattern_uris:
- NotationPt.cic_appl_pattern ->
- [`Uri of UriManager.uri | `NRef of NReference.reference] list
+ NotationPt.cic_appl_pattern -> NReference.reference list
val find_branch:
NotationPt.term -> NotationPt.term
let lookup_uri ids_to_uris id =
try
let uri = Hashtbl.find ids_to_uris id in
- Some (UriManager.string_of_uri uri)
+ Some (NReference.string_of_reference uri)
with Not_found -> None
;;
(** {2 Rendering} *)
-val lookup_uri: (Interpretations.cic_id,UriManager.uri) Hashtbl.t ->
+val lookup_uri: (Interpretations.cic_id,NReference.reference) Hashtbl.t ->
Interpretations.cic_id -> string option
(** level 1 -> level 0
(let _ = incr counter; in (string_of_int !counter)))) ::
(List.map (conjecture2pres term2pres) metasenv'))]
-let params2pres params =
- let param2pres uri =
- B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
- (UriManager.name_of_uri uri)
- in
- let rec spatiate = function
- | [] -> []
- | hd :: [] -> [hd]
- | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
- in
- match params with
- | [] -> []
- | p ->
- let params = spatiate (List.map param2pres p) in
- [B.b_space;
- B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
let inductive2pres term2pres ind =
let constructor2pres decl =
B.b_h [] [
let ncontent2pres0
?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
- (id,params,metasenv,obj : NotationPt.term Content.cobj)
+ (id,metasenv,obj : NotationPt.term Content.cobj)
=
match obj with
| `Def (Content.Const, thesis, `Proof p) ->
B.b_v
[Some "helm","xref","id"]
([ B.b_h [] (B.b_kw ("ntheorem " ^ name) ::
- params2pres params @ [B.b_kw ":"]);
+ [B.b_kw ":"]);
B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @
metasenv2pres term2pres metasenv @
[proof ; B.b_kw "qed."])
B.b_v
[Some "helm","xref","id"]
([B.b_h []
- (B.b_kw ("ndefinition " ^ name) :: params2pres params @ [B.b_kw ":"]);
+ (B.b_kw ("ndefinition " ^ name) :: [B.b_kw ":"]);
B.indent (term2pres ty)] @
metasenv2pres term2pres metasenv @
[B.b_kw ":=";
let name = get_name decl.Content.dec_name in
B.b_v
[Some "helm","xref","id"]
- ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: params2pres params);
+ ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: []);
B.b_kw "Type:";
B.indent (term2pres decl.Content.dec_type)] @
metasenv2pres term2pres metasenv)
match href with
| None -> ident i
| Some href ->
- let href = UriManager.string_of_uri href in
+ let href = NReference.string_of_reference href in
add_xml_attrs [Some "xlink", "href", href] (ident i)
let binder_symbol s =
open Printf
open DisambiguateTypes
-open UriManager
module Ast = NotationPt
selection_mode:[`SINGLE | `MULTIPLE] ->
?ok:string ->
?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> UriManager.uri list ->
- UriManager.uri list
+ title:string -> msg:string -> id:string -> NReference.reference list ->
+ NReference.reference list
type interactive_interpretation_choice_type = string -> int ->
(Stdpp.location list * string * string) list list -> int list
type input_or_locate_uri_type =
- title:string -> ?id:string -> unit -> UriManager.uri option
+ title:string -> ?id:string -> unit -> NReference.reference option
let string_of_domain_item = function
| Id s -> Printf.sprintf "ID(%s)" s
selection_mode:[`SINGLE | `MULTIPLE] ->
?ok:string ->
?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> UriManager.uri list ->
- UriManager.uri list
+ title:string -> msg:string -> id:string -> NReference.reference list ->
+ NReference.reference list
type interactive_interpretation_choice_type = string -> int ->
(Stdpp.location list * string * string) list list -> int list
type input_or_locate_uri_type =
- title:string -> ?id:string -> unit -> UriManager.uri option
+ title:string -> ?id:string -> unit -> NReference.reference option
val string_of_domain_item: domain_item -> string
let uri = deref_index_theory ~local uri in
Http_getter_storage.exists ~local (uri ^ xml_suffix)
-let is_an_obj s =
- try
- s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
- with UriManager.IllFormedUri _ -> true
+let is_an_obj s = s <> NUri.baseuri_of_uri (NUri.uri_of_string s)
let resolve ~local ~writable uri =
if remote () then
(* Shorthands from now on *)
-let getxml' uri = getxml (UriManager.string_of_uri uri)
+let getxml' uri = getxml (NUri.string_of_uri uri)
let resolve' ~local ~writable uri =
- resolve ~local ~writable (UriManager.string_of_uri uri)
+ resolve ~local ~writable (NUri.string_of_uri uri)
;;
-let exists' ~local uri = exists ~local (UriManager.string_of_uri uri)
+let exists' ~local uri = exists ~local (NUri.string_of_uri uri)
let filename' ~local ~writable uri =
- filename ~local ~writable (UriManager.string_of_uri uri)
+ filename ~local ~writable (NUri.string_of_uri uri)
;;
let tilde_expand_key k =
(** {2 UriManager shorthands} *)
-val getxml' : UriManager.uri -> string
-val resolve' : local:bool -> writable:bool -> UriManager.uri -> string
-val exists' : local:bool -> UriManager.uri -> bool
-val filename' : local:bool -> writable:bool -> UriManager.uri -> string
+val getxml' : NUri.uri -> string
+val resolve' : local:bool -> writable:bool -> NUri.uri -> string
+val exists' : local:bool -> NUri.uri -> bool
+val filename' : local:bool -> writable:bool -> NUri.uri -> string
(** {2 Misc} *)
(raw: moo)
let rehash_cmd_uris =
- let rehash_uri uri =
- UriManager.uri_of_string (UriManager.string_of_uri uri) in
function
| GrafiteAst.Include _ as cmd -> cmd
| cmd ->
do_heavy_checks: bool ;
}
-let concat_nuris uris nuris =
- match uris,nuris with
- | `New uris, `New nuris -> `New (nuris@uris)
- | _ -> assert false
-;;
-
let basic_eval_unification_hint (t,n) status =
NCicUnifHint.add_user_provided_hint status t n
;;
let status = basic_eval_unification_hint (t,n) status in
let dump = inject_unification_hint (t,n)::status#dump in
let status = status#set_dump dump in
- status,`New []
+ status,[]
;;
let basic_index_obj l status =
let status = basic_eval_add_constraint (u1,u2) status in
let dump = inject_constraint (u1,u2)::status#dump in
let status = status#set_dump dump in
- status,`New []
+ status,[]
;;
let eval_ng_tac tac =
let uris = uri::List.rev uris_rev in
*)
let status = status#set_ng_mode `CommandMode in
- let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+ let status = LexiconSync.add_aliases_for_objs status [uri] in
let status,uris =
List.fold_left
(fun (status,uris) boxml ->
status, uris
end
else
- nstatus, concat_nuris uris nuris
+ nstatus, uris@nuris
with
| MultiPassDisambiguator.DisambiguationError _
| NCicTypeChecker.TypeCheckerFailure _ ->
(*HLog.warn "error in generating projection/eliminator";*)
status,uris
- ) (status,`New [] (* uris *)) boxml in
+ ) (status,[] (* uris *)) boxml in
let _,_,_,_,nobj = obj in
let status = match nobj with
NCic.Inductive (is_ind,leftno,[it],_) ->
let _,_,menv,_,_ = invobj in
fst (match menv with
[] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> status,`New []))
+ | _ -> status,[]))
(* XXX *)
with _ -> (*HLog.warn "error in generating inversion principle"; *)
let status = status#set_ng_mode `CommandMode in status)
basic_eval_and_record_ncoercion_from_t_cpos_arity
status (name,t,cpos,arity)
in
- let uris = concat_nuris nuris uris in
+ let uris = nuris@uris in
status, uris
with MultiPassDisambiguator.DisambiguationError _->
HLog.warn ("error in generating coercion: "^name);
(match nmenv with
[] ->
eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
- | _ -> status,`New [])
+ | _ -> status,[])
| GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
(match menv with
[] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> prerr_endline ("Discriminator: non empty metasenv");
- status, `New []) *)
+ status, []) *)
| GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
;;
let eval_comment ~disambiguate_command opts status (text,prefix_len,c) =
- status, `New []
+ status, []
let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
GrafiteTypes.add_moo_content
[GrafiteAst.Include (loc,baseuri)] status
in
- status,`New []
- | GrafiteAst.Print (_,_) -> status,`New []
- | GrafiteAst.Set (loc, name, value) -> status, `New []
+ status,[]
+ | GrafiteAst.Print (_,_) -> status,[]
+ | GrafiteAst.Set (loc, name, value) -> status, []
in
status,uris
subst_metasenv_and_fix_names status)
status tacl
in
- status,`New []
+ status,[]
| GrafiteAst.Command (_, cmd) ->
eval_command ~disambiguate_command opts status (text,prefix_len,cmd)
| GrafiteAst.NCommand (_, cmd) ->
eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
status ast
in
- assert (lemmas=`New []);
+ assert (lemmas=[]);
status)
status moo
GrafiteTypes.status ->
GrafiteAst.statement disambiguator_input ->
(* the new status and generated objects, if any *)
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
+ GrafiteTypes.status * NUri.uri list
let status, uris =
basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
in
- status,`New uris
+ status,uris
;;
let eval_ncoercion status name t ty (id,src) tgt =
let status, uris =
basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
in
- status,`New uris
+ status,uris
;;
NotationPt.term ->
NotationPt.term ->
string * NotationPt.term ->
- NotationPt.term -> 'status * [> `New of NUri.uri list ]
+ NotationPt.term -> 'status * NUri.uri list
(* for records, the term is the projection, already refined, while the
* first integer is the number of left params and the second integer is
* the arity in the `:arity>` syntax *)
val basic_eval_and_record_ncoercion_from_t_cpos_arity:
#GrafiteTypes.status as 'status ->
- string * NCic.term * int * int -> 'status * [> `New of NUri.uri list ]
+ string * NCic.term * int * int -> 'status * NUri.uri list
(* statements meaningful for matitadep *)
type dependency =
| IncludeDep of string
- | UriDep of UriManager.uri
+ | UriDep of NUri.uri
| InlineDep of string
let pp_dependency = function
| IncludeDep str -> "include \"" ^ str ^ "\""
- | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+ | UriDep uri -> "uri \"" ^ NUri.string_of_uri uri ^ "\""
| InlineDep str -> "inline \"" ^ str ^ "\""
let parse_dependencies lexbuf =
(parser
| [< '("QSTRING", s) >] ->
(* because of alias id qstring = qstring :-( *)
- (try
- true, (UriDep (UriManager.uri_of_string s) :: acc)
- with
- UriManager.IllFormedUri _ -> true, acc)
+ if String.sub s 0 5 <> "cic:/" then true,acc
+ else
+ true, (UriDep (NUri.uri_of_string s) :: acc)
| [< '("URI", u) >] ->
- true, (UriDep (UriManager.uri_of_string u) :: acc)
+ true, (UriDep (NUri.uri_of_string u) :: acc)
| [< '("IDENT", "include"); '("QSTRING", fname) >] ->
true, (IncludeDep fname :: acc)
| [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] ->
(* statements meaningful for matitadep *)
type dependency =
| IncludeDep of string
- | UriDep of UriManager.uri
+ | UriDep of NUri.uri
| InlineDep of string
val pp_dependency: dependency -> string
| false -> NCic.Implicit `Term)
~mk_appl:(function
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_uri:(fun _ -> assert false)
~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
| LexiconAst.Number_alias (_, dsc) ->
let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
let rex = Str.regexp ("^"^ident^"$") in
if Str.string_match rex id 0 then
- if (try ignore (UriManager.uri_of_string uri); true
- with UriManager.IllFormedUri _ -> false) ||
- (try ignore (NReference.reference_of_string uri); true
+ if (try ignore (NReference.reference_of_string uri); true
with NReference.IllFormedReference _ -> false)
then
L.Ident_alias (id, uri)
]
];
level3_term: [
- [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
- | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
+ [ r = NREF -> N.NRefPattern (NReference.reference_of_string r)
| IMPLICIT -> N.ImplicitPattern
| id = IDENT -> N.VarPattern id
| LPAREN; terms = LIST1 SELF; RPAREN ->
begin try
match DisambiguateTypes.Environment.find item status.aliases with
L.Ident_alias (_, uri) ->
- (try
- NotationPt.NRefPattern
- (NReference.reference_of_string uri)
- with
- NReference.IllFormedReference _ ->
- NotationPt.UriPattern (UriManager.uri_of_string uri))
+ NotationPt.NRefPattern (NReference.reference_of_string uri)
| _ -> assert false
with Not_found ->
prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
(raw: lexicon)
let rehash_cmd_uris =
- let rehash_uri uri =
- UriManager.uri_of_string (UriManager.string_of_uri uri) in
function
| LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
let rec aux =
function
- | NotationPt.UriPattern uri ->
- NotationPt.UriPattern (rehash_uri uri)
| NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
let uri = NCicLibrary.refresh_uri uri in
NotationPt.NRefPattern (NReference.reference_of_spec uri spec)
status#lstatus.LexiconEngine.aliases []
;;
-(** given a uri and a type list (the contructors types) builds a list of pairs
- * (name,uri) that is used to generate automatic aliases **)
-let extract_alias types uri =
- fst(List.fold_left (
- fun (acc,i) (name, _, _, cl) ->
- (name, UriManager.uri_of_uriref uri i None) ::
- (fst(List.fold_left (
- fun (acc,j) (name,_) ->
- (((name,UriManager.uri_of_uriref uri i
- (Some j)) :: acc) , j+1)
- ) (acc,1) cl)),i+1
- ) ([],0) types)
-
-let build_aliases =
- List.map
- (fun (name,uri) ->
- DisambiguateTypes.Id name, LexiconAst.Ident_alias (name,
- UriManager.string_of_uri uri))
-
-let add_aliases_for_inductive_def status types uri =
- let aliases = build_aliases (extract_alias types uri) in
- LexiconEngine.set_proof_aliases status aliases
-
-let add_alias_for_constant status uri =
- let name = UriManager.name_of_uri uri in
- let new_env = build_aliases [(name,uri)] in
- LexiconEngine.set_proof_aliases status new_env
-
let add_aliases_for_objs status =
- function
- `Old _ -> assert false (* MATITA 1.0 *)
- | `New nrefs ->
- List.fold_left
- (fun status nref ->
- let references = NCicLibrary.aliases_of nref in
- let new_env =
- List.map
- (fun u ->
- let name = NCicPp.r2s true u in
- DisambiguateTypes.Id name,
- LexiconAst.Ident_alias (name,NReference.string_of_reference u)
- ) references
- in
- LexiconEngine.set_proof_aliases status new_env
- ) status nrefs
+ List.fold_left
+ (fun status nref ->
+ let references = NCicLibrary.aliases_of nref in
+ let new_env =
+ List.map
+ (fun u ->
+ let name = NCicPp.r2s true u in
+ DisambiguateTypes.Id name,
+ LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+ ) references
+ in
+ LexiconEngine.set_proof_aliases status new_env
+ ) status
module OrderedId =
struct
*)
val add_aliases_for_objs:
- #LexiconEngine.status as 'status ->
- [`Old of UriManager.uri list | `New of NUri.uri list]-> 'status
+ #LexiconEngine.status as 'status -> NUri.uri list -> 'status
val time_travel:
present:#LexiconEngine.status -> past:#LexiconEngine.status -> unit
module HGT = Http_getter_types;;
module HG = Http_getter;;
-module UM = UriManager;;
+(*module UM = UriManager;;*)
let decompile = ref (fun ~baseuri -> assert false);;
let set_decompile_cb f = decompile := f;;
List.iter debug_prerr buris;
let l = close_db cache_of_processed_baseuri [] buris in
let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
- let l = List.map UriManager.uri_of_string l in
+ let l = List.map NUri.uri_of_string l in
debug_prerr "clean_baseuri will remove:";
if debug then
- List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
+ List.iter (fun u -> debug_prerr (NUri.string_of_uri u)) l;
List.iter
(fun baseuri ->
!decompile ~baseuri;
HExtlib.rmdir_descend (Filename.chop_extension lexiconfile)
with Http_getter_types.Key_not_found _ -> ())
(HExtlib.list_uniq (List.fast_sort Pervasives.compare
- (List.map (UriManager.buri_of_uri) l @ buris)))
+ (List.map NUri.baseuri_of_uri l @ buris)))
let res =
match kind with
| NCic.Fixpoint (is_rec, ifl, _) ->
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Joint
{ K.joint_id = gen_id joint_prefix seed;
K.joint_kind =
K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
})
| NCic.Inductive (is_ind, lno, itl, _) ->
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Joint
{ K.joint_id = gen_id joint_prefix seed;
K.joint_kind =
| NCic.Constant (_,_,Some bo,ty,_) ->
let ty = nast_of_cic ~context:[] ty in
let bo = nast_of_cic ~context:[] bo in
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Def (K.Const,ty,
build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
| NCic.Constant (_,_,None,ty,_) ->
let ty = nast_of_cic ~context:[] ty in
- (gen_id object_prefix seed, [], conjectures,
+ (gen_id object_prefix seed, conjectures,
`Decl (K.Const,
(*CSC: ??? get_id ty here used to be the id of the axiom! *)
build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))
module Ast = NotationPt
module Util = NotationUtil
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
-
module Matcher32 =
struct
module Pattern32 =
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
- | Ast.UriPattern uri -> NRef (!reference_of_oxuri uri), []
| Ast.NRefPattern nref -> NRef nref, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> Blob, []
let classify = function
| Ast.ImplicitPattern
| Ast.VarPattern _ -> PatternMatcher.Variable
- | Ast.UriPattern _
| Ast.NRefPattern _
| Ast.ApplPattern _ -> PatternMatcher.Constructor
end
* http://helm.cs.unibo.it/
*)
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
-
module Matcher32:
sig
(** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *)
List.find (has_description dsc) !nnum_choices
with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
-let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl_pattern)=
+let mk_choice ~mk_appl ~mk_implicit ~term_of_nref (dsc, args, appl_pattern)=
dsc,
`Sym_interp
(fun cic_args ->
in
let combined =
Interpretations.instantiate_appl_pattern
- ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern
+ ~mk_appl ~mk_implicit ~term_of_nref env' appl_pattern
in
match rest with
[] -> combined
| _::_ -> mk_appl (combined::rest))
-let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc =
+let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_nref symbol dsc =
let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in
try
- mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref
+ mk_choice ~mk_appl ~mk_implicit ~term_of_nref
(List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
with Interpretations.Interpretation_not_found | Not_found ->
raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))
val lookup_symbol_by_dsc:
mk_appl: ('term list -> 'term) ->
mk_implicit: (bool -> 'term) ->
- term_of_uri: (UriManager.uri -> 'term) ->
term_of_nref: (NReference.reference -> 'term) ->
string -> string -> 'term codomain_item
val mk_choice:
mk_appl: ('term list -> 'term) ->
mk_implicit: (bool -> 'term) ->
- term_of_uri: (UriManager.uri -> 'term) ->
term_of_nref: (NReference.reference -> 'term) ->
string * NotationPt.argument_pattern list *
NotationPt.cic_appl_pattern ->
open Printf
open DisambiguateTypes
-open UriManager
module Ast = NotationPt
module NRef = NReference
let debug_print s = prerr_endline (Lazy.force s);;
let debug_print _ = ();;
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
-
let cic_name_of_name = function
| Ast.Ident (n, None) -> n
| _ -> assert false
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
+ NCic.Const (NReference.reference_of_string uri)
with NRef.IllFormedReference _ ->
NotationPt.fail loc "Ill formed reference")
| NotationPt.NRef nref -> NCic.Const nref
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
-
val disambiguate_term :
context:NCic.context ->
metasenv:NCic.metasenv ->
+++ /dev/null
-uriManager.cmi:
-uriManager.cmo: uriManager.cmi
-uriManager.cmx: uriManager.cmi
+++ /dev/null
-uriManager.cmi:
-uriManager.cmo: uriManager.cmi
-uriManager.cmx: uriManager.cmi
+++ /dev/null
-PACKAGE = urimanager
-PREDICATES =
-
-INTERFACE_FILES = uriManager.mli
-IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
-EXTRA_OBJECTS_TO_INSTALL =
-EXTRA_OBJECTS_TO_CLEAN =
-
-include ../../Makefile.defs
-include ../Makefile.common
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-(*
- * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id )
- * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id)
- * "cic:/a/b/c.ind#xpointer(1/1/1)" => ("cic:/a/b/c.con#xpointer(1/1/1)", id)
- *)
-
-let fresh_id =
- let id = ref 0 in
- function () ->
- incr id;
- !id
-
-(* (uriwithxpointer, uniqueid)
- * where uniqueid is used to build a set of uri *)
-type uri = string * int;;
-
-let eq uri1 uri2 =
- uri1 == uri2
-;;
-
-let string_of_uri (uri,_) =
- uri
-
-let name_of_uri (uri, _) =
- let xpointer_offset =
- try String.rindex uri '#' with Not_found -> String.length uri - 1
- in
- let index1 = String.rindex_from uri xpointer_offset '/' + 1 in
- let index2 = String.rindex uri '.' in
- String.sub uri index1 (index2 - index1)
-
-let nameext_of_uri (uri, _) =
- let xpointer_offset, mah =
- try String.rindex uri '#', 0 with Not_found -> String.length uri - 1, 1
- in
- let index1 = String.rindex_from uri xpointer_offset '/' + 1 in
- String.sub uri index1 (xpointer_offset - index1 + mah)
-
-let buri_of_uri (uri,_) =
- let xpointer_offset =
- try String.rindex uri '#' with Not_found -> String.length uri - 1
- in
- let index = String.rindex_from uri xpointer_offset '/' in
- String.sub uri 0 index
-
-module OrderedStrings =
- struct
- type t = string
- let compare (s1 : t) (s2 : t) = compare s1 s2
- end
-;;
-
-module MapStringsToUri = Map.Make(OrderedStrings);;
-
-(* Invariant: the map is the identity function,
- * i.e.
- * let str' = (MapStringsToUri.find str !set_of_uri) in
- * str' == (MapStringsToUri.find str' !set_of_uri)
- *)
-let set_of_uri = ref MapStringsToUri.empty;;
-
-exception IllFormedUri of string;;
-
-let _dottypes = ".types"
-let _types = "types",5
-let _dotuniv = ".univ"
-let _univ = "univ",4
-let _dotann = ".ann"
-let _ann = "ann",3
-let _var = "var",3
-let _dotbody = ".body"
-let _con = "con",3
-let _ind = "ind",3
-let _xpointer = "#xpointer(1/"
-let _con3 = "con"
-let _var3 = "var"
-let _ind3 = "ind"
-let _ann3 = "ann"
-let _univ4 = "univ"
-let _types5 = "types"
-let _xpointer8 = "xpointer"
-let _cic5 = "cic:/"
-
-let is_malformed suri =
- try
- if String.sub suri 0 5 <> _cic5 then true
- else
- let len = String.length suri - 5 in
- let last5 = String.sub suri len 5 in
- let last4 = String.sub last5 1 4 in
- let last3 = String.sub last5 2 3 in
- if last3 = _con3 || last3 = _var3 || last3 = _ind3 ||
- last3 = _ann3 || last5 = _types5 || last5 = _dotbody ||
- last4 = _univ4 then
- false
- else
- try
- let index = String.rindex suri '#' + 1 in
- let xptr = String.sub suri index 8 in
- if xptr = _xpointer8 then
- false
- else
- true
- with Not_found -> true
- with Invalid_argument _ -> true
-
-(* hash conses an uri *)
-let uri_of_string suri =
- try
- MapStringsToUri.find suri !set_of_uri
- with Not_found ->
- if is_malformed suri then
- raise (IllFormedUri suri)
- else
- let new_uri = suri, fresh_id () in
- set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri;
- new_uri
-
-
-let strip_xpointer ((uri,_) as olduri) =
- try
- let index = String.rindex uri '#' in
- let no_xpointer = String.sub uri 0 index in
- uri_of_string no_xpointer
- with
- Not_found -> olduri
-
-let clear_suffix uri ?(pat2="",0) pat1 =
- try
- let index = String.rindex uri '.' in
- let index' = index + 1 in
- let suffix = String.sub uri index' (String.length uri - index') in
- if fst pat1 = suffix || fst pat2 = suffix then
- String.sub uri 0 index
- else
- uri
- with
- Not_found -> assert false
-
-let has_suffix uri (pat,n) =
- try
- let suffix = String.sub uri (String.length uri - n) n in
- pat = suffix
- with
- Not_found -> assert false
-
-
-let cicuri_of_uri (uri, _) = uri_of_string (clear_suffix uri ~pat2:_types _ann)
-
-let annuri_of_uri (uri , _) = uri_of_string ((clear_suffix uri _ann) ^ _dotann)
-
-let uri_is_annuri (uri, _) = has_suffix uri _ann
-
-let uri_is_var (uri, _) = has_suffix uri _var
-
-let uri_is_con (uri, _) = has_suffix uri _con
-
-let uri_is_ind (uri, _) = has_suffix uri _ind
-
-let bodyuri_of_uri (uri, _) =
- if has_suffix uri _con then
- Some (uri_of_string (uri ^ _dotbody))
- else
- None
-;;
-
-let ind_uri_split ((s, _) as uri) =
- let noxp = strip_xpointer uri in
- try
- (let arg_index = String.rindex s '(' in
- try
- (let ty_index = String.index_from s arg_index '/' in
- try
- (let k_index = String.index_from s (ty_index+1) '/' in
- let tyno = int_of_string (String.sub s (ty_index + 1) (k_index - ty_index - 1)) in
- let kno = int_of_string (String.sub s (k_index + 1) (String.length s - k_index - 2)) in
- noxp, Some tyno, Some kno)
- with Not_found ->
- let tyno = int_of_string (String.sub s (ty_index + 1) (String.length s - ty_index - 2)) in
- noxp, Some tyno, None)
- with Not_found -> noxp, None, None
- )
- with Not_found -> noxp, None, None
-;;
-
-(* these are bugged!
- * we should remove _types, _univ, _ann all toghether *)
-let innertypesuri_of_uri (uri, _) =
- uri_of_string ((clear_suffix uri _types) ^ _dottypes)
-;;
-let univgraphuri_of_uri (uri,_) =
- uri_of_string ((clear_suffix uri _univ) ^ _dotuniv)
-;;
-
-
-let uri_of_uriref (uri, _) typeno consno =
- let typeno = typeno + 1 in
- let suri =
- match consno with
- | None -> Printf.sprintf "%s%s%d)" uri _xpointer typeno
- | Some n -> Printf.sprintf "%s%s%d/%d)" uri _xpointer typeno n
- in
- uri_of_string suri
-
-let compare (_,id1) (_,id2) = id1 - id2
-
-module OrderedUri =
-struct
- type t = uri
- let compare = compare (* the one above, not Pervasives.compare *)
-end
-
-module UriSet = Set.Make (OrderedUri)
-
-(*
-module OrderedUriPair =
-struct
- type t = uri * uri
- let compare (u11, u12) (u21, u22) =
- match compare u11 u21 with
- | 0 -> compare u12 u22
- | x -> x
-end
-
-module UriPairSet = Set.Make (OrderedUriPair)
-*)
-
-module HashedUri =
-struct
- type t = uri
- let equal = eq
- let hash = snd
-end
-
-module UriHashtbl = Hashtbl.Make (HashedUri)
-
-
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-exception IllFormedUri of string;;
-
-type uri
-
-val eq : uri -> uri -> bool
-val compare : uri -> uri -> int
-
-val uri_of_string : string -> uri
-
-val string_of_uri : uri -> string (* complete uri *)
-val name_of_uri : uri -> string (* name only (without extension)*)
-val nameext_of_uri : uri -> string (* name only (with extension)*)
-val buri_of_uri : uri -> string (* base uri only, without trailing '/' *)
-
-(* given an uri, returns the uri of the corresponding cic file, *)
-(* i.e. removes the [.types][.ann] suffix *)
-val cicuri_of_uri : uri -> uri
-
-val strip_xpointer: uri -> uri (* remove trailing #xpointer..., if any *)
-
-(* given an uri, returns the uri of the corresponding annotation file, *)
-(* i.e. adds the .ann suffix if not already present *)
-val annuri_of_uri : uri -> uri
-
-val uri_is_annuri : uri -> bool
-val uri_is_var : uri -> bool
-val uri_is_con : uri -> bool
-val uri_is_ind : uri -> bool
-
-(* given an uri of a constant, it gives back the uri of its body *)
-(* it gives back None if the uri refers to a Variable or MutualInductiveType *)
-val bodyuri_of_uri : uri -> uri option
-
-val ind_uri_split : uri -> uri * int option * int option
-
-(* given an uri, it gives back the uri of its inner types *)
-val innertypesuri_of_uri : uri -> uri
-(* given an uri, it gives back the uri of its univgraph *)
-val univgraphuri_of_uri : uri -> uri
-
-(* builder for MutInd and MutConstruct URIs
- * [uri] -> [typeno] -> [consno option]
- *)
-val uri_of_uriref : uri -> int -> int option -> uri
-
-module UriSet: Set.S with type elt = uri
-(*module UriPairSet: Set.S with type elt = uri * uri*)
-
-module UriHashtbl : Hashtbl.S with type key = uri
-
<property name="use_underline">True</property>
<child>
<widget class="GtkMenu" id="BrowserViewMenu_menu">
- <child>
- <widget class="GtkMenuItem" id="univMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Universes</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
<child>
<widget class="GtkMenuItem" id="HBugsTutorsMenuItem">
<property name="visible">True</property>
sequents_viewer#load_logo;
cic_math_view#set_href_callback
(Some (fun uri ->
- let uri =
- try
- `Uri (UriManager.uri_of_string uri)
- with
- UriManager.IllFormedUri _ ->
- `NRef (NReference.reference_of_string uri)
- in
- (MatitaMathView.cicBrowser ())#load uri));
+ let uri = `NRef (NReference.reference_of_string uri) in
+ (MatitaMathView.cicBrowser ())#load uri));
let browser_observer _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer grafite_status =
sequents_viewer#reset;
| GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
| CicNotationParser.Parse_error err ->
None, sprintf "Parse error: %s" err
- | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri
| Unix.Unix_error (code, api, param) ->
let err = Unix.error_message code in
None, "Unix Error (" ^ api ^ "): " ^ err
~id uris
=
let gui = instance () in
- let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
then
- Lazy.force nonvars_uris
+ uris
else begin
let dialog = gui#newUriDialog () in
if hide_uri_entry then
| _ -> ()));
dialog#uriChoiceDialog#set_title title;
dialog#uriChoiceLabel#set_text msg;
- List.iter model#easy_append (List.map UriManager.string_of_uri uris);
+ List.iter model#easy_append (List.map NReference.string_of_reference uris);
dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
let return v =
choices := v;
in
ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceConstantsButton (fun _ ->
- return (Some (Lazy.force nonvars_uris)));
+ return (Some uris));
if ok_action = `AUTO then
connect_button dialog#uriChoiceAutoButton (fun _ ->
Helm_registry.set_bool "matita.auto_disambiguation" true;
- return (Some (Lazy.force nonvars_uris)))
+ return (Some uris))
else
connect_button dialog#uriChoiceAutoButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
GtkThread.main ();
?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
?ok_action:[`AUTO|`SELECT] ->
?copy_cb:(string -> unit) -> unit ->
- id:'a -> UriManager.uri list -> UriManager.uri list
+ id:'a -> NReference.reference list -> NReference.reference list
(** @raise MatitaTypes.Cancel *)
val interactive_interp_choice:
object (self)
inherit scriptAccessor
- val mutable gviz_uri = UriManager.uri_of_string "cic:/dummy.con";
+ val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
val dep_contextual_menu = GMenu.menu ()
handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
mathView#set_href_callback (Some (fun uri ->
handle_error (fun () ->
- let uri =
- try
- `Uri (UriManager.uri_of_string uri)
- with
- UriManager.IllFormedUri _ ->
- `NRef (NReference.reference_of_string uri)
- in
+ let uri = `NRef (NReference.reference_of_string uri) in
self#load uri)));
gviz#connect_href (fun button_ev attrs ->
let time = GdkEvent.Button.time button_ev in
let uri = List.assoc "href" attrs in
- gviz_uri <- UriManager.uri_of_string uri;
+ gviz_uri <- NReference.reference_of_string uri;
match GdkEvent.Button.button button_ev with
- | button when button = left_button -> self#load (`Uri gviz_uri)
+ | button when button = left_button -> self#load (`NRef gviz_uri)
| button when button = right_button ->
dep_contextual_menu#popup ~button ~time
| _ -> ());
win#hBugsTutorsMenuItem#misc#hide ();
connect_menu_item win#browserUrlMenuItem (fun () ->
win#browserUri#misc#grab_focus ());
- connect_menu_item win#univMenuItem (fun () ->
- match self#currentCicUri with
- | Some uri -> self#load (`Univs uri)
- | None -> ());
self#_load (`About `Blank);
toplevel#show ()
(** @return None if no object uri can be built from the current entry *)
method private currentCicUri =
match current_entry with
- | `Uri uri -> Some uri
+ | `NRef uri -> Some uri
| _ -> None
val model =
self#_loadTermNCic term metasenv subst ctx
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
- | `Uri uri -> assert false (* MATITA 1.0 *)
- | `NRef nref -> self#_loadNReference nref
- | `Univs uri -> assert false (* MATITA 1.0 *));
+ | `NRef nref -> self#_loadNReference nref);
self#setEntry entry
end)
gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
(match center_on with
| None -> ()
- | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
+ | Some uri -> gviz#center_on_href (NReference.string_of_reference uri));
HExtlib.safe_remove tmpfile
else
MatitaGtkMisc.report_error ~title:"graphviz error"
let entry =
match txt with
| txt when is_uri txt ->
- `Uri (UriManager.uri_of_string ((*fix_uri*) txt))
+ `NRef (NReference.reference_of_string ((*fix_uri*) txt))
| txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
| txt ->
(try
type guistuff = {
mathviewer:MatitaTypes.mathViewer;
- urichooser: UriManager.uri list -> UriManager.uri list;
+ urichooser: NReference.reference list -> NReference.reference list;
ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
}
val script:
source_view:GSourceView2.source_view ->
mathviewer: MatitaTypes.mathViewer->
- urichooser: (UriManager.uri list -> UriManager.uri list) ->
+ urichooser: (NReference.reference list -> NReference.reference list) ->
ask_confirmation:
(title:string -> message:string -> [`YES | `NO | `CANCEL]) ->
set_star: (bool -> unit) ->
| `Check of string (* term *)
| `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
| `Dir of string (* "directory" in cic uris namespace *)
- | `Uri of UriManager.uri (* cic object uri *)
| `NRef of NReference.reference (* cic object uri *)
- | `Univs of UriManager.uri
]
let string_of_entry = function
| `Check _ -> "check:"
| `NCic (_, _, _, _) -> "nterm:"
| `Dir uri -> uri
- | `Uri uri -> UriManager.string_of_uri uri
| `NRef nref -> NReference.string_of_reference nref
- | `Univs uri -> "univs:" ^ UriManager.string_of_uri uri
let entry_of_string = function
| "about:blank" -> `About `Blank
*)
method show_entry: ?reuse:bool -> mathViewer_entry -> unit
method show_uri_list:
- ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
+ ?reuse:bool -> entry:mathViewer_entry -> NReference.reference list -> unit
method screenshot:
GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv ->
NCic.substitution -> string -> unit
| `Check of string
| `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
| `Dir of string
- | `Uri of UriManager.uri
| `NRef of NReference.reference
- | `Univs of UriManager.uri
]
val string_of_entry : mathViewer_entry -> string
object
method show_entry : ?reuse:bool -> mathViewer_entry -> unit
method show_uri_list :
- ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
+ ?reuse:bool -> entry:mathViewer_entry -> NReference.reference list -> unit
method screenshot:
GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv ->
NCic.substitution -> string -> unit
open Printf
-module UM = UriManager
module TA = GrafiteAst
let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ]
List.fold_left
(fun uris_to_remove suri ->
let uri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with UM.IllFormedUri _ ->
+ (*MATITA 1.0, CSC: verify that suri is a reasonable uri *)
+ (*try*)
+ NUri.baseuri_of_uri (NUri.uri_of_string suri)
+ (*with UM.IllFormedUri _ ->
let _,u,_,_ = Librarian.baseuri_of_script ~include_paths:[] suri in
if Librarian.is_uri u then u else begin
HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u);
exit 1
- end
+ end *)
in
uri::uris_to_remove) [] files
in
module S = Set.Make (String)
module GA = GrafiteAst
-module U = UriManager
module HR = Helm_registry
let print_times msg =
HLog.error ("possibly incorrect verbatim URIs in the .ma file.");
None
in
- let buri alias = U.buri_of_uri (U.uri_of_string alias) in
+ let buri alias = NUri.baseuri_of_uri (NUri.uri_of_string alias) in
let resolve alias current_buri =
let buri = buri alias in
if buri <> current_buri then Some buri else None
List.iter
(function
| DependenciesParser.UriDep uri ->
- let uri = UriManager.string_of_uri uri in
+ let uri = NUri.string_of_uri uri in
handle_uri uri
| DependenciesParser.InlineDep path ->
if Librarian.is_uri path
projects / helm.git / commitdiff