1open HolKernel Parse boolLib bossLib;
2
3
4open EmitML;
5open basis_emitTheory;
6
7open regexExecutableTheory;
8open regexMarkedTheory;
9open regexCachedMarkedTheory;
10
11
12val _ = new_theory "emit_regex";
13
14
15
16
17(* prepare empty directory *)
18(* ============================================================================================== *)
19
20val emitDir = OS.Path.concat(OS.FileSys.getDir(), "../emit");
21
22val _ = ignore (OS.Process.system ("rm -rf " ^ emitDir));
23
24val _ = if (not (OS.FileSys.access(emitDir, []))) then (OS.FileSys.mkDir emitDir) else ();
25
26
27
28
29
30
31(* emit the regexEMCML library *)
32(* ============================================================================================== *)
33
34(* regexExecutableTheory *)
35
36val defsE = map DEFN [split_def, parts_def, accept_def];
37
38val datatypeDefE = DATATYPE regexDatatypes.Reg_datatype_quot;
39
40
41
42(* regexMarkedTheory *)
43
44val defsM = map DEFN [MARK_REG_def, empty_def, final_def, shift_def, acceptM_def];
45
46val datatypeDefM = DATATYPE regexDatatypes.MReg_datatype_quot;
47
48
49
50(* regexCachedMarkedTheory *)
51
52val defsCM = map DEFN [cempty_def, cfinal_def, cmEps_def, cmSym_def, cmAlt_def,
53                       cmSeq_def, cmRep_def, CACHE_REG_def, cshift_def, acceptCM_def];
54
55val datatypeDefCMReg   = DATATYPE regexDatatypes.CMReg_datatype_quot;
56
57
58
59(* bundle everything and emit as SML library *)
60
61val name = "regexEMC";
62
63val contents =
64  (OPEN ["list"])::
65  (datatypeDefE)::
66  (datatypeDefM)::
67  (datatypeDefCMReg)::
68  (defsE @ defsM @ defsCM);
69
70val _ = emitML emitDir (name, contents);
71(*val _ = eSML name contents;*)
72
73
74
75
76
77(* copy dependencies *)
78(* ============================================================================================== *)
79
80fun copyDep name =
81        ignore (List.map (fn suffix => ignore (OS.Process.system ("cp " ^ (OS.Path.concat(!Globals.emitMLDir, name ^ suffix)) ^ " " ^ emitDir))) ["ML.sml", "ML.sig"]);
82
83
84
85copyDep "combin";
86copyDep "pair";
87copyDep "num";
88copyDep "list";
89copyDep "rich_list";
90
91
92
93val _ = export_theory ();
94
95
96