109 |
109 |
110 |
110 |
111 (** term_to_ast **) |
111 (** term_to_ast **) |
112 |
112 |
113 fun mark_freevars ((t as Const (c, _)) $ u) = |
113 fun mark_freevars ((t as Const (c, _)) $ u) = |
114 if c mem_string SynExt.standard_token_markers then (t $ u) |
114 if member (op =) SynExt.standard_token_markers c then (t $ u) |
115 else t $ mark_freevars u |
115 else t $ mark_freevars u |
116 | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u |
116 | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u |
117 | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t) |
117 | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t) |
118 | mark_freevars (t as Free _) = Lexicon.const "_free" $ t |
118 | mark_freevars (t as Free _) = Lexicon.const "_free" $ t |
119 | mark_freevars (t as Var (xi, T)) = |
119 | mark_freevars (t as Var (xi, T)) = |
124 fun ast_of_term thy trf show_all_types no_freeTs show_types show_sorts tm = |
124 fun ast_of_term thy trf show_all_types no_freeTs show_types show_sorts tm = |
125 let |
125 let |
126 fun prune_typs (t_seen as (Const _, _)) = t_seen |
126 fun prune_typs (t_seen as (Const _, _)) = t_seen |
127 | prune_typs (t as Free (x, ty), seen) = |
127 | prune_typs (t as Free (x, ty), seen) = |
128 if ty = dummyT then (t, seen) |
128 if ty = dummyT then (t, seen) |
129 else if no_freeTs orelse t mem seen then (Lexicon.free x, seen) |
129 else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen) |
130 else (t, t :: seen) |
130 else (t, t :: seen) |
131 | prune_typs (t as Var (xi, ty), seen) = |
131 | prune_typs (t as Var (xi, ty), seen) = |
132 if ty = dummyT then (t, seen) |
132 if ty = dummyT then (t, seen) |
133 else if no_freeTs orelse t mem seen then (Lexicon.var xi, seen) |
133 else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen) |
134 else (t, t :: seen) |
134 else (t, t :: seen) |
135 | prune_typs (t_seen as (Bound _, _)) = t_seen |
135 | prune_typs (t_seen as (Bound _, _)) = t_seen |
136 | prune_typs (Abs (x, ty, t), seen) = |
136 | prune_typs (Abs (x, ty, t), seen) = |
137 let val (t', seen') = prune_typs (t, seen); |
137 let val (t', seen') = prune_typs (t, seen); |
138 in (Abs (x, ty, t'), seen') end |
138 in (Abs (x, ty, t'), seen') end |