Skip to content

webdsl-modules.stx

pdmosses/webdsl-statix/webdslstatix/trans/static-semantics/webdsl-modules.stx

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
module static-semantics/webdsl-modules

imports
  static-semantics/webdsl-ac
  static-semantics/webdsl-ui
  static-semantics/webdsl

signature

  relations

     : list(string) * scope

rules // unit rules

  unitOk(, Application(, )) :- {  }
    new s_mod, s_mod -IMPORT-> s_global, s_global -GLOBAL-> s_mod,
    declareACBuiltIns(s_global, s_mod),
    declareMod(s_global, [app], s_mod),
    importModules(s_global, s_mod, sections),
    importLibrary(s_global, s_mod, ["_BUILTIN"]),
    sectionsOk(s_mod, sections),
    rootPageDefined(s_mod, app).

  unitOk(, Module(ModuleName(mps), )) :- {  }
    new s_mod, s_mod -IMPORT-> s_global, s_global -GLOBAL-> s_mod,
    declareMod(s_global, modulePartsToStrings(mps), s_mod),
    importModules(s_global, s_mod, sections),
    importLibrary(s_global, s_mod, ["_BUILTIN"]),
    sectionsOk(s_mod, sections).

  unitOk(, BuiltIn(sections)) :-
    // only analyze built-in if no library is present
    builtInOk(s_global, sections, notB(usesBuiltInLibraryB(s_global))).

  unitOk(, BuiltInLibrary(sections)) :-
    !library[["_BUILTIN_LIBRARY"], new] in s_global,
    builtInOk(s_global, sections, TRUE()).

   : scope * list(Section) * BOOL
  builtInOk(s_global, sections, FALSE()).
  builtInOk(, , TRUE()) :- {  }
    new s_mod, s_mod -IMPORT-> s_global, s_global -GLOBAL-> s_mod,
    declareBuiltIns(s_mod),
    declareMod(s_global, ["_BUILTIN"], s_mod),
    importModules(s_global, s_mod, sections),
    sectionsOk(s_mod, sections).

rules // import definition rules

  defOk(_, Imports(_)). // imports are handled in another rule, discard them here
  defOk(_, ImportsBuiltIn()).

   : scope * scope * list(Section)
  importModules(_, _, []).
  importModules(s, s_mod, [_ | ss]) :-
    importModules(s, s_mod, ss).

  importModules(, , [Section(_, defs) | ss]) :-
    importModulesInSection(s, s_mod, defs),
    importModules(s, s_mod, ss).

   : scope * scope * list(Definition)
  importModulesInSection(_, _, []).
  importModulesInSection(s, s_mod, [_ | defs]) :- importModulesInSection(s, s_mod, defs).
  importModulesInSection(, , [Imports(ImportName(ModuleName(mps), NoWildcardImport())) | defs]) :-
    importModule(s, s_mod, modulePartsToStrings(mps)),
    importModulesInSection(s, s_mod, defs).

   : scope * scope * list(string)
  importModule(, s_mod, ) :- {}
    resolveMod(s, mps) == [(_, (_, s_y))] | error $[Cannot resolve module [mps]],
    importModuleScopeIfDeclared(s_mod, s_y, modDeclaredB(resolveMod(s, mps))).

   : list((path * (list(string) * scope))) -> BOOL
  modDeclaredB([]) = FALSE().
  modDeclaredB(_) = TRUE().

   : scope * scope * BOOL
  importModuleScopeIfDeclared(s_mod, s_y, TRUE()) :- s_mod -IMPORT-> s_y.
  importModuleScopeIfDeclared(s_mod, s_mod, TRUE()). // restrict self import
  importModuleScopeIfDeclared(_, _, FALSE()).

  importModulesInSection(, , [i@Imports(ImportName(ModuleName(mps), WildcardImport())) | defs]) :-
    importModulesWildcard(s_mod, resolveModWildcard(s, modulePartsToStrings(mps)), i),
    importModulesInSection(s, s_mod, defs).

   : scope * list((path * (list(string) * scope))) * Definition
  importModulesWildcard(_, [], i) :- false | error $[Cannot resolve modules] @i.
  importModulesWildcard(s_mod, mods, _) :- importModulesWildcard_internal(s_mod, mods).

  importModulesWildcard_internal maps importModuleWildcard_internal(*, list(*))
   : scope * (path * (list(string) * scope))
  importModuleWildcard_internal(s_mod, (_, (_, s_y))) :- s_mod -IMPORT-> s_y.
  importModuleWildcard_internal(s_mod, (_, (_, s_mod))). // restrict self import

   : scope * scope * list(string)
  importLibrary(, s_mod, ) :- {  }
    resolveMod(s_global, lib) == [(_, (_, s_lib))] | error $[Cannot resolve module [lib]],
    importLibraryScopeIfDeclared(s_mod, s_lib, modDeclaredB(resolveMod(s_global, lib))).

   : scope * scope * BOOL
  importLibraryScopeIfDeclared(s_mod, s_lib, TRUE()) :- s_mod -IMPORTLIB-> s_lib.
  importLibraryScopeIfDeclared(s_mod, s_mod, TRUE()). // restrict self import
  importLibraryScopeIfDeclared(_, _, FALSE()).

rules // utils

   : scope -> BOOL
  usesBuiltInLibraryB(s_global) = usesLibraryB_internal(ps) :-
        query library filter e
          and { m' :- m' == (["_BUILTIN_LIBRARY"], _) }
          in s_global |-> ps.

   : list((path * (list(string) * scope))) -> BOOL
  usesLibraryB_internal([]) = FALSE().
  usesLibraryB_internal([_ | _]) = TRUE().

   maps modulePartToString(list(*)) = list(*)
   : ModulePart -> string
  modulePartToString(ModulePart(s)) = s.