summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 28 Oct 2014 09:57:12 +0100 | |

changeset 58797 | 6d71f19a9fd6 |

parent 58796 | cc5a9a54d340 |

child 58798 | 49ed5eea15d4 |

more abstract type;

src/Pure/General/stack.ML | file | annotate | diff | comparison | revisions | |

src/Pure/Isar/proof.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/General/stack.ML Tue Oct 28 09:32:18 2014 +0100 +++ b/src/Pure/General/stack.ML Tue Oct 28 09:57:12 2014 +0100 @@ -6,7 +6,9 @@ signature STACK = sig - type 'a T = 'a * 'a list + type 'a T + val make: 'a -> 'a list -> 'a T + val dest: 'a T -> 'a * 'a list val level: 'a T -> int val init: 'a -> 'a T val top: 'a T -> 'a @@ -19,21 +21,27 @@ structure Stack: STACK = struct -type 'a T = 'a * 'a list; - -fun level (_, xs) = length xs; +abstype 'a T = Stack of 'a * 'a list +with -fun init x = (x, []); +fun make x xs = Stack (x, xs); +fun dest (Stack (x, xs)) = (x, xs); -fun top (x, _) = x; +fun level (Stack (_, xs)) = length xs; + +fun init x = Stack (x, []); -fun map_top f (x, xs) = (f x, xs); +fun top (Stack (x, _)) = x; -fun map_all f (x, xs) = (f x, map f xs); +fun map_top f (Stack (x, xs)) = Stack (f x, xs); -fun push (x, xs) = (x, x :: xs); +fun map_all f (Stack (x, xs)) = Stack (f x, map f xs); -fun pop (_, x :: xs) = (x, xs) - | pop (_, []) = raise List.Empty; +fun push (Stack (x, xs)) = Stack (x, x :: xs); + +fun pop (Stack (_, x :: xs)) = Stack (x, xs) + | pop (Stack (_, [])) = raise List.Empty; end; + +end;

--- a/src/Pure/Isar/proof.ML Tue Oct 28 09:32:18 2014 +0100 +++ b/src/Pure/Isar/proof.ML Tue Oct 28 09:57:12 2014 +0100 @@ -302,18 +302,22 @@ (* nested goal *) -fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = +fun map_goal f g h (State stack) = + (case Stack.dest stack of + (Node {context, facts, mode, goal = SOME goal}, node :: nodes) => let val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); val node' = map_node_context h node; - in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end - | map_goal f g h (State (nd, node :: nodes)) = + val stack' = Stack.make (make_node (f context, facts, mode, SOME goal')) (node' :: nodes); + in State stack' end + | (nd, node :: nodes) => let val nd' = map_node_context f nd; - val State (node', nodes') = map_goal f g h (State (node, nodes)); - in State (nd', node' :: nodes') end - | map_goal _ _ _ state = state; + val State stack' = map_goal f g h (State (Stack.make node nodes)); + val (node', nodes') = Stack.dest stack'; + in State (Stack.make nd' (node' :: nodes')) end + | _ => State stack); fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => (statement, [], using, goal, before_qed, after_qed)) I;