13 |
13 |
14 val next_tac : (*diss: next-tactic-function*) |
14 val next_tac : (*diss: next-tactic-function*) |
15 theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe) |
15 theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe) |
16 val locate_gen : (*diss: locate-function*) |
16 val locate_gen : (*diss: locate-function*) |
17 theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate |
17 theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate |
|
18 |
|
19 (* can these functions be local to Lucin or part of LItools ? *) |
18 val sel_rules : ptree -> pos' -> tac list |
20 val sel_rules : ptree -> pos' -> tac list |
19 val init_form : 'a -> scr -> (term * term) list -> term option |
21 val init_form : 'a -> scr -> (term * term) list -> term option |
20 val formal_args : term -> term list |
|
21 |
|
22 val tac_2tac : tac_ -> tac |
22 val tac_2tac : tac_ -> tac |
23 val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr |
23 val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr |
24 val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr |
24 val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr |
25 val from_pblobj_or_detail' : theory' -> pos * pos_ -> ptree -> |
25 val from_pblobj_or_detail' : theory' -> pos * pos_ -> ptree -> |
26 rls * (istate * Proof.context) * scr |
26 rls * (istate * Proof.context) * scr |
27 val rule2thm'' : rule -> thm'' |
27 val rule2thm'' : rule -> thm'' |
28 val rule2rls' : rule -> string |
28 val rule2rls' : rule -> string |
29 |
29 |
|
30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*) |
|
31 datatype asap = Aundef | AssOnly | AssGen |
|
32 datatype appy_ = Napp_ | Skip_ |
30 val itms2args : 'a -> metID -> itm list -> term list |
33 val itms2args : 'a -> metID -> itm list -> term list |
|
34 val get_stac : 'a -> term -> term option |
|
35 val handle_leaf : string -> theory' -> rls -> env -> term option -> term -> term -> |
|
36 term option * stacexpr |
|
37 val formal_args : term -> term list |
|
38 val go : loc_ -> term -> term |
|
39 val id_of_scr : term -> string |
|
40 type appy |
|
41 val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy |
|
42 val sel_appl_atomic_tacs : ptree -> pos' -> tac list |
|
43 val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ -> |
|
44 term option -> term -> appy |
|
45 val upd_env_opt : env -> term option * term -> env |
|
46 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
31 end |
47 end |
32 |
48 |
|
49 (* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *) |
|
50 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *) |
|
51 |
33 (**) |
52 (**) |
34 structure Lucin: LUCAS_INTERPRETER(**) = |
53 structure Lucin(*: LUCAS_INTERPRETER*) = |
35 struct |
54 struct |
36 (**) |
55 (**) |
37 (* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *) |
|
38 val trace_script = Unsynchronized.ref false; |
|
39 |
|
40 (* data for creating a new node in ctree; designed for use as: |
56 (* data for creating a new node in ctree; designed for use as: |
41 fun ass* scrstate steps = / ... case ass* scrstate steps of / |
57 fun ass* scrstate steps = / ... case ass* scrstate steps of / |
42 Assoc (scrstate, steps) => ... ass* scrstate steps *) |
58 Assoc (scrstate, steps) => ... ass* scrstate steps *) |
43 type step = |
59 type step = |
44 tac_ (*transformed from associated tac *) |
60 tac_ (*transformed from associated tac *) |