equal
deleted
inserted
replaced
738 |
738 |
739 text_raw {* |
739 text_raw {* |
740 \begin{figure}[t] |
740 \begin{figure}[t] |
741 \begin{minipage}{\textwidth} |
741 \begin{minipage}{\textwidth} |
742 \begin{isabelle}*} |
742 \begin{isabelle}*} |
743 ML{*fun pretty_helper f env = |
743 ML{*fun pretty_helper aux env = |
744 env |> Vartab.dest |
744 env |> Vartab.dest |
745 |> map f |
745 |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) |
746 |> commas |
746 |> commas |
747 |> enclose "[" "]" |
747 |> enclose "[" "]" |
748 |> tracing |
748 |> tracing |
749 |
749 |
750 fun pretty_tyenv ctxt tyenv = |
750 fun pretty_tyenv ctxt tyenv = |
751 let |
751 let |
752 fun aux (v, (s, T)) = |
752 fun get_typs (v, (s, T)) = (TVar (v, s), T) |
753 Syntax.string_of_typ ctxt (TVar (v, s)) |
753 val print = pairself (Syntax.string_of_typ ctxt) |
754 ^ " := " ^ Syntax.string_of_typ ctxt T |
|
755 in |
754 in |
756 pretty_helper aux tyenv |
755 pretty_helper (print o get_typs) tyenv |
757 end*} |
756 end*} |
758 text_raw {* |
757 text_raw {* |
759 \end{isabelle} |
758 \end{isabelle} |
760 \end{minipage} |
759 \end{minipage} |
761 \caption{A pretty printing function for type environments, which are |
760 \caption{A pretty printing function for type environments, which are |
925 the function @{text "pretty_env"}: |
924 the function @{text "pretty_env"}: |
926 *} |
925 *} |
927 |
926 |
928 ML{*fun pretty_env ctxt env = |
927 ML{*fun pretty_env ctxt env = |
929 let |
928 let |
930 fun aux (v, (T, t)) = |
929 fun get_trms (v, (T, t)) = (Var (v, T), t) |
931 string_of_term ctxt (Var (v, T)) ^ " := " ^ string_of_term ctxt t |
930 val print = pairself (string_of_term ctxt) |
932 in |
931 in |
933 pretty_helper aux env |
932 pretty_helper (print o get_trms) env |
934 end*} |
933 end*} |
935 |
934 |
936 text {* |
935 text {* |
937 As can be seen from the @{text "aux"}-function, a term environment associates |
936 As can be seen from the @{text "get_trms"}-function, a term environment associates |
938 a schematic term variable with a type and a term. An example of a first-order |
937 a schematic term variable with a type and a term. An example of a first-order |
939 matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern |
938 matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern |
940 @{text "?X ?Y"}. |
939 @{text "?X ?Y"}. |
941 *} |
940 *} |
942 |
941 |