Created
April 8, 2025 13:42
-
-
Save digama0/a092e6339371f6c44da2a2057f03efdf to your computer and use it in GitHub Desktop.
HOL4 script: find lib files that call `prove`
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 characters
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