|
116 | 116 | ctx(ctx(ModuleName, TyName, Sol, []), kind, K). |
117 | 117 |
|
118 | 118 | ctx(ctx(ModuleName, TyName, Sol, _Args), kind, K) :- |
119 | | - %print_message(informational, ctx(kind, ModuleName-TyName-K)), |
| 119 | + print_message(informational, ctx(kind, ModuleName-TyName-K)), |
120 | 120 | first(ModuleName-TyName-K, Sol). |
121 | 121 |
|
122 | | -ctx(ctx(ModuleName, TyName, _Sol, Args), arg('.lambdabuffers.compiler.TyVar'{ |
123 | | - var_name: _{ |
124 | | - name: VarName, |
125 | | - source_info: VnSi |
126 | | - }, |
127 | | - source_info: TvSi |
128 | | - }),K) :- |
129 | | - %print_message(informational, ctx(arg(VarName), ModuleName-TyName-K)), |
130 | | - first( |
131 | | - '.lambdabuffers.compiler.TyArg'{ |
132 | | - arg_name: _{name: VarName, source_info: _}, |
133 | | - arg_kind: K |
134 | | - }, |
135 | | - Args |
136 | | - ) -> true; |
| 122 | +ctx(ctx(ModuleName, TyName, _Sol, Args), arg(TyVar),K) :- |
| 123 | + print_message(informational, ctx(arg(TyVar.var_name.name), ModuleName-TyName-K)), |
137 | 124 | ( |
138 | | - throw(error(missing_ty_var( |
139 | | - ModuleName, |
140 | | - TyName, |
141 | | - '.lambdabuffers.compiler.TyVar'{ |
142 | | - var_name: _{ |
143 | | - name: VarName, |
144 | | - source_info: VnSi |
145 | | - }, |
146 | | - source_info: TvSi |
147 | | - }, |
148 | | - Args)) |
149 | | - ) |
| 125 | + first(_{ |
| 126 | + arg_name: _{name: TyVar.var_name.name, source_info: _}, |
| 127 | + arg_kind: K |
| 128 | + }, |
| 129 | + Args |
| 130 | + ) -> true; |
| 131 | + throw(error(missing_ty_var(ModuleName, TyName,TyVar,Args))) |
150 | 132 | ). |
151 | 133 |
|
152 | | -ctx(ctx(ModuleName, TyName, Sol, _Args), ref('.lambdabuffers.compiler.TyRef'{ |
153 | | - local_ty_ref: _{ |
154 | | - ty_name: _{ |
155 | | - name: LocalTyName, |
156 | | - source_info: LtnSi |
157 | | - }, |
158 | | - source_info: Si |
159 | | - } |
160 | | - } |
161 | | - ), K) :- |
162 | | - first(ModuleName-_{name: LocalTyName, source_info:_}-K, Sol) -> print_message(informational, ctx(local_ref(LocalTyName), ModuleName-TyName-K)), true; |
| 134 | +ctx(ctx(ModuleName, TyName, Sol, _Args), ref(TyRef), K) :- |
| 135 | + _{ local_ty_ref: LTyRef } :< TyRef, |
| 136 | + print_message(informational, ctx(local_ref(LTyRef), ModuleName-TyName-K)), |
163 | 137 | ( |
164 | | - throw(error(missing_ty_ref( |
165 | | - ModuleName, |
166 | | - TyName, |
167 | | - '.lambdabuffers.compiler.TyRef'{ |
168 | | - local_ty_ref: '.lambdabuffers.compiler.TyRef.Local'{ |
169 | | - ty_name: '.lambdabuffers.compiler.TyRef.TyName'{ |
170 | | - name: LocalTyName, |
171 | | - source_info: LtnSi |
172 | | - }, |
173 | | - source_info: Si |
174 | | - } |
175 | | - }, |
176 | | - Sol) |
177 | | - )) |
| 138 | + find_sol(Sol, ModuleName, LTyRef.ty_name, K) -> true; |
| 139 | + throw(error(missing_ty_ref(ModuleName, TyName, TyRef,Sol))) |
178 | 140 | ). |
179 | 141 |
|
180 | | -ctx(ctx(ModuleName, TyName, Sol, _Args), ref( |
181 | | - '.lambdabuffers.compiler.TyRef'{ |
182 | | - foreign_ty_ref: _{ |
183 | | - ty_name: _{ |
184 | | - name: ForeignTyName, |
185 | | - source_info: FtnSi |
186 | | - }, |
187 | | - module_name: _{ |
188 | | - name: ForeignModuleName, |
189 | | - source_info: FmnSi |
190 | | - }, |
191 | | - source_info: Si |
192 | | - } |
193 | | - } |
194 | | - ), K) :- |
195 | | - first(_{name: ForeignModuleName, source_info:_}-_{name: ForeignTyName, source_info: _}-K, Sol) -> true; |
| 142 | +ctx(ctx(ModuleName, TyName, Sol, _Args), ref(TyRef), K) :- |
| 143 | + _{ foreign_ty_ref: FTyRef } :< TyRef, |
| 144 | + print_message(informational, ctx(foreign_ref(FTyRef), ModuleName-TyName-K)), |
196 | 145 | ( |
197 | | - throw(error(missing_ty_ref( |
198 | | - ModuleName, |
199 | | - TyName, |
200 | | - '.lambdabuffers.compiler.TyRef'{ |
201 | | - foreign_ty_ref: { |
202 | | - ty_name: { |
203 | | - name: ForeignTyName, |
204 | | - source_info: FtnSi |
205 | | - }, |
206 | | - module_name: { |
207 | | - name: ForeignModuleName, |
208 | | - source_info: FmnSi |
209 | | - }, |
210 | | - source_info: Si |
211 | | - } |
212 | | - }, |
213 | | - Sol) |
214 | | - )) |
| 146 | + find_sol(Sol, FTyRef.module_name, FTyRef.ty_name, K) -> true; |
| 147 | + throw(error(missing_ty_ref(ModuleName, TyName, TyRef, Sol))) |
| 148 | + ). |
| 149 | + |
| 150 | +find_sol([Mn-Tn-K_|Sol], ModuleName, TyName, K) :- |
| 151 | + pretty_module_name(ModuleName, ModuleName_), |
| 152 | + pretty_module_name(Mn, Mn_), |
| 153 | + ( |
| 154 | + ModuleName_ = Mn_, TyName.name = Tn.name -> K=K_, true; |
| 155 | + find_sol(Sol, ModuleName, TyName, K) |
215 | 156 | ). |
216 | 157 |
|
217 | 158 | kind_check_ty(Ctx, '.lambdabuffers.compiler.Ty'{ty_var: TyVar}, K) :- |
|
321 | 262 | "Mod"-"Foo"-(((*)->(*))->(*)) |
322 | 263 | ]). |
323 | 264 |
|
324 | | - |
325 | | - |
326 | 265 | test("\nmodule Mod\nsum Foo", [ ]) :- |
327 | 266 | sum([], TyBody), |
328 | 267 | ty_def_body("Foo", TyBody, TyDef), |
|
479 | 418 | kind_check(CompIn, Solution), |
480 | 419 | print_solution(Solution). |
481 | 420 |
|
| 421 | +test("\nmodule ModFoo\nsum Foo = MkFoo Bar\nmodule ModBar\nopaque Bar", [ ]) :- |
| 422 | + ty_def_opaque("Bar", BarTyDef), |
| 423 | + mod("ModBar", [BarTyDef], ModBar), |
| 424 | + ty_foreign_ref_(["ModBar"], "Bar", BarTyRef), |
| 425 | + ntuple([BarTyRef], MkFooProd), |
| 426 | + constr("MkFoo", MkFooProd, MkFooConstr), |
| 427 | + sum([MkFooConstr], FooTyBody), |
| 428 | + ty_def_body("Foo", FooTyBody, FooTyDef), |
| 429 | + mod("ModFoo", [FooTyDef], ModFoo), |
| 430 | + comp_input([ModFoo, ModBar], CompIn), |
| 431 | + kind_check(CompIn, Solution), |
| 432 | + print_solution(Solution), |
| 433 | + pretty_solution(Solution, [ |
| 434 | + "ModFoo"-"Foo"-(*), |
| 435 | + "ModFoo"-"Foo'Sum"-((*)->(*)), |
| 436 | + "ModFoo"-"Foo'Sum'MkFoo"-((*)->(*)), |
| 437 | + "ModBar"-"Bar"-(*) |
| 438 | + ]). |
| 439 | + |
| 440 | + |
482 | 441 | :- end_tests(kind_check). |
483 | 442 |
|
484 | 443 | :- multifile prolog:message//1. |
|
491 | 450 | ]. |
492 | 451 |
|
493 | 452 | prolog:message(missing_ty_ref(ModuleName, TyName, _{foreign_ty_ref: ForeignTyRef}, _Sol)) |
494 | | ---> {pretty_module_name(ModuleName, Mn)},[ |
| 453 | +--> { |
| 454 | + pretty_module_name(ModuleName, Mn), |
| 455 | + pretty_foreign_ty_ref(ForeignTyRef, FTyRef) |
| 456 | + |
| 457 | + }, |
| 458 | + [ |
495 | 459 | 'Error while kind checking type ~w.~w: Missing foreign type reference ~w '-[ |
496 | | - Mn, TyName.name, ForeignTyRef.ty_name.name |
| 460 | + Mn, TyName.name, FTyRef |
497 | 461 | ] |
498 | 462 | ]. |
499 | 463 |
|
|
0 commit comments