51 | appy_2str Napp_ = "Napp_" |
51 | appy_2str Napp_ = "Napp_" |
52 | appy_2str Skip_ = "Skip_" |
52 | appy_2str Skip_ = "Skip_" |
53 |
53 |
54 type pstate = |
54 type pstate = |
55 {env: Env.T, (* environment for variables in a program *) |
55 {env: Env.T, (* environment for variables in a program *) |
56 path: Celem.path, (* to the current location in a program *) |
56 path: TermC.path, (* to the current location in a program *) |
57 eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *) |
57 eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *) |
58 form_arg: term option,(* argument of a curried function *) |
58 form_arg: term option,(* argument of a curried function *) |
59 act_arg: term, (* value for the curried argument *) |
59 act_arg: term, (* value for the curried argument *) |
60 or: asap, (* flag for scanning tactical "Or" *) |
60 or: asap, (* flag for scanning tactical "Or" *) |
61 finish: appy_, (* flag set after execution of a tactic *) |
61 finish: appy_, (* flag set after execution of a tactic *) |
64 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term, |
64 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term, |
65 or = ORundef, finish = AppUndef_, assoc = false} |
65 or = ORundef, finish = AppUndef_, assoc = false} |
66 fun topt2str NONE = "NONE" |
66 fun topt2str NONE = "NONE" |
67 | topt2str (SOME t) = "SOME" ^ Rule.term2str t; |
67 | topt2str (SOME t) = "SOME" ^ Rule.term2str t; |
68 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *) |
68 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *) |
69 "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^ |
69 "(" ^ Env.env2str env ^ ", " ^ TermC.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^ |
70 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
70 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^ |
71 appy_2str finish ^ ", " ^ bool2str assoc ^ ")"; |
71 appy_2str finish ^ ", " ^ bool2str assoc ^ ")"; |
72 |
72 |
73 (* for handling type T see fun from_pblobj_or_detail', +? *) |
73 (* for handling type T see fun from_pblobj_or_detail', +? *) |
74 datatype T = (*interpreter state*) |
74 datatype T = (*interpreter state*) |