X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=4a730283208354abffc7529ac3822640747923f0;hb=373eaf73bebec626e031a4a534ddfdd4f1c1b474;hp=83d959ca38f77f4ed8b76ca31a24611a50971eba;hpb=86122a3ce11bdf45ecb93f8f7efaffa49bd31fa2;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 83d959ca3..4a7302832 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -61,13 +61,21 @@ let htmlfooter = (* let prooffile = "/home/tassi/miohelm/tmp/currentproof";; -*) let prooffile = "/public/sacerdot/currentproof";; +*) + +let prooffile = "/home/galata/miohelm/currentproof";; +let prooffiletype = "/home/galata/miohelm/currentprooftype";; + (*CSC: the getter should handle the innertypes, not the FS *) (* let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; -*) let innertypesfile = "/public/sacerdot/innertypes";; +*) + +let innertypesfile = "/home/galata/miohelm/innertypes";; +let constanttypefile = "/home/galata/miohelm/constanttype";; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -91,6 +99,38 @@ Arg.parse argspec ignore "" (* MISC FUNCTIONS *) +let cic_textual_parser_uri_of_uri uri' = + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then + CicTextualParser0.ConUri (UriManager.uri_of_string uri') + else + if String.sub uri' (String.length uri' - 4) 4 = ".var" then + CicTextualParser0.VarUri (UriManager.uri_of_string uri') + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in + CicTextualParser0.IndTyUri (uri'',typeno) + with + _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in + CicTextualParser0.IndConUri (uri'',typeno,consno) + ) +;; + +let term_of_uri uri = + let module C = Cic in + let module CTP = CicTextualParser0 in + match (cic_textual_parser_uri_of_uri uri) with + CTP.ConUri uri -> C.Const (uri,[]) + | CTP.VarUri uri -> C.Var (uri,[]) + | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) + | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) +;; + let domImpl = Gdome.domImplementation ();; let parseStyle name = @@ -173,14 +213,21 @@ let applyStylesheets input styles args = ;; let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = - let xml = +(*CSC: ????????????????? *) + let xml, bodyxml = Cic2Xml.print_object uri ~ids_to_inner_sorts annobj in let xmlinnertypes = Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types in - let input = Xml2Gdome.document_of_xml domImpl xml in + let input = + match bodyxml with + None -> Xml2Gdome.document_of_xml domImpl xml + | Some bodyxml' -> + Xml.pp xml (Some constanttypefile) ; + Xml2Gdome.document_of_xml domImpl bodyxml' + in (*CSC: We save the innertypes to disk so that we can retrieve them in the *) (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) (*CSC: local. *) @@ -201,7 +248,8 @@ let refresh_proof (output : GMathView.math_view) = match !ProofEngine.proof with None -> assert false | Some (uri,metasenv,bo,ty) -> - uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty)) + (*CSC: Wrong: [] is just plainly wrong *) + 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, @@ -220,7 +268,7 @@ let refresh_proof (output : GMathView.math_view) = match !ProofEngine.proof with None -> assert false | Some (uri,metasenv,bo,ty) -> -prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ; +prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ; raise (RefreshProofException e) ;; @@ -665,8 +713,8 @@ let exact rendering_window = let apply rendering_window = call_tactic_with_input ProofEngine.apply rendering_window ;; -let elimintrossimpl rendering_window = - call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window +let elimsimplintros rendering_window = + call_tactic_with_input ProofEngine.elim_simpl_intros rendering_window ;; let elimtype rendering_window = call_tactic_with_input ProofEngine.elim_type rendering_window @@ -705,7 +753,29 @@ let fourier rendering_window = let rewritesimpl rendering_window = call_tactic_with_input ProofEngine.rewrite_simpl rendering_window ;; - +let reflexivity rendering_window = + call_tactic ProofEngine.reflexivity rendering_window +;; +let symmetry rendering_window = + call_tactic ProofEngine.symmetry rendering_window +;; +let transitivity rendering_window = + call_tactic_with_input ProofEngine.transitivity rendering_window +;; +let left rendering_window = + call_tactic ProofEngine.left rendering_window +;; +let right rendering_window = + call_tactic ProofEngine.right rendering_window +;; +let assumption rendering_window = + call_tactic ProofEngine.assumption rendering_window +;; +(* +let prova_tatticali rendering_window = + call_tactic ProofEngine.prova_tatticali rendering_window +;; +*) let whd_in_scratch scratch_window = @@ -740,7 +810,7 @@ let qed rendering_window () = then begin (*CSC: Wrong: [] is just plainly wrong *) - let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in + let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) @@ -763,8 +833,9 @@ let qed rendering_window () = (*???? let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; -*) let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; +*) +let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";; let save rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -772,41 +843,49 @@ let save rendering_window () = None -> assert false | Some (uri, metasenv, bo, ty) -> let currentproof = - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty) + (*CSC: Wrong: [] is just plainly wrong *) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[]) in 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 - let xml' = - [< Xml.xml_cdata "\n" ; - Xml.xml_cdata - ("\n\n") ; - xml - >] - in - Xml.pp ~quiet:true xml' (Some prooffile) ; - output_html outputhtml - ("

Current proof saved to " ^ - prooffile ^ "

") + let xml, bodyxml = + match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with + xml,Some bodyxml -> xml,bodyxml + | _,None -> assert false + in + Xml.pp ~quiet:true xml (Some prooffiletype) ; + output_html outputhtml + ("

Current proof type saved to " ^ + prooffiletype ^ "

") ; + Xml.pp ~quiet:true bodyxml (Some prooffile) ; + output_html outputhtml + ("

Current proof body saved to " ^ + prooffile ^ "

") ;; (* Used to typecheck the loaded proofs *) let typecheck_loaded_proof metasenv bo ty = let module T = CicTypeChecker in - (*CSC: bisogna controllare anche il metasenv!!! *) + ignore ( + List.fold_left + (fun metasenv ((_,context,ty) as conj) -> + ignore (T.type_of_aux' metasenv context ty) ; + metasenv @ [conj] + ) [] metasenv) ; ignore (T.type_of_aux' metasenv [] ty) ; ignore (T.type_of_aux' metasenv [] bo) ;; +(*CSC: ancora da implementare *) let load rendering_window () = 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 try let uri = UriManager.uri_of_string "cic:/dummy.con" in - match CicParser.obj_of_xml prooffile uri with - Cic.CurrentProof (_,metasenv,bo,ty) -> + match CicParser.obj_of_xml prooffiletype (Some prooffile) with + Cic.CurrentProof (_,metasenv,bo,ty,_) -> typecheck_loaded_proof metasenv bo ty ; ProofEngine.proof := Some (uri, metasenv, bo, ty) ; @@ -818,7 +897,10 @@ let load rendering_window () = refresh_proof output ; refresh_sequent proofw ; output_html outputhtml - ("

Current proof loaded from " ^ + ("

Current proof type loaded from " ^ + prooffiletype ^ "

") ; + output_html outputhtml + ("

Current proof body loaded from " ^ prooffile ^ "

") | _ -> assert false with @@ -977,15 +1059,15 @@ let open_ rendering_window () = 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 + let input = inputt#get_chars 0 inputlen in try let uri = UriManager.uri_of_string ("cic:" ^ input) in CicTypeChecker.typecheck uri ; let metasenv,bo,ty = - match CicEnvironment.get_cooked_obj uri 0 with - Cic.Definition (_,bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty - | Cic.Axiom _ + match CicEnvironment.get_cooked_obj uri with + Cic.Constant (_,Some bo,ty,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty + | Cic.Constant _ | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in @@ -1080,7 +1162,6 @@ let check rendering_window scratch_window () = | None -> None ) context in - (* Do something interesting *) let lexbuf = Lexing.from_string input in try while true do @@ -1094,6 +1175,7 @@ let check rendering_window scratch_window () = try let ty = CicTypeChecker.type_of_aux' metasenv' context expr in let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in +prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; scratch_window#show () ; scratch_window#mmlwidget#load_tree ~dom:mml with @@ -1159,7 +1241,7 @@ let locate rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ;; -let backward rendering_window () = +let searchPattern rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let inputt = (rendering_window#inputt : GEdit.text) in let inputlen = inputt#length in @@ -1175,7 +1257,7 @@ let backward rendering_window () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let result = MQueryGenerator.backward metasenv ey ty level in + let result = MQueryGenerator.searchPattern metasenv ey ty level in let uris = List.map (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) @@ -1183,12 +1265,44 @@ let backward rendering_window () = let html = "

Backward Query:

" ^ "

Levels:

" ^ - MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ - " 
" ^ get_last_query result ^ "
" in + MQueryGenerator.string_of_levels + (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ + " 
" ^ get_last_query result ^ "
" + in output_html outputhtml html ; - let uri' = user_uri_choice uris in - inputt#delete_text 0 inputlen ; - ignore ((inputt#insert_text uri') ~pos:0) + let uris',exc = + let rec filter_out = + function + [] -> [],"" + | uri::tl -> + let tl',exc = filter_out tl in + try + if ProofEngine.can_apply (term_of_uri uri) then + uri::tl',exc + else + tl',exc + with + e -> + let exc' = + "

^ Exception raised trying to apply " ^ + uri ^ ": " ^ Printexc.to_string e ^ "

" ^ exc + in + tl',exc' + in + filter_out uris + in + let html' = + "

Objects that can actually be applied:

" ^ + String.concat "
" uris' ^ exc ^ + "

Number of false matches: " ^ + string_of_int (List.length uris - List.length uris') ^ "

" ^ + "

Number of good matches: " ^ + string_of_int (List.length uris') ^ "

" + in + output_html outputhtml html' ; + let uri' = user_uri_choice uris' in + inputt#delete_text 0 inputlen ; + ignore ((inputt#insert_text uri') ~pos:0) with e -> output_html outputhtml @@ -1440,8 +1554,8 @@ class rendering_window output proofw (label : GMisc.label) = let locateb = GButton.button ~label:"Locate" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let backwardb = - GButton.button ~label:"Backward" + let searchpatternb = + GButton.button ~label:"SearchPattern" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 ~packing:(vbox#pack ~padding:5) () in @@ -1462,8 +1576,8 @@ class rendering_window output proofw (label : GMisc.label) = let applyb = GButton.button ~label:"Apply" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimintrossimplb = - GButton.button ~label:"ElimIntrosSimpl" + let elimsimplintrosb = + GButton.button ~label:"ElimSimplIntros" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let elimtypeb = GButton.button ~label:"ElimType" @@ -1506,6 +1620,27 @@ class rendering_window output proofw (label : GMisc.label) = let rewritesimplb = GButton.button ~label:"RewriteSimpl ->" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let reflexivityb = + GButton.button ~label:"Reflexivity" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let symmetryb = + GButton.button ~label:"Symmetry" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let transitivityb = + GButton.button ~label:"Transitivity" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let leftb = + GButton.button ~label:"Left" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rightb = + GButton.button ~label:"Right" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let assumptionb = + GButton.button ~label:"Assumption" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let prova_tatticalib = + GButton.button ~label:"Prova_tatticali" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -1544,10 +1679,10 @@ object(self) ignore(openb#connect#clicked (open_ self)) ; ignore(checkb#connect#clicked (check self scratch_window)) ; ignore(locateb#connect#clicked (locate self)) ; - ignore(backwardb#connect#clicked (backward self)) ; + ignore(searchpatternb#connect#clicked (searchPattern self)) ; ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; - ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ; + ignore(elimsimplintrosb#connect#clicked (elimsimplintros self)) ; ignore(elimtypeb#connect#clicked (elimtype self)) ; ignore(whdb#connect#clicked (whd self)) ; ignore(reduceb#connect#clicked (reduce self)) ; @@ -1561,6 +1696,15 @@ object(self) ignore(clearb#connect#clicked (clear self)) ; ignore(fourierb#connect#clicked (fourier self)) ; ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; + ignore(reflexivityb#connect#clicked (reflexivity self)) ; + ignore(symmetryb#connect#clicked (symmetry self)) ; + ignore(transitivityb#connect#clicked (transitivity self)) ; + ignore(leftb#connect#clicked (left self)) ; + ignore(rightb#connect#clicked (right self)) ; + ignore(assumptionb#connect#clicked (assumption self)) ; +(* + ignore(prova_tatticalib#connect#clicked (prova_tatticali self)) ; +*) ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) @@ -1584,18 +1728,23 @@ let initialize_everything () = ;; let _ = - CicCooking.init () ; if !usedb then begin - Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; +(* + Mqint.init "dbname=helm" ; +*) + Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; CicTextualParser0.set_locate_object (function id -> let result = MQueryGenerator.locate id in let uris = List.map - (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) - result in - let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in + (function uri,_ -> + wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + let html = + ("

Locate Query: 

" ^ get_last_query result ^ "
") + in begin match !rendering_window with None -> assert false @@ -1624,26 +1773,7 @@ let _ = None in match uri with - Some uri' -> - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then -(*CSC: what cooking number? Here I always use 0, which may be bugged *) - Some (Cic.Const (UriManager.uri_of_string uri',0)) - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in -(*CSC: what cooking number? Here I always use 0, which may be bugged *) - Some (Cic.MutInd (uri'',0,typeno)) - with - _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in -(*CSC: what cooking number? Here I always use 0, which may be bugged *) - Some (Cic.MutConstruct (uri'',0,typeno,consno)) - ) + Some uri' -> Some (cic_textual_parser_uri_of_uri uri') | None -> None ) end ;