From 4f3b04e9966484011328d5b0eb358da4416e29b0 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 21 Sep 2011 14:56:17 +0000 Subject: [PATCH] 1) removed many debug prints 2) solved a bug in automation (we had forgotten to saturate clauses in forward_infer_step, a mistake that prevented equations from being indexed, resulting in almost certain failure of automation). 3) disabled alpha_eq in NCicBlob.compare, because it now requires a status containing the correct environment, which can't be guessed inside compare (enabling alpha_eq results in the automation sporadically failing). --- .../content_pres/termContentPres.ml | 2 +- matitaB/components/ng_library/nCicLibrary.ml | 9 ++-- .../components/ng_paramodulation/nCicBlob.ml | 18 ++++---- .../ng_paramodulation/nCicParamod.ml | 11 +++-- .../ng_paramodulation/nCicParamod.mli | 1 + .../components/ng_paramodulation/paramod.ml | 3 ++ .../components/ng_paramodulation/paramod.mli | 1 + matitaB/components/ng_paramodulation/stats.ml | 2 +- .../ng_paramodulation/superposition.ml | 27 +++++------ matitaB/components/ng_paramodulation/terms.ml | 2 +- .../components/ng_paramodulation/terms.mli | 2 +- matitaB/components/ng_tactics/nTacStatus.ml | 2 + matitaB/matita/index.html | 2 + matitaB/matita/matitadaemon.ml | 46 ++++++++++++++++++- matitaB/matita/matitaweb.css | 6 +-- matitaB/matita/matitaweb.js | 21 +++++++++ matitaB/matita/netplex.conf | 7 +++ 17 files changed, 125 insertions(+), 37 deletions(-) diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index d724acf85..13c70be47 100644 --- a/matitaB/components/content_pres/termContentPres.ml +++ b/matitaB/components/content_pres/termContentPres.ml @@ -474,7 +474,7 @@ let rec pp_ast1 status term = | NotationEnv.DisambiguationValue _ as v -> v in let ast_env_of_env env = - prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env); + (* prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env); *) List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in (* prerr_endline ("### pattern matching from 2 to 1 on term " ^ diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml index 47a62c048..201b5ac08 100644 --- a/matitaB/components/ng_library/nCicLibrary.ml +++ b/matitaB/components/ng_library/nCicLibrary.ml @@ -56,7 +56,7 @@ let ng_path_of_baseuri ?(no_suffix=false) user baseuri = let path = String.sub uri 4 (String.length uri - 4) in let path = match user with | Some u -> "/" ^ u ^ path - | _ -> path + | _ -> prerr_endline "WARNING: ng_path_of_baseuri called without a uid"; path in let path = Helm_registry.get "matita.basedir" ^ path in let dirname = Filename.dirname path in @@ -361,7 +361,9 @@ let resolve st name = (fun (_,name',nref) -> if name'=name then Some nref else None) (!(st#lib_db.local_aliases) @ get_global_aliases ()) with - Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) + Not_found -> + (prerr_endline ("can't resolve object " ^ name); + raise (NCicEnvironment.ObjectNotFound (lazy name))) ;; let aliases_of st uri = @@ -428,7 +430,8 @@ let get_obj status u = with Not_found ->*) try fetch_obj (status#user) status u with Sys_error _ -> - raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u))) + (prerr_endline ("can't fetch object " ^ NUri.string_of_uri u); + raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))) ;; NCicEnvironment.set_get_obj diff --git a/matitaB/components/ng_paramodulation/nCicBlob.ml b/matitaB/components/ng_paramodulation/nCicBlob.ml index beef0ae45..14454c58b 100644 --- a/matitaB/components/ng_paramodulation/nCicBlob.ml +++ b/matitaB/components/ng_paramodulation/nCicBlob.ml @@ -11,15 +11,15 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) -let eqPref = ref (fun _ -> assert false);; -let set_eqP t = eqPref := fun _ -> t;; - -let default_eqP() = +let default_eqP = let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in NCic.Const ref ;; +let eqPref = ref default_eqP;; +let set_eqP t = eqPref := t;; + let equivalence_relation = let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con" in @@ -84,20 +84,22 @@ with type t = NCic.term and type input = NCic.term = struct ;; - let compare x y = + (* let compare x y = (* CSC: NCicPp.status is the best I can put here *) (* WR: and I can't guess a user id, so I must put None *) if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y then 0 (* if x = y then 0 *) else compare x y - ;; + ;; *) - let eqP = (!eqPref)() + let eqP = fun () -> !eqPref ;; let is_eq = function - | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt -> + | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq (eqP()) eqt -> Some (ty,l,r) + | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] -> + None (* | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r] when eq equivalence_relation eqt && eq setoid_eq eqt2 -> diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml index 0f92c6620..5906bc06d 100644 --- a/matitaB/components/ng_paramodulation/nCicParamod.ml +++ b/matitaB/components/ng_paramodulation/nCicParamod.ml @@ -92,14 +92,17 @@ module P = NCicParamod type state = P.state let empty_state = P.empty_state +let size_of_state = P.size_of_state + let forward_infer_step status metasenv subst context s t ty = let bag = P.bag_of_state s in let saturate (t,ty) = NCicBlob.saturate status metasenv subst context t ty in - let bag,clause = P.mk_passive bag (t,ty) in + let bag,clause = P.mk_passive bag (saturate (t,ty)) in if Terms.is_eq_clause clause then - P.forward_infer_step (P.replace_bag s bag) clause 0 - else (debug (lazy "not eq"); s) + ((*prerr_endline "is eq";*) + P.forward_infer_step (P.replace_bag s bag) clause 0) + else ((*print (lazy "not eq");*) s) ;; let index_obj status s uri = @@ -152,7 +155,7 @@ let is_equation status metasenv subst context ty = NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0 in match hty with - | NCic.Appl (eq ::tl) when eq = CB.eqP -> true + | NCic.Appl (eq ::tl) when eq = CB.eqP() -> true | _ -> false ;; diff --git a/matitaB/components/ng_paramodulation/nCicParamod.mli b/matitaB/components/ng_paramodulation/nCicParamod.mli index b46d0ade0..93d322dd1 100644 --- a/matitaB/components/ng_paramodulation/nCicParamod.mli +++ b/matitaB/components/ng_paramodulation/nCicParamod.mli @@ -19,6 +19,7 @@ val nparamod : type state val empty_state: state +val size_of_state: state -> int * int val forward_infer_step: #NCicCoercion.status -> NCic.metasenv -> diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml index 33f802f7f..83845673b 100644 --- a/matitaB/components/ng_paramodulation/paramod.ml +++ b/matitaB/components/ng_paramodulation/paramod.ml @@ -30,6 +30,7 @@ module type Paramod = type bag = t Terms.bag * int type state val empty_state : state + val size_of_state : state -> int*int val bag_of_state : state -> bag val replace_bag: state -> bag -> state val mk_passive : bag -> input * input -> bag * t Terms.unit_clause @@ -336,6 +337,8 @@ module Paramod (B : Orderings.Blob) = struct add_passive_goals g_passives new_goals ;; + let size_of_state (_,_,(a,_),p,_,_) = List.length a, passive_set_cardinal p;; + let debug_status (_,_,actives,passives,g_actives,g_passives) = lazy ((Printf.sprintf "Number of active goals : %d\n" diff --git a/matitaB/components/ng_paramodulation/paramod.mli b/matitaB/components/ng_paramodulation/paramod.mli index 60691a57c..d91ba1b34 100644 --- a/matitaB/components/ng_paramodulation/paramod.mli +++ b/matitaB/components/ng_paramodulation/paramod.mli @@ -24,6 +24,7 @@ module type Paramod = | Timeout of int * t Terms.bag type bag = t Terms.bag * int val empty_state : state + val size_of_state : state -> int * int val bag_of_state :state -> bag val replace_bag : state -> bag -> state (* we suppose input has been already saturated *) diff --git a/matitaB/components/ng_paramodulation/stats.ml b/matitaB/components/ng_paramodulation/stats.ml index fd68f0fe7..29db6c902 100644 --- a/matitaB/components/ng_paramodulation/stats.ml +++ b/matitaB/components/ng_paramodulation/stats.ml @@ -73,7 +73,7 @@ module Stats (B : Terms.Blob) = in aux [] (match goal with - | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] + | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] | _,Terms.Predicate p,_,_ -> p) ;; diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml index 42cf063b6..1152571ce 100644 --- a/matitaB/components/ng_paramodulation/superposition.ml +++ b/matitaB/components/ng_paramodulation/superposition.ml @@ -27,7 +27,8 @@ module Superposition (B : Orderings.Blob) = * B.t Terms.substitution let print s = prerr_endline (Lazy.force s);; - let debug _ = ();; + let debug _ = ();; + (* let debug = print;; *) let enable = true;; let rec list_first f = function @@ -140,7 +141,7 @@ module Superposition (B : Orderings.Blob) = if filter subst then let literal = match t with - | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> + | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq (B.eqP()) eq -> let o = Order.compare_terms l r in Terms.Equation (l, r, ty, o) | t -> Terms.Predicate t @@ -281,12 +282,12 @@ module Superposition (B : Orderings.Blob) = | Terms.Equation (l,r,ty,_) -> let bag,l,id1 = visit bag [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) id l (ctx_demod table vl) in let bag,_,id2 = visit bag [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) id1 r (ctx_demod table vl) in let cl,_,_ = Terms.get_from_bag id2 bag in @@ -310,7 +311,7 @@ module Superposition (B : Orderings.Blob) = match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,ty,_) -> - Terms.Node [Terms.Leaf B.eqP; ty; l ; r] + Terms.Node [Terms.Leaf (B.eqP()); ty; l ; r] in try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true with FoUnif.UnificationFailure _ -> false @@ -379,11 +380,11 @@ module Superposition (B : Orderings.Blob) = let reverse = (dir = Terms.Left2Right) = b in let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right else r,l, Terms.Right2Left in - (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl) + (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl) in let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in - let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in + let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in let locked_vars = if unify then [] else vl in let rec aux = function | [] -> None @@ -403,7 +404,7 @@ module Superposition (B : Orderings.Blob) = match rewrite_eq ~unify l r ty vl table with | None -> None | Some (id2, dir, subst) -> - let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in + let id_t = Terms.Node [ Terms.Leaf (B.eqP()); ty; r; r ] in build_new_clause bag maxvar (fun _ -> true) Terms.Superposition id_t subst id id2 [2] dir ;; @@ -437,7 +438,7 @@ module Superposition (B : Orderings.Blob) = let newsubst = Subst.concat subst1 subst in let id_t = FoSubst.apply_subst newsubst - (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) + (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r]) in (match build_new_clause_reloc bag maxvar (fun _ -> true) @@ -714,14 +715,14 @@ module Superposition (B : Orderings.Blob) = fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) r (superposition table vl)) | Terms.Equation (l,r,ty,Terms.Invertible) | Terms.Equation (l,r,ty,Terms.Gt) -> fold_build_new_clause bag maxvar id Terms.Superposition (fun _ -> true) (all_positions [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) l (superposition table vl)) | Terms.Equation (l,r,ty,Terms.Incomparable) -> let filtering avoid subst = (* Riazanov: p.33 condition (iv) *) @@ -734,14 +735,14 @@ module Superposition (B : Orderings.Blob) = fold_build_new_clause bag maxvar id Terms.Superposition (filtering Terms.Gt) (all_positions [3] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) r (superposition table vl)) in let bag, maxvar, l_terms = fold_build_new_clause bag maxvar id Terms.Superposition (filtering Terms.Lt) (all_positions [2] - (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) + (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) l (superposition table vl)) in bag, maxvar, r_terms @ l_terms diff --git a/matitaB/components/ng_paramodulation/terms.ml b/matitaB/components/ng_paramodulation/terms.ml index e0fcad181..6ad494965 100644 --- a/matitaB/components/ng_paramodulation/terms.ml +++ b/matitaB/components/ng_paramodulation/terms.ml @@ -95,7 +95,7 @@ module type Blob = type t val eq : t -> t -> bool val compare : t -> t -> int - val eqP : t + val eqP : unit -> t val is_eq: t foterm -> (t foterm* t foterm *t foterm) option val pp : t -> string type input diff --git a/matitaB/components/ng_paramodulation/terms.mli b/matitaB/components/ng_paramodulation/terms.mli index 020eefecd..d84f37b02 100644 --- a/matitaB/components/ng_paramodulation/terms.mli +++ b/matitaB/components/ng_paramodulation/terms.mli @@ -83,7 +83,7 @@ module type Blob = type t val eq : t -> t -> bool val compare : t -> t -> int - val eqP : t + val eqP : unit -> t (* TODO: consider taking in input an imperative buffer for Format * val pp : Format.formatter -> t -> unit * *) diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml index 3684c051f..3a07acc05 100644 --- a/matitaB/components/ng_tactics/nTacStatus.ml +++ b/matitaB/components/ng_tactics/nTacStatus.ml @@ -500,6 +500,8 @@ type 'status tactic = #tac_status as 'status -> 'status let pp_tac_status (status: #tac_status) = prerr_endline (status#ppobj status#obj); + (* let a,p = NCicParamod.size_of_state status#eq_cache in + prerr_endline ("number of actives: " ^ string_of_int a ^ "and number of passives: " ^ string_of_int p) *) prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack) ;; diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 14027f7f2..c7be10ff1 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -24,6 +24,8 @@ Retract + Top Play diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 06b465b13..e9e03b0b2 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -107,12 +107,11 @@ let output_status s = "" ^ markup ^ txt0 ^ "" ^ acc in - let res = "" ^ + "" ^ (Stack.fold ~env:(render_sequent true) ~cont:(render_sequent false) ~todo:(render_sequent false) "" s#stack) ^ "" - in (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; @@ -508,6 +507,41 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#commit_work() ;; +let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + prerr_endline "executing goto Top"; + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + (* + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + *) + let status = MatitaAuthentication.get_status sid in + let uid = MatitaAuthentication.user_of_session sid in + let baseuri = status#baseuri in + let new_status = new MatitaEngine.status (Some uid) baseuri in + NCicLibrary.time_travel new_status; + let new_history = [new_status] in + MatitaAuthentication.set_history sid new_history; + MatitaAuthentication.set_status sid new_status; + NCicLibrary.time_travel new_status; + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string "ok" + with _ -> + (cgi#set_header ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" (); + cgi#out_channel#output_string "ok"); + cgi#out_channel#commit_work()) +;; + let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in @@ -644,6 +678,13 @@ let start() = dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in + let goto_top = + { Nethttpd_services.dyn_handler = (fun _ -> gotoTop); + dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; + dyn_uri = None; (* not needed *) + dyn_translator = (fun _ -> ""); (* not needed *) + dyn_accept_all_conditionals = false; + } in let retrieve = { Nethttpd_services.dyn_handler = (fun _ -> retrieve); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; @@ -706,6 +747,7 @@ let start() = ~handlers:[ "advance", do_advance ; "retract", do_retract ; "bottom", goto_bottom + ; "top", goto_top ; "open", retrieve ; "register", do_register ; "login", do_login diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css index b75aaf301..aed752a8e 100644 --- a/matitaB/matita/matitaweb.css +++ b/matitaB/matita/matitaweb.css @@ -112,7 +112,7 @@ div.navibar { margin-left: auto; margin-right: auto; height:100%; - width:33%; + width:370px; float:left; } @@ -121,7 +121,7 @@ div.toolbar { margin-left: auto; margin-right: auto; height:100%; - width:33%; + width:300px; float:left; } @@ -130,7 +130,7 @@ div.caption { margin-left: auto; margin-right: auto; height:100%; - width:34%; + width:220px; text-align: center; float:right; } diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 837c687cb..d9bd38aa8 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -535,6 +535,27 @@ function gotoBottom() } +function gotoTop() +{ + processor = function(xml) { + if (is_defined(xml)) { + if (xml.childNodes[0].textContent != "ok") { + debug("goto top failed"); + } + else + unlocked.innerHTML = locked.innerHTML + unlocked.innerHTML + locked.innerHTML = "" + hideSequent(); + unlocked.scrollIntoView(true); + } else { + debug("goto top failed"); + } + resume(); + }; + pause(); + callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); + +} function gotoPos(offset) { if (!is_defined(offset)) { diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf index 10e9c55dc..858ea6e8e 100644 --- a/matitaB/matita/netplex.conf +++ b/matitaB/matita/netplex.conf @@ -60,6 +60,13 @@ netplex { handler = "bottom"; } }; + uri { + path = "/top"; + service { + type = "dynamic"; + handler = "top"; + } + }; uri { path = "/register"; service { -- 2.39.2