From 2329c7fd13fb6c88f9f82ccad6b25a67c9ce7acf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Apr 2002 11:53:11 +0000 Subject: [PATCH] First commit of our future proof-assistant/proof-improver (???) This commit is based on some un-committed changes to our libraries. So, it won't compile out-of-the-box. --- helm/gTopLevel/.depend | 8 + helm/gTopLevel/Makefile | 50 +++ helm/gTopLevel/cic2Xml.ml | 147 ++++++++ helm/gTopLevel/cic2acic.ml | 108 ++++++ helm/gTopLevel/gTopLevel.ml | 526 ++++++++++++++++++++++++++++ helm/gTopLevel/logicalOperations.ml | 73 ++++ helm/gTopLevel/proofEngine.ml | 8 + helm/gTopLevel/sequentPp.ml | 68 ++++ helm/gTopLevel/xml2Gdome.ml | 47 +++ 9 files changed, 1035 insertions(+) create mode 100644 helm/gTopLevel/.depend create mode 100644 helm/gTopLevel/Makefile create mode 100644 helm/gTopLevel/cic2Xml.ml create mode 100644 helm/gTopLevel/cic2acic.ml create mode 100644 helm/gTopLevel/gTopLevel.ml create mode 100644 helm/gTopLevel/logicalOperations.ml create mode 100644 helm/gTopLevel/proofEngine.ml create mode 100644 helm/gTopLevel/sequentPp.ml create mode 100644 helm/gTopLevel/xml2Gdome.ml diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend new file mode 100644 index 000000000..661d1055b --- /dev/null +++ b/helm/gTopLevel/.depend @@ -0,0 +1,8 @@ +logicalOperations.cmo: proofEngine.cmo +logicalOperations.cmx: proofEngine.cmx +sequentPp.cmo: cic2Xml.cmo cic2acic.cmo proofEngine.cmo +sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx +gTopLevel.cmo: cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \ + xml2Gdome.cmo +gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx sequentPp.cmx \ + xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile new file mode 100644 index 000000000..08a8acd17 --- /dev/null +++ b/helm/gTopLevel/Makefile @@ -0,0 +1,50 @@ +BIN_DIR = /usr/local/bin +REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ + helm-xml gdome_xslt +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep -pp camlp4o + +LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) + +all: gTopLevel +opt: gTopLevel.opt + +DEPOBJS = xml2Gdome.ml proofEngine.ml cic2Xml.ml cic2acic.ml \ + logicalOperations.ml sequentPp.ml gTopLevel.ml + +TOPLEVELOBJS = xml2Gdome.cmo proofEngine.cmo cic2Xml.cmo cic2acic.cmo \ + logicalOperations.cmo sequentPp.cmo gTopLevel.cmo + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) + $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS) + +gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: $(LIBRARIES) + $(OCAMLC) -c $< +.mli.cmi: $(LIBRARIES) + $(OCAMLC) -c $< +.ml.cmx: $(LIBRARIES_OPT) + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt + +install: + cp gTopLevel gTopLevel.opt $(BIN_DIR) + +uninstall: + rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml new file mode 100644 index 000000000..692037311 --- /dev/null +++ b/helm/gTopLevel/cic2Xml.ml @@ -0,0 +1,147 @@ + +(* 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/. + *) + +(*CSC codice cut & paste da cicPp e xmlcommand *) + +exception ImpossiblePossible;; +exception NotImplemented;; +let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";; + +(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +let print_term curi = + let rec aux = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + function + C.ARel (id,n,b) -> + X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id] + | C.AVar (id,uri) -> + let vdepth = U.depth_of_uri uri + and cdepth = U.depth_of_uri curi in + X.xml_empty "VAR" + ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^ + (U.name_of_uri uri) ; + "id",id] + | C.AMeta (id,n) -> + X.xml_empty "META" ["no",(string_of_int n) ; "id",id] + | C.ASort (id,s) -> + let string_of_sort = + function + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type -> "Type" + in + X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] + | C.AImplicit _ -> raise NotImplemented + | C.AProd (id,C.Anonimous,s,t) -> + X.xml_nempty "PROD" ["id",id] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] + | C.AProd (xid,C.Name id,s,t) -> + X.xml_nempty "PROD" ["id",xid] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] + | C.ACast (id,v,t) -> + X.xml_nempty "CAST" ["id",id] + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] + | C.ALambda (id,C.Anonimous,s,t) -> + X.xml_nempty "LAMBDA" ["id",id] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" [] (aux t) + >] + | C.ALambda (xid,C.Name id,s,t) -> + X.xml_nempty "LAMBDA" ["id",xid] + [< X.xml_nempty "source" [] (aux s) ; + X.xml_nempty "target" ["binder",id] (aux t) + >] + | C.ALetIn (xid,C.Anonimous,s,t) -> + assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*) + | C.ALetIn (xid,C.Name id,s,t) -> + X.xml_nempty "LETIN" ["id",xid] + [< X.xml_nempty "term" [] (aux s) ; + X.xml_nempty "letintarget" ["binder",id] (aux t) + >] + | C.AAppl (id,li) -> + X.xml_nempty "APPLY" ["id",id] + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) + >] + | C.AConst (id,uri,_) -> + X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id] + | C.AAbst (id,uri) -> raise NotImplemented + | C.AMutInd (id,uri,_,i) -> + X.xml_empty "MUTIND" + ["uri", (U.string_of_uri uri) ; + "noType",(string_of_int i) ; + "id",id] + | C.AMutConstruct (id,uri,_,i,j) -> + X.xml_empty "MUTCONSTRUCT" + ["uri", (U.string_of_uri uri) ; + "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; + "id",id] + | C.AMutCase (id,uri,_,typeno,ty,te,patterns) -> + X.xml_nempty "MUTCASE" + ["uriType",(U.string_of_uri uri) ; + "noType", (string_of_int typeno) ; + "id", id] + [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; + X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; + List.fold_right + (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>]) + patterns [<>] + >] + | C.AFix (id, no, funs) -> + X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id] + [< List.fold_right + (fun (fi,ai,ti,bi) i -> + [< X.xml_nempty "FixFunction" + ["name", fi; "recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + | C.ACoFix (id,no,funs) -> + X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id] + [< List.fold_right + (fun (fi,ti,bi) i -> + [< X.xml_nempty "CofixFunction" ["name", fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + in + aux +;; diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml new file mode 100644 index 000000000..825544afe --- /dev/null +++ b/helm/gTopLevel/cic2acic.ml @@ -0,0 +1,108 @@ +(* 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 NotImplemented;; + +let fresh_id ids_to_terms ids_to_father_ids = + let id = ref 0 in + fun father t -> + let res = "i" ^ string_of_int !id in + incr id ; + Hashtbl.add ids_to_father_ids res father ; + Hashtbl.add ids_to_terms res t ; + res +;; + +exception NotEnoughElements;; +exception NameExpected;; + +(*CSC: cut&paste da cicPp.ml *) +(* get_nth l n returns the nth element of the list l if it exists or *) +(* raises NotEnoughElements if l has less than n elements *) +let rec get_nth l n = + match (n,l) with + (1, he::_) -> he + | (n, he::tail) when n > 1 -> get_nth tail (n-1) + | (_,_) -> raise NotEnoughElements +;; + +let acic_of_cic_env env t = + let module C = Cic in + let ids_to_terms = Hashtbl.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let fresh_id' = fresh_id ids_to_terms ids_to_father_ids in + let rec aux father bs tt = + let fresh_id'' = fresh_id' father tt in + let aux' = aux (Some fresh_id'') in + match tt with + C.Rel n -> + let id = + match get_nth bs n with + C.Name s -> s + | _ -> raise NameExpected + in + C.ARel (fresh_id'', n, id) + | C.Var uri -> C.AVar (fresh_id'', uri) + | C.Meta n -> C.AMeta (fresh_id'', n) + | C.Sort s -> C.ASort (fresh_id'', s) + | C.Implicit -> C.AImplicit (fresh_id'') + | C.Cast (v,t) -> + C.ACast (fresh_id'', aux' bs v, aux' bs t) + | C.Prod (n,s,t) -> + C.AProd (fresh_id'', n, aux' bs s, aux' (n::bs) t) + | C.Lambda (n,s,t) -> + C.ALambda (fresh_id'',n, aux' bs s, aux' (n::bs) t) + | C.LetIn (n,s,t) -> + C.ALetIn (fresh_id'', n, aux' bs s, aux' (n::bs) t) + | C.Appl l -> C.AAppl (fresh_id'', List.map (aux' bs) l) + | C.Const (uri,cn) -> C.AConst (fresh_id'', uri, cn) + | C.Abst _ -> raise NotImplemented + | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno) + | C.MutConstruct (uri,cn,tyno,consno) -> + C.AMutConstruct (fresh_id'', uri, cn, tyno, consno) + | C.MutCase (uri, cn, tyno, outty, term, patterns) -> + C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty, + aux' bs term, List.map (aux' bs) patterns) + | C.Fix (funno, funs) -> + let names = List.map (fun (name,_,_,_) -> C.Name name) funs in + C.AFix (fresh_id'', funno, + List.map + (fun (name, indidx, ty, bo) -> + (name, indidx, aux' bs ty, aux' (names@bs) bo) + ) funs + ) + | C.CoFix (funno, funs) -> + let names = List.map (fun (name,_,_) -> C.Name name) funs in + C.ACoFix (fresh_id'', funno, + List.map + (fun (name, ty, bo) -> + (name, aux' bs ty, aux' (names@bs) bo) + ) funs + ) + in + aux None env t, ids_to_terms, ids_to_father_ids +;; + +let acic_of_cic = acic_of_cic_env [];; diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml new file mode 100644 index 000000000..7c01b4d75 --- /dev/null +++ b/helm/gTopLevel/gTopLevel.ml @@ -0,0 +1,526 @@ +(* 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/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(******************************************************************************) + +(* GLOBAL CONSTANTS *) + +let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; + +let htmlheader = + "" ^ + " " +;; + +let htmlfooter = + " " ^ + "" +;; + +(* GLOBAL REFERENCES (USED BY CALLBACKS) *) + +let htmlheader_and_content = ref htmlheader;; + +let filename4uwobo = "/public/sacerdot/prova.xml";; + +let current_cic_infos = ref None;; + + +(* MISC FUNCTIONS *) + +let domImpl = Gdome.domImplementation ();; + +let parseStyle name = + let style = + domImpl#createDocumentFromURI +(* + ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None +*) + ~uri:("styles/" ^ name) () + in + Gdome_xslt.processStylesheet style +;; + +let d_c = parseStyle "drop_coercions.xsl";; +let tc1 = parseStyle "objtheorycontent.xsl";; +let hc2 = parseStyle "content_to_html.xsl";; +let l = parseStyle "link.xsl";; + +let c1 = parseStyle "rootcontent.xsl";; +let g = parseStyle "genmmlid.xsl";; +let c2 = parseStyle "annotatedpres.xsl";; + +(* +let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";; +let getterURL = "http://phd.cs.unibo.it:8081/";; +*) +let processorURL = "http://localhost:8080/helm/servelt/uwobo/";; +let getterURL = "http://localhost:8081/";; + +let mml_styles = [d_c ; c1 ; g ; c2 ; l];; +let mml_args = + ["processorURL", "'" ^ processorURL ^ "'" ; + "getterURL", "'" ^ getterURL ^ "'" ; + "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; + "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; + "UNICODEvsSYMBOL", "'symbol'" ; + "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; + "encoding", "'iso-8859-1'" ; + "media-type", "'text/html'" ; + "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; + "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; + "naturalLanguage", "'no'" ; + "annotations", "'no'" ; + "topurl", "'http://phd.cs.unibo.it/helm'" ; + "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] +;; + +let sequent_styles = [d_c ; c1 ; g ; c2 ; l];; +let sequent_args = + ["processorURL", "'" ^ processorURL ^ "'" ; + "getterURL", "'" ^ getterURL ^ "'" ; + "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; + "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; + "UNICODEvsSYMBOL", "'symbol'" ; + "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; + "encoding", "'iso-8859-1'" ; + "media-type", "'text/html'" ; + "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; + "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; + "naturalLanguage", "'no'" ; + "annotations", "'no'" ; + "topurl", "'http://phd.cs.unibo.it/helm'" ; + "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] +;; + +let parse_file filename = + let inch = open_in filename in + let rec read_lines () = + try + let line = input_line inch in + line ^ read_lines () + with + End_of_file -> "" + in + read_lines () +;; + +let applyStylesheets input styles args = + List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args) + input styles +;; + +let mml_of_cic acic = +prerr_endline "BBB CREAZIONE" ; + let xml = + Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic + in + Xml.pp ~quiet:true xml (Some filename4uwobo) ; +prerr_endline "BBB PARSING" ; + let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in +prerr_endline "BBB STYLESHEETS" ; + let output = applyStylesheets input mml_styles mml_args in +prerr_endline "BBB RESA" ; +ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ; + output +;; + + +(* CALLBACKS *) + +let exact rendering_window () = + let inputt = (rendering_window#inputt : GEdit.text) in +(*CSC: Gran cut&paste da sotto... *) + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen ^ "\n" in + let lexbuf = Lexing.from_string input in + try + while true do + (* Execute the actions *) + match CicTextualParser.main CicTextualLexer.token lexbuf with + None -> () + | Some expr -> + try +(*??? Ma servira' da qualche parte! + let ty = CicTypeChecker.type_of_aux' [] expr in +*) + let (acic, ids_to_terms, ids_to_father_ids) = + Cic2acic.acic_of_cic expr + in +(*CSC: chiamare la vera tattica exact qui! *) + () + with + e -> + print_endline ("? " ^ CicPp.ppterm expr) ; + raise e + done + with + CicTextualParser0.Eof -> + inputt#delete_text 0 inputlen +(*CSC: fare qualcosa di utile *) + | e -> + print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout +;; + +let proveit rendering_window () = + let module G = Gdome in + match rendering_window#output#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + (*CSC: OCAML DIVERGE + ((element : G.element)#getAttributeNS + *) + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + match !current_cic_infos with + Some (ids_to_terms, ids_to_father_ids) -> + let id = xpath in + let sequent = + LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids + in + SequentPp.TextualPp.print_sequent sequent ; + let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in + let sequent_doc = + Xml2Gdome.document_of_xml domImpl sequent_gdome + in + let sequent_mml = + applyStylesheets sequent_doc sequent_styles sequent_args + in + rendering_window#proofw#load_tree ~dom:sequent_mml ; +ignore(domImpl#saveDocumentToFile ~doc:sequent_doc + ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; +ignore(domImpl#saveDocumentToFile ~doc:sequent_mml + ~name:"/public/sacerdot/guruguru2" ~indent:true ()) + | None -> assert false (* "ERROR: No current term!!!" *) + end + | None -> assert false (* "ERROR: No selection!!!" *) +;; + +let output_html outputhtml msg = + htmlheader_and_content := !htmlheader_and_content ^ msg ; + outputhtml#source (!htmlheader_and_content ^ htmlfooter) +;; + +let execute rendering_window () = + let inputt = (rendering_window#inputt : GEdit.text) in + let oldinputt = (rendering_window#oldinputt : GEdit.text) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let output = (rendering_window#output : GMathView.math_view) in + let proofw = (rendering_window#proofw : GMathView.math_view) in + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen ^ "\n" in + (* Do something interesting *) + let lexbuf = Lexing.from_string input in + try + while true do + (* Execute the actions *) + match CicTextualParser.main CicTextualLexer.token lexbuf with + None -> () + | Some expr -> + try + let ty = CicTypeChecker.type_of_aux' [] expr in + let whd = CicReduction.whd expr in + + let (acic, ids_to_terms, ids_to_father_ids) = + Cic2acic.acic_of_cic expr + in + let mml = mml_of_cic acic in + output#load_tree mml ; +prerr_endline "BBB FINE RESA" ; + current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ; +print_endline ("? " ^ CicPp.ppterm expr) ; +print_endline (">> " ^ CicPp.ppterm whd) ; +print_endline (": " ^ CicPp.ppterm ty) ; +flush stdout ; + with + e -> + print_endline ("? " ^ CicPp.ppterm expr) ; + raise e + done + with + CicTextualParser0.Eof -> + inputt#delete_text 0 inputlen ; + ignore(oldinputt#insert_text input oldinputt#length) ; + | e -> + print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout +;; + +let choose_selection + (mmlwidget : GMathView.math_view) (element : Gdome.element option) += + let module G = Gdome in + let rec aux element = + if element#hasAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref") + then + mmlwidget#set_selection (Some element) + else + match element#get_parentNode with + None -> assert false + (*CSC: OCAML DIVERGES! + | Some p -> aux (new G.element_of_node p) + *) + | Some p -> aux (new Gdome.element_of_node p) + in + match element with + Some x -> aux x + | None -> mmlwidget#set_selection None +;; + +(* STUFF TO BUILD THE GTK INTERFACE *) + +(* Stuff for the widget settings *) + +let export_to_postscript (output : GMathView.math_view) () = + output#export_to_postscript ~filename:"output.ps" (); +;; + +let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing + button_set_kerning button_set_transparency button_export_to_postscript + button_t1 () += + let is_set = button_t1#active in + output#set_font_manager_type + (if is_set then `font_manager_t1 else `font_manager_gtk) ; + if is_set then + begin + button_set_anti_aliasing#misc#set_sensitive true ; + button_set_kerning#misc#set_sensitive true ; + button_set_transparency#misc#set_sensitive true ; + button_export_to_postscript#misc#set_sensitive true ; + end + else + begin + button_set_anti_aliasing#misc#set_sensitive false ; + button_set_kerning#misc#set_sensitive false ; + button_set_transparency#misc#set_sensitive false ; + button_export_to_postscript#misc#set_sensitive false ; + end +;; + +let set_anti_aliasing output button_set_anti_aliasing () = + output#set_anti_aliasing button_set_anti_aliasing#active +;; + +let set_kerning output button_set_kerning () = + output#set_kerning button_set_kerning#active +;; + +let set_transparency output button_set_transparency () = + output#set_transparency button_set_transparency#active +;; + +let changefont output font_size_spinb () = + output#set_font_size font_size_spinb#value_as_int +;; + +let set_log_verbosity output log_verbosity_spinb () = + output#set_log_verbosity log_verbosity_spinb#value_as_int +;; + +class settings_window (output : GMathView.math_view) sw + button_export_to_postscript selection_changed_callback += + let settings_window = GWindow.window ~title:"GtkMathView settings" () in + let vbox = + GPack.vbox ~packing:settings_window#add () in + let table = + GPack.table + ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 + ~border_width:5 ~packing:vbox#add () in + let button_t1 = + GButton.toggle_button ~label:"activate t1 fonts" + ~packing:(table#attach ~left:0 ~top:0) () in + let button_set_anti_aliasing = + GButton.toggle_button ~label:"set_anti_aliasing" + ~packing:(table#attach ~left:0 ~top:1) () in + let button_set_kerning = + GButton.toggle_button ~label:"set_kerning" + ~packing:(table#attach ~left:1 ~top:1) () in + let button_set_transparency = + GButton.toggle_button ~label:"set_transparency" + ~packing:(table#attach ~left:2 ~top:1) () in + let table = + GPack.table + ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 + ~border_width:5 ~packing:vbox#add () in + let font_size_label = + GMisc.label ~text:"font size:" + ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in + let font_size_spinb = + let sadj = + GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () + in + GEdit.spin_button + ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in + let log_verbosity_label = + GMisc.label ~text:"log verbosity:" + ~packing:(table#attach ~left:0 ~top:1) () in + let log_verbosity_spinb = + let sadj = + GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () + in + GEdit.spin_button + ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let closeb = + GButton.button ~label:"Close" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in +object(self) + method show = settings_window#show + initializer + button_set_anti_aliasing#misc#set_sensitive false ; + button_set_kerning#misc#set_sensitive false ; + button_set_transparency#misc#set_sensitive false ; + (* Signals connection *) + ignore(button_t1#connect#clicked + (activate_t1 output button_set_anti_aliasing button_set_kerning + button_set_transparency button_export_to_postscript button_t1)) ; + ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; + ignore(button_set_anti_aliasing#connect#toggled + (set_anti_aliasing output button_set_anti_aliasing)); + ignore(button_set_kerning#connect#toggled + (set_kerning output button_set_kerning)) ; + ignore(button_set_transparency#connect#toggled + (set_transparency output button_set_transparency)) ; + ignore(log_verbosity_spinb#connect#changed + (set_log_verbosity output log_verbosity_spinb)) ; + ignore(closeb#connect#clicked settings_window#misc#hide) +end;; + +(* Main windows *) + +class rendering_window output proofw (label : GMisc.label) = + let window = + GWindow.window ~title:"MathML viewer" ~border_width:2 () in + let hbox0 = + GPack.hbox ~packing:window#add () in + let vbox = + GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in + let scrolled_window0 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~padding:5) () in + let _ = scrolled_window0#add output#coerce in + let hbox1 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let settingsb = + GButton.button ~label:"Settings" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let button_export_to_postscript = + GButton.button ~label:"export_to_postscript" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let closeb = + GButton.button ~label:"Close" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let hbox2 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let proveitb = + GButton.button ~label:"Prove It" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 + ~packing:(vbox#pack ~padding:5) () in + let executeb = + GButton.button ~label:"Execute" + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 + ~packing:(vbox#pack ~padding:5) () in + let vbox1 = + GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window1 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox1#pack ~expand:true ~padding:5) () in + let _ = scrolled_window1#add proofw#coerce in + let hbox3 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let exactb = + GButton.button ~label:"Exact" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let outputhtml = + GHtml.xmhtml + ~source:"" + ~width:400 ~height: 200 + ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) + ~show:true () in +object(self) + method outputhtml = outputhtml + method oldinputt = oldinputt + method inputt = inputt + method output = (output : GMathView.math_view) + method proofw = (proofw : GMathView.math_view) + method show () = window#show () + initializer + button_export_to_postscript#misc#set_sensitive false ; + + (* signal handlers here *) + ignore(output#connect#selection_changed + (function elem -> proofw#unload ; choose_selection output elem)) ; + ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; + let settings_window = new settings_window output scrolled_window0 + button_export_to_postscript (choose_selection output) in + ignore(settingsb#connect#clicked settings_window#show) ; + ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; + ignore(proveitb#connect#clicked (proveit self)) ; + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; + ignore(executeb#connect#clicked (execute self)) ; + ignore(exactb#connect#clicked (exact self)) ; + Logger.log_callback := + (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) +end;; + +(* MAIN *) + +let initialize_everything () = + let module U = Unix in + let output = GMathView.math_view ~width:400 ~height:280 () + and proofw = GMathView.math_view ~width:400 ~height:275 () + and label = GMisc.label ~text:"gTopLevel" () in + let rendering_window = + new rendering_window output proofw label + in + rendering_window#show () ; + GMain.Main.main () +;; + +let _ = + CicCooking.init () ; + initialize_everything () +;; diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml new file mode 100644 index 000000000..664425062 --- /dev/null +++ b/helm/gTopLevel/logicalOperations.ml @@ -0,0 +1,73 @@ +let get_parent id ids_to_terms ids_to_father_ids = + match Hashtbl.find ids_to_father_ids id with + None -> None + | Some id -> Some (id, Hashtbl.find ids_to_terms id) +;; + +let get_context ids_to_terms ids_to_father_ids = + let module P = ProofEngine in + let module C = Cic in + let rec aux id = + match get_parent id ids_to_terms ids_to_father_ids with + None -> [] + | Some (parentid,parent) -> + let term = Hashtbl.find ids_to_terms id in + let binding = + match parent with + C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit + | C.Cast _ -> [] + | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s] + | C.Prod _ -> [] + | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s] + | C.Lambda _ -> [] + | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s] + | C.LetIn _ -> [] + | C.Appl _ + | C.Const _ -> [] + | C.Abst _ -> assert false + | C.MutInd _ + | C.MutConstruct _ + | C.MutCase _ -> [] +(*CSC: sbagliato: manca il when *) + | C.Fix (_,ifl) -> + let counter = ref 0 in + List.rev_map + (function (name,_,ty,bo) -> + let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in + incr counter ; + res + ) ifl + | C.CoFix (_,ifl) -> + let counter = ref 0 in + List.rev_map + (function (name,ty,bo) -> + let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in + incr counter ; + res + ) ifl + in + binding@(aux parentid) + in + aux +;; + +exception NotImplemented;; + +let to_sequent id ids_to_terms ids_to_father_ids = + let module P = ProofEngine in + let term = Hashtbl.find ids_to_terms id in + let context = get_context ids_to_terms ids_to_father_ids id in + let type_checker_env_of_context = + List.map + (function + P.Declaration,_,t -> t + | P.Definition,_,_ -> raise NotImplemented + ) context + in + let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in + ((context,ty) : ProofEngine.sequent) +;; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml new file mode 100644 index 000000000..fc0df2d02 --- /dev/null +++ b/helm/gTopLevel/proofEngine.ml @@ -0,0 +1,8 @@ +type binder_type = + Declaration + | Definition +;; + +type context = (binder_type * Cic.name * Cic.term) list;; + +type sequent = context * Cic.term;; diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml new file mode 100644 index 000000000..8fbb78b2a --- /dev/null +++ b/helm/gTopLevel/sequentPp.ml @@ -0,0 +1,68 @@ +module TextualPp = + struct + (* It also returns the pretty-printing context! *) + let print_context ctx = + let module P = ProofEngine in + let print_name = + function + Cic.Name n -> n + | Cic.Anonimous -> "_" + in + List.fold_right + (fun i env -> + match i with + (P.Declaration,n,t) -> + print_endline (print_name n ^ ":" ^ CicPp.pp t env) ; + flush stdout ; + n::env + | (P.Definition,n,t) -> + print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ; + flush stdout ; + n::env + ) ctx [] + ;; + + exception NotImplemented;; + + let print_sequent (context,goal) = + let module P = ProofEngine in + print_newline () ; + let pretty_printer_env_of_context = + print_context context + in + print_endline "----------------------" ; + print_endline (CicPp.pp goal pretty_printer_env_of_context) ; flush stdout + ;; + end +;; + +module XmlPp = + struct + let print_sequent (context,goal) = + let module X = Xml in + X.xml_nempty "Sequent" [] + (let final_s,final_env = + (List.fold_right + (fun (b,n,t) (s,env) -> + [< s ; + X.xml_nempty + (match b with + ProofEngine.Definition -> "Definition" + | ProofEngine.Declaration -> "Declaration" + ) ["name",(match n with Cic.Name n -> n | _ -> assert false)] + (Cic2Xml.print_term + (UriManager.uri_of_string "cic:/dummy.con") + (let (acic,_,_) = Cic2acic.acic_of_cic_env env t in acic)) ; + >],(n::env) + ) context ([<>],[]) + ) + in + [< final_s ; + Xml.xml_nempty "Goal" [] + (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") + (let (acic,_,_) = Cic2acic.acic_of_cic_env final_env goal in acic)) + >] + ) + ;; + end +;; diff --git a/helm/gTopLevel/xml2Gdome.ml b/helm/gTopLevel/xml2Gdome.ml new file mode 100644 index 000000000..43a2fc7dd --- /dev/null +++ b/helm/gTopLevel/xml2Gdome.ml @@ -0,0 +1,47 @@ +let document_of_xml (domImplementation : Gdome.domImplementation) strm = + let module G = Gdome in + let module X = Xml in + let root_name,root_attributes,root_content = + match Stream.next strm with + X.Empty(n,l) -> n,l,[<>] + | X.NEmpty(n,l,c) -> n,l,c + | _ -> assert false + in + let document = +(*CSC: erroraccio bruttissimo in gmetadom!!! *) + new Gdome.document ( + domImplementation#createDocument ~namespaceURI:None + ~qualifiedName:(Gdome.domString root_name) ~doctype:None + ) + in + let rec aux (node : Gdome.node) = + parser + [< 'X.Str a ; s >] -> + let textnode = document#createTextNode ~data:(Gdome.domString a) in + ignore (node#appendChild ~newChild:(textnode :> Gdome.node)) ; + aux node s + | [< 'X.Empty(n,l) ; s >] -> + let element = document#createElement ~tagName:(Gdome.domString n) in + List.iter (function (n,v) -> element#setAttribute + ~name:(Gdome.domString n) ~value:(Gdome.domString v)) l ; + ignore + (node#appendChild ~newChild:(element : Gdome.element :> Gdome.node)) ; + aux node s + | [< 'X.NEmpty(n,l,c) ; s >] -> + let element = document#createElement ~tagName:(Gdome.domString n) in + List.iter + (function (n,v) -> + element#setAttribute ~name:(Gdome.domString n) + ~value:(Gdome.domString v) + ) l ; + ignore (node#appendChild ~newChild:(element :> Gdome.node)) ; + aux (element :> Gdome.node) c ; + aux node s + | [< >] -> () + in + let root = document#get_documentElement in + List.iter (function (n,v) -> root#setAttribute + ~name:(Gdome.domString n) ~value:(Gdome.domString v)) root_attributes ; + aux (root : Gdome.element :> Gdome.node) root_content ; + document +;; -- 2.39.2