diff --git a/src/HOL/Tools/sat_solver.ML b/src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML +++ b/src/HOL/Tools/sat_solver.ML @@ -1,1033 +1,1033 @@ (* Title: HOL/Tools/sat_solver.ML Author: Tjark Weber Copyright 2004-2009 Interface to external SAT solvers, and (simple) built-in SAT solvers. Relevant Isabelle environment settings: # MiniSat 1.14 #MINISAT_HOME=/usr/local/bin # zChaff #ZCHAFF_HOME=/usr/local/bin # BerkMin561 #BERKMIN_HOME=/usr/local/bin #BERKMIN_EXE=BerkMin561-linux #BERKMIN_EXE=BerkMin561-solaris # Jerusat 1.3 #JERUSAT_HOME=/usr/local/bin *) signature SAT_SOLVER = sig exception NOT_CONFIGURED type assignment = int -> bool option type proof = int list Inttab.table * int datatype result = SATISFIABLE of assignment | UNSATISFIABLE of proof option | UNKNOWN type solver = Prop_Logic.prop_formula -> result (* auxiliary functions to create external SAT solvers *) val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit val read_std_result_file : Path.T -> string * string * string -> result val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) -> (unit -> result) -> solver val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula (* generic solver interface *) val get_solvers : unit -> (string * solver) list val add_solver : string * solver -> unit val invoke_solver : string -> solver (* exception Option *) end; structure SAT_Solver : SAT_SOLVER = struct open Prop_Logic; (* ------------------------------------------------------------------------- *) (* should be raised by an external SAT solver to indicate that the solver is *) (* not configured properly *) (* ------------------------------------------------------------------------- *) exception NOT_CONFIGURED; (* ------------------------------------------------------------------------- *) (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is *) (* a satisfying assignment regardless of the value of variable 'i' *) (* ------------------------------------------------------------------------- *) type assignment = int -> bool option; (* ------------------------------------------------------------------------- *) (* a proof of unsatisfiability, to be interpreted as follows: each integer *) (* is a clause ID, each list 'xs' stored under the key 'x' in the table *) (* contains the IDs of clauses that must be resolved (in the given *) (* order) to obtain the new clause 'x'. Each list 'xs' must be *) (* non-empty, and the literal to be resolved upon must always be unique *) (* (e.g. "A | ~B" must not be resolved with "~A | B"). Circular *) (* dependencies of clauses are not allowed. (At least) one of the *) (* clauses in the table must be the empty clause (i.e. contain no *) (* literals); its ID is given by the second component of the proof. *) (* The clauses of the original problem passed to the SAT solver have *) (* consecutive IDs starting with 0. Clause IDs must be non-negative, *) (* but do not need to be consecutive. *) (* ------------------------------------------------------------------------- *) type proof = int list Inttab.table * int; (* ------------------------------------------------------------------------- *) (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) (* assignment must be returned as well; if the result is *) (* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) (* ------------------------------------------------------------------------- *) datatype result = SATISFIABLE of assignment | UNSATISFIABLE of proof option | UNKNOWN; (* ------------------------------------------------------------------------- *) (* type of SAT solvers: given a propositional formula, a satisfying *) (* assignment may be returned *) (* ------------------------------------------------------------------------- *) type solver = prop_formula -> result; (* ------------------------------------------------------------------------- *) (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) (* to a file in DIMACS CNF format (see "Satisfiability Suggested *) (* Format", May 8 1993, Section 2.1) *) (* Note: 'fm' must not contain a variable index less than 1. *) (* Note: 'fm' must be given in CNF. *) (* ------------------------------------------------------------------------- *) fun write_dimacs_cnf_file path fm = let fun cnf_True_False_elim True = Or (BoolVar 1, Not (BoolVar 1)) | cnf_True_False_elim False = And (BoolVar 1, Not (BoolVar 1)) | cnf_True_False_elim fm = fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) fun cnf_number_of_clauses (And (fm1, fm2)) = (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) | cnf_number_of_clauses _ = 1 fun write_cnf_file out = let fun write_formula True = error "formula is not in CNF" | write_formula False = error "formula is not in CNF" | write_formula (BoolVar i) = (i>=1 orelse error "formula contains a variable index less than 1"; - File.output out (string_of_int i)) + File_Stream.output out (string_of_int i)) | write_formula (Not (BoolVar i)) = - (File.output out "-"; + (File_Stream.output out "-"; write_formula (BoolVar i)) | write_formula (Not _) = error "formula is not in CNF" | write_formula (Or (fm1, fm2)) = (write_formula fm1; - File.output out " "; + File_Stream.output out " "; write_formula fm2) | write_formula (And (fm1, fm2)) = (write_formula fm1; - File.output out " 0\n"; + File_Stream.output out " 0\n"; write_formula fm2) val fm' = cnf_True_False_elim fm val number_of_vars = maxidx fm' val number_of_clauses = cnf_number_of_clauses fm' in - File.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n"; - File.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^ + File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n"; + File_Stream.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); write_formula fm'; - File.output out " 0\n" + File_Stream.output out " 0\n" end in - File.open_output write_cnf_file path + File_Stream.open_output write_cnf_file path end; (* ------------------------------------------------------------------------- *) (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) (* Format", May 8 1993, Section 2.2) *) (* Note: 'fm' must not contain a variable index less than 1. *) (* ------------------------------------------------------------------------- *) fun write_dimacs_sat_file path fm = let fun write_sat_file out = let fun write_formula True = - File.output out "*()" + File_Stream.output out "*()" | write_formula False = - File.output out "+()" + File_Stream.output out "+()" | write_formula (BoolVar i) = (i>=1 orelse error "formula contains a variable index less than 1"; - File.output out (string_of_int i)) + File_Stream.output out (string_of_int i)) | write_formula (Not (BoolVar i)) = - (File.output out "-"; + (File_Stream.output out "-"; write_formula (BoolVar i)) | write_formula (Not fm) = - (File.output out "-("; + (File_Stream.output out "-("; write_formula fm; - File.output out ")") + File_Stream.output out ")") | write_formula (Or (fm1, fm2)) = - (File.output out "+("; + (File_Stream.output out "+("; write_formula_or fm1; - File.output out " "; + File_Stream.output out " "; write_formula_or fm2; - File.output out ")") + File_Stream.output out ")") | write_formula (And (fm1, fm2)) = - (File.output out "*("; + (File_Stream.output out "*("; write_formula_and fm1; - File.output out " "; + File_Stream.output out " "; write_formula_and fm2; - File.output out ")") + File_Stream.output out ")") (* optimization to make use of n-ary disjunction/conjunction *) and write_formula_or (Or (fm1, fm2)) = (write_formula_or fm1; - File.output out " "; + File_Stream.output out " "; write_formula_or fm2) | write_formula_or fm = write_formula fm and write_formula_and (And (fm1, fm2)) = (write_formula_and fm1; - File.output out " "; + File_Stream.output out " "; write_formula_and fm2) | write_formula_and fm = write_formula fm val number_of_vars = Int.max (maxidx fm, 1) in - File.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n"; - File.output out ("p sat " ^ string_of_int number_of_vars ^ "\n"); - File.output out "("; + File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n"; + File_Stream.output out ("p sat " ^ string_of_int number_of_vars ^ "\n"); + File_Stream.output out "("; write_formula fm; - File.output out ")\n" + File_Stream.output out ")\n" end in - File.open_output write_sat_file path + File_Stream.open_output write_sat_file path end; (* ------------------------------------------------------------------------- *) (* read_std_result_file: scans a SAT solver's output file for a satisfying *) (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) (* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *) (* neither 'satisfiable' nor 'unsatisfiable'. Empty lines are ignored. *) (* The assignment must be given in one or more lines immediately after *) (* the line that contains 'satisfiable'. These lines must begin with *) (* 'assignment_prefix'. Variables must be separated by " ". Non- *) (* integer strings are ignored. If variable i is contained in the *) (* assignment, then i is interpreted as 'true'. If ~i is contained in *) (* the assignment, then i is interpreted as 'false'. Otherwise the *) (* value of i is taken to be unspecified. *) (* ------------------------------------------------------------------------- *) fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = let fun int_list_from_string s = map_filter Int.fromString (space_explode " " s) fun assignment_from_list [] i = NONE (* the SAT solver didn't provide a value for this variable *) | assignment_from_list (x::xs) i = if x=i then (SOME true) else if x=(~i) then (SOME false) else assignment_from_list xs i fun parse_assignment xs [] = assignment_from_list xs | parse_assignment xs (line::lines) = if String.isPrefix assignment_prefix line then parse_assignment (xs @ int_list_from_string line) lines else assignment_from_list xs fun is_substring needle haystack = let val length1 = String.size needle val length2 = String.size haystack in if length2 < length1 then false else if needle = String.substring (haystack, 0, length1) then true else is_substring needle (String.substring (haystack, 1, length2-1)) end fun parse_lines [] = UNKNOWN | parse_lines (line::lines) = if is_substring unsatisfiable line then UNSATISFIABLE NONE else if is_substring satisfiable line then SATISFIABLE (parse_assignment [] lines) else parse_lines lines in (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path end; (* ------------------------------------------------------------------------- *) (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) (* ------------------------------------------------------------------------- *) fun make_external_solver cmd writefn readfn fm = (writefn fm; Isabelle_System.bash cmd; readfn ()); (* ------------------------------------------------------------------------- *) (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *) (* a SAT problem given in DIMACS CNF format *) (* ------------------------------------------------------------------------- *) fun read_dimacs_cnf_file path = let fun filter_preamble [] = error "problem line not found in DIMACS CNF file" | filter_preamble (line::lines) = if String.isPrefix "c " line orelse line = "c" then (* ignore comments *) filter_preamble lines else if String.isPrefix "p " line then (* ignore the problem line (which must be the last line of the preamble) *) (* Ignoring the problem line implies that if the file contains more clauses *) (* or variables than specified in its preamble, we will accept it anyway. *) lines else error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" fun int_from_string s = case Int.fromString s of SOME i => i | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number") fun clauses xs = let val (xs1, xs2) = chop_prefix (fn i => i <> 0) xs in case xs2 of [] => [xs1] | (0::[]) => [xs1] | (0::tl) => xs1 :: clauses tl | _ => raise Fail "SAT_Solver.clauses" end fun literal_from_int i = (i<>0 orelse error "variable index in DIMACS CNF file is 0"; if i>0 then Prop_Logic.BoolVar i else Prop_Logic.Not (Prop_Logic.BoolVar (~i))) fun disjunction [] = error "empty clause in DIMACS CNF file" | disjunction (x::xs) = (case xs of [] => x | _ => Prop_Logic.Or (x, disjunction xs)) fun conjunction [] = error "no clause in DIMACS CNF file" | conjunction (x::xs) = (case xs of [] => x | _ => Prop_Logic.And (x, conjunction xs)) in (conjunction o (map disjunction) o (map (map literal_from_int)) o clauses o (map int_from_string) o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"]))) o filter_preamble o filter (fn l => l <> "") o split_lines o File.read) path end; (* ------------------------------------------------------------------------- *) (* solvers: a table of all registered SAT solvers *) (* ------------------------------------------------------------------------- *) val solvers = Synchronized.var "solvers" ([] : (string * solver) list); fun get_solvers () = Synchronized.value solvers; (* ------------------------------------------------------------------------- *) (* add_solver: updates 'solvers' by adding a new solver *) (* ------------------------------------------------------------------------- *) fun add_solver (name, new_solver) = Synchronized.change solvers (fn the_solvers => let val _ = if AList.defined (op =) the_solvers name then warning ("SAT solver " ^ quote name ^ " was defined before") else (); in AList.update (op =) (name, new_solver) the_solvers end); (* ------------------------------------------------------------------------- *) (* invoke_solver: returns the solver associated with the given 'name' *) (* Note: If no solver is associated with 'name', exception 'Option' will be *) (* raised. *) (* ------------------------------------------------------------------------- *) fun invoke_solver name = the (AList.lookup (op =) (get_solvers ()) name); end; (* SAT_Solver *) (* ------------------------------------------------------------------------- *) (* Predefined SAT solvers *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Internal SAT solver, available as 'SAT_Solver.invoke_solver "cdclite"' -- *) (* a simplified implementation of the conflict-driven clause-learning *) (* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean *) (* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models *) (* and proof traces. *) (* ------------------------------------------------------------------------- *) let type clause = int list * int type value = bool option datatype reason = Decided | Implied of clause | Level0 of int type variable = bool option * reason * int * int type proofs = int * int list Inttab.table type state = int * int list * variable Inttab.table * clause list Inttab.table * proofs exception CONFLICT of clause * state exception UNSAT of clause * state fun neg i = ~i fun lit_value lit value = if lit > 0 then value else Option.map not value fun var_of vars lit: variable = the (Inttab.lookup vars (abs lit)) fun value_of vars lit = lit_value lit (#1 (var_of vars lit)) fun reason_of vars lit = #2 (var_of vars lit) fun level_of vars lit = #3 (var_of vars lit) fun is_true vars lit = (value_of vars lit = SOME true) fun is_false vars lit = (value_of vars lit = SOME false) fun is_unassigned vars lit = (value_of vars lit = NONE) fun assignment_of vars lit = the_default NONE (try (value_of vars) lit) fun put_var value reason level (_, _, _, rank) = (value, reason, level, rank) fun incr_rank (value, reason, level, rank) = (value, reason, level, rank + 1) fun update_var lit f = Inttab.map_entry (abs lit) f fun add_var lit = Inttab.update (abs lit, (NONE, Decided, ~1, 0)) fun assign lit r l = update_var lit (put_var (SOME (lit > 0)) r l) fun unassign lit = update_var lit (put_var NONE Decided ~1) fun add_proof [] (idx, ptab) = (idx, (idx + 1, ptab)) | add_proof ps (idx, ptab) = (idx, (idx + 1, Inttab.update (idx, ps) ptab)) fun level0_proof_of (Level0 idx) = SOME idx | level0_proof_of _ = NONE fun level0_proofs_of vars = map_filter (level0_proof_of o reason_of vars) fun prems_of vars (lits, p) = p :: level0_proofs_of vars lits fun mk_proof vars cls proofs = add_proof (prems_of vars cls) proofs fun push lit cls (level, trail, vars, clss, proofs) = let val (reason, proofs) = if level = 0 then apfst Level0 (mk_proof vars cls proofs) else (Implied cls, proofs) in (level, lit :: trail, assign lit reason level vars, clss, proofs) end fun push_decided lit (level, trail, vars, clss, proofs) = let val vars' = assign lit Decided (level + 1) vars in (level + 1, lit :: 0 :: trail, vars', clss, proofs) end fun prop (cls as (lits, _)) (cx as (units, state as (level, _, vars, _, _))) = if exists (is_true vars) lits then cx else if forall (is_false vars) lits then if level = 0 then raise UNSAT (cls, state) else raise CONFLICT (cls, state) else (case filter (is_unassigned vars) lits of [lit] => (lit :: units, push lit cls state) | _ => cx) fun propagate units (state as (_, _, _, clss, _)) = (case fold (fold prop o Inttab.lookup_list clss) units ([], state) of ([], state') => (NONE, state') | (units', state') => propagate units' state') handle CONFLICT (cls, state') => (SOME cls, state') fun max_unassigned (v, (NONE, _, _, rank)) (x as (_, r)) = if rank > r then (SOME v, rank) else x | max_unassigned _ x = x fun decide (state as (_, _, vars, _, _)) = (case Inttab.fold max_unassigned vars (NONE, 0) of (SOME lit, _) => SOME (lit, push_decided lit state) | (NONE, _) => NONE) fun mark lit = Inttab.update (abs lit, true) fun marked ms lit = the_default false (Inttab.lookup ms (abs lit)) fun ignore l ms lit = ((lit = l) orelse marked ms lit) fun first_lit _ [] = raise Empty | first_lit _ (0 :: _) = raise Empty | first_lit pred (lit :: lits) = if pred lit then (lit, lits) else first_lit pred lits fun reason_cls_of vars lit = (case reason_of vars lit of Implied cls => cls | _ => raise Option) fun analyze conflicting_cls (level, trail, vars, _, _) = let fun back i lit (lits, p) trail ms ls ps = let val (lits0, lits') = List.partition (equal 0 o level_of vars) lits val lits1 = filter_out (ignore lit ms) lits' val lits2 = filter_out (equal level o level_of vars) lits1 val i' = length lits1 - length lits2 + i val ms' = fold mark lits1 ms val ls' = lits2 @ ls val ps' = level0_proofs_of vars lits0 @ (p :: ps) val (lit', trail') = first_lit (marked ms') trail in if i' = 1 then (neg lit', ls', rev ps') else back (i' - 1) lit' (reason_cls_of vars lit') trail' ms' ls' ps' end in back 0 0 conflicting_cls trail Inttab.empty [] [] end fun keep_clause (cls as (lits, _)) (level, trail, vars, clss, proofs) = let val vars' = fold (fn lit => update_var lit incr_rank) lits vars val clss' = fold (fn lit => Inttab.cons_list (neg lit, cls)) lits clss in (level, trail, vars', clss', proofs) end fun learn (cls as (lits, _)) = (length lits <= 2) ? keep_clause cls fun backjump _ (state as (_, [], _, _, _)) = state | backjump i (level, 0 :: trail, vars, clss, proofs) = (level - 1, trail, vars, clss, proofs) |> (i > 1) ? backjump (i - 1) | backjump i (level, lit :: trail, vars, clss, proofs) = backjump i (level, trail, unassign lit vars, clss, proofs) fun search units state = (case propagate units state of (NONE, state' as (_, _, vars, _, _)) => (case decide state' of NONE => SAT_Solver.SATISFIABLE (assignment_of vars) | SOME (lit, state'') => search [lit] state'') | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) => let val (lit, lits, ps) = analyze conflicting_cls state' val (idx, proofs') = add_proof ps proofs val cls = (lit :: lits, idx) in (level, trail, vars, clss, proofs') |> backjump (level - fold (Integer.max o level_of vars) lits 0) |> learn cls |> push lit cls |> search [lit] end) fun has_opposing_lits [] = false | has_opposing_lits (lit :: lits) = member (op =) lits (neg lit) orelse has_opposing_lits lits fun add_clause (cls as ([_], _)) (units, state) = let val (units', state') = prop cls (units, state) in (units', state') end | add_clause (cls as (lits, _)) (cx as (units, state)) = if has_opposing_lits lits then cx else (units, keep_clause cls state) fun mk_clause lits proofs = apfst (pair (distinct (op =) lits)) (add_proof [] proofs) fun solve litss = let val (clss, proofs) = fold_map mk_clause litss (0, Inttab.empty) val vars = fold (fold add_var) litss Inttab.empty val state = (0, [], vars, Inttab.empty, proofs) in uncurry search (fold add_clause clss ([], state)) end handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) => let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs in SAT_Solver.UNSATISFIABLE (SOME (ptab, idx)) end fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable" | variable_of (Prop_Logic.BoolVar i) = i | variable_of _ = error "expected formula in CNF" fun literal_of (Prop_Logic.Not fm) = neg (variable_of fm) | literal_of fm = variable_of fm fun clause_of (Prop_Logic.Or (fm1, fm2)) = clause_of fm1 @ clause_of fm2 | clause_of fm = [literal_of fm] fun clauses_of (Prop_Logic.And (fm1, fm2)) = clauses_of fm1 @ clauses_of fm2 | clauses_of Prop_Logic.True = [[1, ~1]] | clauses_of Prop_Logic.False = [[1], [~1]] | clauses_of fm = [clause_of fm] fun dpll_solver fm = let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm in solve (clauses_of fm') end in SAT_Solver.add_solver ("cdclite", dpll_solver) end; (* ------------------------------------------------------------------------- *) (* Internal SAT solver, available as 'SAT_Solver.invoke_solver "auto"': uses *) (* the last installed solver (other than "auto" itself) that does not raise *) (* 'NOT_CONFIGURED'. (However, the solver may return 'UNKNOWN'.) *) (* ------------------------------------------------------------------------- *) let fun auto_solver fm = let fun loop [] = SAT_Solver.UNKNOWN | loop ((name, solver)::solvers) = if name="auto" then (* do not call solver "auto" from within "auto" *) loop solvers else ( (* apply 'solver' to 'fm' *) solver fm handle SAT_Solver.NOT_CONFIGURED => loop solvers ) in loop (SAT_Solver.get_solvers ()) end in SAT_Solver.add_solver ("auto", auto_solver) end; (* ------------------------------------------------------------------------- *) (* MiniSat 1.14 *) (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *) (* Matthews, which can output ASCII proof traces. Replaying binary proof *) (* traces generated by MiniSat-p_v1.14 has _not_ been implemented. *) (* ------------------------------------------------------------------------- *) (* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *) (* that the latter is preferred by the "auto" solver *) (* There is a complication that is dealt with in the code below: MiniSat *) (* introduces IDs for original clauses in the proof trace. It does not (in *) (* general) follow the convention that the original clauses are numbered *) (* from 0 to n-1 (where n is the number of clauses in the formula). *) let exception INVALID_PROOF of string fun minisat_with_proofs fm = let val _ = if (getenv "MINISAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf")) val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " -t " ^ File.bash_path proofpath ^ "> /dev/null" fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val cnf = Prop_Logic.defcnf fm val result = SAT_Solver.make_external_solver cmd writefn readfn cnf val _ = try File.rm inpath val _ = try File.rm outpath in case result of SAT_Solver.UNSATISFIABLE NONE => (let val proof_lines = (split_lines o File.read) proofpath handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" (* representation of clauses as ordered lists of literals (with duplicates removed) *) fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) = Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) | clause_to_lit_list (Prop_Logic.BoolVar i) = [i] | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) = [~i] | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula." fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = 1 val number_of_clauses = cnf_number_of_clauses cnf (* int list array *) val clauses = Array.array (number_of_clauses, []) (* initialize the 'clauses' array *) fun init_array (Prop_Logic.And (fm1, fm2), n) = init_array (fm2, init_array (fm1, n)) | init_array (fm, n) = (Array.update (clauses, n, clause_to_lit_list fm); n+1) val _ = init_array (cnf, 0) (* optimization for the common case where MiniSat "R"s clauses in their *) (* original order: *) val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1) (* search the 'clauses' array for the given list of literals 'lits', *) (* starting at index '!last_ref_clause + 1' *) fun original_clause_id lits = let fun original_clause_id_from index = if index = number_of_clauses then (* search from beginning again *) original_clause_id_from 0 (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) (* testing for equality should suffice -- barring duplicate literals *) else if Array.sub (clauses, index) = lits then ( (* success *) last_ref_clause := index; SOME index ) else if index = !last_ref_clause then (* failure *) NONE else (* continue search *) original_clause_id_from (index + 1) in original_clause_id_from (!last_ref_clause + 1) end fun int_from_string s = (case Int.fromString s of SOME i => i | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")) (* parse the proof file *) val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) val empty_id = Unsynchronized.ref ~1 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) (* our proof format, where original clauses are numbered starting from 0 *) val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table) fun sat_to_proof id = ( case Inttab.lookup (!clause_id_map) id of SOME id' => id' | NONE => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.") ) val next_id = Unsynchronized.ref (number_of_clauses - 1) fun process_tokens [] = () | process_tokens (tok::toks) = if tok="R" then ( case toks of id::sep::lits => let val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." val cid = int_from_string id val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") val ls = sort int_ord (map int_from_string lits) val proof_id = case original_clause_id ls of SOME orig_id => orig_id | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") in (* extend the mapping of clause IDs with this newly defined ID *) clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") (* the proof itself doesn't change *) end | _ => raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." ) else if tok="C" then ( case toks of id::sep::ids => let val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." val cid = int_from_string id val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") (* ignore the pivot literals in MiniSat's trace *) fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." | unevens (x :: []) = x :: [] | unevens (x :: _ :: xs) = x :: unevens xs val rs = (map sat_to_proof o unevens o map int_from_string) ids (* extend the mapping of clause IDs with this newly defined ID *) val proof_id = Unsynchronized.inc next_id val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") in (* update clause table *) clause_table := Inttab.update_new (proof_id, rs) (!clause_table) handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") end | _ => raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." ) else if tok="D" then ( case toks of [id] => let val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." val _ = sat_to_proof (int_from_string id) in (* simply ignore "D" *) () end | _ => raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." ) else if tok="X" then ( case toks of [id1, id2] => let val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." val _ = sat_to_proof (int_from_string id1) val new_empty_id = sat_to_proof (int_from_string id2) in (* update conflict id *) empty_id := new_empty_id end | _ => raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." ) else raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") fun process_lines [] = () | process_lines (l::ls) = ( process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); process_lines ls ) (* proof *) val _ = process_lines proof_lines val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." in SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE)) | result => result end in SAT_Solver.add_solver ("minisat_with_proofs", minisat_with_proofs) end; let fun minisat fm = let val _ = if getenv "MINISAT_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = "\"$MINISAT_HOME/minisat\" " ^ File.bash_path inpath ^ " -r " ^ File.bash_path outpath ^ " > /dev/null" fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in SAT_Solver.add_solver ("minisat", minisat) end; (* ------------------------------------------------------------------------- *) (* zChaff (https://www.princeton.edu/~chaff/zchaff.html) *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if *) (* zChaff finds that the formula is unsatisfiable, a proof of this is read *) (* from a file "resolve_trace" that was generated by zChaff. See the code *) (* below for the expected format of the "resolve_trace" file. Aside from *) (* some basic syntactic checks, no verification of the proof is performed. *) (* ------------------------------------------------------------------------- *) (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so *) (* that the latter is preferred by the "auto" solver *) let exception INVALID_PROOF of string fun zchaff_with_proofs fm = case SAT_Solver.invoke_solver "zchaff" fm of SAT_Solver.UNSATISFIABLE NONE => (let (* FIXME File.tmp_path (!?) *) val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = 1 fun int_from_string s = ( case Int.fromString s of SOME i => i | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") ) (* parse the "resolve_trace" file *) val clause_offset = Unsynchronized.ref ~1 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) val empty_id = Unsynchronized.ref ~1 fun process_tokens [] = () | process_tokens (tok::toks) = if tok="CL:" then ( case toks of id::sep::ids => let val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") val cid = int_from_string id val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") val rs = map int_from_string ids in (* update clause table *) clause_table := Inttab.update_new (cid, rs) (!clause_table) handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") end | _ => raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." ) else if tok="VAR:" then ( case toks of id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => let val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") (* set 'clause_offset' to the largest used clause ID *) val _ = if !clause_offset = ~1 then clause_offset := (case Inttab.max (!clause_table) of SOME (id, _) => id | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) else () val vid = int_from_string id val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") val _ = int_from_string levid val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") val _ = int_from_string valid val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") val aid = int_from_string anteid val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") val ls = map int_from_string lits (* convert the data provided by zChaff to our resolution-style proof format *) (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) (* given by the literals in the antecedent clause *) (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) val cid = !clause_offset + vid (* the low bit of each literal gives its sign (positive/negative), therefore *) (* we have to divide each literal by 2 to obtain the proper variable ID; then *) (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) val vids = filter (not_equal vid) (map (fn l => l div 2) ls) val rs = aid :: map (fn v => !clause_offset + v) vids in (* update clause table *) clause_table := Inttab.update_new (cid, rs) (!clause_table) handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") end | _ => raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." ) else if tok="CONF:" then ( case toks of id::sep::ids => let val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." val cid = int_from_string id val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") val ls = map int_from_string ids (* the conflict clause must be resolved with the unit clauses *) (* for its literals to obtain the empty clause *) val vids = map (fn l => l div 2) ls val rs = cid :: map (fn v => !clause_offset + v) vids val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1 in (* update clause table and conflict id *) clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); empty_id := new_empty_id end | _ => raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." ) else raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") fun process_lines [] = () | process_lines (l::ls) = ( process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); process_lines ls ) (* proof *) val _ = process_lines proof_lines val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." in SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE)) | result => result in SAT_Solver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) end; let fun zchaff fm = let val _ = if getenv "ZCHAFF_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = "\"$ZCHAFF_HOME/zchaff\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in SAT_Solver.add_solver ("zchaff", zchaff) end; (* ------------------------------------------------------------------------- *) (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *) (* ------------------------------------------------------------------------- *) let fun berkmin fm = let val _ = if (getenv "BERKMIN_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = "\"$BERKMIN_HOME/${BERKMIN_EXE:-BerkMin561}\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SAT_Solver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in SAT_Solver.add_solver ("berkmin", berkmin) end; (* ------------------------------------------------------------------------- *) (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *) (* ------------------------------------------------------------------------- *) let fun jerusat fm = let val _ = if (getenv "JERUSAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = "\"$JERUSAT_HOME/Jerusat1.3\" " ^ File.bash_path inpath ^ " > " ^ File.bash_path outpath fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in SAT_Solver.add_solver ("jerusat", jerusat) end; diff --git a/src/Pure/General/bytes.ML b/src/Pure/General/bytes.ML --- a/src/Pure/General/bytes.ML +++ b/src/Pure/General/bytes.ML @@ -1,221 +1,221 @@ (* Title: Pure/General/bytes.ML Author: Makarius Scalable byte strings, with incremental construction (add content to the end). Note: type string is implicitly limited by String.maxSize (approx. 64 MB on 64_32 architecture). *) signature BYTES = sig val chunk_size: int type T val eq: T * T -> bool val length: T -> int val contents: T -> string list val contents_blob: T -> XML.body val content: T -> string val is_empty: T -> bool val empty: T val build: (T -> T) -> T val add_substring: substring -> T -> T val add: string -> T -> T val beginning: int -> T -> string val exists_string: (string -> bool) -> T -> bool val forall_string: (string -> bool) -> T -> bool val last_string: T -> string option val trim_line: T -> T val append: T -> T -> T val appends: T list -> T val string: string -> T val newline: T val buffer: Buffer.T -> T val space_explode: string -> T -> string list val split_lines: T -> string list val trim_split_lines: T -> string list val cat_lines: string list -> T val read_block: int -> BinIO.instream -> string val read_stream: int -> BinIO.instream -> T val write_stream: BinIO.outstream -> T -> unit val read: Path.T -> T val write: Path.T -> T -> unit end; structure Bytes: BYTES = struct (* primitive operations *) val chunk_size = 1024 * 1024; abstype T = Bytes of {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)} with fun length (Bytes {m, n, ...}) = m + n; val compact = implode o rev; fun eq (Bytes {buffer, chunks, m, n}, Bytes {buffer = buffer', chunks = chunks', m = m', n = n'}) = m = m' andalso n = n' andalso chunks = chunks' andalso (buffer = buffer' orelse compact buffer = compact buffer); fun contents (Bytes {buffer, chunks, ...}) = rev (chunks |> not (null buffer) ? cons (compact buffer)); val contents_blob = contents #> XML.blob; val content = implode o contents; fun is_empty bytes = length bytes = 0; val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0}; fun build (f: T -> T) = f empty; fun add_substring s (bytes as Bytes {buffer, chunks, m, n}) = if Substring.isEmpty s then bytes else let val l = Substring.size s in if l + m < chunk_size then Bytes {buffer = Substring.string s :: buffer, chunks = chunks, m = l + m, n = n} else let val k = chunk_size - m; val chunk = compact (Substring.string (Substring.slice (s, 0, SOME k)) :: buffer); val s' = Substring.slice (s, k, SOME (l - k)); val bytes' = Bytes {buffer = [], chunks = chunk :: chunks, m = 0, n = chunk_size + n}; in add_substring s' bytes' end end; val add = add_substring o Substring.full; fun exists_string pred (Bytes {buffer, chunks, ...}) = let val ex = (exists o Library.exists_string) pred in ex buffer orelse ex chunks end; fun forall_string pred = not o exists_string (not o pred); fun last_string (Bytes {buffer, chunks, ...}) = (case buffer of s :: _ => Library.last_string s | [] => (case chunks of s :: _ => Library.last_string s | [] => NONE)); fun trim_line (bytes as Bytes {buffer, chunks, ...}) = let val is_line = (case last_string bytes of SOME s => Symbol.is_ascii_line_terminator s | NONE => false); in if is_line then let val (last_chunk, chunks') = (case chunks of [] => ("", []) | c :: cs => (c, cs)); val trimed = Library.trim_line (last_chunk ^ compact buffer); in build (fold_rev add chunks' #> add trimed) end else bytes end; end; (* derived operations *) fun beginning n bytes = let val dots = " ..."; val m = (String.maxSize - size dots) div chunk_size; val a = implode (take m (contents bytes)); val b = String.substring (a, 0, Int.min (n, size a)); in if size b < length bytes then b ^ dots else b end; fun append bytes1 bytes2 = (*left-associative*) if is_empty bytes1 then bytes2 else if is_empty bytes2 then bytes1 else bytes1 |> fold add (contents bytes2); val appends = build o fold (fn b => fn a => append a b); val string = build o add; val newline = string "\n"; val buffer = build o fold add o Buffer.contents; (* space_explode *) fun space_explode sep bytes = if is_empty bytes then [] else if size sep <> 1 then [content bytes] else let val sep_char = String.sub (sep, 0); fun add_part s part = Buffer.add (Substring.string s) (the_default Buffer.empty part); fun explode head tail part res = if Substring.isEmpty head then (case tail of [] => (case part of NONE => rev res | SOME buf => rev (Buffer.content buf :: res)) | chunk :: chunks => explode (Substring.full chunk) chunks part res) else (case Substring.fields (fn c => c = sep_char) head of [a] => explode Substring.empty tail (SOME (add_part a part)) res | a :: rest => let val (bs, c) = split_last rest; val res' = res |> cons (Buffer.content (add_part a part)) |> fold (cons o Substring.string) bs; val part' = SOME (add_part c NONE); in explode Substring.empty tail part' res' end) in explode Substring.empty (contents bytes) NONE [] end; val split_lines = space_explode "\n"; val trim_split_lines = trim_line #> split_lines #> map Library.trim_line; fun cat_lines lines = build (fold add (separate "\n" lines)); (* IO *) fun read_block limit = - File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit)); + File_Stream.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit)); fun read_stream limit stream = let fun read bytes = (case read_block (limit - length bytes) stream of "" => bytes | s => read (add s bytes)) in read empty end; fun write_stream stream bytes = - File.outputs stream (contents bytes); + File_Stream.outputs stream (contents bytes); -fun read path = File.open_input (fn stream => read_stream ~1 stream) path; +fun read path = File_Stream.open_input (fn stream => read_stream ~1 stream) path; -fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path; +fun write path bytes = File_Stream.open_output (fn stream => write_stream stream bytes) path; (* ML pretty printing *) val _ = ML_system_pp (fn _ => fn _ => fn bytes => PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}")) end; diff --git a/src/Pure/General/file.ML b/src/Pure/General/file.ML --- a/src/Pure/General/file.ML +++ b/src/Pure/General/file.ML @@ -1,180 +1,140 @@ (* Title: Pure/General/file.ML Author: Makarius File-system operations. *) signature FILE = sig val standard_path: Path.T -> string val platform_path: Path.T -> string val bash_path: Path.T -> string val bash_paths: Path.T list -> string val bash_platform_path: Path.T -> string val absolute_path: Path.T -> Path.T val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool val rm: Path.T -> unit val is_dir: Path.T -> bool val is_file: Path.T -> bool val check_dir: Path.T -> Path.T val check_file: Path.T -> Path.T - val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a - val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a - val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a - val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_dir: Path.T -> string list - val input: BinIO.instream -> string - val input_size: int -> BinIO.instream -> string - val input_all: BinIO.instream -> string val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_lines: Path.T -> string list val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit - val output: BinIO.outstream -> string -> unit - val outputs: BinIO.outstream -> string list -> unit val write_list: Path.T -> string list -> unit val append_list: Path.T -> string list -> unit val eq: Path.T * Path.T -> bool end; structure File: FILE = struct (* system path representations *) val standard_path = Path.implode o Path.expand; val platform_path = ML_System.platform_path o standard_path; val bash_path = Bash.string o standard_path; val bash_paths = Bash.strings o map standard_path; val bash_platform_path = Bash.string o platform_path; (* full_path *) val absolute_path = Path.expand #> (fn path => if Path.is_absolute path then path else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path); fun full_path dir path = let val path' = Path.expand path; val _ = Path.is_current path' andalso error "Bad file specification"; in absolute_path (dir + path') end; (* tmp_path *) fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path; (* directory entries *) val exists = can OS.FileSys.modTime o platform_path; val rm = OS.FileSys.remove o platform_path; fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); fun is_dir path = exists path andalso test_dir path; fun is_file path = exists path andalso not (test_dir path); fun check_dir path = if is_dir path then path else error ("No such directory: " ^ Path.print (Path.expand path)); fun check_file path = if is_file path then path else error ("No such file: " ^ Path.print (Path.expand path)); -(* open streams *) - -local - -fun with_file open_file close_file f = - Thread_Attributes.uninterruptible (fn restore_attributes => fn path => - let - val file = open_file path; - val result = Exn.capture (restore_attributes f) file; - in close_file file; Exn.release result end); - -in - -fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path; -fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path; -fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path; -fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path; - -end; - - (* directory content *) fun fold_dir f path a = - check_dir path |> open_dir (fn stream => + check_dir path |> File_Stream.open_dir (fn stream => let fun read x = (case OS.FileSys.readDir stream of NONE => x | SOME entry => read (f entry x)); in read a end); fun read_dir path = sort_strings (fold_dir cons path []); -(* input *) - -val input = Byte.bytesToString o BinIO.input; -fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n)); -val input_all = Byte.bytesToString o BinIO.inputAll; - (* scalable iterator: . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine . optional terminator at end-of-input *) -fun fold_lines f path a = open_input (fn file => +fun fold_lines f path a = File_Stream.open_input (fn file => let fun read buf x = - (case input file of + (case File_Stream.input file of "" => (case Buffer.content buf of "" => x | line => f line x) | input => (case String.fields (fn c => c = #"\n") input of [rest] => read (Buffer.add rest buf) x | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x))) and read_more [rest] x = read (Buffer.add rest Buffer.empty) x | read_more (line :: more) x = read_more more (f line x); in read Buffer.empty a end) path; fun read_lines path = rev (fold_lines cons path []); -val read = open_input input_all; +val read = File_Stream.open_input File_Stream.input_all; -(* output *) +(* write *) -fun output file txt = BinIO.output (file, Byte.stringToBytes txt); -val outputs = List.app o output; - -fun output_list txts file = List.app (output file) txts; -fun write_list path txts = open_output (output_list txts) path; -fun append_list path txts = open_append (output_list txts) path; +fun write_list path ss = File_Stream.open_output (fn stream => File_Stream.outputs stream ss) path; +fun append_list path ss = File_Stream.open_append (fn stream => File_Stream.outputs stream ss) path; fun write path txt = write_list path [txt]; fun append path txt = append_list path [txt]; (* eq *) fun eq paths = (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); end; diff --git a/src/Pure/General/file_stream.ML b/src/Pure/General/file_stream.ML new file mode 100644 --- /dev/null +++ b/src/Pure/General/file_stream.ML @@ -0,0 +1,58 @@ +(* Title: Pure/General/file_stream.ML + Author: Makarius + +File-system stream operations. +*) + +signature FILE_STREAM = +sig + val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a + val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a + val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a + val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a + val input: BinIO.instream -> string + val input_size: int -> BinIO.instream -> string + val input_all: BinIO.instream -> string + val output: BinIO.outstream -> string -> unit + val outputs: BinIO.outstream -> string list -> unit +end; + +structure File_Stream: FILE_STREAM = +struct + +(* open streams *) + +local + +val platform_path = ML_System.platform_path o Path.implode o Path.expand; + +fun with_file open_file close_file f = + Thread_Attributes.uninterruptible (fn restore_attributes => fn path => + let + val file = open_file path; + val result = Exn.capture (restore_attributes f) file; + in close_file file; Exn.release result end); + +in + +fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path; +fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path; +fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path; +fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path; + +end; + + +(* input *) + +val input = Byte.bytesToString o BinIO.input; +fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n)); +val input_all = Byte.bytesToString o BinIO.inputAll; + + +(* output *) + +fun output file txt = BinIO.output (file, Byte.stringToBytes txt); +val outputs = List.app o output; + +end; diff --git a/src/Pure/PIDE/byte_message.ML b/src/Pure/PIDE/byte_message.ML --- a/src/Pure/PIDE/byte_message.ML +++ b/src/Pure/PIDE/byte_message.ML @@ -1,127 +1,128 @@ (* Title: Pure/General/byte_message.ML Author: Makarius Byte-oriented messages. *) signature BYTE_MESSAGE = sig val write: BinIO.outstream -> Bytes.T list -> unit val write_yxml: BinIO.outstream -> XML.tree -> unit val flush: BinIO.outstream -> unit val write_line: BinIO.outstream -> Bytes.T -> unit val read: BinIO.instream -> int -> Bytes.T val read_block: BinIO.instream -> int -> Bytes.T option * int val read_line: BinIO.instream -> Bytes.T option val write_message: BinIO.outstream -> Bytes.T list -> unit val write_message_string: BinIO.outstream -> string list -> unit val write_message_yxml: BinIO.outstream -> XML.body list -> unit val read_message: BinIO.instream -> Bytes.T list option val read_message_string: BinIO.instream -> string list option val write_line_message: BinIO.outstream -> Bytes.T -> unit val read_line_message: BinIO.instream -> Bytes.T option end; structure Byte_Message: BYTE_MESSAGE = struct (* output operations *) val write = List.app o Bytes.write_stream; -fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree (); +fun write_yxml stream tree = + YXML.traverse (fn s => fn () => File_Stream.output stream s) tree (); fun flush stream = ignore (try BinIO.flushOut stream); fun write_line stream bs = (write stream [bs, Bytes.newline]; flush stream); (* input operations *) fun read stream n = Bytes.read_stream n stream; fun read_block stream n = let val msg = read stream n; val len = Bytes.length msg; in (if len = n then SOME msg else NONE, len) end; fun read_line stream = let val result = SOME o Bytes.trim_line; fun read_body bs = (case BinIO.input1 stream of NONE => if Bytes.is_empty bs then NONE else result bs | SOME b => (case Byte.byteToChar b of #"\n" => result bs | c => read_body (Bytes.add (str c) bs))); in read_body Bytes.empty end; (* messages with multiple chunks (arbitrary content) *) fun make_header ns = [Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline]; fun write_message stream chunks = (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream); fun write_message_string stream = write_message stream o map Bytes.string; fun write_message_yxml stream chunks = (write stream (make_header (map YXML.body_size chunks)); (List.app o List.app) (write_yxml stream) chunks; flush stream); fun parse_header line = map Value.parse_nat (space_explode "," line) handle Fail _ => error ("Malformed message header: " ^ quote line); fun read_chunk stream n = (case read_block stream n of (SOME chunk, _) => chunk | (NONE, len) => error ("Malformed message chunk: unexpected EOF after " ^ string_of_int len ^ " of " ^ string_of_int n ^ " bytes")); fun read_message stream = read_line stream |> Option.map (Bytes.content #> parse_header #> map (read_chunk stream)); fun read_message_string stream = read_message stream |> (Option.map o map) Bytes.content; (* hybrid messages: line or length+block (with content restriction) *) (* line message format *) fun is_length msg = not (Bytes.is_empty msg) andalso Bytes.forall_string Symbol.is_ascii_digit msg; fun is_terminated msg = (case Bytes.last_string msg of NONE => false | SOME s => Symbol.is_ascii_line_terminator s); fun write_line_message stream msg = if is_length msg orelse is_terminated msg then error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg) else let val n = Bytes.length msg in write stream ((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg then make_header [n + 1] else []) @ [msg, Bytes.newline]); flush stream end; fun read_line_message stream = (case read_line stream of NONE => NONE | SOME line => (case try (Value.parse_nat o Bytes.content) line of NONE => SOME line | SOME n => Option.map Bytes.trim_line (#1 (read_block stream n)))); end; diff --git a/src/Pure/PIDE/yxml.ML b/src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML +++ b/src/Pure/PIDE/yxml.ML @@ -1,175 +1,175 @@ (* Title: Pure/PIDE/yxml.ML Author: Makarius Efficient text representation of XML trees using extra characters X and Y -- no escaping, may nest marked text verbatim. Suitable for direct inlining into plain text. Markup ...body... is encoded as: X Y name Y att=val ... X ... body ... X Y X *) signature YXML = sig val X: Symbol.symbol val Y: Symbol.symbol val embed_controls: string -> string val detect: string -> bool val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a val tree_size: XML.tree -> int val body_size: XML.body -> int val string_of_body: XML.body -> string val string_of: XML.tree -> string val write_body: Path.T -> XML.body -> unit val output_markup: Markup.T -> string * string val output_markup_elem: Markup.T -> (string * string) * string val parse_body: string -> XML.body val parse: string -> XML.tree val content_of: string -> string val is_wellformed: string -> bool end; structure YXML: YXML = struct (** string representation **) (* idempotent recoding of certain low ASCII control characters *) fun pseudo_utf8 c = if Symbol.is_ascii_control c then chr 192 ^ chr (128 + ord c) else c; fun embed_controls str = if exists_string Symbol.is_ascii_control str then translate_string pseudo_utf8 str else str; (* markers *) val X_char = Char.chr 5; val Y_char = Char.chr 6; val X = String.str X_char; val Y = String.str Y_char; val XY = X ^ Y; val XYX = XY ^ X; fun detect s = Char.contains s X_char orelse Char.contains s Y_char; (* traverse *) fun traverse string = let fun attrib (a, x) = string Y #> string a #> string "=" #> string x; fun tree (XML.Elem (markup as (name, atts), ts)) = if Markup.is_empty markup then fold tree ts else string XY #> string name #> fold attrib atts #> string X #> fold tree ts #> string XYX | tree (XML.Text s) = string s; in tree end; fun tree_size tree = traverse (Integer.add o size) tree 0; fun body_size body = fold (Integer.add o tree_size) body 0; (* output *) val string_of_body = Buffer.build_content o fold (traverse Buffer.add); val string_of = string_of_body o single; fun write_body path body = - path |> File.open_output (fn file => - fold (traverse (fn s => fn () => File.output file s)) body ()); + path |> File_Stream.open_output (fn file => + fold (traverse (fn s => fn () => File_Stream.output file s)) body ()); (* markup elements *) val Z = chr 0; val Z_text = [XML.Text Z]; fun output_markup (markup as (name, atts)) = if Markup.is_empty markup then Markup.no_output else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX); fun output_markup_elem markup = let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text))) in ((bg1, bg2), en) end; (** efficient YXML parsing **) local (* splitting *) val split_string = Substring.full #> Substring.tokens (fn c => c = X_char) #> map (Substring.fields (fn c => c = Y_char) #> map Substring.string); (* structural errors *) fun err msg = raise Fail ("Malformed YXML: " ^ msg); fun err_attribute () = err "bad attribute"; fun err_element () = err "bad element"; fun err_unbalanced "" = err "unbalanced element" | err_unbalanced name = err ("unbalanced element " ^ quote name); (* stack operations *) fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending; fun push "" _ _ = err_element () | push name atts pending = ((name, atts), []) :: pending; fun pop ((("", _), _) :: _) = err_unbalanced "" | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending; (* parsing *) fun parse_attrib s = (case first_field "=" s of NONE => err_attribute () | SOME ("", _) => err_attribute () | SOME att => att); fun parse_chunk ["", ""] = pop | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts) | parse_chunk txts = fold (add o XML.Text) txts; in fun parse_body source = (case fold parse_chunk (split_string source) [(("", []), [])] of [(("", _), result)] => rev result | ((name, _), _) :: _ => err_unbalanced name); fun parse source = (case parse_body source of [result] => result | [] => XML.Text "" | _ => err "multiple results"); end; val content_of = parse_body #> XML.content_of; fun is_wellformed s = string_of_body (parse_body s) = s handle Fail _ => false; end; diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,362 +1,363 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash.ML"; +ML_file "General/file_stream.ML"; +ML_file "General/bytes.ML"; ML_file "General/file.ML"; -ML_file "General/bytes.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/seq.ML"; ML_file "General/time.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/yxml.ML"; ML_file "ML/ml_profiling.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/socket_io.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_items.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "cterm_items.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; ML_file "ML/ml_antiquotations.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/bundle.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; ML_file "System/process_result.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/document_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*ML add-ons*) ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_instantiate.ML"; ML_file "ML/ml_file.ML"; ML_file "ML/ml_pid.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala_compiler.ML"; ML_file "System/isabelle_tool.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/doc.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML"