equal
deleted
inserted
replaced
163 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, |
163 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty, |
164 Name.make_context names); |
164 Name.make_context names); |
165 |
165 |
166 fun intro_vars names (namemap, namectxt) = |
166 fun intro_vars names (namemap, namectxt) = |
167 let |
167 let |
168 val (names', namectxt') = Name.variants names namectxt; |
168 val (names', namectxt') = fold_map Name.variant names namectxt; |
169 val namemap' = fold2 (curry Symtab.update) names names' namemap; |
169 val namemap' = fold2 (curry Symtab.update) names names' namemap; |
170 in (namemap', namectxt') end; |
170 in (namemap', namectxt') end; |
171 |
171 |
172 fun lookup_var (namemap, _) name = case Symtab.lookup namemap name |
172 fun lookup_var (namemap, _) name = case Symtab.lookup namemap name |
173 of SOME name' => name' |
173 of SOME name' => name' |
184 fun fillup_param _ (_, SOME v) = v |
184 fun fillup_param _ (_, SOME v) = v |
185 | fillup_param x (i, NONE) = x ^ string_of_int i; |
185 | fillup_param x (i, NONE) = x ^ string_of_int i; |
186 val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); |
186 val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); |
187 val x = singleton (Name.variant_list (map_filter I fished1)) "x"; |
187 val x = singleton (Name.variant_list (map_filter I fished1)) "x"; |
188 val fished2 = map_index (fillup_param x) fished1; |
188 val fished2 = map_index (fillup_param x) fished1; |
189 val (fished3, _) = Name.variants fished2 Name.context; |
189 val (fished3, _) = fold_map Name.variant fished2 Name.context; |
190 val vars' = intro_vars fished3 vars; |
190 val vars' = intro_vars fished3 vars; |
191 in map (lookup_var vars') fished3 end; |
191 in map (lookup_var vars') fished3 end; |
192 |
192 |
193 fun intro_base_names no_syntax deresolve names = names |
193 fun intro_base_names no_syntax deresolve names = names |
194 |> map_filter (fn name => if no_syntax name then |
194 |> map_filter (fn name => if no_syntax name then |