From 57e3de08d963ff08d671c639c0e9990368b86f20 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 May 2007 11:03:51 +0000 Subject: [PATCH] added pruning option in autogui --- helm/software/components/tactics/auto.ml | 21 ++++++- helm/software/components/tactics/auto.mli | 3 + helm/software/components/tactics/tactics.mli | 2 +- helm/software/matita/Makefile | 12 +++- helm/software/matita/matitaAutoGui.ml | 14 ++++- helm/software/matita/matitaScript.ml | 63 ++++++++++++-------- 6 files changed, 83 insertions(+), 32 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index d24c244a7..4cd6bf62f 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -831,9 +831,13 @@ let pause b = in_pause := b;; let cond = Condition.create ();; let mutex = Mutex.create ();; let hint = ref None;; +let prune_hint = ref [];; let step _ = Condition.signal cond;; let give_hint n = hint := Some n;; +let give_prune_hint hint = + prune_hint := hint :: !prune_hint +;; let check_pause _ = if !in_pause then @@ -1240,7 +1244,18 @@ let prunable menv subst ty todo = aux todo ;; - +let condition_for_prune_hint prune (m, s, size, don, todo, fl) = + let s = + HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo + in + List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s +;; +let filter_prune_hint l = + let prune = !prune_hint in + prune_hint := []; (* possible race... *) + if prune = [] then l + else List.filter (condition_for_prune_hint prune) l +;; let auto_main tables maxm context flags universe cache elems = auto_context := context; let rec aux tables maxm flags cache (elems : status) = @@ -1249,8 +1264,9 @@ let auto_main tables maxm context flags universe cache elems = auto_status := elems; check_pause (); *) + let elems = filter_prune_hint elems in match elems with - | (m, s, size, don, todo, fl)::orlist as status when !hint <> None -> + | (m, s, size, don, todo, fl)::orlist when !hint <> None -> (match !hint with | Some i when condition_for_hint i todo -> aux tables maxm flags cache orlist @@ -1755,3 +1771,4 @@ let demodulate_tac ~dbd ~universe = let pp_proofterm = Equality.pp_proofterm;; let revision = "$Revision$";; +let size_and_depth context metasenv t = 100, 100 diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index eb612ac3a..57bb26b60 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -50,8 +50,11 @@ val get_auto_status : unit -> auto_status val pause: bool -> unit val step : unit -> unit val give_hint : int -> unit +val give_prune_hint : int -> unit val lambda_close : ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term val pp_proofterm: Cic.term -> string +val revision : string (* svn revision *) +val size_and_depth : Cic.context -> Cic.metasenv -> Cic.term -> int * int diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index f8eeefa3c..70773a4a7 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Thu May 24 10:00:33 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Fri May 25 11:09:42 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 886f7d58d..444febcae 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -10,9 +10,10 @@ PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g +#OCAMLOPT_DEBUG_FLAGS = -p OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) INSTALL_PROGRAMS= matita matitac INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser @@ -84,6 +85,15 @@ CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) $(CMOS): $(LIB_DEPS) $(CMXOS): $(LIBX_DEPS) +ifeq ($(MAKECMDGOALS),all) + $(CMOS:%.cmo=%.cmi): $(LIB_DEPS) +endif +ifeq ($(MAKECMDGOALS),) + $(CMOS:%.cmo=%.cmi): $(LIB_DEPS) +endif +ifeq ($(MAKECMDGOALS),opt) + $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS) +endif LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES)) LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml index 0436c206d..06b6b5f1e 100644 --- a/helm/software/matita/matitaAutoGui.ml +++ b/helm/software/matita/matitaAutoGui.ml @@ -81,7 +81,17 @@ let cell_of_candidate height context ?(active=false) g id c = in tooltip#set_tip ~text (button :> GObj.widget); ignore(button#connect#clicked - (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id)); + (fun _ -> + let menu = GMenu.menu () in + let follow = GMenu.menu_item ~label:"Follow" () in + let prune = GMenu.menu_item ~label:"Prune" () in + ignore (follow#connect#activate + (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id)); + ignore (prune#connect#activate + (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id)); + menu#append follow; + menu#append prune; + menu#popup 0 (GtkMain.Main.get_current_event_time ()))); button ;; let cell_of_goal height win_width context goal = @@ -114,7 +124,7 @@ let cell_of_candidates height grey context goal cads = ;; let elems_to_rows height context win_width (table : GPack.table) (or_list) = - let height = height / (List.length or_list) in + let height = height / ((List.length or_list) + 1) in let _ = List.fold_left (fun position (goal_id, goal, grey, depth, candidates) -> diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index f6610911f..c6f21c3f6 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -541,36 +541,47 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status CicMetaSubst.apply_subst subst (Cic.Meta (i,irl)) in let time = Unix.gettimeofday () -. timestamp in - let text = - comment parsed_text ^ "\n" ^ - cic2grafite cc menv proof_term ^ - (Printf.sprintf "\n(* end auto proof: %4.2f *)" time) + let size, depth = Auto.size_and_depth cc menv proof_term in + let trailer = + Printf.sprintf + "\n(* end auto(%s) proof: TIME=%4.2f SIZE=%d DEPTH=%d *)" + Auto.revision time size depth in - (* alternative using FG stuff - let proof_term = - Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc - in - let ty,_ = - CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph - in - let obj = - Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) + let proof_script = + if List.exists (fun (s,_) -> s = "paramodulation") params then + (* use declarative output *) + "Not supported yet" + else + if true then + (* use cic2grafite *) + cic2grafite cc menv proof_term + else + (* alternative using FG stuff *) + let proof_term = + Auto.lambda_close ~prefix_name:"orrible_hack_" + proof_term menv cc + in + let ty,_ = + CicTypeChecker.type_of_aux' + menv [] proof_term CicUniv.empty_ugraph + in + let obj = + Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) + in + Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" + (strip_comments + (ApplyTransformation.txt_of_cic_object + ~map_unicode_to_tex:false + ~skip_thm_and_qed:true + ~skip_initial_lambdas:true + 80 (GrafiteAst.Procedural None) "" obj)) in - let text = - comment parsed_text ^ - Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" - (strip_comments - (ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:false - ~skip_thm_and_qed:true - ~skip_initial_lambdas:true - 80 (GrafiteAst.Procedural None) "" obj)) ^ - "(* end auto proof *)" - in - *) + let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length with - ProofEngineTypes.Fail _ -> [], comment parsed_text, parsed_text_length) + ProofEngineTypes.Fail _ as exn -> + raise exn + (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) | TA.Inline (_,style,suri,prefix) -> let str = ApplyTransformation.txt_of_inline_macro style suri prefix in [], str, String.length parsed_text -- 2.39.2