]> matita.cs.unibo.it Git - helm.git/commitdiff
added pruning option in autogui
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 29 May 2007 11:03:51 +0000 (11:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 29 May 2007 11:03:51 +0000 (11:03 +0000)
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/Makefile
helm/software/matita/matitaAutoGui.ml
helm/software/matita/matitaScript.ml

index d24c244a75f4f24e26530dd5319229affd2fa0be..4cd6bf62ff477db6033aafcd9eeb9e82871fbbe8 100644 (file)
@@ -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
index eb612ac3a05221fdbe59be4f1deb1239f414fcc8..57bb26b60ca52a5e2ad6d7f2118fd4fbfc58c16c 100644 (file)
@@ -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
index f8eeefa3c364f9ddd381d6ab4feec433a1b6b092..70773a4a7fd41bf370ffe9ddde6d4a94a91de865 100644 (file)
@@ -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 :
index 886f7d58ddac68ded069d67d3a461ac30f89969b..444febcae67301c924373c956e35e9ac71e2fce1 100644 (file)
@@ -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))
index 0436c206dbb3827b52b5f083c1a46644bdab4e94..06b6b5f1e9e8696aaef3f78d976f7d1acf3ed8ca 100644 (file)
@@ -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) ->
index f6610911f5ac2ebcb450bde106c46a616ef2fa0b..c6f21c3f62dc19f74f1115013925913ad0306d29 100644 (file)
@@ -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