conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
option is provided in session ROOT, or interactively via $ISABELLE_HOME_USER/etc/preferences (i.e. Isabelle/jEdit plugin preferences);
1 (* Title: Interpret/lucas-interpreter.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
13 val id_to_string: id -> string
16 (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
17 val prep_input : theory -> Check_Unique.id -> string list -> id ->
18 id * Problem.model_input * input * thm -> T * id
20 val from_store: id -> T
21 val from_store': theory -> id -> T
25 structure MethodC(**): METHOD(**) =
30 val empty = Meth_Def.empty;
32 type id = Meth_Def.id;
33 val id_empty = Meth_Def.id_empty;
34 val id_to_string = Meth_Def.id_to_string;
37 (** prepare MethodC for Store **)
39 (* a subset of MethodC.T record's fields *)
41 {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
42 prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
44 fun prep_input thy guh maa init
46 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
47 errpats = ep, nrls = nr}, scr) =
49 fun eq f (f', _) = f = f';
50 val gi = filter (eq "#Given") ppc;
52 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
53 | ((_, gi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'
54 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
55 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
56 val gi = map (pair "#Given") gi;
58 val fi = filter (eq "#Find") ppc;
60 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
61 | ((_, fi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'
62 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
63 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
64 val fi = map (pair "#Find") fi;
66 val re = filter (eq "#Relate") ppc;
68 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
69 | ((_,re') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'
70 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
71 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
72 val re = map (pair "#Relate") re;
74 val wh = filter (eq "#Where") ppc;
76 [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
77 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
78 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
79 | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
80 val sc = Program.prep_program scr
81 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
83 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
84 erls = rls, srls = srls, prls = prls, calc = calc,
85 crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
89 (** get MethodC from Store **)
91 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
92 fun from_store metID = Store.get (get_mets ()) metID metID;
93 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;