38 types pttrns |
38 types pttrns |
39 |
39 |
40 syntax |
40 syntax |
41 "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") |
41 "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") |
42 |
42 |
43 "@pttrn" :: "pttrns => pttrn" ("'(_')") |
43 "@pttrn" :: "[pttrn,pttrns] => pttrn" ("'(_,/_')") |
44 "" :: " pttrn => pttrns" ("_") |
44 "" :: " pttrn => pttrns" ("_") |
45 "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") |
45 "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") |
46 |
46 |
47 translations |
47 translations |
48 "(x, y, z)" == "(x, (y, z))" |
48 "(x, y, z)" == "(x, (y, z))" |
49 "(x, y)" == "Pair x y" |
49 "(x, y)" == "Pair x y" |
50 |
50 |
51 "%(x,y,zs).b" => "split(%x (y,zs).b)" |
51 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
52 "%(x,y).b" => "split(%x y.b)" |
52 "%(x,y).b" == "split(%x y.b)" |
53 (* The <= direction fails if split has more than one argument because |
53 (* The <= direction fails if split has more than one argument because |
54 ast-matching fails. Otherwise it would work fine *) |
54 ast-matching fails. Otherwise it would work fine *) |
55 |
55 |
56 defs |
56 defs |
57 Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" |
57 Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" |
73 |
73 |
74 defs |
74 defs |
75 Unity_def "() == Abs_Unit(True)" |
75 Unity_def "() == Abs_Unit(True)" |
76 |
76 |
77 end |
77 end |
78 |
78 (* |
79 ML |
79 ML |
80 |
80 |
81 local open Syntax |
81 local open Syntax |
82 |
82 |
83 fun pttrn s = const"@pttrn" $ s; |
83 fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t; |
84 fun pttrns s t = const"@pttrns" $ s $ t; |
84 fun pttrns s t = const"@pttrns" $ s $ t; |
85 |
85 |
86 fun split2(Abs(x,T,t)) = |
86 fun split2(Abs(x,T,t)) = |
87 let val (pats,u) = split1 t |
87 let val (pats,u) = split1 t |
88 in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end |
88 in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end |