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