1(****************************************************************************
2*Copyright 2008
3*  Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow
4****************************************************************************)
5(****************************************************************************
6* This file is part of Teyjus.
7*
8* Teyjus is free software: you can redistribute it and/or modify
9* it under the terms of the GNU General Public License as published by
10* the Free Software Foundation, either version 3 of the License, or
11* (at your option) any later version.
12*
13* Teyjus is distributed in the hope that it will be useful,
14* but WITHOUT ANY WARRANTY; without even the implied warranty of
15* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16* GNU General Public License for more details.
17*
18* You should have received a copy of the GNU General Public License
19* along with Teyjus.  If not, see <http://www.gnu.org/licenses/>.
20****************************************************************************)
21(***************************************************************************)
22(*                           CODE GENERATION                               *)
23(* Functions and data structures are defined here for preparing all        *)
24(* information gathered from a module for dumping out into a bytecode file.*)
25(* 1). Indexes are assigned to different categories of kind and constant   *)
26(*     symbols, type skeletons and strings.                                *)
27(* 2). Imported and accumulated module lists are mapped into lists and all *)
28(*     information needed for dumping out the renaming functions is stored *)
29(*     in these lists.                                                     *)
30(* 3). Predicate defintions are processed and transformed into instructions*)
31(*     together with the size of code space. (The functions in this module *)
32(*     are in charge of generating switching and indexing code and in this *)
33(*     process, hash tables are formed and stored, ready for dumping.      *)
34(*     Clause code is gethered by invocation of functions from             *)
35(*     the module Clausegen. Back patching is performed over call and      *)
36(*     execute instructions after offsets of all clause defintions of this *)
37(*     module become available.)                                           *)
38(* 4). Antecedents of implication goals are processed, definitions are     *)
39(*     translated and information for generating the dump for such tables  *)
40(*     is left in a list.                                                  *)
41(***************************************************************************)
42
43
44(****************************************************************************)
45(*   DATA STRUCTURES FOR RECORDING INFORMATION NEEDED FOR SPITTING CODE     *)
46(****************************************************************************)
47
48(**************************************************************************)
49(* global kinds and local kinds                                           *)
50(*========================================================================*)
51(* kinds lists: (kinds list, number of kinds)                             *)
52(**************************************************************************)
53type cgkinds =  KindList of Absyn.akind list * int
54
55
56(**************************************************************************)
57(* global, local and hidden constants                                     *)
58(*========================================================================*)
59(* constants lists: (constants list, number of constants)                 *)
60(**************************************************************************)
61type cgconsts = ConstantList of Absyn.aconstant list * int
62
63
64(**************************************************************************)
65(* type skeletons                                                         *)
66(*========================================================================*)
67(* type skeletons list: (type skeletons, number of type skeletons)        *)
68(**************************************************************************)
69type cgtypeskeletons = TypeSkeletonList of Absyn.askeleton list * int
70
71
72(**************************************************************************)
73(* strings                                                                *)
74(*========================================================================*)
75(* string list: (strings list, number of strings)                         *)
76(**************************************************************************)
77type cgstrings = StringList of Absyn.astringinfo list * int
78
79
80(**************************************************************************)
81(* predicates defined in this module;                                     *)
82(* global, non-exportdef predicates in this module (predicates whose      *)
83(* previous defintions could be extended by this module);                 *)
84(* (global) exportdef predicates in this module;                          *)
85(* local predicates in this module;                                       *)
86(*========================================================================*)
87(* predicates list: (predicates (names) list, number of predicates)       *)
88(**************************************************************************)
89type cgpreds = PredList of Absyn.aconstant list * int
90
91
92(**************************************************************************)
93(* renaming information of imported and accumulated modules               *)
94(*========================================================================*)
95(* renaming lists: (modname, kinds renaming, constant renaming            *)
96(**************************************************************************)
97type cgrenaming = RenamingInfo of string * cgkinds * cgconsts
98
99
100(**************************************************************************)
101(* predicate instructions                                                 *)
102(*========================================================================*)
103(* instruction list: (instructions, total number of bytes)                *)
104(**************************************************************************)
105type cginstructions = Instructions of Instr.instruction list * int
106
107
108(**************************************************************************)
109(* hash tables:                                                           *)
110(*========================================================================*)
111(* hash tables list: (hash table list, number hash tables)                *)
112(**************************************************************************)
113type cghashtabs = ConstHashTabs of (cghashtab list * int)
114(* hash table structure for indexing on constants: (size, tab entries)    *)
115and  cghashtab = ConstHashTab of int * (cghashtabentry list)
116(* hash table entry: (const category, index, code location )              *)
117and  cghashtabentry = ConstHashTabEntry of Absyn.aconstanttype * int * int
118
119
120(**************************************************************************)
121(* information for implication tables:                                    *)
122(*========================================================================*)
123(* implication goals list : (implication goal list , number of imp goals) *)
124(**************************************************************************)
125type cgimpgoallist = ImpGoalList of (cgimpgoalcode list * int)
126(* information for each implication goal:                                 *)
127(*  (extending preds, preds in antecedent, number of preds in antecendent *)
128and  cgimpgoalcode = ImpGoalCode of (cgpreds * cgimppredinfo list * int)
129(* predicates defined in an implication goal: (predicate, offset)         *)
130and  cgimppredinfo = ImpPredInfo of (Absyn.aconstant * int )
131
132
133(**************************************************************************)
134(* module:                                                                *)
135(*========================================================================*)
136(* (module name,                                                          *)
137(*  global kinds,                                                         *)
138(*  local kinds,                                                          *)
139(*  global constants,                                                     *)
140(*  local constants,                                                      *)
141(*  hidden constants,                                                     *)
142(*  predicates defined in this module,                                    *)
143(*  global, non-exportdef predicates in this module (predicate whose      *)
144(*  previous definitions could be extended by this module),               *)
145(*  (global) exportdef predicates in this module,                         *)
146(*  local predicates in this module,                                      *)
147(*  type skeletons,                                                       *)
148(*  strings,                                                              *)
149(*  imported modules renaming info,                                       *)
150(*  accumulated modules renaming info,                                    *)
151(*  instructions,                                                         *)
152(*  hash tables for constant indexing,                                    *)
153(*  implication goal list                                                 *)
154(* )                                                                      *)
155(**************************************************************************)
156type cgmodule =
157	Module of string * cgkinds * cgkinds * cgconsts * cgconsts *
158	    cgconsts * cgpreds * cgpreds * cgpreds * cgpreds *
159		cgtypeskeletons * cgstrings * cgrenaming list * cgrenaming list *
160		cginstructions * cghashtabs * cgimpgoallist
161
162
163(*****************************************************************************)
164(*                CODE GENERATION FOR A MODULE                               *)
165(*****************************************************************************)
166val generateModuleCode : Absyn.amodule -> cgmodule
167
168
169
170
171