| author | Walther Neuper <walther.neuper@jku.at> |
| Sat, 02 May 2020 15:41:27 +0200 | |
| changeset 59928 | 7601a1fa20b9 |
| parent 59861 | 65ec9f679c3f |
| child 59934 | 955d6fa8bb9b |
| permissions | -rw-r--r-- |
1 (* Title: calculation abstracted from Ctree
2 Author: Walther Neuper 200117
3 (c) due to copyright terms
4 *)
6 signature CALCULATION =
7 sig
8 type T
9 val current_formula: T -> term
11 end
13 (**)
14 structure Calc(**): CALCULATION(**) =
15 struct
16 (**)
17 type T = Ctree.state
19 fun current_formula (pt, (p, p_)) =
20 case p_ of
21 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
22 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
23 | _ => raise ERROR ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
25 (**)end(**)