From: Claudio Sacerdoti Coen Date: Wed, 22 May 2002 10:13:34 +0000 (+0000) Subject: Conjectures and Hypotheses inside every conjecture and in the sequents now X-Git-Tag: V_0_3_0_debian_8~84 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b57c31a1593872c181249135bc05ebd9a72f523b;p=helm.git Conjectures and Hypotheses inside every conjecture and in the sequents now have an id and thus can be selected. --- diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd index 088c78abf..47280b845 100644 --- a/helm/dtd/cic.dtd +++ b/helm/dtd/cic.dtd @@ -91,7 +91,8 @@ + no NMTOKEN #REQUIRED + id ID #REQUIRED> + name CDATA #IMPLIED + id ID #REQUIRED> + name CDATA #IMPLIED + id ID #REQUIRED> + diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index f04df2f2f..ad1d1f881 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -185,25 +185,26 @@ let print_object curi ids_to_inner_sorts = 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 >] diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index d7688499c..ffe9dbd4d 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -205,14 +205,16 @@ let acic_of_cic_context metasenv context t = 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 @@ -230,34 +232,43 @@ let acic_object_of_cic_object obj = | 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 ;; diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 789a65ba5..cfe4d2e06 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -171,7 +171,8 @@ let refresh_proof (output : GMathView.math_view) = 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 @@ -179,7 +180,8 @@ let refresh_proof (output : GMathView.math_view) = 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 @@ -200,7 +202,7 @@ let refresh_sequent (proofw : GMathView.math_view) = | 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 = @@ -210,7 +212,8 @@ let refresh_sequent (proofw : GMathView.math_view) = 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 = @@ -248,7 +251,7 @@ let mml_of_cic_term metano term = 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 = @@ -257,7 +260,8 @@ let mml_of_cic_term metano term = 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 ;; @@ -397,7 +401,7 @@ let call_tactic_with_goal_input tactic rendering_window () = 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 ; @@ -451,7 +455,7 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = 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 @@ -547,7 +551,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () = 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 @@ -632,7 +636,7 @@ let qed rendering_window () = 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 @@ -640,7 +644,10 @@ let qed rendering_window () = 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 @@ -660,7 +667,7 @@ let save rendering_window () = 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 @@ -731,7 +738,7 @@ let proveit rendering_window () = 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 ; @@ -772,7 +779,7 @@ let focus rendering_window () = 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 diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index bffb3030c..df504e75a 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -43,6 +43,8 @@ module XmlPp = 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 @@ -51,20 +53,24 @@ module XmlPp = 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 @@ -75,7 +81,7 @@ module XmlPp = (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 ;; diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 550d4a8f6..a556aadca 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -40,6 +40,8 @@ type id = string (* the abstract type of the (annotated) node identifiers *) type anntarget = Object of annobj | Term of annterm + | Conjecture of annconjecture + | Hypothesis of annhypothesis (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) and sort = @@ -93,9 +95,13 @@ and inductiveFun = 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 *) @@ -150,14 +156,20 @@ and 'a exactness = 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;; diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index 4865c6e4a..154b294ce 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -152,6 +152,7 @@ let get_conjs_value_type l = [] -> (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) @@ -162,17 +163,21 @@ let get_conjs_value_type l = 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 diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index f0ae11879..27ea5b3b7 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -101,17 +101,20 @@ let deannotate_obj = 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, diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 8fb002f3f..7ea0b7b63 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -119,10 +119,12 @@ let pp_annotation obj i2a curi = | 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_term i2a at | Some (_,C.ADef at) -> print_term i2a at | None -> [< >] diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml index 76cb7f75a..eef9880bc 100644 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -116,13 +116,16 @@ let get_ids_to_targets annobj = 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 diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 7aeec143f..6ab6ffe1f 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -181,12 +181,12 @@ which generates the toplevel element (see for instance xlink) --> - + __ - + @@ -200,7 +200,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -214,7 +214,7 @@ which generates the toplevel element (see for instance xlink) --> - + _ :? _ @@ -424,7 +424,7 @@ which generates the toplevel element (see for instance xlink) --> - + diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl index 5b375084b..b4a0e748d 100644 --- a/helm/style/objcontent.xsl +++ b/helm/style/objcontent.xsl @@ -61,6 +61,9 @@ + + + @@ -114,10 +117,13 @@ - + - + + + +