92 |
92 |
93 fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) = |
93 fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) = |
94 annquote_tr' (Syntax.const name) (r :: t :: ts) |
94 annquote_tr' (Syntax.const name) (r :: t :: ts) |
95 | annbexp_tr' _ _ = raise Match; |
95 | annbexp_tr' _ _ = raise Match; |
96 |
96 |
97 fun upd_tr' (x_upd, T) = |
|
98 (case try (unsuffix Record.updateN) x_upd of |
|
99 SOME x => (x, if T = dummyT then T else Term.domain_type T) |
|
100 | NONE => raise Match); |
|
101 |
|
102 fun update_name_tr' (Free x) = Free (upd_tr' x) |
|
103 | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) = |
|
104 c $ Free (upd_tr' x) |
|
105 | update_name_tr' (Const x) = Const (upd_tr' x) |
|
106 | update_name_tr' _ = raise Match; |
|
107 |
|
108 fun K_tr' (Abs (_, _, t)) = |
97 fun K_tr' (Abs (_, _, t)) = |
109 if null (loose_bnos t) then t else raise Match |
98 if null (loose_bnos t) then t else raise Match |
110 | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = |
99 | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = |
111 if null (loose_bnos t) then t else raise Match |
100 if null (loose_bnos t) then t else raise Match |
112 | K_tr' _ = raise Match; |
101 | K_tr' _ = raise Match; |
113 |
102 |
114 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
103 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
115 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f) |
104 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) |
116 (Abs (x, dummyT, K_tr' k) :: ts) |
105 (Abs (x, dummyT, K_tr' k) :: ts) |
117 | assign_tr' _ = raise Match; |
106 | assign_tr' _ = raise Match; |
118 |
107 |
119 fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = |
108 fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = |
120 quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ update_name_tr' f) |
109 quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f) |
121 (Abs (x, dummyT, K_tr' k) :: ts) |
110 (Abs (x, dummyT, K_tr' k) :: ts) |
122 | annassign_tr' _ = raise Match; |
111 | annassign_tr' _ = raise Match; |
123 |
112 |
124 fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $ |
113 fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $ |
125 (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $ |
114 (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $ |