From a970a6b5d44947e466b94ff3df4fa66d85d0d9ca Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Apr 2009 09:20:41 +0000 Subject: [PATCH] + Chain NCic.term -> content -> presentation very very roughly implemented + The sequent viewer now prints also the neq sequents --- .../METAS/meta.helm-content_pres.src | 2 +- helm/software/components/Makefile | 1 + .../components/content_pres/sequent2pres.ml | 11 +- .../components/content_pres/sequent2pres.mli | 2 + .../components/ng_cic_content/.depend | 3 + .../components/ng_cic_content/Makefile | 13 + .../ng_cic_content/nTermCicContent.ml | 411 ++++++++++++++++++ .../ng_cic_content/nTermCicContent.mli | 80 ++++ helm/software/configure.ac | 1 + helm/software/matita/applyTransformation.ml | 7 + helm/software/matita/applyTransformation.mli | 5 + helm/software/matita/matita.ml | 16 +- helm/software/matita/matitaGuiTypes.mli | 2 + helm/software/matita/matitaMathView.ml | 104 ++++- 14 files changed, 650 insertions(+), 8 deletions(-) create mode 100644 helm/software/components/ng_cic_content/.depend create mode 100644 helm/software/components/ng_cic_content/Makefile create mode 100644 helm/software/components/ng_cic_content/nTermCicContent.ml create mode 100644 helm/software/components/ng_cic_content/nTermCicContent.mli diff --git a/helm/software/components/METAS/meta.helm-content_pres.src b/helm/software/components/METAS/meta.helm-content_pres.src index 976b8f10c..74b1b23c9 100644 --- a/helm/software/components/METAS/meta.helm-content_pres.src +++ b/helm/software/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-acic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" +requires="helm-acic_content helm-ng_cic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 1f13fc94a..b9c7c651b 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -36,6 +36,7 @@ MODULES = \ ng_kernel \ ng_refiner \ ng_disambiguation \ + ng_cic_content \ grafite_parser \ ng_tactics \ grafite_engine \ diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml index d9c3a325e..41683b94f 100644 --- a/helm/software/components/content_pres/sequent2pres.ml +++ b/helm/software/components/content_pres/sequent2pres.ml @@ -47,7 +47,7 @@ let b_ink a = Box.Ink a module K = Content module P = Mpresentation -let sequent2pres term2pres (_,_,context,ty) = +let sequent2pres0 term2pres (_,_,context,ty) = let context2pres context = let rec aux accum = function @@ -96,7 +96,7 @@ let sequent2pres term2pres (_,_,context,ty) = pres_goal]))]) let sequent2pres ~ids_to_inner_sorts = - sequent2pres + sequent2pres0 (fun annterm -> let ast, ids_to_uris = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm @@ -105,3 +105,10 @@ let sequent2pres ~ids_to_inner_sorts = (CicNotationPres.render ids_to_uris (TermContentPres.pp_ast ast))) +let nsequent2pres = + sequent2pres0 + (fun term -> + let ast = NTermCicContent.nast_of_cic term in + CicNotationPres.box_of_mpres + (CicNotationPres.render (Hashtbl.create 1) + (TermContentPres.pp_ast ast))) diff --git a/helm/software/components/content_pres/sequent2pres.mli b/helm/software/components/content_pres/sequent2pres.mli index a9384eb18..b49263136 100644 --- a/helm/software/components/content_pres/sequent2pres.mli +++ b/helm/software/components/content_pres/sequent2pres.mli @@ -36,3 +36,5 @@ val sequent2pres : ids_to_inner_sorts:(Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> Cic.annterm Content.conjecture -> CicNotationPres.boxml_markup + +val nsequent2pres : NCic.term Content.conjecture -> CicNotationPres.boxml_markup diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend new file mode 100644 index 000000000..31202f452 --- /dev/null +++ b/helm/software/components/ng_cic_content/.depend @@ -0,0 +1,3 @@ +nTermCicContent.cmi: +nTermCicContent.cmo: nTermCicContent.cmi +nTermCicContent.cmx: nTermCicContent.cmi diff --git a/helm/software/components/ng_cic_content/Makefile b/helm/software/components/ng_cic_content/Makefile new file mode 100644 index 000000000..e899d62bd --- /dev/null +++ b/helm/software/components/ng_cic_content/Makefile @@ -0,0 +1,13 @@ +PACKAGE = ng_cic_content + +INTERFACE_FILES = \ + nTermCicContent.mli + +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + + +all: + + +include ../../Makefile.defs +include ../Makefile.common diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml new file mode 100644 index 000000000..d770837bc --- /dev/null +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -0,0 +1,411 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +(* $Id: termAcicContent.ml 9304 2008-12-05 23:12:39Z sacerdot $ *) + +open Printf + +module Ast = CicNotationPt + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +(* +type interpretation_id = int + +let idref id t = Ast.AttributedTerm (`IdRef id, t) + +type term_info = + { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; + uri: (Cic.id, UriManager.uri) Hashtbl.t; + } + +let get_types uri = + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + match o with + | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno + | _ -> assert false + +let name_of_inductive_type uri i = + let types, _ = get_types uri in + let (name, _, _, _) = try List.nth types i with Not_found -> assert false in + name + + (* returns pairs *) +let constructors_of_inductive_type uri i = + let types, _ = get_types uri in + let (_, _, _, constructors) = + try List.nth types i with Not_found -> assert false + in + constructors + + (* returns name only *) +let constructor_of_inductive_type uri i j = + (try + fst (List.nth (constructors_of_inductive_type uri i) (j-1)) + with Not_found -> assert false) + + (* returns the number of left parameters *) +let left_params_no_of_inductive_type uri = + snd (get_types uri) +*) + +(* CODICE c&p da NCicPp *) +let r2s pp_fix_name r = + try + match r with + | NReference.Ref (u,NReference.Ind (_,i,_)) -> + (match NCicLibrary.get_obj u with + | _,_,_,_, NCic.Inductive (_,_,itl,_) -> + let _,name,_,_ = List.nth itl i in name + | _ -> assert false) + | NReference.Ref (u,NReference.Con (i,j,_)) -> + (match NCicLibrary.get_obj u with + | _,_,_,_, NCic.Inductive (_,_,itl,_) -> + let _,_,_,cl = List.nth itl i in + let _,name,_ = List.nth cl (j-1) in name + | _ -> assert false) + | NReference.Ref (u,(NReference.Decl | NReference.Def _)) -> + (match NCicLibrary.get_obj u with + | _,_,_,_, NCic.Constant (_,name,_,_,_) -> name + | _ -> assert false) + | NReference.Ref (u,(NReference.Fix (i,_,_)|NReference.CoFix i)) -> + (match NCicLibrary.get_obj u with + | _,_,_,_, NCic.Fixpoint (_,fl,_) -> + if pp_fix_name then + let _,name,_,_,_ = List.nth fl i in name + else + NUri.name_of_uri u ^"("^ string_of_int i ^ ")" + | _ -> assert false) + with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r +;; + +let nast_of_cic = + let rec k = function + | NCic.Rel n -> Ast.Ident (string_of_int n, None) + | NCic.Const r -> Ast.Ident (r2s true r, None) + | NCic.Meta (n,l) -> Ast.Meta (n, [](*aux_context l*)) + | NCic.Sort NCic.Prop -> Ast.Sort `Prop + | NCic.Sort NCic.Type _ -> Ast.Sort `Set + | NCic.Implicit `Hole -> Ast.UserInput + | NCic.Implicit _ -> Ast.Implicit + | NCic.Prod (n,s,t) -> + let binder_kind = `Forall in + Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k s)), k t) + | NCic.Lambda (n,s,t) -> + Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k s)), k t) + | NCic.LetIn (n,s,ty,t) -> + Ast.LetIn ((Ast.Ident (n,None), Some (k ty)), k s, k t) + | NCic.Appl args -> Ast.Appl (List.map k args) + (*| NCic.AConst (id,uri,substs) -> + register_uri id uri; + idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))*) + | NCic.Match (uri,ty,te,patterns) -> +(* + let name = NReference.name_of_reference uri in + let uri_str = UriManager.string_of_uri uri in + let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in + let ctor_puri j = + UriManager.uri_of_string + (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) + in + let case_indty = name, Some (UriManager.uri_of_string puri_str) in + let constructors = constructors_of_inductive_type uri typeno in + let lpsno = left_params_no_of_inductive_type uri in + let rec eat_branch n ty pat = + match (ty, pat) with + | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat + | NCic.Prod (_, _, t), NCic.ALambda (_, name, s, t') -> + let (cv, rhs) = eat_branch 0 t t' in + (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs + | _, _ -> [], k pat + in + let j = ref 0 in + let patterns = + try + List.map2 + (fun (name, ty) pat -> + incr j; + let name,(capture_variables,rhs) = + match output_type with + `Term -> name, eat_branch lpsno ty pat + | `Pattern -> "_", ([], k pat) + in + Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs + ) constructors patterns + with Invalid_argument _ -> assert false + in + let indty = + match output_type with + `Pattern -> None + | `Term -> Some case_indty + in + idref id (Ast.Case (k te, indty, Some (k ty), patterns)) +*) Ast.Ident ("Un case",None) + in + k +;; + +let map_sequent (i,(n,context,ty):int * NCic.conjecture) = + let module K = Content in + let context' = + List.map + (function + | name,NCic.Decl t -> + Some + (* We should call build_decl_item, but we have not computed *) + (* the inner-types ==> we always produce a declaration *) + (`Declaration + { K.dec_name = (Some name); + K.dec_id = "-1"; + K.dec_inductive = false; + K.dec_aref = "-1"; + K.dec_type = t + }) + | name,NCic.Def (t,ty) -> + Some + (* We should call build_def_item, but we have not computed *) + (* the inner-types ==> we always produce a declaration *) + (`Definition + { K.def_name = (Some name); + K.def_id = "-1"; + K.def_aref = "-1"; + K.def_term = t; + K.def_type = ty + }) + ) context + in + "-1",i,context',ty +;; + +(* + (* persistent state *) + +let initial_level2_patterns32 () = Hashtbl.create 211 +let initial_interpretations () = Hashtbl.create 211 + +let level2_patterns32 = ref (initial_level2_patterns32 ()) +(* symb -> id list ref *) +let interpretations = ref (initial_interpretations ()) +let compiled32 = ref None +let pattern32_matrix = ref [] +let counter = ref ~-1 + +let stack = ref [] + +let push () = + stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack; + counter := ~-1; + level2_patterns32 := initial_level2_patterns32 (); + interpretations := initial_interpretations (); + compiled32 := None; + pattern32_matrix := [] +;; + +let pop () = + match !stack with + [] -> assert false + | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old -> + stack := old; + counter := ocounter; + level2_patterns32 := olevel2_patterns32; + interpretations := ointerpretations; + compiled32 := ocompiled32; + pattern32_matrix := opattern32_matrix +;; + +let get_compiled32 () = + match !compiled32 with + | None -> assert false + | Some f -> Lazy.force f + +let set_compiled32 f = compiled32 := Some f + +let add_idrefs = + List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) + +let instantiate32 term_info idrefs env symbol args = + let rec instantiate_arg = function + | Ast.IdentArg (n, name) -> + let t = + try List.assoc name env + with Not_found -> prerr_endline ("name not found in env: "^name); + assert false + in + let rec count_lambda = function + | Ast.AttributedTerm (_, t) -> count_lambda t + | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body + | _ -> 0 + in + let rec add_lambda t n = + if n > 0 then + let name = CicNotationUtil.fresh_name () in + Ast.Binder (`Lambda, (Ast.Ident (name, None), None), + Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) + else + t + in + add_lambda t (n - count_lambda t) + in + let head = + let symbol = Ast.Symbol (symbol, 0) in + add_idrefs idrefs symbol + in + if args = [] then head + else Ast.Appl (head :: List.map instantiate_arg args) + +let rec ast_of_acic1 ~output_type term_info annterm = + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in + match (get_compiled32 ()) annterm with + | None -> + ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type) + | Some (env, ctors, pid) -> + let idrefs = + List.map + (fun annterm -> + let idref = CicUtil.id_of_annterm annterm in + (try + register_uri idref + (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) + with Invalid_argument _ -> ()); + idref) + ctors + in + let env' = + List.map + (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env + in + let _, symbol, args, _ = + try + Hashtbl.find !level2_patterns32 pid + with Not_found -> assert false + in + let ast = instantiate32 term_info idrefs env' symbol args in + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) + +let load_patterns32 t = + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t + in + set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) + +let ast_of_acic ~output_type id_to_sort annterm = + debug_print (lazy ("ast_of_acic <- " + ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); + let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in + let ast = ast_of_acic1 ~output_type term_info annterm in + debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); + ast, term_info.uri + +let fresh_id = + fun () -> + incr counter; + !counter + +let add_interpretation dsc (symbol, args) appl_pattern = + let id = fresh_id () in + Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern); + pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix; + load_patterns32 !pattern32_matrix; + (try + let ids = Hashtbl.find !interpretations symbol in + ids := id :: !ids + with Not_found -> Hashtbl.add !interpretations symbol (ref [id])); + id + +let get_all_interpretations () = + List.map + (function (_, _, id) -> + let (dsc, _, _, _) = + try + Hashtbl.find !level2_patterns32 id + with Not_found -> assert false + in + (id, dsc)) + !pattern32_matrix + +let get_active_interpretations () = + HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None) + !pattern32_matrix + +let set_active_interpretations ids = + let pattern32_matrix' = + List.map + (function + | (_, ap, id) when List.mem id ids -> (true, ap, id) + | (_, ap, id) -> (false, ap, id)) + !pattern32_matrix + in + pattern32_matrix := pattern32_matrix'; + load_patterns32 !pattern32_matrix + +exception Interpretation_not_found + +let lookup_interpretations symbol = + try + HExtlib.list_uniq + (List.sort Pervasives.compare + (List.map + (fun id -> + let (dsc, _, args, appl_pattern) = + try + Hashtbl.find !level2_patterns32 id + with Not_found -> assert false + in + dsc, args, appl_pattern) + !(Hashtbl.find !interpretations symbol))) + with Not_found -> raise Interpretation_not_found + +let remove_interpretation id = + (try + let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in + let ids = Hashtbl.find !interpretations symbol in + ids := List.filter ((<>) id) !ids; + Hashtbl.remove !level2_patterns32 id; + with Not_found -> raise Interpretation_not_found); + pattern32_matrix := + List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; + load_patterns32 !pattern32_matrix + +let _ = load_patterns32 [] + +let instantiate_appl_pattern + ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern += + let lookup name = + try List.assoc name env + with Not_found -> + prerr_endline (sprintf "Name %s not found" name); + assert false + in + let rec aux = function + | Ast.UriPattern uri -> term_of_uri uri + | Ast.ImplicitPattern -> mk_implicit false + | Ast.VarPattern name -> lookup name + | Ast.ApplPattern terms -> mk_appl (List.map aux terms) + in + aux appl_pattern +*) diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli new file mode 100644 index 000000000..2f2acb077 --- /dev/null +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -0,0 +1,80 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + + +(* + (** {2 Persistant state handling} *) + +type interpretation_id + +val add_interpretation: + string -> (* id / description *) + string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *) + CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + interpretation_id + + (** @raise Interpretation_not_found *) +val lookup_interpretations: + string -> (* symbol *) + (string * CicNotationPt.argument_pattern list * + CicNotationPt.cic_appl_pattern) list + +exception Interpretation_not_found + + (** @raise Interpretation_not_found *) +val remove_interpretation: interpretation_id -> unit + + (** {3 Interpretations toggling} *) + +val get_all_interpretations: unit -> (interpretation_id * string) list +val get_active_interpretations: unit -> interpretation_id list +val set_active_interpretations: interpretation_id list -> unit + + (** {2 acic -> content} *) + +val ast_of_acic: + output_type:[`Pattern|`Term] -> + (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) + Cic.annterm -> (* acic *) + CicNotationPt.term (* ast *) + * (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *) + + (** {2 content -> acic} *) + + (** @param env environment from argument_pattern to cic terms + * @param pat cic_appl_pattern *) +val instantiate_appl_pattern: + mk_appl:('term list -> 'term) -> + mk_implicit:(bool -> 'term) -> + term_of_uri : (UriManager.uri -> 'term) -> + (string * 'term) list -> CicNotationPt.cic_appl_pattern -> + 'term + +val push: unit -> unit +val pop: unit -> unit +*) + +val nast_of_cic : NCic.term -> CicNotationPt.term +val map_sequent : int * NCic.conjecture -> NCic.term Content.conjecture diff --git a/helm/software/configure.ac b/helm/software/configure.ac index 8e0335d9e..9fbae9851 100644 --- a/helm/software/configure.ac +++ b/helm/software/configure.ac @@ -79,6 +79,7 @@ helm-grafite \ helm-grafite_engine \ helm-tptp_grafite \ helm-ng_disambiguation \ +helm-ng_cic_content \ helm-grafite_parser \ helm-acic_procedural \ helm-content_pres \ diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 670fd2e0c..27725882e 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -64,6 +64,13 @@ let mml_of_cic_sequent metasenv sequent = (asequent, (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.map_sequent sequent in + let pres_sequent = + Sequent2pres.nsequent2pres content_sequent in + let xmlpres = mpres_document pres_sequent in + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres + let mml_of_cic_object obj = let (annobj, 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/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 95712f78e..a65e1e70c 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -44,6 +44,11 @@ val mml_of_cic_sequent: (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) (Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *) +val nmml_of_cic_sequent: + NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) + int * NCic.conjecture -> (* sequent *) + Gdome.document (* Math ML *) + val mml_of_cic_object: Cic.obj -> (* object *) Gdome.document * (* Math ML *) diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index b3963bf02..aecf026aa 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -99,7 +99,21 @@ let _ = sequents_viewer#goto_sequent goal with Failure _ -> script#setGoal None); | Proof proof -> sequents_viewer#load_logo_with_qed - | No_proof -> sequents_viewer#load_logo + | No_proof -> + (match grafite_status.ng_status with + ProofMode nstatus -> + sequents_viewer#nload_sequents nstatus; + (try + script#setGoal (Some (Continuationals.Stack.find_goal nstatus.NTacStatus.gstatus)); + let goal = + match script#goal with + None -> assert false + | Some n -> n + in + sequents_viewer#goto_sequent goal + with Failure _ -> script#setGoal None); + | CommandMode _ -> sequents_viewer#load_logo + ) | Intermediate _ -> assert false (* only the engine may be in this state *) in script#addObserver sequents_observer; diff --git a/helm/software/matita/matitaGuiTypes.mli b/helm/software/matita/matitaGuiTypes.mli index d42775827..51c700dc3 100644 --- a/helm/software/matita/matitaGuiTypes.mli +++ b/helm/software/matita/matitaGuiTypes.mli @@ -124,6 +124,7 @@ object (** load a sequent and render it into parent widget *) method load_sequent: Cic.metasenv -> int -> unit + method nload_sequent: NCic.metasenv -> NCic.substitution -> int -> unit method load_object: Cic.obj -> unit end @@ -134,6 +135,7 @@ object method load_logo: unit method load_logo_with_qed: unit method load_sequents: GrafiteTypes.incomplete_proof -> unit + method nload_sequents: NTacStatus.tac_status -> unit method goto_sequent: int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index f57dc4d32..9c259a1cb 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -593,6 +593,19 @@ object (self) end; self#load_root ~root:mathml#get_documentElement + method nload_sequent metasenv subst metano = + let sequent = List.assoc metano metasenv in + let mathml = + ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent) + in + if BuildTimeConf.debug then begin + let name = + "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in + HLog.debug ("load_sequent: dumping MathML to ./" ^ name); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) + end; + self#load_root ~root:mathml#get_documentElement + method load_object obj = let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) let (mathml, @@ -642,7 +655,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) - val mutable _metasenv = [] + val mutable _metasenv = `Old [] val mutable scrolledWin: GBin.scrolled_window option = None (* scrolled window to which the sequentViewer is currently attached *) val logo = (GMisc.image @@ -681,13 +694,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- []; + _metasenv <- `Old []; self#script#setGoal None method load_sequents { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } = - _metasenv <- metasenv; + _metasenv <- `Old metasenv; pages <- 0; let win goal_switch = let w = @@ -764,9 +777,92 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal (Some (goal_of_switch goal_switch)); self#render_page ~page ~goal_switch)) + method nload_sequents + { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack } + = + _metasenv <- `New (metasenv,subst); + pages <- 0; + let win goal_switch = + let w = + GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS + ~shadow_type:`IN ~show:true () + in + let reparent () = + scrolledWin <- Some w; + match cicMathView#misc#parent with + | None -> w#add cicMathView#coerce + | Some parent -> + let parent = + match cicMathView#misc#parent with + None -> assert false + | Some p -> GContainer.cast_container p + in + parent#remove cicMathView#coerce; + w#add cicMathView#coerce + in + goal2win <- (goal_switch, reparent) :: goal2win; + w#coerce + in + assert ( + let stack_goals = Stack.open_goals stack in + let proof_goals = List.map fst metasenv in + if + HExtlib.list_uniq (List.sort Pervasives.compare stack_goals) + <> List.sort Pervasives.compare proof_goals + then begin + prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals)); + prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals)); + false + end + else true + ); + let render_switch = + function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i) + in + let page = ref 0 in + let added_goals = ref [] in + (* goals can be duplicated on the tack due to focus, but we should avoid + * multiple labels in the user interface *) + let add_tab markup goal_switch = + let goal = Stack.goal_of_switch goal_switch in + if not (List.mem goal !added_goals) then begin + ignore(notebook#append_page + ~tab_label:(tab_label markup) (win goal_switch)); + page2goal <- (!page, goal_switch) :: page2goal; + goal2page <- (goal_switch, !page) :: goal2page; + incr page; + pages <- pages + 1; + added_goals := goal :: !added_goals + end + in + let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in + Stack.iter (** populate notebook with tabs *) + ~env:(fun depth tag (pos, sw) -> + let markup = + match depth, pos with + | 0, 0 -> `Current (render_switch sw) + | 0, _ -> `Shift (pos, `Current (render_switch sw)) + | 1, pos when Stack.head_tag stack = `BranchTag -> + `Shift (pos, render_switch sw) + | _ -> render_switch sw + in + add_tab markup sw) + ~cont:add_switch ~todo:add_switch + stack; + switch_page_callback <- + Some (notebook#connect#switch_page ~callback:(fun page -> + let goal_switch = + try List.assoc page page2goal with Not_found -> assert false + in + self#script#setGoal (Some (goal_of_switch goal_switch)); + self#render_page ~page ~goal_switch)) + method private render_page ~page ~goal_switch = (match goal_switch with - | Stack.Open goal -> cicMathView#load_sequent _metasenv goal + | Stack.Open goal -> + (match _metasenv with + `Old menv -> cicMathView#load_sequent menv goal + | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal) | Stack.Closed goal -> let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); -- 2.39.2