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
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) =
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
let pp_proofterm = Equality.pp_proofterm;;
let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100
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
-(* 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 :
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
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))
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 =
;;
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) ->
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
projects / helm.git / commitdiff