diff --git a/LiFtEr/Example/Concrete_Semantics/Induction_Demo.thy b/LiFtEr/Example/Concrete_Semantics/Induction_Demo.thy index d9a7cf8b..bb4dd8cf 100644 --- a/LiFtEr/Example/Concrete_Semantics/Induction_Demo.thy +++ b/LiFtEr/Example/Concrete_Semantics/Induction_Demo.thy @@ -118,7 +118,6 @@ val Example6 = ind_is_not_arb And vars_in_ind_terms_are_generalized; end; \ -setup\ Apply_LiFtEr.update_assert "example_0" (LiFtEr.Some_Rule (LiFtEr.Rule 1, (LiFtEr.True))) \ setup\ Apply_LiFtEr.update_assert "example_1a" all_ind_term_are_non_const_wo_syntactic_sugar \ setup\ Apply_LiFtEr.update_assert "example_1b" all_ind_term_are_non_const_with_syntactic_sugar \ setup\ Apply_LiFtEr.update_assert "example_2" all_ind_terms_have_an_occ_as_variable_at_bottom \ @@ -166,11 +165,15 @@ setup\ Apply_LiFtEr.update_ind_mod "induct_on_xs_arbitrary_ys" official_ setup\ Apply_LiFtEr.update_ind_mod "induct_on_itrev_arbitrary_ys" bad_answer_for_itrev_equals_rev \ setup\ Apply_LiFtEr.update_ind_mod "induct_on_xs_ys_rule_itrev_induct" xs_ys_rule_itrev_induct \ - 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 diff --git a/LiFtEr/LiFtEr.thy b/LiFtEr/LiFtEr.thy index 65b4bd5f..fa7c4a8a 100644 --- a/LiFtEr/LiFtEr.thy +++ b/LiFtEr/LiFtEr.thy @@ -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" @@ -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\ Apply_LiFtEr.activate (); \ +ML\ Apply_LiFtEr.activate (); \ ML\ Apply_LiFtEr.activate2 (); \ +ML\ Apply_LiFtEr.activate3 (); \ ML\ Symbol.is_printable "\"; diff --git a/LiFtEr/src/Apply_LiFtEr_Struct.ML b/LiFtEr/src/Apply_LiFtEr_Struct.ML index 9c31a387..7c8f1eba 100644 --- a/LiFtEr/src/Apply_LiFtEr_Struct.ML +++ b/LiFtEr/src/Apply_LiFtEr_Struct.ML @@ -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; \ No newline at end of file