Skip to content

Instantly share code, notes, and snippets.

@digama0

digama0/test.sml

Created April 8, 2025 13:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save digama0/a092e6339371f6c44da2a2057f03efdf to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save digama0/a092e6339371f6c44da2a2057f03efdf to your computer and use it in GitHub Desktop.
Download ZIP
HOL4 script: find lib files that call `prove`
Raw
test.sml
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);
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment