Created
April 8, 2025 13:42
-
-
Save digama0/a092e6339371f6c44da2a2057f03efdf to your computer and use it in GitHub Desktop.
Revisions
-
digama0 created this gist
Apr 8, 2025 .There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,703 @@ val ls = [ ("KernelTypes", "src/0/KernelTypes.sml"), ("Net", "src/0/Net.sml"), ("Subst", "src/0/Subst.sml"), ("Term", "src/0/Term.sml"), ("Type", "src/0/Type.sml"), ("Abbrev", "src/1/Abbrev.sml"), ("AC_Sort", "src/1/AC_Sort.sml"), ("BoolExtractShared", "src/1/BoolExtractShared.sml"), ("boolLib", "src/1/boolLib.sml"), ("boolSyntax", "src/1/boolSyntax.sml"), ("BoundedRewrites", "src/1/BoundedRewrites.sml"), ("ConseqConv", "src/1/ConseqConv.sml"), ("Conv", "src/1/Conv.sml"), ("DefnBaseCore", "src/1/DefnBaseCore.sml"), ("dep_rewrite", "src/1/dep_rewrite.sml"), ("DiskThms", "src/1/DiskThms.sml"), ("Drule", "src/1/Drule.sml"), ("fastbuild", "src/1/fastbuild.sml"), ("FullUnify", "src/1/FullUnify.sml"), ("Ho_Net", "src/1/Ho_Net.sml"), ("Ho_Rewrite", "src/1/Ho_Rewrite.sml"), ("holmake_interactive", "src/1/holmake_interactive.sml"), ("holmake_not_interactive", "src/1/holmake_not_interactive.sml"), ("holmakebuild", "src/1/holmakebuild.sml"), ("LVTermNetFunctorApplied", "src/1/LVTermNetFunctorApplied.sml"), ("MakeBigTerm", "src/1/MakeBigTerm.sml"), ("match_goal", "src/1/match_goal.sml"), ("mp_then", "src/1/mp_then.sml"), ("Mutual", "src/1/Mutual.sml"), ("newtypeTools", "src/1/newtypeTools.sml"), ("ParseExtras", "src/1/ParseExtras.sml"), ("Pmatch", "src/1/Pmatch.sml"), ("PmatchHeuristics", "src/1/PmatchHeuristics.sml"), ("Prim_rec", "src/1/Prim_rec.sml"), ("Psyntax", "src/1/Psyntax.sml"), ("resolve_then", "src/1/resolve_then.sml"), ("Rewrite", "src/1/Rewrite.sml"), ("Rsyntax", "src/1/Rsyntax.sml"), ("Sanity", "src/1/Sanity.sml"), ("ScaledTests", "src/1/ScaledTests.sml"), ("simpfrag", "src/1/simpfrag.sml"), ("Tactic", "src/1/Tactic.sml"), ("Tactical", "src/1/Tactical.sml"), ("term_tactic", "src/1/term_tactic.sml"), ("Thm_cont", "src/1/Thm_cont.sml"), ("ThmAttribute", "src/1/ThmAttribute.sml"), ("thmpos_dtype", "src/1/thmpos_dtype.sml"), ("ThmSetData", "src/1/ThmSetData.sml"), ("TypeBase", "src/1/TypeBase.sml"), ("TypeBasePure", "src/1/TypeBasePure.sml"), ("wlogLib", "src/1/wlogLib.sml"), ("aiLib", "src/AI/aiLib.sml"), ("mlFeature", "src/AI/machine_learning/mlFeature.sml"), ("mlMatrix", "src/AI/machine_learning/mlMatrix.sml"), ("mlNearestNeighbor", "src/AI/machine_learning/mlNearestNeighbor.sml"), ("mlNeuralNetwork", "src/AI/machine_learning/mlNeuralNetwork.sml"), ("mlReinforce", "src/AI/machine_learning/mlReinforce.sml"), ("mlTacticData", "src/AI/machine_learning/mlTacticData.sml"), ("mlThmData", "src/AI/machine_learning/mlThmData.sml"), ("mlTreeNeuralNetwork", "src/AI/machine_learning/mlTreeNeuralNetwork.sml"), ("psBigSteps", "src/AI/proof_search/psBigSteps.sml"), ("psMCTS", "src/AI/proof_search/psMCTS.sml"), ("psMinimize", "src/AI/proof_search/psMinimize.sml"), ("psTermGen", "src/AI/proof_search/psTermGen.sml"), ("infix_file", "src/AI/sml_inspection/infix_file.sml"), ("smlExecScripts", "src/AI/sml_inspection/smlExecScripts.sml"), ("smlExecute", "src/AI/sml_inspection/smlExecute.sml"), ("smlInfix", "src/AI/sml_inspection/smlInfix.sml"), ("smlLexer", "src/AI/sml_inspection/smlLexer.sml"), ("smlOpen", "src/AI/sml_inspection/smlOpen.sml"), ("smlParallel", "src/AI/sml_inspection/smlParallel.sml"), ("smlParser", "src/AI/sml_inspection/smlParser.sml"), ("smlPrettify", "src/AI/sml_inspection/smlPrettify.sml"), ("smlRedirect", "src/AI/sml_inspection/smlRedirect.sml"), ("smlTimeout", "src/AI/sml_inspection/smlTimeout.sml"), ("jcLib", "src/algebra/construction/jcLib.sml"), ("bagLib", "src/bag/bagLib.sml"), ("bagSimpleLib", "src/bag/bagSimpleLib.sml"), ("bagSimps", "src/bag/bagSimps.sml"), ("bagSyntax", "src/bag/bagSyntax.sml"), ("BasicProvers", "src/basicProof/BasicProvers.sml"), ("boolpp", "src/bool/boolpp.sml"), ("TexTokenMap", "src/bool/TexTokenMap.sml"), ("Encode", "src/Boolify/src/Encode.sml"), ("PreListEncode", "src/Boolify/src/PreListEncode.sml"), ("bossLib", "src/boss/bossLib.sml"), ("EvalRef", "src/boss/ml_evaluation/EvalRef.sml"), ("Lift", "src/boss/ml_evaluation/Lift.sml"), ("combinLib", "src/combin/combinLib.sml"), ("combinpp", "src/combin/combinpp.sml"), ("combinSyntax", "src/combin/combinSyntax.sml"), ("Arith", "src/compute/examples/Arith.sml"), ("clauses", "src/compute/src/clauses.sml"), ("compute_rules", "src/compute/src/compute_rules.sml"), ("computeLib", "src/compute/src/computeLib.sml"), ("equations", "src/compute/src/equations.sml"), ("groundEval", "src/compute/src/groundEval.sml"), ("DefnBase", "src/coretypes/DefnBase.sml"), ("oneSyntax", "src/coretypes/oneSyntax.sml"), ("optionLib", "src/coretypes/optionLib.sml"), ("optionSimps", "src/coretypes/optionSimps.sml"), ("optionSyntax", "src/coretypes/optionSyntax.sml"), ("PairedLambda", "src/coretypes/PairedLambda.sml"), ("pairLib", "src/coretypes/pairLib.sml"), ("PairRules", "src/coretypes/PairRules.sml"), ("pairSimps", "src/coretypes/pairSimps.sml"), ("pairSyntax", "src/coretypes/pairSyntax.sml"), ("pairTools", "src/coretypes/pairTools.sml"), ("sumSimps", "src/coretypes/sumSimps.sml"), ("sumSyntax", "src/coretypes/sumSyntax.sml"), ("DataSize", "src/datatype/DataSize.sml"), ("Datatype", "src/datatype/Datatype.sml"), ("DatatypeSimps", "src/datatype/DatatypeSimps.sml"), ("EnumType", "src/datatype/EnumType.sml"), ("ind_types", "src/datatype/ind_types.sml"), ("RecordType", "src/datatype/record/RecordType.sml"), ("ConstMapML", "src/emit/ConstMapML.sml"), ("EmitML", "src/emit/EmitML.sml"), ("KernelTypes", "src/experimental-kernel/KernelTypes.sml"), ("Net", "src/experimental-kernel/Net.sml"), ("Term", "src/experimental-kernel/Term.sml"), ("Type", "src/experimental-kernel/Type.sml"), ("alist_treeLib", "src/finite_maps/alist_treeLib.sml"), ("alistLib", "src/finite_maps/alistLib.sml"), ("enumTacs", "src/finite_maps/enumTacs.sml"), ("finite_mapLib", "src/finite_maps/finite_mapLib.sml"), ("finite_mapSyntax", "src/finite_maps/finite_mapSyntax.sml"), ("flookupLib", "src/finite_maps/flookupLib.sml"), ("fmapalTacs", "src/finite_maps/fmapalTacs.sml"), ("sptreeLib", "src/finite_maps/sptreeLib.sml"), ("sptreepp", "src/finite_maps/sptreepp.sml"), ("sptreeSyntax", "src/finite_maps/sptreeSyntax.sml"), ("tcTacs", "src/finite_maps/tcTacs.sml"), ("totoTacs", "src/finite_maps/totoTacs.sml"), ("hol88Lib", "src/hol88/hol88Lib.sml"), ("def_cnf", "src/HolSat/def_cnf.sml"), ("dimacsTools", "src/HolSat/dimacsTools.sml"), ("dpll", "src/HolSat/dpll.sml"), ("HolSatLib", "src/HolSat/HolSatLib.sml"), ("minisatParse", "src/HolSat/minisatParse.sml"), ("minisatProve", "src/HolSat/minisatProve.sml"), ("minisatResolve", "src/HolSat/minisatResolve.sml"), ("satCommonTools", "src/HolSat/satCommonTools.sml"), ("satConfig", "src/HolSat/satConfig.sml"), ("SatSolvers", "src/HolSat/SatSolvers.sml"), ("satTools", "src/HolSat/satTools.sml"), ("defCNF", "src/HolSat/vector_def_CNF/defCNF.sml"), ("Z3_Proof", "src/HolSmt/Z3_Proof.sml"), ("hhExportFof", "src/holyhammer/hhExportFof.sml"), ("hhExportLib", "src/holyhammer/hhExportLib.sml"), ("hhExportSexpr", "src/holyhammer/hhExportSexpr.sml"), ("hhExportTf0", "src/holyhammer/hhExportTf0.sml"), ("hhExportTf1", "src/holyhammer/hhExportTf1.sml"), ("hhExportTh0", "src/holyhammer/hhExportTh0.sml"), ("hhExportTh1", "src/holyhammer/hhExportTh1.sml"), ("hhReconstruct", "src/holyhammer/hhReconstruct.sml"), ("hhTptp", "src/holyhammer/hhTptp.sml"), ("hhTranslate", "src/holyhammer/hhTranslate.sml"), ("holyHammer", "src/holyhammer/holyHammer.sml"), ("CoIndDefLib", "src/IndDef/CoIndDefLib.sml"), ("IndDefLib", "src/IndDef/IndDefLib.sml"), ("IndDefRules", "src/IndDef/IndDefRules.sml"), ("InductiveDefinition", "src/IndDef/InductiveDefinition.sml"), ("Cooper", "src/integer/Cooper.sml"), ("CooperCore", "src/integer/CooperCore.sml"), ("CooperMath", "src/integer/CooperMath.sml"), ("CooperShell", "src/integer/CooperShell.sml"), ("CooperSyntax", "src/integer/CooperSyntax.sml"), ("CooperThms", "src/integer/CooperThms.sml"), ("CSimp", "src/integer/CSimp.sml"), ("IntDP_Munge", "src/integer/IntDP_Munge.sml"), ("integerRingLib", "src/integer/integerRingLib.sml"), ("intLib", "src/integer/intLib.sml"), ("intReduce", "src/integer/intReduce.sml"), ("intSimps", "src/integer/intSimps.sml"), ("intSyntax", "src/integer/intSyntax.sml"), ("inttoTacs", "src/integer/inttoTacs.sml"), ("Omega", "src/integer/Omega.sml"), ("OmegaMath", "src/integer/OmegaMath.sml"), ("OmegaMLShadow", "src/integer/OmegaMLShadow.sml"), ("OmegaShell", "src/integer/OmegaShell.sml"), ("OmegaSimple", "src/integer/OmegaSimple.sml"), ("OmegaSymbolic", "src/integer/OmegaSymbolic.sml"), ("indexedListsSimps", "src/list/src/indexedListsSimps.sml"), ("ListConv1", "src/list/src/ListConv1.sml"), ("listLib", "src/list/src/listLib.sml"), ("listSimps", "src/list/src/listSimps.sml"), ("listSyntax", "src/list/src/listSyntax.sml"), ("numposrepLib", "src/list/src/numposrepLib.sml"), ("numposrepSyntax", "src/list/src/numposrepSyntax.sml"), ("rich_listSimps", "src/list/src/rich_listSimps.sml"), ("rich_listSyntax", "src/list/src/rich_listSyntax.sml"), ("liteLib", "src/lite/liteLib.sml"), ("markerLib", "src/marker/markerLib.sml"), ("markerSyntax", "src/marker/markerSyntax.sml"), ("Canon_Port", "src/meson/src/Canon_Port.sml"), ("jrhTactics", "src/meson/src/jrhTactics.sml"), ("mesonLib", "src/meson/src/mesonLib.sml"), ("folMapping", "src/metis/folMapping.sml"), ("folTools", "src/metis/folTools.sml"), ("matchTools", "src/metis/matchTools.sml"), ("metisLib", "src/metis/metisLib.sml"), ("metisTools", "src/metis/metisTools.sml"), ("mlibArbint", "src/metis/mlibArbint.sml"), ("mlibArbnum", "src/metis/mlibArbnum.sml"), ("mlibCanon", "src/metis/mlibCanon.sml"), ("mlibClause", "src/metis/mlibClause.sml"), ("mlibClauseset", "src/metis/mlibClauseset.sml"), ("mlibHeap", "src/metis/mlibHeap.sml"), ("mlibKernel", "src/metis/mlibKernel.sml"), ("mlibLiteralnet", "src/metis/mlibLiteralnet.sml"), ("mlibMatch", "src/metis/mlibMatch.sml"), ("mlibMeson", "src/metis/mlibMeson.sml"), ("mlibMeter", "src/metis/mlibMeter.sml"), ("mlibMetis", "src/metis/mlibMetis.sml"), ("mlibModel", "src/metis/mlibModel.sml"), ("mlibMultiset", "src/metis/mlibMultiset.sml"), ("mlibOmega", "src/metis/mlibOmega.sml"), ("mlibOmegaint", "src/metis/mlibOmegaint.sml"), ("mlibParser", "src/metis/mlibParser.sml"), ("mlibPatricia", "src/metis/mlibPatricia.sml"), ("mlibPortable", "src/metis/mlibPortable.sml"), ("mlibResolution", "src/metis/mlibResolution.sml"), ("mlibRewrite", "src/metis/mlibRewrite.sml"), ("mlibSolver", "src/metis/mlibSolver.sml"), ("mlibStream", "src/metis/mlibStream.sml"), ("mlibSubst", "src/metis/mlibSubst.sml"), ("mlibSubsume", "src/metis/mlibSubsume.sml"), ("mlibSupport", "src/metis/mlibSupport.sml"), ("mlibTerm", "src/metis/mlibTerm.sml"), ("mlibTermnet", "src/metis/mlibTermnet.sml"), ("mlibTermorder", "src/metis/mlibTermorder.sml"), ("mlibThm", "src/metis/mlibThm.sml"), ("mlibTptp", "src/metis/mlibTptp.sml"), ("mlibUnits", "src/metis/mlibUnits.sml"), ("mlibUseful", "src/metis/mlibUseful.sml"), ("normalForms", "src/metis/normalForms.sml"), ("monadsyntax", "src/monad/monadsyntax.sml"), ("state_monadLib", "src/monad/more_monads/state_monadLib.sml"), ("state_transformerSyntax", "src/monad/more_monads/state_transformerSyntax.sml"), ("parmonadsyntax", "src/monad/parmonadsyntax.sml"), ("fcpLib", "src/n-bit/fcpLib.sml"), ("fcpSyntax", "src/n-bit/fcpSyntax.sml"), ("wordspp", "src/n-bit/wordspp.sml"), ("Arith", "src/num/arith/src/Arith.sml"), ("Arith_cons", "src/num/arith/src/Arith_cons.sml"), ("Exists_arith", "src/num/arith/src/Exists_arith.sml"), ("Gen_arith", "src/num/arith/src/Gen_arith.sml"), ("GenPolyCanon", "src/num/arith/src/GenPolyCanon.sml"), ("GenRelNorm", "src/num/arith/src/GenRelNorm.sml"), ("Instance", "src/num/arith/src/Instance.sml"), ("Int_extra", "src/num/arith/src/Int_extra.sml"), ("Norm_arith", "src/num/arith/src/Norm_arith.sml"), ("Norm_bool", "src/num/arith/src/Norm_bool.sml"), ("Norm_ineqs", "src/num/arith/src/Norm_ineqs.sml"), ("NumRelNorms", "src/num/arith/src/NumRelNorms.sml"), ("numSimps", "src/num/arith/src/numSimps.sml"), ("Prenex", "src/num/arith/src/Prenex.sml"), ("Rationals", "src/num/arith/src/Rationals.sml"), ("RJBConv", "src/num/arith/src/RJBConv.sml"), ("Sol_ranges", "src/num/arith/src/Sol_ranges.sml"), ("Solve", "src/num/arith/src/Solve.sml"), ("Solve_ineqs", "src/num/arith/src/Solve_ineqs.sml"), ("Sub_and_cond", "src/num/arith/src/Sub_and_cond.sml"), ("Sup_Inf", "src/num/arith/src/Sup_Inf.sml"), ("Term_coeffs", "src/num/arith/src/Term_coeffs.sml"), ("Theorems", "src/num/arith/src/Theorems.sml"), ("Thm_convs", "src/num/arith/src/Thm_convs.sml"), ("bitLib", "src/num/extra_theories/bitLib.sml"), ("bitSyntax", "src/num/extra_theories/bitSyntax.sml"), ("numLib", "src/num/numLib.sml"), ("Arithconv", "src/num/reduce/conv-old/Arithconv.sml"), ("Arithconv", "src/num/reduce/conv/Arithconv.sml"), ("Boolconv", "src/num/reduce/src/Boolconv.sml"), ("Grobner", "src/num/reduce/src/Grobner.sml"), ("Normalizer", "src/num/reduce/src/Normalizer.sml"), ("reduceLib", "src/num/reduce/src/reduceLib.sml"), ("TotalDefn", "src/num/termination/TotalDefn.sml"), ("basicSize", "src/num/theories/basicSize.sml"), ("basicSizeSyntax", "src/num/theories/basicSizeSyntax.sml"), ("cv_computeLib", "src/num/theories/cv_compute/cv_computeLib.sml"), ("cvSyntax", "src/num/theories/cv_compute/cvSyntax.sml"), ("tailrecLib", "src/num/theories/cv_compute/tailrecLib.sml"), ("DecimalFractionPP", "src/num/theories/DecimalFractionPP.sml"), ("Num_conv", "src/num/theories/Num_conv.sml"), ("numSyntax", "src/num/theories/numSyntax.sml"), ("OpenTheoryCommon", "src/opentheory/OpenTheoryCommon.sml"), ("OpenTheoryMap", "src/opentheory/OpenTheoryMap.sml"), ("OpenTheoryReader", "src/opentheory/reader/OpenTheoryReader.sml"), ("Absyn", "src/parse/Absyn.sml"), ("Absyn_dtype", "src/parse/Absyn_dtype.sml"), ("AncestryData", "src/parse/AncestryData.sml"), ("base_lexer", "src/parse/base_lexer.sml"), ("base_tokens", "src/parse/base_tokens.sml"), ("base_tokens_dtype", "src/parse/base_tokens_dtype.sml"), ("CharSet", "src/parse/CharSet.sml"), ("FCNet", "src/parse/FCNet.sml"), ("GrammarAncestry", "src/parse/GrammarAncestry.sml"), ("GrammarDeltas", "src/parse/GrammarDeltas.sml"), ("GrammarSpecials", "src/parse/GrammarSpecials.sml"), ("Hol_pp", "src/parse/Hol_pp.sml"), ("HOLgrammars", "src/parse/HOLgrammars.sml"), ("HOLtokens", "src/parse/HOLtokens.sml"), ("Literal", "src/parse/Literal.sml"), ("LVTermNet", "src/parse/LVTermNet.sml"), ("LVTermNetFunctor", "src/parse/LVTermNetFunctor.sml"), ("MLstring", "src/parse/MLstring.sml"), ("Overload", "src/parse/Overload.sml"), ("Parse", "src/parse/Parse.sml"), ("Parse_support", "src/parse/Parse_support.sml"), ("Parse_supportENV", "src/parse/Parse_supportENV.sml"), ("parse_term", "src/parse/parse_term.sml"), ("parse_term_dtype", "src/parse/parse_term_dtype.sml"), ("parse_type", "src/parse/parse_type.sml"), ("ParseDatatype", "src/parse/ParseDatatype.sml"), ("ParseDatatype_dtype", "src/parse/ParseDatatype_dtype.sml"), ("PPBackEnd", "src/parse/PPBackEnd.sml"), ("PrecAnalysis", "src/parse/PrecAnalysis.sml"), ("Preterm", "src/parse/Preterm.sml"), ("Preterm_dtype", "src/parse/Preterm_dtype.sml"), ("Pretype", "src/parse/Pretype.sml"), ("Pretype_dtype", "src/parse/Pretype_dtype.sml"), ("ProvideUnicode", "src/parse/ProvideUnicode.sml"), ("qbuf", "src/parse/qbuf.sml"), ("TacticParse", "src/parse/TacticParse.sml"), ("term_grammar", "src/parse/term_grammar.sml"), ("term_grammar_dtype", "src/parse/term_grammar_dtype.sml"), ("term_pp", "src/parse/term_pp.sml"), ("term_pp_types", "src/parse/term_pp_types.sml"), ("term_pp_utils", "src/parse/term_pp_utils.sml"), ("term_pp_utils_dtype", "src/parse/term_pp_utils_dtype.sml"), ("term_tokens", "src/parse/term_tokens.sml"), ("TermParse", "src/parse/TermParse.sml"), ("testutils", "src/parse/testutils.sml"), ("type_grammar", "src/parse/type_grammar.sml"), ("type_grammar_dtype", "src/parse/type_grammar_dtype.sml"), ("type_pp", "src/parse/type_pp.sml"), ("type_tokens", "src/parse/type_tokens.sml"), ("type_tokens_dtype", "src/parse/type_tokens_dtype.sml"), ("typecheck_error", "src/parse/typecheck_error.sml"), ("TypeNet", "src/parse/TypeNet.sml"), ("constrFamiliesLib", "src/pattern_matches/constrFamiliesLib.sml"), ("parsePMATCH", "src/pattern_matches/parsePMATCH.sml"), ("patternMatchesLib", "src/pattern_matches/patternMatchesLib.sml"), ("patternMatchesSyntax", "src/pattern_matches/patternMatchesSyntax.sml"), ("AList", "src/portableML/AList.sml"), ("Arbint", "src/portableML/Arbint.sml"), ("Arbnum", "src/portableML/Arbnum.sml"), ("Arbrat", "src/portableML/Arbrat.sml"), ("FlagDB", "src/portableML/FlagDB.sml"), ("Graph", "src/portableML/Graph.sml"), ("HOLdict", "src/portableML/HOLdict.sml"), ("holmake_holpathdb", "src/portableML/holmake_holpathdb.sml"), ("HOLPP", "src/portableML/HOLPP.sml"), ("HOLquotation", "src/portableML/HOLquotation.sml"), ("HOLset", "src/portableML/HOLset.sml"), ("HOLsexp", "src/portableML/HOLsexp.sml"), ("HOLsexp_dtype", "src/portableML/HOLsexp_dtype.sml"), ("HOLsexp_parser", "src/portableML/HOLsexp_parser.sml"), ("ImplicitGraph", "src/portableML/ImplicitGraph.sml"), ("Int_Graph", "src/portableML/Int_Graph.sml"), ("Inttab", "src/portableML/Inttab.sml"), ("JSON", "src/portableML/json/JSON.sml"), ("JSONDecode", "src/portableML/json/JSONDecode.sml"), ("JSONErrors", "src/portableML/json/JSONErrors.sml"), ("JSONParser", "src/portableML/json/JSONParser.sml"), ("JSONSource", "src/portableML/json/JSONSource.sml"), ("JSONStreamParser", "src/portableML/json/JSONStreamParser.sml"), ("JSONUtil", "src/portableML/json/JSONUtil.sml"), ("Listener", "src/portableML/Listener.sml"), ("errormonad", "src/portableML/monads/errormonad.sml"), ("optmonad", "src/portableML/monads/optmonad.sml"), ("readermonad", "src/portableML/monads/readermonad.sml"), ("seqmonad", "src/portableML/monads/seqmonad.sml"), ("stmonad", "src/portableML/monads/stmonad.sml"), ("OldPP", "src/portableML/OldPP.sml"), ("PEGParse", "src/portableML/PEGParse.sml"), ("PIntMap", "src/portableML/PIntMap.sml"), ("Arbintcore", "src/portableML/poly/Arbintcore.sml"), ("Arbnumcore", "src/portableML/poly/Arbnumcore.sml"), ("ConcIsaLib", "src/portableML/poly/ConcIsaLib.sml"), ("Event_Timer", "src/portableML/poly/concurrent/Event_Timer.sml"), ("Future", "src/portableML/poly/concurrent/Future.sml"), ("Parmap", "src/portableML/poly/concurrent/Parmap.sml"), ("poly_decide_threadcount", "src/portableML/poly/concurrent/poly_decide_threadcount.sml"), ("Sref", "src/portableML/poly/concurrent/Sref.sml"), ("Task_Queue", "src/portableML/poly/concurrent/Task_Queue.sml"), ("Timeout", "src/portableML/poly/concurrent/Timeout.sml"), ("CoreReplVARS", "src/portableML/poly/CoreReplVARS.sml"), ("Counter", "src/portableML/poly/Counter.sml"), ("Dynarray", "src/portableML/poly/Dynarray.sml"), ("Exn", "src/portableML/poly/Exn.sml"), ("Intmap", "src/portableML/poly/Intmap.sml"), ("Intset", "src/portableML/poly/Intset.sml"), ("MD5", "src/portableML/poly/MD5.sml"), ("MLSYSPortable", "src/portableML/poly/MLSYSPortable.sml"), ("Multithreading", "src/portableML/poly/Multithreading.sml"), ("Par_Exn", "src/portableML/poly/Par_Exn.sml"), ("PrettyImpl", "src/portableML/poly/PrettyImpl.sml"), ("Random", "src/portableML/poly/Random.sml"), ("SHA1_ML", "src/portableML/poly/SHA1_ML.sml"), ("Single_Assignment", "src/portableML/poly/Single_Assignment.sml"), ("Standard_Thread", "src/portableML/poly/Standard_Thread.sml"), ("Susp", "src/portableML/poly/Susp.sml"), ("Synchronized", "src/portableML/poly/Synchronized.sml"), ("Thread_Attributes", "src/portableML/poly/Thread_Attributes.sml"), ("Thread_Data", "src/portableML/poly/Thread_Data.sml"), ("Unsynchronized", "src/portableML/poly/Unsynchronized.sml"), ("Portable", "src/portableML/Portable.sml"), ("Profile", "src/portableML/Profile.sml"), ("quotation_dtype", "src/portableML/quotation_dtype.sml"), ("RawTheory_dtype", "src/portableML/rawtheory/RawTheory_dtype.sml"), ("RawTheoryReader", "src/portableML/rawtheory/RawTheoryReader.sml"), ("Redblackmap", "src/portableML/Redblackmap.sml"), ("Redblackset", "src/portableML/Redblackset.sml"), ("seq", "src/portableML/seq.sml"), ("SHA1", "src/portableML/SHA1.sml"), ("smpp", "src/portableML/smpp.sml"), ("Streams", "src/portableML/Streams.sml"), ("SymGraph", "src/portableML/SymGraph.sml"), ("Symreltab", "src/portableML/Symreltab.sml"), ("Symtab", "src/portableML/Symtab.sml"), ("Table", "src/portableML/Table.sml"), ("UC_ASCII_Encode", "src/portableML/UC_ASCII_Encode.sml"), ("UnicodeChars", "src/portableML/UnicodeChars.sml"), ("UniversalType", "src/portableML/UniversalType.sml"), ("Uref", "src/portableML/Uref.sml"), ("UTF8", "src/portableML/UTF8.sml"), ("UTF8Set", "src/portableML/UTF8Set.sml"), ("DB", "src/postkernel/DB.sml"), ("DB_dtype", "src/postkernel/DB_dtype.sml"), ("DBSearchParser", "src/postkernel/DBSearchParser.sml"), ("HolKernel", "src/postkernel/HolKernel.sml"), ("SharingTables", "src/postkernel/SharingTables.sml"), ("Termtab", "src/postkernel/Termtab.sml"), ("Theory", "src/postkernel/Theory.sml"), ("TheoryDelta", "src/postkernel/TheoryDelta.sml"), ("TheoryGraph", "src/postkernel/TheoryGraph.sml"), ("TheoryPP", "src/postkernel/TheoryPP.sml"), ("TheoryReader", "src/postkernel/TheoryReader.sml"), ("ThmKind_dtype", "src/postkernel/ThmKind_dtype.sml"), ("ThyDataSexp", "src/postkernel/ThyDataSexp.sml"), ("hurdUtils", "src/pred_set/src/hurdUtils.sml"), ("countable_typesLib", "src/pred_set/src/more_theories/countable_typesLib.sml"), ("PFset_conv", "src/pred_set/src/PFset_conv.sml"), ("PGspec", "src/pred_set/src/PGspec.sml"), ("pred_setLib", "src/pred_set/src/pred_setLib.sml"), ("pred_setpp", "src/pred_set/src/pred_setpp.sml"), ("pred_setSimps", "src/pred_set/src/pred_setSimps.sml"), ("pred_setSyntax", "src/pred_set/src/pred_setSyntax.sml"), ("PSet_ind", "src/pred_set/src/PSet_ind.sml"), ("Coding", "src/prekernel/Coding.sml"), ("Count", "src/prekernel/Count.sml"), ("Dep", "src/prekernel/Dep.sml"), ("Feedback", "src/prekernel/Feedback.sml"), ("Globals", "src/prekernel/Globals.sml"), ("KNametab", "src/prekernel/KNametab.sml"), ("Lexis", "src/prekernel/Lexis.sml"), ("Lib", "src/prekernel/Lib.sml"), ("locn", "src/prekernel/locn.sml"), ("Nonce", "src/prekernel/Nonce.sml"), ("stringfindreplace", "src/prekernel/stringfindreplace.sml"), ("Tag", "src/prekernel/Tag.sml"), ("extrealSimps", "src/probability/extrealSimps.sml"), ("goalStack", "src/proofman/goalStack.sml"), ("goalTree", "src/proofman/goalTree.sml"), ("History", "src/proofman/History.sml"), ("Manager", "src/proofman/Manager.sml"), ("proofManagerLib", "src/proofman/proofManagerLib.sml"), ("OldAbbrevTactics", "src/q/OldAbbrevTactics.sml"), ("Q", "src/q/Q.sml"), ("QLib", "src/q/QLib.sml"), ("quantHeuristicsLib", "src/quantHeuristics/quantHeuristicsLib.sml"), ("quantHeuristicsLibAbbrev", "src/quantHeuristics/quantHeuristicsLibAbbrev.sml"), ("quantHeuristicsLibBase", "src/quantHeuristics/quantHeuristicsLibBase.sml"), ("quantHeuristicsLibFunRemove", "src/quantHeuristics/quantHeuristicsLibFunRemove.sml"), ("quantHeuristicsLibParameters", "src/quantHeuristics/quantHeuristicsLibParameters.sml"), ("quantHeuristicsLibSimple", "src/quantHeuristics/quantHeuristicsLibSimple.sml"), ("quantHeuristicsTools", "src/quantHeuristics/quantHeuristicsTools.sml"), ("quotient", "src/quotient/src/quotient.sml"), ("quotientLib", "src/quotient/src/quotientLib.sml"), ("fracLib", "src/rational/fracLib.sml"), ("fracSyntax", "src/rational/fracSyntax.sml"), ("fracUtils", "src/rational/fracUtils.sml"), ("intExtensionLib", "src/rational/intExtensionLib.sml"), ("ratLib", "src/rational/ratLib.sml"), ("ratPP", "src/rational/ratPP.sml"), ("ratReduce", "src/rational/ratReduce.sml"), ("ratRingLib", "src/rational/ratRingLib.sml"), ("ratSyntax", "src/rational/ratSyntax.sml"), ("ratUtils", "src/rational/ratUtils.sml"), ("schneiderUtils", "src/rational/schneiderUtils.sml"), ("complexPP", "src/real/analysis/complexPP.sml"), ("Diff", "src/real/analysis/Diff.sml"), ("bitArithLib", "src/real/bitArithLib.sml"), ("intrealSyntax", "src/real/intrealSyntax.sml"), ("isqrtLib", "src/real/isqrtLib.sml"), ("RealArith", "src/real/RealArith.sml"), ("RealField", "src/real/RealField.sml"), ("realLib", "src/real/realLib.sml"), ("realPP", "src/real/realPP.sml"), ("realSimps", "src/real/realSimps.sml"), ("realSyntax", "src/real/realSyntax.sml"), ("AC", "src/refute/AC.sml"), ("Canon", "src/refute/Canon.sml"), ("refuteLib", "src/refute/refuteLib.sml"), ("relationSyntax", "src/relation/relationSyntax.sml"), ("Cond_rewrite", "src/res_quan/src/Cond_rewrite.sml"), ("jrhUtils", "src/res_quan/src/jrhUtils.sml"), ("res_quanLib", "src/res_quan/src/res_quanLib.sml"), ("res_quanTools", "src/res_quan/src/res_quanTools.sml"), ("abs_tools", "src/ring/src/abs_tools.sml"), ("abstraction", "src/ring/src/abstraction.sml"), ("EVAL_numRingLib", "src/ring/src/EVAL_numRingLib.sml"), ("EVAL_quote", "src/ring/src/EVAL_quote.sml"), ("EVAL_ringLib", "src/ring/src/EVAL_ringLib.sml"), ("BackchainingLib", "src/simp/src/BackchainingLib.sml"), ("boolSimps", "src/simp/src/boolSimps.sml"), ("Cache", "src/simp/src/Cache.sml"), ("combinSimps", "src/simp/src/combinSimps.sml"), ("Cond_rewr", "src/simp/src/Cond_rewr.sml"), ("congLib", "src/simp/src/congLib.sml"), ("Opening", "src/simp/src/Opening.sml"), ("pureSimps", "src/simp/src/pureSimps.sml"), ("Satisfy", "src/simp/src/Satisfy.sml"), ("SatisfySimps", "src/simp/src/SatisfySimps.sml"), ("Sequence", "src/simp/src/Sequence.sml"), ("simpLib", "src/simp/src/simpLib.sml"), ("Trace", "src/simp/src/Trace.sml"), ("Traverse", "src/simp/src/Traverse.sml"), ("Travrules", "src/simp/src/Travrules.sml"), ("Unify", "src/simp/src/Unify.sml"), ("Unwind", "src/simp/src/Unwind.sml"), ("permLib", "src/sort/permLib.sml"), ("sortingLib", "src/sort/sortingLib.sml"), ("sortingSyntax", "src/sort/sortingSyntax.sml"), ("ASCIInumbersLib", "src/string/ASCIInumbersLib.sml"), ("ASCIInumbersSyntax", "src/string/ASCIInumbersSyntax.sml"), ("stringLib", "src/string/stringLib.sml"), ("stringSimps", "src/string/stringSimps.sml"), ("stringSyntax", "src/string/stringSyntax.sml"), ("tacticToe", "src/tactictoe/src/tacticToe.sml"), ("tttEval", "src/tactictoe/src/tttEval.sml"), ("tttLearn", "src/tactictoe/src/tttLearn.sml"), ("tttRecord", "src/tactictoe/src/tttRecord.sml"), ("tttSearch", "src/tactictoe/src/tttSearch.sml"), ("tttSetup", "src/tactictoe/src/tttSetup.sml"), ("tttToken", "src/tactictoe/src/tttToken.sml"), ("tttTrain", "src/tactictoe/src/tttTrain.sml"), ("tttUnfold", "src/tactictoe/src/tttUnfold.sml"), ("tautLib", "src/taut/tautLib.sml"), ("AssembleHolindexParser", "src/TeX/AssembleHolindexParser.sml"), ("EmitTeX", "src/TeX/EmitTeX.sml"), ("holindex", "src/TeX/holindex.sml"), ("holindexData", "src/TeX/holindexData.sml"), ("mkmkcline", "src/TeX/mkmkcline.sml"), ("mkmkmunge", "src/TeX/mkmkmunge.sml"), ("mkmunger", "src/TeX/mkmunger.sml"), ("mungeTools", "src/TeX/mungeTools.sml"), ("warning_stream", "src/TeX/warning_stream.sml"), ("Defn", "src/tfl/src/Defn.sml"), ("Extract", "src/tfl/src/Extract.sml"), ("Induction", "src/tfl/src/Induction.sml"), ("Rules", "src/tfl/src/Rules.sml"), ("wfrecUtils", "src/tfl/src/wfrecUtils.sml"), ("Compute", "src/thm/Compute.sml"), ("Overlay", "src/thm/Overlay.sml"), ("Thm", "src/thm/Thm.sml"), ("liftLib", "src/transfer/liftLib.sml"), ("transferLib", "src/transfer/transferLib.sml"), ("unwindLib", "src/unwind/unwindLib.sml"), ("updateSyntax", "src/update/updateSyntax.sml")]; fun maybeWriteStderr s = (TextIO.output(TextIO.stdErr, s ^ "\n"); TextIO.flushOut TextIO.stdErr); fun die s = (maybeWriteStderr s; raise Fail s) fun warn s = maybeWriteStderr ("WARNING: " ^ s) val meta_debug = ref true fun MDBG s = if !meta_debug then TextIO.print("META_DEBUG: " ^ s() ^ "\n") else () infix ++ fun p1 ++ p2 = OS.Path.concat (p1, p2) open Systeml structure HFS = HOLFileSys val loadpathdb = ref (Binarymap.mkDict String.compare : (string,string) Binarymap.dict) exception CalledProve; val called = ref false; val results = ref ([]:string list); val loadedMods = ref (Binaryset.empty String.compare); fun quse s = let val _ = if HFS.access (s, [HFS.A_READ]) then () else die ("Use: non-existent file "^s) val _ = MDBG (fn _ => "Call quse " ^ s ^ " (total " ^ Int.toString (Binaryset.numItems (!loadedMods)) ^ ")") val full = OS.Path.mkCanonical (OS.Path.mkAbsolute{path = s, relativeTo = HFS.getDir()}) in called := false; set_prover (fn (t, _) => (called := true; mk_oracle_thm "fast_proof" ([], t))); time QUse.use s; if !called then (warn ("CALLING PROVE: "^s^"\n"); results := s :: !results) else (); loadpathdb := Binarymap.insert(!loadpathdb,OS.Path.file full,OS.Path.dir full) end handle OS.Path.Path => die ("Path exception in quse "^s) | e => ( if !called then (warn ("CALLING PROVE: "^s^"\n"); results := s :: !results) else (); maybeWriteStderr("error in quse " ^ s ^ " : " ^ General.exnMessage e); PolyML.Exception.reraise e) fun myuse f = let val op ++ = OS.Path.concat val file = OS.Path.file f val pd = !PolyML.Compiler.printDepth in PolyML.print_depth 0; (quse f handle e => (PolyML.print_depth pd; PolyML.Exception.reraise e)); PolyML.print_depth pd end handle OS.Path.Path => die ("Path exception in myuse "^f) val loadPath : string list ref = ref [OS.Path.concat(HOLDIR, "sigobj")]; val _ = loadedMods := Binaryset.addList (!loadedMods, Meta.loaded ()) fun findUo modPath [] = NONE | findUo modPath (search::rest) = let val path = OS.Path.mkAbsolute {path = modPath, relativeTo = OS.Path.mkAbsolute {path=search, relativeTo = HFS.getDir ()}}; in if HFS.access (path, []) then SOME path else findUo modPath rest end; val _ = holpathdb.extend_db {vname = "HOLDIR", path = Systeml.HOLDIR} fun loadUo ps uo = let val i = HFS.openIn uo val files = String.tokens (fn c => c = #"\n") (HFS.inputAll i) val _ = HFS.closeIn i fun str f = ">" ^ f ^ "< -- " ^ String.concatWith " -- " ps fun loadOne f = (case OS.Path.ext f of SOME "sml" => myuse (holpathdb.subst_pathvars f) | SOME "sig" => myuse (holpathdb.subst_pathvars f) | _ => load (uo::ps) f) handle OS.Path.InvalidArc => die ("Invalid arc exception in loading "^str f) | OS.Path.Path => die ("Path exception in loading "^str f) | OS.SysErr(msg,_) => die ("System error '"^msg^"' in loading "^str f) in List.app loadOne files end and load ps modPath = let val _ = MDBG (fn _ => "Call load " ^ modPath) val modPath = holpathdb.subst_pathvars modPath val modName = OS.Path.file modPath fun l ext = case findUo (modPath ^ ext) ("."::(!loadPath)) of NONE => die ("Cannot find file " ^ modPath ^ ext) | SOME uo => loadUo ps uo in if Binaryset.member (!loadedMods, modName) then () else (loadedMods := Binaryset.add (!loadedMods, modName); (l ".ui"; l ".uo") handle e => ( (* loadedMods := Binaryset.delete (!loadedMods, modName); *) PolyML.Exception.reraise e)) end handle e => ( maybeWriteStderr("error in load " ^ modPath ^ " : " ^ General.exnMessage e); PolyML.Exception.reraise e) val _ = app (fn (a, b) => (( warn ("load "^a); (load [] a handle _ => ())))) ls; val _ = app (fn a => warn ("CALLED PROVE: "^a^"\n")) (!results);