src/Tools/Code/code_printer.ML
changeset 43326 47cf4bc789aa
parent 43324 2b47822868e4
child 43947 9b00f09f7721
equal deleted inserted replaced
43325:4384f4ae0574 43326:47cf4bc789aa
   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