-requires="helm-library"
+requires="helm-library helm-ng_kernel"
version="0.0.1"
archive(byte)="acic_content.cma"
archive(native)="acic_content.cmxa"
cic_exportation \
metadata \
library \
- acic_content \
ng_kernel \
+ acic_content \
grafite \
ng_cic_content \
content_pres \
type cic_mask_t =
Blob
| Uri of UriManager.uri
+ | NRef of NReference.reference
| Appl of cic_mask_t list
let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
+ | Ast.NRefPattern nref -> NRef nref, []
| Ast.UriPattern uri -> Uri uri, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> Blob, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> PatternMatcher.Variable
| Ast.UriPattern _
+ | Ast.NRefPattern _
| Ast.ApplPattern _ -> PatternMatcher.Constructor
end
(String.concat " and " (List.map map definitions))
(pp_term term)
| Ast.Ident (name, Some []) | Ast.Ident (name, None)
- | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
- name
+ | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+ | Ast.NRef nref -> NReference.string_of_reference nref
| Ast.Ident (name, Some substs)
| Ast.Uri (name, Some substs) ->
sprintf "%s \\subst [%s]" name (pp_substs substs)
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 -> "?"
| Ast.ApplPattern aps ->
| UserInput (* place holder for user input, used by MatitaConsole, not to be
used elsewhere *)
| Uri of string * subst list option (* as Ident, for long names *)
+ | NRef of NReference.reference
(* Syntax pattern extensions *)
type cic_appl_pattern =
| UriPattern of UriManager.uri
+ | NRefPattern of NReference.reference
| VarPattern of string
| ImplicitPattern
| ApplPattern of cic_appl_pattern list
| Ast.Magic _
| Ast.Variable _) as t -> special_k t
| (Ast.Ident _
+ | Ast.NRef _
| Ast.Implicit
| Ast.Num _
| Ast.Sort _
let find_appl_pattern_uris ap =
let rec aux acc =
function
- | Ast.UriPattern uri -> uri :: acc
+ | Ast.UriPattern uri -> `Uri uri :: acc
+ | Ast.NRefPattern nref -> `NRef nref :: acc
| Ast.ImplicitPattern
| Ast.VarPattern _ -> acc
| Ast.ApplPattern apl -> List.fold_left aux acc apl
in
let uris = aux [] ap in
- HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
+ 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)
let rec find_branch =
function
val ungroup: CicNotationPt.term list -> CicNotationPt.term list
val find_appl_pattern_uris:
- CicNotationPt.cic_appl_pattern -> UriManager.uri list
+ CicNotationPt.cic_appl_pattern ->
+ [`Uri of UriManager.uri | `NRef of NReference.reference] list
val find_branch:
CicNotationPt.term -> CicNotationPt.term
in
let rec aux = function
| Ast.UriPattern uri -> term_of_uri uri
+ | Ast.NRefPattern _ -> assert false
| Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
| Ast.ApplPattern terms -> mk_appl (List.map aux terms)
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
List.fold_right (build_term inductiveFuns) inductiveFuns
cic_body)
| CicNotationPt.Ident _
- | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
- | CicNotationPt.Ident (name, subst)
+ | CicNotationPt.Uri _
+ | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | CicNotationPt.NRef _ -> assert false
+ | CicNotationPt.Ident (name,subst)
| CicNotationPt.Uri (name, subst) as ast ->
let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
(try
| Cic.Cast (te,ty) -> check_rec ctx string_name te
| Cic.Prod (name,so,dest) ->
let l_string_name = check_rec ctx string_name so in
- check_rec (name::ctx) string_name dest
+ check_rec (name::ctx) l_string_name dest
| Cic.Lambda (name,so,dest) ->
let string_name =
match name with
('.' ident)+ (* ext *)
("#xpointer(" number ('/' number)+ ")")? (* xpointer *)
+let regexp nreference =
+ "cic:/" (* schema *)
+ uri_step ('/' uri_step)* (* path *)
+ '.'
+ ( "dec"
+ | "def" "(" number ")"
+ | "fix" "(" number "," number "," number ")"
+ | "cfx" "(" number ")"
+ | "ind" "(" number "," number "," number ")"
+ | "con" "(" number "," number "," number ")") (* ext + reference *)
+
let error lexbuf msg =
let begin_cnum, end_cnum = Ulexing.loc lexbuf in
raise (Error (begin_cnum, end_cnum, msg))
| pident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "PIDENT"
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
| tex_token -> return lexbuf (expand_macro lexbuf)
+ | nreference -> return lexbuf ("NREF", Ulexing.utf8_lexeme lexbuf)
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| qstring ->
return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
return_term loc (Ast.Ident (id, Some s))
| s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
| u = URI -> return_term loc (Ast.Uri (u, None))
+ | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
| n = NUMBER -> return_term loc (Ast.Num (n, 0))
| IMPLICIT -> return_term loc (Ast.Implicit)
| PLACEHOLDER -> return_term loc Ast.UserInput
BoxPp.render_to_string (function x::_->x|_->assert false)
~map_unicode_to_tex:false 80 t);*)t)
-let render ids_to_uris ?(prec=(-1)) =
+let lookup_uri ids_to_uris id =
+ try
+ let uri = Hashtbl.find ids_to_uris id in
+ Some (UriManager.string_of_uri uri)
+ with Not_found -> None
+;;
+
+let render ~lookup_uri ?(prec=(-1)) =
let module A = Ast in
let module P = Mpresentation in
(* let use_unicode = true in *)
- let lookup_uri id =
- (try
- let uri = Hashtbl.find ids_to_uris id in
- Some (UriManager.string_of_uri uri)
- with Not_found -> None)
- in
let make_href xmlattrs xref =
let xref_uris =
List.fold_right
(** {2 Rendering} *)
+val lookup_uri: (Cic.id,UriManager.uri) Hashtbl.t -> Cic.id -> string option
+
(** level 1 -> level 0
* @param ids_to_uris mapping id -> uri for hyperlinking
* @param prec precedence level *)
val render:
- (Cic.id, UriManager.uri) Hashtbl.t -> ?prec:int -> CicNotationPt.term -> markup
+ lookup_uri:(Cic.id -> string option) -> ?prec:int -> CicNotationPt.term ->
+ markup
(** level 0 -> xml stream *)
val print_xml: markup -> Xml.token Stream.t
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
- (CicNotationPres.render ids_to_uris ~prec
+ (CicNotationPres.render
+ ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
(TermContentPres.pp_ast ast)))
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
- (CicNotationPres.render ids_to_uris
+ (CicNotationPres.render
+ ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
(TermContentPres.pp_ast ast)))
-let nsequent2pres ~subst =
+let nsequent2pres ~ids_to_nrefs ~subst =
+ let lookup_uri id =
+ try
+ let nref = Hashtbl.find ids_to_nrefs id in
+ Some (NReference.string_of_reference nref)
+ with Not_found -> None
+ in
sequent2pres0
(fun ast ->
CicNotationPres.box_of_mpres
- (CicNotationPres.render (Hashtbl.create 1)
+ (CicNotationPres.render ~lookup_uri
(TermContentPres.pp_ast ast)))
CicNotationPres.boxml_markup
val nsequent2pres :
+ ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t ->
subst:NCic.substitution -> CicNotationPt.term Content.conjecture ->
CicNotationPres.boxml_markup
[] subst in
[ Node ([loc], Id name, terms) ]))
| Ast.Uri _ -> []
+ | Ast.NRef _ -> []
| Ast.Implicit -> []
| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
+ | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
| NonPunctuationTactical (_, tac, punct) ->
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
+ | NNonPunctuationTactical (_, tac, punct) ->
+ pp_non_punctuation_tactical tac
+ ^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
let name = UriManager.name_of_uri uri in
let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
let status, lemmas = add_obj uri obj status in
- {status with
- GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
(*CSC: I throw away the arities *)
`Old (uri::lemmas)
| GrafiteAst.NQed loc ->
| GrafiteTypes.ProofMode
{ NTacStatus.istatus =
{NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
- let uri,height,menv,subst,obj = pstatus in
+ let uri,height,menv,subst,obj_kind = pstatus in
if menv <> [] then
raise
(GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
else
- let obj =
-prerr_endline "CSC: here we should fix the height!!!";
- (uri,height,[],[],
- NCicUntrusted.map_obj_kind
- (NCicUntrusted.apply_subst subst [])
- obj) in
- NCicTypeChecker.typecheck_obj obj;
- NCicLibrary.add_obj uri obj;
- let objs = NCicElim.mk_elims obj in
- let uris =
- uri::
- List.map
- (fun (uri,_,_,_,_) as obj ->
- NCicTypeChecker.typecheck_obj obj;
- NCicLibrary.add_obj uri obj;
- uri
- ) objs
- in
- {status with
+ let obj_kind =
+ NCicUntrusted.map_obj_kind
+ (NCicUntrusted.apply_subst subst []) obj_kind in
+ let height = NCicUntrusted.height_of_obj_kind uri obj_kind in
+ let obj = uri,height,[],[],obj_kind in
+ NCicTypeChecker.typecheck_obj obj;
+ NCicLibrary.add_obj uri obj;
+ let objs = NCicElim.mk_elims obj in
+ let uris =
+ uri::
+ List.map
+ (fun (uri,_,_,_,_) as obj ->
+ NCicTypeChecker.typecheck_obj obj;
+ NCicLibrary.add_obj uri obj;
+ uri
+ ) objs
+ in
+ {status with
GrafiteTypes.ng_status =
GrafiteTypes.CommandMode lexicon_status },`New uris
| _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
];
level3_term: [
[ u = URI -> N.UriPattern (UriManager.uri_of_string u)
+ | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
| IMPLICIT -> N.ImplicitPattern
| id = IDENT -> N.VarPattern id
| LPAREN; terms = LIST1 SELF; RPAREN ->
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body))
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ body = term ->
+ G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.Obj (loc, N.Theorem (flavour, name, typ, body))
prerr_endline (sprintf "dumping MathML to %s ..." fname);
flush stdout;
let oc = open_out fname in
- let markup = CicNotationPres.render id_to_uri t in
+ let markup =
+ CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri id_to_uri)t in
let xml_stream = CicNotationPres.print_xml markup in
Xml.pp_to_outchan xml_stream oc;
close_out oc
->
let item = DisambiguateTypes.Id id in
begin try
- let uri =
- match DisambiguateTypes.Environment.find item status.aliases with
- L.Ident_alias (_, uri)-> UriManager.uri_of_string uri
- | _ -> assert false
- in
- CicNotationPt.UriPattern uri
+ match DisambiguateTypes.Environment.find item status.aliases with
+ L.Ident_alias (_, uri) ->
+ (try
+ CicNotationPt.NRefPattern
+ (NReference.reference_of_string uri)
+ with
+ NReference.IllFormedReference _ ->
+ CicNotationPt.UriPattern (UriManager.uri_of_string uri))
+ | _ -> assert false
with Not_found ->
prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
(DisambiguateTypes.string_of_domain_item item));
function
| CicNotationPt.UriPattern uri ->
CicNotationPt.UriPattern (rehash_uri uri)
+ | CicNotationPt.NRefPattern _ -> assert false
| CicNotationPt.ApplPattern args ->
CicNotationPt.ApplPattern (List.map aux args)
| CicNotationPt.VarPattern _
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+type id = string
+
(*
type interpretation_id = int
| _ -> assert false
*)
-let idref () =
+let idref register_ref =
let id = ref 0 in
- function t ->
+ fun ?reference t ->
incr id;
- Ast.AttributedTerm (`IdRef ("i" ^ string_of_int !id), t)
+ let id = "i" ^ string_of_int !id in
+ (match reference with None -> () | Some r -> register_ref id r);
+ Ast.AttributedTerm (`IdRef id, t)
;;
(* CODICE c&p da NCicPp *)
-let nast_of_cic0 ~idref ~output_type ~subst k ~context =
+let nast_of_cic0
+ ~(idref:
+ ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
+ ~output_type ~subst k ~context =
function
| NCic.Rel n ->
(try
idref (Ast.Ident (name,None))
with Failure "nth" | Invalid_argument "List.nth" ->
idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None)))
- | NCic.Const r -> idref (Ast.Ident (NCicPp.r2s true r, None))
+ | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s true r, None))
| NCic.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
k ~context (NCicSubstitution.subst_meta lc t)
else Ast.Appl (head :: List.map instantiate_arg args)
let rec nast_of_cic1 ~idref ~output_type ~subst ~context term =
-(*
- let register_uri id uri = assert false in
-*)
match (get_compiled32 ()) term with
| None ->
nast_of_cic0 ~idref ~output_type ~subst
(nast_of_cic1 ~idref ~output_type ~subst) ~context term
| Some (env, ctors, pid) ->
let idrefs =
-(*
- List.map
- (fun term ->
- let idref = idref term in
- (try
- register_uri idref
- (CicUtil.uri_of_term (Deannotate.deannotate_term term))
- with Invalid_argument _ -> ());
- idref)
- ctors
-*) []
+ List.map
+ (fun term ->
+ let attrterm =
+ idref
+ ~reference:
+ (match term with NCic.Const nref -> nref | _ -> assert false)
+ (CicNotationPt.Ident ("dummy",None))
+ in
+ match attrterm with
+ Ast.AttributedTerm (`IdRef id, _) -> id
+ | _ -> assert false
+ ) ctors
in
let env =
List.map
(fun (name, term) ->
- name, nast_of_cic1 ~idref ~output_type ~subst ~context term) env
+ name,
+ nast_of_cic1 ~idref ~output_type ~subst ~context term
+ ) env
in
let _, symbol, args, _ =
try
let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
let module K = Content in
- let nast_of_cic = nast_of_cic1 ~idref:(idref ()) ~output_type:`Term ~subst in
+ let ids_to_refs = Hashtbl.create 211 in
+ let register_ref = Hashtbl.add ids_to_refs in
+ let nast_of_cic =
+ nast_of_cic1 ~idref:(idref register_ref) ~output_type:`Term
+ ~subst in
let context',_ =
List.fold_right
(fun item (res,context) ->
})::res,item::context
) context ([],[])
in
- "-1",i,context',nast_of_cic ~context ty
+ ("-1",i,context',nast_of_cic ~context ty), ids_to_refs
;;
subst:NCic.substitution -> context:NCic.context -> NCic.term ->
CicNotationPt.term
*)
-val nmap_sequent : subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture
+
+type id = string
+
+val nmap_sequent:
+ subst:NCic.substitution -> int * NCic.conjecture ->
+ CicNotationPt.term Content.conjecture *
+ (id, NReference.reference) Hashtbl.t (* id -> reference *)
struct
type cic_mask_t =
Blob
- | Uri of UriManager.uri
+ | NRef of NReference.reference
| Appl of cic_mask_t list
let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
let mask_of_cic = function
| NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl
- | NCic.Const nref -> Uri (NCic2OCic.ouri_of_reference nref), []
+ | NCic.Const nref -> NRef nref, []
| _ -> Blob, []
let tag_of_term t =
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
- | Ast.UriPattern uri -> Uri uri, []
+ | Ast.UriPattern uri -> NRef (OCic2NCic.reference_of_oxuri uri), []
+ | Ast.NRefPattern nref -> NRef nref, []
| Ast.ImplicitPattern
| Ast.VarPattern _ -> Blob, []
| Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
| Ast.ImplicitPattern
| Ast.VarPattern _ -> PatternMatcher.Variable
| Ast.UriPattern _
+ | Ast.NRefPattern _
| Ast.ApplPattern _ -> PatternMatcher.Constructor
end
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
| CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
| CicNotationPt.Ident _
- | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | CicNotationPt.Uri _
+ | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
| CicNotationPt.Ident (name, subst) ->
assert (subst = None);
(try
try NCic.Const (List.assoc name obj_context)
with Not_found ->
Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
- | CicNotationPt.Uri (name, subst) ->
+ | CicNotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (NRef.reference_of_string name)
+ NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
+ | CicNotationPt.NRef nref -> NCic.Const nref
| CicNotationPt.Implicit -> NCic.Implicit `Term
| CicNotationPt.UserInput -> NCic.Implicit `Hole
| CicNotationPt.Num (num, i) ->
(fun context item1 item2 ->
let convertible =
match item1,item2 with
- (n1,C.Decl ty1),(n2,C.Decl ty2) ->
- n1 = n2 &&
+ (_,C.Decl ty1),(_,C.Decl ty2) ->
R.are_convertible ~metasenv ~subst context ty1 ty2
- | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
- n1 = n2
- && R.are_convertible ~metasenv ~subst context ty1 ty2
- && R.are_convertible ~metasenv ~subst context bo1 bo2
+ | (_,C.Def (bo1,ty1)),(_,C.Def (bo2,ty2)) ->
+ R.are_convertible ~metasenv ~subst context ty1 ty2 &&
+ R.are_convertible ~metasenv ~subst context bo1 bo2
| _,_ -> false
in
if not convertible then
let _,_,recno1,arity,_ = List.nth fl i in
if h1 <> h2 || recno1 <> recno2 then error ();
arity
- | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Decl) -> ty
- | (_,h1,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Def h2) ->
+ | (_,_,_,_,C.Constant (_,_,None,ty,_)), Ref.Ref (_,Ref.Decl) -> ty
+ | (_,h1,_,_,C.Constant (_,_,Some _,ty,_)), Ref.Ref (_,Ref.Def h2) ->
if h1 <> h2 then error ();
ty
| _ ->
(i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) ::
apply_subst_metasenv subst tl
;;
+
+let height_of_term tl =
+ let h = ref 0 in
+ let get_height (NReference.Ref (uri,_)) =
+ let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
+ height in
+ let rec aux =
+ function
+ NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
+ | NCic.Meta _ -> ()
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Implicit _ -> assert false
+ | NCic.Const nref -> h := max !h (get_height nref)
+ | NCic.Prod (_,t1,t2)
+ | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | NCic.Appl l -> List.iter aux l
+ | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ in
+ List.iter aux tl;
+ 1 + !h
+;;
+
+let height_of_obj_kind uri =
+ function
+ NCic.Inductive _
+ | NCic.Constant (_,_,None,_,_)
+ | NCic.Fixpoint (false,_,_) -> 0
+ | NCic.Fixpoint (true,ifl,_) ->
+ let iflno = List.length ifl in
+ height_of_term
+ (List.fold_left
+ (fun l (_,_,_,ty,bo) ->
+ let bo = NCicTypeChecker.debruijn uri iflno [] bo in
+ ty::bo::l
+ ) [] ifl)
+ | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
+;;
(* the context is needed only to honour Barendregt's naming convention *)
val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term
val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv
+
+val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int
let eq = (==);;
+let compare (Ref (u1,s1)) (Ref (u2,s2)) =
+ let res = NUri.compare u1 u2 in
+ if res = 0 then compare s1 s2 else res
+;;
+
module OrderedStrings =
struct
type t = string
- let compare (s1 : t) (s2 : t) = compare s1 s2
+ let compare (s1 : t) (s2 : t) = Pervasives.compare s1 s2
end
;;
val reference_of_spec: NUri.uri -> spec -> reference
val eq: reference -> reference -> bool
+val compare: reference -> reference -> int
val string_of_reference: reference -> string
val reference_of_string: string -> reference
let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
let mk_type n =
- if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
- else
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
let mk_cprop n =
aux false [] [] 0 uri t
;;
*)
+
+let reference_of_oxuri u =
+ let t = CicUtil.term_of_uri u in
+ let t',l = convert_term (UriManager.uri_of_string "cic:/dummy/dummy.con") t in
+ match t',l with
+ NCic.Const nref, [] -> nref
+ | _,_ -> assert false
+;;
val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference
+val reference_of_oxuri: UriManager.uri -> NReference.reference
+
val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list
val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list
(BoxPp.render_to_string
~map_unicode_to_tex:false
(function x::_ -> x | _ -> assert false)
- 80 (CicNotationPres.render (Hashtbl.create 0)
+ 80 (CicNotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));
[]
| _ -> []
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
rel_X_relation_class = Cic.Sort Cic.Prop; (* dummy value, overwritten below *)
rel_Xreflexive_relation_class = Cic.Sort Cic.Prop (* dummy value, overwritten below *)
} in
- let x_relation_class =
+ let _x_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
list_map_i (fun i _ -> Cic.Rel (len - i + 2)) 0 a_quantifiers_rev in
IsDefinition Definition) in
*) () in
let id_precise = id ^ "_precise_relation_class" in
- let xreflexive_relation_class =
+ let _xreflexive_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
list_map_i (fun i _ -> Cic.Rel (len - i)) 0 a_quantifiers_rev
let width = max_int in
let term_pp content_term =
let pres_term = TermContentPres.pp_ast content_term in
- let dummy_tbl = Hashtbl.create 1 in
- let markup = CicNotationPres.render dummy_tbl pres_term in
+ let lookup_uri = fun _ -> None in
+ let markup = CicNotationPres.render ~lookup_uri pres_term in
let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
Pcre.substitute
~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
let ind_uri_split ((s, _) as uri) =
let noxp = strip_xpointer uri in
- let length = String.length s in
try
(let arg_index = String.rindex s '(' in
try
(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
let nmml_of_cic_sequent metasenv subst sequent =
- let content_sequent = NTermCicContent.nmap_sequent ~subst sequent in
+ let content_sequent,ids_to_refs =
+ NTermCicContent.nmap_sequent ~subst sequent in
let pres_sequent =
- Sequent2pres.nsequent2pres subst content_sequent in
+ Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
let xmlpres = mpres_document pres_sequent in
Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
(ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
ids_to_inner_sorts,ids_to_inner_types)))
+let nmml_of_cic_object obj =
+ prerr_endline (NCicPp.ppobj obj);
+ assert false
+;;
+
let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
let unsh_sequent,(asequent,ids_to_terms,
ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
let t, ids_to_uris =
TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
let t = TermContentPres.pp_ast t in
- let t = CicNotationPres.render ids_to_uris t in
- BoxPp.render_to_string ~map_unicode_to_tex
+ let t =
+ CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) t
+ in
+ BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size t
let txt_of_cic_term ~map_unicode_to_tex size metasenv context t =
let ast, ids_to_uris =
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
let bobj =
- CicNotationPres.box_of_mpres (
- CicNotationPres.render ~prec:90 ids_to_uris
- (TermContentPres.pp_ast ast)) in
+ CicNotationPres.box_of_mpres (
+ CicNotationPres.render ~prec:90
+ ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
+ (TermContentPres.pp_ast ast)) in
let render = function _::x::_ -> x | _ -> assert false in
let mpres = CicNotationPres.mpres_of_box bobj in
let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
(Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
(Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *)
+val nmml_of_cic_object: NCic.obj -> Gdome.document
+
val txt_of_cic_term:
map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
string
let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
sequents_viewer#load_logo;
cic_math_view#set_href_callback
- (Some (fun uri -> (MatitaMathView.cicBrowser ())#load
- (`Uri (UriManager.uri_of_string uri))));
+ (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 browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer _ grafite_status =
sequents_viewer#reset;
method nload_sequent: NCic.metasenv -> NCic.substitution -> int -> unit
method load_object: Cic.obj -> unit
+ method load_nobject: NCic.obj -> unit
end
class type sequentsViewer =
end;
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
+
+ method load_nobject obj =
+ let mathml = ApplyTransformation.nmml_of_cic_object obj in
+(*
+ self#set_cic_info
+ (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
+ (match current_mathml with
+ | Some current_mathml when use_diff ->
+ self#freeze;
+ XmlDiff.update_dom ~from:current_mathml mathml;
+ self#thaw
+ | _ ->
+*)
+ if BuildTimeConf.debug then begin
+ let name =
+ "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
+ HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+ end;
+ self#load_root ~root:mathml#get_documentElement;
+ (*current_mathml <- Some mathml*)(*)*);
end
let tab_label meta_markup =
handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
mathView#set_href_callback (Some (fun uri ->
handle_error (fun () ->
- self#load (`Uri (UriManager.uri_of_string uri)))));
+ let uri =
+ try
+ `Uri (UriManager.uri_of_string uri)
+ with
+ UriManager.IllFormedUri _ ->
+ `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
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
self#dependencies dir uri ()
| `Uri uri -> self#_loadUriManagerUri uri
+ | `NRef nref -> self#_loadNReference nref
| `Univs uri -> self#_loadUnivs uri
| `Whelp (query, results) ->
set_whelp_query query;
let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
self#_loadObj obj
+ method private _loadNReference (NReference.Ref (uri,_)) =
+ let obj = NCicEnvironment.get_checked_obj uri in
+ self#_loadNObj obj
+
method private _loadUnivs uri =
let uri = UriManager.strip_xpointer uri in
let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
self#_showMath;
mathView#load_object obj
+ method private _loadNObj obj =
+ (* showMath must be done _before_ loading the document, since if the
+ * widget is not mapped (hidden by the notebook) the document is not
+ * rendered *)
+ self#_showMath;
+ mathView#load_nobject obj
+
method private _loadTermCic term metasenv =
let context = self#script#proofContext in
let dummyno = CicMkImplicit.new_meta metasenv [] in
let width = max_int in
let term_pp content_term =
let pres_term = TermContentPres.pp_ast content_term in
- let dummy_tbl = Hashtbl.create 1 in
- let markup = CicNotationPres.render dummy_tbl pres_term in
+ let lookup_uri = fun _ -> None in
+ let markup = CicNotationPres.render ~lookup_uri pres_term in
let s = "(" ^ BoxPp.render_to_string
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
| `HBugs of [ `Tutors ] (* list of available HBugs tutors *)
| `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
| `Uri of UriManager.uri (* cic object uri *)
+ | `NRef of NReference.reference (* cic object uri *)
| `Whelp of string * UriManager.uri list (* query and results *)
| `Univs of UriManager.uri
]
String.sub suri 4 (len - 4) in (* strip "cic:" prefix *)
(match dir with | `Fwd -> "forward" | `Back -> "backward") ^ suri)
| `Uri uri -> UriManager.string_of_uri uri
+ | `NRef nref -> NReference.string_of_reference nref
| `Whelp (query, _) -> query
| `Univs uri -> "univs:" ^ UriManager.string_of_uri uri
| `HBugs of [ `Tutors ]
| `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]
| `Uri of UriManager.uri
+ | `NRef of NReference.reference
| `Whelp of string * UriManager.uri list
| `Univs of UriManager.uri
]
projects / helm.git / commitdiff