have an id and thus can be selected.
<!ELEMENT Conjecture %sequent;>
<!ATTLIST Conjecture
- no NMTOKEN #REQUIRED>
+ no NMTOKEN #REQUIRED
+ id ID #REQUIRED>
<!ELEMENT Constructor %term;>
<!ATTLIST Constructor
<!ELEMENT Decl %term;>
<!ATTLIST Decl
- name CDATA #IMPLIED>
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
<!ELEMENT Def %term;>
<!ATTLIST Def
- name CDATA #IMPLIED>
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
<!ELEMENT Hidden EMPTY>
+<!ATTLIST Hidden
+ id ID #REQUIRED>
<!ELEMENT Goal %term;>
C.ACurrentProof (id,n,conjectures,bo,ty) ->
X.xml_nempty "CurrentProof" ["name",n ; "id", id]
[< List.fold_left
- (fun i (n,canonical_context,t) ->
+ (fun i (cid,n,canonical_context,t) ->
[< i ;
- X.xml_nempty "Conjecture" ["no",(string_of_int n)]
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",(string_of_int n)]
[< List.fold_left
- (fun i t ->
+ (fun i (hid,t) ->
[< (match t with
Some (n,C.ADecl t) ->
X.xml_nempty "Decl"
(match n with
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])
(print_term curi ids_to_inner_sorts t)
| Some (n,C.ADef t) ->
X.xml_nempty "Def"
(match n with
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])
(print_term curi ids_to_inner_sorts t)
- | None -> X.xml_empty "Hidden" []
+ | None -> X.xml_empty "Hidden" ["id",hid]
) ;
i
>]
exception Found of (Cic.name * Cic.context_entry) list;;
-exception NotImplemented;;
-
let acic_object_of_cic_object obj =
let module C = Cic in
let ids_to_terms = Hashtbl.create 503 in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
+ let ids_to_conjectures = Hashtbl.create 11 in
+ let ids_to_hypotheses = Hashtbl.create 127 in
+ let hypotheses_seed = ref 0 in
+ let conjectures_seed = ref 0 in
let seed = ref 0 in
let acic_term_of_cic_term_context' =
acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
| C.CurrentProof (id,conjectures,bo,ty) ->
let aconjectures =
List.map
- (function (i,canonical_context,term) ->
- let acanonical_context =
- let rec aux =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- let at =
- acic_term_of_cic_term_context' conjectures tl t
- in
- Some (n,C.ADecl at)::(aux tl)
- | (Some (n,C.Def t))::tl ->
- let at =
- acic_term_of_cic_term_context' conjectures tl t
- in
- Some (n,C.ADef at)::(aux tl)
- | None::tl -> None::(aux tl)
- in
- aux canonical_context
- in
- let aterm =
- acic_term_of_cic_term_context' conjectures canonical_context term
+ (function (i,canonical_context,term) as conjecture ->
+ let cid = "c" ^ string_of_int !conjectures_seed in
+ Hashtbl.add ids_to_conjectures cid conjecture ;
+ incr conjectures_seed ;
+ let acanonical_context =
+ let rec aux =
+ function
+ [] -> []
+ | hyp::tl ->
+ let hid = "h" ^ string_of_int !hypotheses_seed in
+ Hashtbl.add ids_to_hypotheses hid hyp ;
+ incr hypotheses_seed ;
+ match hyp with
+ (Some (n,C.Decl t)) ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ (hid,Some (n,C.ADecl at))::(aux tl)
+ | (Some (n,C.Def t)) ->
+ let at =
+ acic_term_of_cic_term_context' conjectures tl t
+ in
+ (hid,Some (n,C.ADef at))::(aux tl)
+ | None -> (hid,None)::(aux tl)
+ in
+ aux canonical_context
in
- (i, acanonical_context,aterm)
+ let aterm =
+ acic_term_of_cic_term_context' conjectures canonical_context term
+ in
+ (cid,i,acanonical_context,aterm)
) conjectures in
let abo = acic_term_of_cic_term_context' conjectures [] bo in
let aty = acic_term_of_cic_term_context' conjectures [] ty in
C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
| C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
in
- aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types
+ aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
+ ids_to_conjectures,ids_to_hypotheses
;;
uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
in
let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
+ (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
+ ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
=
Cic2acic.acic_object_of_cic_object currentproof
in
mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
in
output#load_tree mml ;
- current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ current_cic_infos :=
+ Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
with
e ->
match !ProofEngine.proof with
| Some (_,metasenv,_,_) -> metasenv
in
let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
- let sequent_gdome,ids_to_terms,ids_to_father_ids =
+ let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
SequentPp.XmlPp.print_sequent metasenv currentsequent
in
let sequent_doc =
applyStylesheets sequent_doc sequent_styles sequent_args
in
proofw#load_tree ~dom:sequent_mml ;
- current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+ current_goal_infos :=
+ Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
with
e ->
let metano =
in
canonical_context
in
- let sequent_gdome,ids_to_terms,ids_to_father_ids =
+ let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
in
let sequent_doc =
let res =
applyStylesheets sequent_doc sequent_styles sequent_args ;
in
- current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
+ current_scratch_infos :=
+ Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
res
;;
begin
try
match !current_goal_infos with
- Some (ids_to_terms, ids_to_father_ids) ->
+ Some (ids_to_terms, ids_to_father_ids,_) ->
let id = xpath in
tactic (Hashtbl.find ids_to_terms id) ;
refresh_sequent rendering_window#proofw ;
begin
try
match !current_goal_infos with
- Some (ids_to_terms, ids_to_father_ids) ->
+ Some (ids_to_terms, ids_to_father_ids,_) ->
let id = xpath in
(* Let's parse the input *)
let inputlen = inputt#length in
try
match !current_scratch_infos with
(* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids) ->
+ Some (term,ids_to_terms, ids_to_father_ids,_) ->
let id = xpath in
let expr = tactic term (Hashtbl.find ids_to_terms id) in
let mml = mml_of_cic_term 111 expr in
let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types)
+ ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
=
Cic2acic.acic_object_of_cic_object proof
in
mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
in
(rendering_window#output : GMathView.math_view)#load_tree mml ;
- current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ current_cic_infos :=
+ Some
+ (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses)
end
else
raise WrongProof
let currentproof =
Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
in
- let (acurrentproof,_,_,ids_to_inner_sorts,_) =
+ let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
Cic2acic.acic_object_of_cic_object currentproof
in
let xml = Cic2Xml.print_object uri ids_to_inner_sorts acurrentproof in
begin
try
match !current_cic_infos with
- Some (ids_to_terms, ids_to_father_ids) ->
+ Some (ids_to_terms, ids_to_father_ids, _, _) ->
let id = xpath in
L.to_sequent id ids_to_terms ids_to_father_ids ;
refresh_proof rendering_window#output ;
begin
try
match !current_cic_infos with
- Some (ids_to_terms, ids_to_father_ids) ->
+ Some (ids_to_terms, ids_to_father_ids, _, _) ->
let id = xpath in
L.focus id ids_to_terms ids_to_father_ids ;
refresh_sequent rendering_window#proofw
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
+ let ids_to_hypotheses = Hashtbl.create 11 in
+ let hypotheses_seed = ref 0 in
let seed = ref 0 in
let acic_of_cic_context =
Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
let final_s,_ =
(List.fold_right
(fun binding (s,context) ->
- match binding with
- (Some (n,(Cic.Def t as b)) as entry)
- | (Some (n,(Cic.Decl t as b)) as entry) ->
- let acic = acic_of_cic_context context t in
- [< s ;
- X.xml_nempty
- (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
- ["name",(match n with Cic.Name n -> n | _ -> assert false)]
- (Cic2Xml.print_term
- (UriManager.uri_of_string "cic:/dummy.con")
- ids_to_inner_sorts acic)
- >], (entry::context)
- | None ->
- [< s ; X.xml_empty "Hidden" [] >], (None::context)
+ let hid = "h" ^ string_of_int !hypotheses_seed in
+ Hashtbl.add ids_to_hypotheses hid binding ;
+ incr hypotheses_seed ;
+ match binding with
+ (Some (n,(Cic.Def t as b)) as entry)
+ | (Some (n,(Cic.Decl t as b)) as entry) ->
+ let acic = acic_of_cic_context context t in
+ [< s ;
+ X.xml_nempty
+ (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
+ ["name",(match n with Cic.Name n -> n | _ -> assert false);
+ "id",hid]
+ (Cic2Xml.print_term
+ (UriManager.uri_of_string "cic:/dummy.con")
+ ids_to_inner_sorts acic)
+ >], (entry::context)
+ | None ->
+ [< s ; X.xml_empty "Hidden" [] >], (None::context)
) context ([<>],[])
)
in
(Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
ids_to_inner_sorts acic)
>],
- ids_to_terms,ids_to_father_ids
+ ids_to_terms,ids_to_father_ids,ids_to_hypotheses
;;
end
;;
type anntarget =
Object of annobj
| Term of annterm
+ | Conjecture of annconjecture
+ | Hypothesis of annhypothesis
(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
and sort =
and coInductiveFun =
string * term * term (* name, type, body *)
-and metasenv = (int * context * term) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and conjecture = int * context * term
+and metasenv = conjecture list
-and annmetasenv = (int * anncontext * annterm) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and annconjecture = id * int * anncontext * annterm
+and annmetasenv = annconjecture list
and annterm =
ARel of id * int * string (* DeBrujin index, binder *)
Possible of 'a (* an approximation to something *)
| Actual of 'a (* something *)
-and context_entry = (* Contexts are lists of context_entry *)
+and context_entry = (* A declaration or definition *)
Decl of term
| Def of term
-and context = ((name * context_entry) option) list
+and hypothesis =
+ (name * context_entry) option (* None means no more accessible *)
-and anncontext_entry = (* Contexts are lists of context_entry *)
+and context = hypothesis list
+
+and anncontext_entry = (* A declaration or definition *)
ADecl of annterm
| ADef of annterm
-and anncontext = ((name * anncontext_entry) option) list;;
+and annhypothesis =
+ id * (name * anncontext_entry) option (* None means no more accessible *)
+
+and anncontext = annhypothesis list;;
[] -> (c, v, t)
| conj::tl when conj#node_type = D.T_element "Conjecture" ->
let no = int_of_attr (conj#attribute "no") in
+ let xid = string_of_attr (conj#attribute "id") in
let typ,canonical_context =
match List.rev (conj#sub_nodes) with
[] -> raise (IllFormedXml 13)
match n#node_type with
D.T_element "Decl" ->
let name = name_of_attr (n#attribute "name") in
+ let hid = string_of_attr (n#attribute "id") in
let term = (get_content n)#extension#to_cic_term in
- Some (name,Cic.ADecl term)
+ hid,Some (name,Cic.ADecl term)
| D.T_element "Def" ->
let name = name_of_attr (n#attribute "name") in
+ let hid = string_of_attr (n#attribute "id") in
let term = (get_content n)#extension#to_cic_term in
- Some (name,Cic.ADef term)
- | D.T_element "Hidden" -> None
+ hid,Some (name,Cic.ADef term)
+ | D.T_element "Hidden" ->
+ let hid = string_of_attr (n#attribute "id") in
+ hid,None
| _ -> raise (IllFormedXml 14)
) canonical_context
in
- rget ((no, canonical_context, typ)::c, v, t) tl
+ rget ((xid, no, canonical_context, typ)::c, v, t) tl
| value::tl when value#node_type = D.T_element "body" ->
let v' = (get_content value)#extension#to_cic_term in
(match v with
name,
List.map
(function
- (id,acontext,con) ->
+ (_,id,acontext,con) ->
let context =
List.map
(function
- Some (n,(C.ADef at)) -> Some (n,(C.Def (deannotate_term at)))
- | Some (n,(C.ADecl at)) ->Some (n,(C.Decl (deannotate_term at)))
- | None -> None) acontext
+ _,Some (n,(C.ADef at)) ->
+ Some (n,(C.Def (deannotate_term at)))
+ | _,Some (n,(C.ADecl at)) ->
+ Some (n,(C.Decl (deannotate_term at)))
+ | _,None -> None
+ ) acontext
in
- (id,context, deannotate_term con)
+ (id,context,deannotate_term con)
) conjs,
- deannotate_term bo, deannotate_term ty
+ deannotate_term bo,deannotate_term ty
)
| C.AInductiveDefinition (_, tys, params, parno) ->
C.InductiveDefinition ( List.map deannotate_inductiveType tys,
| C.ACurrentProof (xid, _, conjs, bo, ty) ->
[< print_ann i2a xid ;
List.fold_right
- (fun (_, context, t) i ->
- [< List.fold_right
- (fun context_entry i ->
- [<(match context_entry with
+ (fun (cid, _, context, t) i ->
+ [< print_ann i2a cid ;
+ List.fold_right
+ (fun (hid,context_entry) i ->
+ [<print_ann i2a hid ;
+ (match context_entry with
Some (_,C.ADecl at) -> print_term i2a at
| Some (_,C.ADef at) -> print_term i2a at
| None -> [< >]
add_target_term ty
| C.ACurrentProof (id,_,cl,bo,ty) ->
set_target id (C.Object annobj) ;
- List.iter (function (_,context, t) ->
+ List.iter (function (cid,_,context, t) as annconj ->
+ set_target cid (C.Conjecture annconj) ;
List.iter
- (function
- Some (_,C.ADecl at) -> add_target_term at
- | Some (_,C.ADef at) -> add_target_term at
- | None -> ()
- ) context;
+ (function ((hid,h) as annhyp) ->
+ set_target hid (C.Hypothesis annhyp) ;
+ match h with
+ Some (_,C.ADecl at) -> add_target_term at
+ | Some (_,C.ADef at) -> add_target_term at
+ | None -> ()
+ ) context;
add_target_term t) cl ;
add_target_term bo ;
add_target_term ty
<xsl:for-each select="Conjecture">
<m:mtr>
<m:mtd>
- <m:mrow>
+ <m:mrow helm:xref="{@helm:xref}">
<m:mphantom><m:mtext>__</m:mtext></m:mphantom>
<xsl:for-each select="Decl|Def|Hidden">
<xsl:choose>
<xsl:when test="name(.)='Decl'">
- <m:mrow>
+ <m:mrow helm:xref="{@helm:xref}">
<xsl:choose>
<xsl:when test="@name">
<m:mi><xsl:value-of select="@name"/></m:mi>
</m:mrow>
</xsl:when>
<xsl:when test="name(.)='Def'">
- <m:mrow>
+ <m:mrow helm:xref="{@helm:xref}">
<xsl:choose>
<xsl:when test="@name">
<m:mi><xsl:value-of select="@name"/></m:mi>
</m:mrow>
</xsl:when>
<xsl:otherwise>
- <m:mrow>
+ <m:mrow helm:xref="{@helm:xref}">
<m:mi>_</m:mi>
<m:mo>:?</m:mo>
<m:mi>_</m:mi>
<xsl:for-each select="Decl|Def">
<m:mtr>
<m:mtd>
- <m:mrow>
+ <m:mrow helm:xref="{@helm:xref}">
<m:mi><xsl:value-of select="@name"/></m:mi>
<xsl:choose>
<xsl:when test="name(.) = 'Decl'">
<xsl:attribute name="name">
<xsl:value-of select="@name"/>
</xsl:attribute>
+ <xsl:attribute name="helm-xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
<xsl:apply-templates select="*[1]"/>
</xsl:copy>
</xsl:for-each>
<xsl:template match="CurrentProof" mode="noannot">
<CurrentProof name="{@name}" helm:xref="{@id}">
<xsl:for-each select="Conjecture">
- <Conjecture no="{@no}">
+ <Conjecture no="{@no}" helm:xref="{@id}">
<xsl:for-each select="*">
<xsl:copy>
- <xsl:copy-of select="@*"/>
+ <xsl:copy-of select="@name"/>
+ <xsl:attribute name="helm:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
<xsl:apply-templates select="*"/>
</xsl:copy>
</xsl:for-each>
projects / helm.git / commitdiff