9 signature CODE_TARGET = |
9 signature CODE_TARGET = |
10 sig |
10 sig |
11 include BASIC_CODE_THINGOL; |
11 include BASIC_CODE_THINGOL; |
12 |
12 |
13 val add_syntax_class: string -> class |
13 val add_syntax_class: string -> class |
14 -> (string * (CodeUnit.const * string) list) option -> theory -> theory; |
14 -> (string * (string * string) list) option -> theory -> theory; |
15 val add_syntax_inst: string -> string * class -> bool -> theory -> theory; |
15 val add_syntax_inst: string -> string * class -> bool -> theory -> theory; |
16 val add_syntax_tycoP: string -> string -> OuterParse.token list |
16 val add_syntax_tycoP: string -> string -> OuterParse.token list |
17 -> (theory -> theory) * OuterParse.token list; |
17 -> (theory -> theory) * OuterParse.token list; |
18 val add_syntax_constP: string -> string -> OuterParse.token list |
18 val add_syntax_constP: string -> string -> OuterParse.token list |
19 -> (theory -> theory) * OuterParse.token list; |
19 -> (theory -> theory) * OuterParse.token list; |
21 val add_undefined: string -> string -> string -> theory -> theory; |
21 val add_undefined: string -> string -> string -> theory -> theory; |
22 val add_pretty_list: string -> string -> string -> theory -> theory; |
22 val add_pretty_list: string -> string -> string -> theory -> theory; |
23 val add_pretty_list_string: string -> string -> string |
23 val add_pretty_list_string: string -> string -> string |
24 -> string -> string list -> theory -> theory; |
24 -> string -> string list -> theory -> theory; |
25 val add_pretty_char: string -> string -> string list -> theory -> theory |
25 val add_pretty_char: string -> string -> string list -> theory -> theory |
26 val add_pretty_numeral: string -> bool -> string * typ -> string -> string -> string |
26 val add_pretty_numeral: string -> bool -> string -> string -> string -> string |
27 -> string -> string -> theory -> theory; |
27 -> string -> string -> theory -> theory; |
28 val add_pretty_ml_string: string -> string -> string list -> string |
28 val add_pretty_ml_string: string -> string -> string list -> string |
29 -> string -> string -> theory -> theory; |
29 -> string -> string -> theory -> theory; |
30 val add_pretty_imperative_monad_bind: string -> string -> theory -> theory; |
30 val add_pretty_imperative_monad_bind: string -> string -> theory -> theory; |
31 |
31 |
1791 |
1791 |
1792 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy = |
1792 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy = |
1793 let |
1793 let |
1794 val cls = prep_class thy raw_class; |
1794 val cls = prep_class thy raw_class; |
1795 val class = CodeName.class thy cls; |
1795 val class = CodeName.class thy cls; |
1796 fun mk_classop (const as (c, _)) = case AxClass.class_of_param thy c |
1796 fun mk_classop c = case AxClass.class_of_param thy c |
1797 of SOME class' => if cls = class' then CodeName.const thy const |
1797 of SOME class' => if cls = class' then CodeName.const thy c |
1798 else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c) |
1798 else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c) |
1799 | NONE => error ("Not a class operation: " ^ quote c); |
1799 | NONE => error ("Not a class operation: " ^ quote c); |
1800 fun mk_syntax_ops raw_ops = AList.lookup (op =) |
1800 fun mk_syntax_ops raw_ops = AList.lookup (op =) |
1801 ((map o apfst) (mk_classop o prep_const thy) raw_ops); |
1801 ((map o apfst) (mk_classop o prep_const thy) raw_ops); |
1802 in case raw_syn |
1802 in case raw_syn |
1972 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco; |
1966 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco; |
1973 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings); |
1967 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings); |
1974 |
1968 |
1975 fun add_undefined target undef target_undefined thy = |
1969 fun add_undefined target undef target_undefined thy = |
1976 let |
1970 let |
1977 val (undef', _) = idfs_of_const thy undef; |
|
1978 fun pr _ _ _ _ = str target_undefined; |
1971 fun pr _ _ _ _ = str target_undefined; |
1979 in |
1972 in |
1980 thy |
1973 thy |
1981 |> add_syntax_const target undef' (SOME (~1, pr)) |
1974 |> add_syntax_const target undef (SOME (~1, pr)) |
1982 end; |
1975 end; |
1983 |
1976 |
1984 fun add_pretty_list target nill cons thy = |
1977 fun add_pretty_list target nill cons thy = |
1985 let |
1978 let |
1986 val (_, nil'') = idfs_of_const thy nill; |
1979 val nil' = CodeName.const thy nill; |
1987 val (cons', cons'') = idfs_of_const thy cons; |
1980 val cons' = CodeName.const thy cons; |
1988 val pr = pretty_list nil'' cons'' target; |
1981 val pr = pretty_list nil' cons' target; |
1989 in |
1982 in |
1990 thy |
1983 thy |
1991 |> add_syntax_const target cons' (SOME pr) |
1984 |> add_syntax_const target cons (SOME pr) |
1992 end; |
1985 end; |
1993 |
1986 |
1994 fun add_pretty_list_string target nill cons charr nibbles thy = |
1987 fun add_pretty_list_string target nill cons charr nibbles thy = |
1995 let |
1988 let |
1996 val (_, nil'') = idfs_of_const thy nill; |
1989 val nil' = CodeName.const thy nill; |
1997 val (cons', cons'') = idfs_of_const thy cons; |
1990 val cons' = CodeName.const thy cons; |
1998 val (_, charr'') = idfs_of_const thy charr; |
1991 val charr' = CodeName.const thy charr; |
1999 val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles); |
1992 val nibbles' = map (CodeName.const thy) nibbles; |
2000 val pr = pretty_list_string nil'' cons'' charr'' nibbles'' target; |
1993 val pr = pretty_list_string nil' cons' charr' nibbles' target; |
2001 in |
1994 in |
2002 thy |
1995 thy |
2003 |> add_syntax_const target cons' (SOME pr) |
1996 |> add_syntax_const target cons (SOME pr) |
2004 end; |
1997 end; |
2005 |
1998 |
2006 fun add_pretty_char target charr nibbles thy = |
1999 fun add_pretty_char target charr nibbles thy = |
2007 let |
2000 let |
2008 val (charr', charr'') = idfs_of_const thy charr; |
2001 val charr' = CodeName.const thy charr; |
2009 val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles); |
2002 val nibbles' = map (CodeName.const thy) nibbles; |
2010 val pr = pretty_char charr'' nibbles'' target; |
2003 val pr = pretty_char charr' nibbles' target; |
2011 in |
2004 in |
2012 thy |
2005 thy |
2013 |> add_syntax_const target charr' (SOME pr) |
2006 |> add_syntax_const target charr (SOME pr) |
2014 end; |
2007 end; |
2015 |
2008 |
2016 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy = |
2009 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy = |
2017 let |
2010 let |
2018 val number_of' = CodeUnit.const_of_cexpr thy number_of; |
2011 val b0' = CodeName.const thy b0; |
2019 val (_, b0'') = idfs_of_const thy b0; |
2012 val b1' = CodeName.const thy b1; |
2020 val (_, b1'') = idfs_of_const thy b1; |
2013 val pls' = CodeName.const thy pls; |
2021 val (_, pls'') = idfs_of_const thy pls; |
2014 val min' = CodeName.const thy min; |
2022 val (_, min'') = idfs_of_const thy min; |
2015 val bit' = CodeName.const thy bit; |
2023 val (_, bit'') = idfs_of_const thy bit; |
2016 val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target; |
2024 val pr = pretty_numeral unbounded b0'' b1'' pls'' min'' bit'' target; |
|
2025 in |
2017 in |
2026 thy |
2018 thy |
2027 |> add_syntax_const target number_of' (SOME pr) |
2019 |> add_syntax_const target number_of (SOME pr) |
2028 end; |
2020 end; |
2029 |
2021 |
2030 fun add_pretty_ml_string target charr nibbles nill cons str thy = |
2022 fun add_pretty_ml_string target charr nibbles nill cons str thy = |
2031 let |
2023 let |
2032 val (_, charr'') = idfs_of_const thy charr; |
2024 val charr' = CodeName.const thy charr; |
2033 val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles); |
2025 val nibbles' = map (CodeName.const thy) nibbles; |
2034 val (_, nil'') = idfs_of_const thy nill; |
2026 val nil' = CodeName.const thy nill; |
2035 val (_, cons'') = idfs_of_const thy cons; |
2027 val cons' = CodeName.const thy cons; |
2036 val (str', _) = idfs_of_const thy str; |
2028 val pr = pretty_ml_string charr' nibbles' nil' cons' target; |
2037 val pr = pretty_ml_string charr'' nibbles'' nil'' cons'' target; |
|
2038 in |
2029 in |
2039 thy |
2030 thy |
2040 |> add_syntax_const target str' (SOME pr) |
2031 |> add_syntax_const target str (SOME pr) |
2041 end; |
2032 end; |
2042 |
2033 |
2043 fun add_pretty_imperative_monad_bind target bind thy = |
2034 fun add_pretty_imperative_monad_bind target bind thy = |
2044 let |
2035 let |
2045 val (bind', _) = idfs_of_const thy bind; |
|
2046 val pr = pretty_imperative_monad_bind |
2036 val pr = pretty_imperative_monad_bind |
2047 in |
2037 in |
2048 thy |
2038 thy |
2049 |> add_syntax_const target bind' (SOME pr) |
2039 |> add_syntax_const target bind (SOME pr) |
2050 end; |
2040 end; |
2051 |
2041 |
2052 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const; |
2042 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const; |
2053 |
2043 |
2054 val code_classP = |
2044 val code_classP = |