87 Positional instantiations are extended to match full length of parameter list |
87 Positional instantiations are extended to match full length of parameter list |
88 of instantiated locale.*) |
88 of instantiated locale.*) |
89 |
89 |
90 fun parameters_of thy strict (expr, fixed) = |
90 fun parameters_of thy strict (expr, fixed) = |
91 let |
91 let |
|
92 val ctxt = Proof_Context.init_global thy; |
|
93 |
92 fun reject_dups message xs = |
94 fun reject_dups message xs = |
93 (case duplicates (op =) xs of |
95 (case duplicates (op =) xs of |
94 [] => () |
96 [] => () |
95 | dups => error (message ^ commas dups)); |
97 | dups => error (message ^ commas dups)); |
96 |
98 |
101 fun params_inst (loc, (prfx, Positional insts)) = |
103 fun params_inst (loc, (prfx, Positional insts)) = |
102 let |
104 let |
103 val ps = params_loc loc; |
105 val ps = params_loc loc; |
104 val d = length ps - length insts; |
106 val d = length ps - length insts; |
105 val insts' = |
107 val insts' = |
106 if d < 0 then error ("More arguments than parameters in instantiation of locale " ^ |
108 if d < 0 then |
107 quote (Locale.extern thy loc)) |
109 error ("More arguments than parameters in instantiation of locale " ^ |
|
110 quote (Locale.markup_name ctxt loc)) |
108 else insts @ replicate d NONE; |
111 else insts @ replicate d NONE; |
109 val ps' = (ps ~~ insts') |> |
112 val ps' = (ps ~~ insts') |> |
110 map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); |
113 map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); |
111 in (ps', (loc, (prfx, Positional insts'))) end |
114 in (ps', (loc, (prfx, Positional insts'))) end |
112 | params_inst (loc, (prfx, Named insts)) = |
115 | params_inst (loc, (prfx, Named insts)) = |
113 let |
116 let |
114 val _ = reject_dups "Duplicate instantiation of the following parameter(s): " |
117 val _ = |
115 (map fst insts); |
118 reject_dups "Duplicate instantiation of the following parameter(s): " |
|
119 (map fst insts); |
116 val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => |
120 val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => |
117 if AList.defined (op =) ps p then AList.delete (op =) p ps |
121 if AList.defined (op =) ps p then AList.delete (op =) p ps |
118 else error (quote p ^ " not a parameter of instantiated expression")); |
122 else error (quote p ^ " not a parameter of instantiated expression")); |
119 in (ps', (loc, (prfx, Named insts))) end; |
123 in (ps', (loc, (prfx, Named insts))) end; |
120 fun params_expr is = |
124 fun params_expr is = |