Skip to content

Commit

Permalink
LiFtEr: test_all_LiFtErs
Browse files Browse the repository at this point in the history
  • Loading branch information
Yutaka Nagashima committed Aug 27, 2019
1 parent b430e40 commit 83f26d5
Show file tree
Hide file tree
Showing 3 changed files with 145 additions and 10 deletions.
13 changes: 8 additions & 5 deletions LiFtEr/Example/Concrete_Semantics/Induction_Demo.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,6 @@ val Example6 = ind_is_not_arb And vars_in_ind_terms_are_generalized;
end;
\<close>

setup\<open> Apply_LiFtEr.update_assert "example_0" (LiFtEr.Some_Rule (LiFtEr.Rule 1, (LiFtEr.True))) \<close>
setup\<open> Apply_LiFtEr.update_assert "example_1a" all_ind_term_are_non_const_wo_syntactic_sugar \<close>
setup\<open> Apply_LiFtEr.update_assert "example_1b" all_ind_term_are_non_const_with_syntactic_sugar \<close>
setup\<open> Apply_LiFtEr.update_assert "example_2" all_ind_terms_have_an_occ_as_variable_at_bottom \<close>
Expand Down Expand Up @@ -166,11 +165,15 @@ setup\<open> Apply_LiFtEr.update_ind_mod "induct_on_xs_arbitrary_ys" official_
setup\<open> Apply_LiFtEr.update_ind_mod "induct_on_itrev_arbitrary_ys" bad_answer_for_itrev_equals_rev \<close>
setup\<open> Apply_LiFtEr.update_ind_mod "induct_on_xs_ys_rule_itrev_induct" xs_ys_rule_itrev_induct \<close>

lemma "itrev xs ys = rev xs @ ys"
lemma "itrev xs ys = rev xs @ ys"
assert_LiFtEr example_1a [on["xs"], arb["ys"],rule[]]
assert_LiFtEr example_1a [on["xs","ys"],arb["ys"],rule["itrev.induct"]]
assert_LiFtEr example_1a [on["itrev"], arb["ys"],rule[]]

assert_LiFtEr example_1a [on["xs","ys"],arb[], rule["itrev.induct"]]
(*assert_LiFtEr example_1a [on["itrev"], arb["ys"],rule[]]*)

test_all_LiFtErs [on["xs"], arb["ys"],rule[]]
test_all_LiFtErs [on["xs","ys"],arb[], rule["itrev.induct"]]
test_all_LiFtErs [on["itrev"], arb["ys"],rule[]]

assert_LiFtEr_false example_1a induct_on_itrev_arbitrary_ys
assert_LiFtEr_true example_1b induct_on_xs_arbitrary_ys
assert_LiFtEr_false example_1b induct_on_itrev_arbitrary_ys
Expand Down
4 changes: 3 additions & 1 deletion LiFtEr/LiFtEr.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ theory LiFtEr
keywords "assert_LiFtEr_true" :: diag
and "assert_LiFtEr_false":: diag
and "assert_LiFtEr" :: diag
and "test_all_LiFtErs" :: diag
begin

ML_file "../src/Utils.ML"
Expand All @@ -35,8 +36,9 @@ ML_file "src/Apply_LiFtEr_Sig.ML"
ML_file "src/Apply_LiFtEr_Struct.ML"
ML_file "src/LiFtEr_Assertion_Struct.ML"

ML\<open> Apply_LiFtEr.activate (); \<close>
ML\<open> Apply_LiFtEr.activate (); \<close>
ML\<open> Apply_LiFtEr.activate2 (); \<close>
ML\<open> Apply_LiFtEr.activate3 (); \<close>

ML\<open>
Symbol.is_printable "\<pi>";
Expand Down
138 changes: 134 additions & 4 deletions LiFtEr/src/Apply_LiFtEr_Struct.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -267,9 +267,139 @@ fun activate2 _ =

end;

val _ = Parse.ML_source;
type dasdf = Input.source parser;
(*abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}*)
type text_of = Input.source -> Symbol_Pos.text;
local

open PC;
open LU;

in

fun get_trans_trans_gen (should_b_true_or_false:bool) (ind_mod(*:ind_mods(*ind_mod_name:string*)*)) =
Toplevel.keep_proof (fn top: Toplevel.state =>
let
val pst = Toplevel.proof_of top : Proof.state;
val ctxt = Toplevel.context_of top : Proof.context;
val all_asserts = (Symtab.dest o LiFtEr_Assertion.get) (Context.Proof ctxt) |> map snd: LiFtEr.assrt list;
val numb_of_all_asserts = length all_asserts: int;
fun mk_clean_mods (ind_mods:LU.ind_mods) =
let
val normalize = IU.normalize_trm_as_string ctxt;
val {ons, arbs, rules} = LU.dest_mods ind_mods;
fun normalize_rule_as_string (rule_as_string:string) =
let
val short_cname_option = try (space_explode ".") rule_as_string
<$> Utils.init <$> Utils.last: string option;
val long_name_option = short_cname_option <$> normalize: string option;
val clean_rule_name = long_name_option <$> curry (op ^) <*> SOME ".induct";
val result = if is_some clean_rule_name then the clean_rule_name else "";
in
result
end;
val clean_ons = map (LU.string_to_induct_on o normalize o LU.induct_on_to_string ) ons : LU.induct_on list;
val clean_arbs = map (LU.string_to_induct_arb o normalize o LU.induct_arb_to_string ) arbs : LU.induct_arb list;
val clean_rules = map (LU.string_to_induct_rule o normalize_rule_as_string o LU.induct_rule_to_string) rules: LU.induct_rule list;
in
LU.Ind_Mods {ons = clean_ons, arbs = clean_arbs, rules = clean_rules}: LU.ind_mods
end;
(*
val ind_mod = get_ind_mod ctxt ind_mod_name: LU.ind_mods;
*)
fun apply_assrt (assrt:LiFtEr.assrt) (pst:Proof.state) (ind_mods:LiFtEr.ind_mods) =
LiFtEr.eval (pst, assrt, ind_mods): bool;
fun run_test (assrt:LiFtEr.assrt) (pst:Proof.state) (ind_mods:LiFtEr.ind_mods) =
apply_assrt assrt pst ind_mods = should_b_true_or_false;
val succeeded_assrts = filter (fn assrt => apply_assrt assrt pst (mk_clean_mods ind_mod)) all_asserts: LiFtEr.assrt list;
val numb_of_succeeded_assrts = length succeeded_assrts: int;

val _ = tracing ("Out of " ^ Int.toString numb_of_all_asserts ^ " assertions, " ^
Int.toString numb_of_succeeded_assrts ^ " assertions succeeded.");
in
()
end)
: trans_trans;

val get_trans_trans_true = get_trans_trans_gen true (*: (string * ind_mods) -> trans_trans;*)

infix plus;

val non_quote_symbol = sat (fn x => not (x = "\""))
: symbols -> (string * symbols) Seq.seq;

fun non_quotation_word' _ =
let
val neWord = non_quote_symbol >>= (fn x =>
non_quotation_word' () >>= (fn xs =>
result (x ^ xs))): symbols -> (string * symbols) Seq.seq;
in
neWord plus result ""
end: string parser;

val non_quotation_word = non_quotation_word' () plus result "": string Parser_Combinator.parser;

val parse_quotation =
bracket
(string "\"" |> token)
(non_quotation_word |> token)
(string "\"" |> token): string Parser_Combinator.parser;

fun parse_list' _ : string Seq.seq parser =
bracket
(string "[" |> token)
(sepby (token (parse_quotation) |> token, (string "," |> token)) |> token)
(string "]" |> token) |> token;

fun parse_list constr name : string list parser =
token
(string name |> token >>= (fn delayer =>
parse_list' delayer >>= (fn strategies : string Seq.seq =>
strategies |> constr |> result)))

fun parse_ons () = parse_list (Seq.list_of) "on" plus result []: string list parser;
fun parse_arbs () = parse_list (Seq.list_of) "arb" plus result []: string list parser;
fun parse_rules () = parse_list (Seq.list_of) "rule" plus result []: string list parser;

fun lifter_parser' () =
token
(parse_ons () |> token >>= (fn ons =>
(string "," |> token) >>= (fn _ =>
parse_arbs () |> token >>= (fn arbs =>
(string "," |> token) >>= (fn _ =>
parse_rules () |> token >>= (fn rules =>
result
(Ind_Mods {
ons = map string_to_induct_on ons,
arbs = map string_to_induct_arb arbs,
rules = map string_to_induct_rule rules})))))));

fun lifter_parser () (*: LiFtEr_Util.ind_mods parser*) =
bracket
(string "[" |> token)

(* (string "test" |> token)*)
(lifter_parser' () |> token)
(string "]" |> token) |> token;

val LiFtEr_parser3 =
PC.bind (lifter_parser ()) (fn ind_mods (*:ind_mods*) =>
PC.result (ind_mods))

val invocation_parser = PC.token LiFtEr_parser3 (*: (ind_mods) PC.parser;*)
val token_parser = PSL_Interface.string_parser_to_token_parser invocation_parser(*: (string * ind_mods) Token.parser;*)
fun get_token_parser_result token = token_parser token |> fst(*: (string * ind_mods);*)

val get_trans_trans_to_token_parser = PSL_Interface.parser_to_trans_trans_parser invocation_parser;

val token_parser_true = get_trans_trans_to_token_parser get_trans_trans_true : trans_trans Token.parser;

fun activate3 _ =
let
val _ =
Outer_Syntax.command @{command_keyword test_all_LiFtErs}
"TODO" token_parser_true;
in () end;

end;



end;

0 comments on commit 83f26d5

Please sign in to comment.