diff --git a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML @@ -1,81 +1,81 @@ (* Title: HOL/Library/Sum_of_Squares/sos_wrapper.ML Author: Philipp Meyer, TU Muenchen Wrapper for "sos" proof method. *) signature SOS_WRAPPER = sig val sos_tac: Proof.context -> string option -> int -> tactic end structure SOS_Wrapper: SOS_WRAPPER = struct datatype prover_result = Success | Failure | Error fun str_of_result Success = "Success" | str_of_result Failure = "Failure" | str_of_result Error = "Error" fun get_result rc = (case rc of 0 => (Success, "SDP solved") | 1 => (Failure, "SDP is primal infeasible") | 2 => (Failure, "SDP is dual infeasible") | 3 => (Success, "SDP solved with reduced accuracy") | 4 => (Failure, "Maximum iterations reached") | 5 => (Failure, "Stuck at edge of primal feasibility") | 6 => (Failure, "Stuck at edge of dual infeasibility") | 7 => (Failure, "Lack of progress") | 8 => (Failure, "X, Z, or O was singular") | 9 => (Failure, "Detected NaN or Inf values") | _ => (Error, "return code is " ^ string_of_int rc)) fun run_solver ctxt input = Isabelle_System.with_tmp_file "sos_in" "" (fn in_path => Isabelle_System.with_tmp_file "sos_out" "" (fn out_path => let val _ = File.write in_path input val (output, rc) = Isabelle_System.bash_output ("\"$ISABELLE_CSDP\" " ^ - Bash.string (File.platform_path in_path) ^ " " ^ - Bash.string (File.platform_path out_path)); + File.bash_platform_path in_path ^ " " ^ + File.bash_platform_path out_path); val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output) val result = if File.exists out_path then File.read out_path else "" val (res, res_msg) = get_result rc val _ = Sum_of_Squares.trace_message ctxt (fn () => str_of_result res ^ ": " ^ res_msg) in (case res of Success => result | Failure => raise Sum_of_Squares.Failure res_msg | Error => error ("Prover failed: " ^ res_msg)) end)) (* method setup *) fun print_cert cert = Output.information ("To repeat this proof with a certificate use this command:\n" ^ Active.sendback_markup_command ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) fun sos_tac ctxt NONE = Sum_of_Squares.sos_tac print_cert (Sum_of_Squares.Prover (run_solver ctxt)) ctxt | sos_tac ctxt (SOME cert) = Sum_of_Squares.sos_tac ignore (Sum_of_Squares.Certificate (Positivstellensatz_Tools.read_cert ctxt cert)) ctxt val _ = Theory.setup (Method.setup \<^binding>\sos\ (Scan.lift (Scan.option Parse.string) >> (fn arg => fn ctxt => SIMPLE_METHOD' (sos_tac ctxt arg))) "prove universal problems over the reals using sums of squares") end diff --git a/src/HOL/Library/code_test.ML b/src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML +++ b/src/HOL/Library/code_test.ML @@ -1,564 +1,562 @@ (* Title: HOL/Library/code_test.ML Author: Andreas Lochbihler, ETH Zürich Test infrastructure for the code generator. *) signature CODE_TEST = sig val add_driver: string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory val overlord: bool Config.T val successN: string val failureN: string val start_markerN: string val end_markerN: string val test_terms: Proof.context -> term list -> string -> unit val test_targets: Proof.context -> term list -> string list -> unit val test_code_cmd: string list -> string list -> Proof.context -> unit val eval_term: string -> Proof.context -> term -> term val check_settings: string -> string -> string -> unit val compile: string -> string -> unit val evaluate: string -> string -> string val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string val ghc_options: string Config.T val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string val target_Scala: string val target_Haskell: string end structure Code_Test: CODE_TEST = struct (* convert a list of terms into nested tuples and back *) fun mk_tuples [] = \<^term>\()\ | mk_tuples [t] = t | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) fun dest_tuples (Const (\<^const_name>\Pair\, _) $ l $ r) = l :: dest_tuples r | dest_tuples t = [t] fun last_field sep str = let val n = size sep val len = size str fun find i = if i < 0 then NONE else if String.substring (str, i, n) = sep then SOME i else find (i - 1) in (case find (len - n) of NONE => NONE | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) end fun split_first_last start stop s = (case first_field start s of NONE => NONE | SOME (initial, rest) => (case last_field stop rest of NONE => NONE | SOME (middle, tail) => SOME (initial, middle, tail))) (* data slot for drivers *) structure Drivers = Theory_Data ( type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list val empty = [] val extend = I fun merge data : T = AList.merge (op =) (K true) data ) val add_driver = Drivers.map o AList.update (op =) val get_driver = AList.lookup (op =) o Drivers.get (* Test drivers must produce output of the following format: The start of the relevant data is marked with start_markerN, its end with end_markerN. Between these two markers, every line corresponds to one test. Lines of successful tests start with successN, failures start with failureN. The failure failureN may continue with the YXML encoding of the evaluated term. There must not be any additional whitespace in between. *) (* parsing of results *) val successN = "True" val failureN = "False" val start_markerN = "*@*Isabelle/Code_Test-start*@*" val end_markerN = "*@*Isabelle/Code_Test-end*@*" fun parse_line line = if String.isPrefix successN line then (true, NONE) else if String.isPrefix failureN line then (false, if size line > size failureN then String.extract (line, size failureN, NONE) |> YXML.parse_body |> Term_XML.Decode.term_raw |> dest_tuples |> SOME else NONE) else raise Fail ("Cannot parse result of evaluation:\n" ^ line) fun parse_result target out = (case split_first_last start_markerN end_markerN out of NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out) | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line) (* pretty printing of test results *) fun pretty_eval _ NONE _ = [] | pretty_eval ctxt (SOME evals) ts = [Pretty.fbrk, Pretty.big_list "Evaluated terms" (map (fn (t, eval) => Pretty.block [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, Syntax.pretty_term ctxt eval]) (ts ~~ evals))] fun pretty_failure ctxt target (((_, evals), query), eval_ts) = Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @ pretty_eval ctxt evals eval_ts) fun pretty_failures ctxt target failures = Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) (* driver invocation *) val overlord = Attrib.setup_config_bool \<^binding>\code_test_overlord\ (K false) fun with_overlord_dir name f = let val dir = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) val _ = Isabelle_System.mkdirs dir in Exn.release (Exn.capture f dir) end fun dynamic_value_strict ctxt t compiler = let val thy = Proof_Context.theory_of ctxt val (driver, target) = (case get_driver thy compiler of NONE => error ("No driver for target " ^ compiler) | SOME drv => drv) val debug = Config.get (Proof_Context.init_global thy) overlord val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir fun eval result = with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result)) |> parse_result compiler fun evaluator program _ vs_ty deps = Exn.interruptible_capture eval (Code_Target.compilation_text ctxt target program deps true vs_ty) fun postproc f = map (apsnd (Option.map (map f))) in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end (* term preprocessing *) fun add_eval (Const (\<^const_name>\Trueprop\, _) $ t) = add_eval t | add_eval (Const (\<^const_name>\HOL.eq\, _) $ lhs $ rhs) = (fn acc => acc |> add_eval rhs |> add_eval lhs |> cons rhs |> cons lhs) | add_eval (Const (\<^const_name>\Not\, _) $ t) = add_eval t | add_eval (Const (\<^const_name>\Orderings.ord_class.less_eq\, _) $ lhs $ rhs) = (fn acc => lhs :: rhs :: acc) | add_eval (Const (\<^const_name>\Orderings.ord_class.less\, _) $ lhs $ rhs) = (fn acc => lhs :: rhs :: acc) | add_eval _ = I fun mk_term_of [] = \<^term>\None :: (unit \ yxml_of_term) option\ | mk_term_of ts = let val tuple = mk_tuples ts val T = fastype_of tuple in \<^term>\Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option\ $ (absdummy \<^typ>\unit\ (\<^const>\yxml_string_of_term\ $ (Const (\<^const_name>\Code_Evaluation.term_of\, T --> \<^typ>\term\) $ tuple))) end fun test_terms ctxt ts target = let val thy = Proof_Context.theory_of ctxt fun term_of t = Sign.of_sort thy (fastype_of t, \<^sort>\term_of\) fun ensure_bool t = (case fastype_of t of \<^typ>\bool\ => () | _ => error (Pretty.string_of (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1, Syntax.pretty_term ctxt t]))) val _ = List.app ensure_bool ts val evals = map (fn t => filter term_of (add_eval t [])) ts val eval = map mk_term_of evals val t = HOLogic.mk_list \<^typ>\bool \ (unit \ yxml_of_term) option\ (map HOLogic.mk_prod (ts ~~ eval)) val result = dynamic_value_strict ctxt t target val failed = filter_out (fst o fst o fst) (result ~~ ts ~~ evals) handle ListPair.UnequalLengths => error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result)) in (case failed of [] => () | _ => error (Pretty.string_of (pretty_failures ctxt target failed))) end fun test_targets ctxt = List.app o test_terms ctxt fun pretty_free ctxt = Syntax.pretty_term ctxt o Free fun test_code_cmd raw_ts targets ctxt = let val ts = Syntax.read_terms ctxt raw_ts val frees = fold Term.add_frees ts [] val _ = if null frees then () else error (Pretty.string_of (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 :: Pretty.commas (map (pretty_free ctxt) frees)))) in test_targets ctxt ts targets end fun eval_term target ctxt t = let val frees = Term.add_frees t [] val _ = if null frees then () else error (Pretty.string_of (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 :: Pretty.commas (map (pretty_free ctxt) frees)))) val T = fastype_of t val _ = if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\term_of\) then () else error ("Type " ^ Syntax.string_of_typ ctxt T ^ " of term not of sort " ^ Syntax.string_of_sort ctxt \<^sort>\term_of\) val t' = HOLogic.mk_list \<^typ>\bool \ (unit \ yxml_of_term) option\ [HOLogic.mk_prod (\<^term>\False\, mk_term_of [t])] val result = dynamic_value_strict ctxt t' target in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end (* check and invoke compiler *) fun check_settings compiler var descr = if getenv var = "" then error (Pretty.string_of (Pretty.para ("Environment variable " ^ var ^ " is not set. To test code generation with " ^ compiler ^ ", set this variable to your " ^ descr ^ " in the $ISABELLE_HOME_USER/etc/settings file."))) else (); fun compile compiler cmd = let val (out, ret) = Isabelle_System.bash_output cmd in if ret = 0 then () else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out) end fun evaluate compiler cmd = let val (out, res) = Isabelle_System.bash_output cmd in if res = 0 then out else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^ string_of_int res ^ "\nCompiler output:\n" ^ out) end (* driver for PolyML *) val polymlN = "PolyML" fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir = let val compiler = polymlN val code_path = Path.append dir (Path.basic "generated.sml") val driver_path = Path.append dir (Path.basic "driver.sml") val driver = "fun main prog_name = \n" ^ " let\n" ^ " fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ " val result = " ^ value_name ^ " ();\n" ^ " val _ = print \"" ^ start_markerN ^ "\";\n" ^ " val _ = map (print o format) result;\n" ^ " val _ = print \"" ^ end_markerN ^ "\";\n" ^ " in\n" ^ " ()\n" ^ " end;\n"; val cmd = - "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^ - " --use " ^ Bash.string (File.platform_path driver_path) ^ + "\"$POLYML_EXE\" --use " ^ File.bash_platform_path code_path ^ + " --use " ^ File.bash_platform_path driver_path ^ " --eval " ^ Bash.string "main ()" in List.app (File.write code_path o snd) code_files; File.write driver_path driver; evaluate compiler cmd end (* driver for mlton *) val mltonN = "MLton" val ISABELLE_MLTON = "ISABELLE_MLTON" fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir = let val compiler = mltonN val generatedN = "generated.sml" val driverN = "driver.sml" val projectN = "test" val code_path = Path.append dir (Path.basic generatedN) val driver_path = Path.append dir (Path.basic driverN) val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb")) val driver = "fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ "val result = " ^ value_name ^ " ();\n" ^ "val _ = print \"" ^ start_markerN ^ "\";\n" ^ "val _ = map (print o format) result;\n" ^ "val _ = print \"" ^ end_markerN ^ "\";\n" val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path in check_settings compiler ISABELLE_MLTON "MLton executable"; List.app (File.write code_path o snd) code_files; File.write driver_path driver; File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN); compile compiler cmd; evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN))) end (* driver for SML/NJ *) val smlnjN = "SMLNJ" val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir = let val compiler = smlnjN val generatedN = "generated.sml" val driverN = "driver.sml" val code_path = Path.append dir (Path.basic generatedN) val driver_path = Path.append dir (Path.basic driverN) val driver = "structure Test = struct\n" ^ "fun main prog_name =\n" ^ " let\n" ^ " fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ " val result = " ^ value_name ^ " ();\n" ^ " val _ = print \"" ^ start_markerN ^ "\";\n" ^ " val _ = map (print o format) result;\n" ^ " val _ = print \"" ^ end_markerN ^ "\";\n" ^ " in\n" ^ " 0\n" ^ " end;\n" ^ "end;" val ml_source = "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^ "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^ "; Test.main ();" in check_settings compiler ISABELLE_SMLNJ "SMLNJ executable"; List.app (File.write code_path o snd) code_files; File.write driver_path driver; evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"") end (* driver for OCaml *) val ocamlN = "OCaml" val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND" fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir = let val compiler = ocamlN val code_path = Path.append dir (Path.basic "generated.ml") val driver_path = Path.append dir (Path.basic "driver.ml") val driver = "let format_term = function\n" ^ " | None -> \"\"\n" ^ " | Some t -> t ();;\n" ^ "let format = function\n" ^ " | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^ " | (false, x) -> \"" ^ failureN ^ "\" ^ format_term x ^ \"\\n\";;\n" ^ "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^ "let main x =\n" ^ " let _ = print_string \"" ^ start_markerN ^ "\" in\n" ^ " let _ = List.map (fun x -> print_string (format x)) result in\n" ^ " print_string \"" ^ end_markerN ^ "\";;\n" ^ "main ();;" val compiled_path = Path.append dir (Path.basic "test") val cmd = "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^ " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " \code_test_ghc\ (K "") fun evaluate_in_ghc ctxt (code_files, value_name) dir = let val compiler = ghcN val modules = map fst code_files val driver_path = Path.append dir (Path.basic "Main.hs") val driver = "module Main where {\n" ^ implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^ "main = do {\n" ^ " let {\n" ^ " format_term Nothing = \"\";\n" ^ " format_term (Just t) = t ();\n" ^ " format (True, _) = \"" ^ successN ^ "\\n\";\n" ^ " format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^ " result = " ^ value_name ^ " ();\n" ^ " };\n" ^ " Prelude.putStr \"" ^ start_markerN ^ "\";\n" ^ " Prelude.mapM_ (putStr . format) result;\n" ^ " Prelude.putStr \"" ^ end_markerN ^ "\";\n" ^ " }\n" ^ "}\n" val compiled_path = Path.append dir (Path.basic "test") val cmd = "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ Config.get ctxt ghc_options ^ " -o " ^ - Bash.string (File.platform_path compiled_path) ^ " " ^ - Bash.string (File.platform_path driver_path) ^ " -i" ^ - Bash.string (File.platform_path dir) + File.bash_platform_path compiled_path ^ " " ^ + File.bash_platform_path driver_path ^ " -i" ^ + File.bash_platform_path dir in check_settings compiler ISABELLE_GHC "GHC executable"; List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files; File.write driver_path driver; compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end (* driver for Scala *) val scalaN = "Scala" fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir = let val compiler = scalaN val generatedN = "Generated_Code" val driverN = "Driver.scala" val code_path = Path.append dir (Path.basic (generatedN ^ ".scala")) val driver_path = Path.append dir (Path.basic driverN) val driver = "import " ^ generatedN ^ "._\n" ^ "object Test {\n" ^ " def format_term(x : Option[Unit => String]) : String = x match {\n" ^ " case None => \"\"\n" ^ " case Some(x) => x(())\n" ^ " }\n" ^ " def format(term : (Boolean, Option[Unit => String])) : String = term match {\n" ^ " case (true, _) => \"True\\n\"\n" ^ " case (false, x) => \"False\" + format_term(x) + \"\\n\"\n" ^ " }\n" ^ " def main(args:Array[String]) = {\n" ^ " val result = " ^ value_name ^ "(());\n" ^ " print(\"" ^ start_markerN ^ "\");\n" ^ " result.map{test:(Boolean, Option[Unit => String]) => print(format(test))};\n" ^ " print(\"" ^ end_markerN ^ "\");\n" ^ " }\n" ^ "}\n" val compile_cmd = - "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path dir) ^ - " -classpath " ^ Bash.string (File.platform_path dir) ^ " " ^ - Bash.string (File.platform_path code_path) ^ " " ^ - Bash.string (File.platform_path driver_path) - val run_cmd = - "isabelle_scala scala -cp " ^ Bash.string (File.platform_path dir) ^ " Test" + "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_platform_path dir ^ + " -classpath " ^ File.bash_platform_path dir ^ " " ^ + File.bash_platform_path code_path ^ " " ^ File.bash_platform_path driver_path + val run_cmd = "isabelle_scala scala -cp " ^ File.bash_platform_path dir ^ " Test" in List.app (File.write code_path o snd) code_files; File.write driver_path driver; compile compiler compile_cmd; evaluate compiler run_cmd end (* command setup *) val _ = Outer_Syntax.command \<^command_keyword>\test_code\ "compile test cases to target languages, execute them and report results" (Scan.repeat1 Parse.prop -- (\<^keyword>\in\ |-- Scan.repeat1 Parse.name) >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of))) val target_Scala = "Scala_eval" val target_Haskell = "Haskell_eval" val _ = Theory.setup (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)])) val _ = Theory.setup (fold add_driver [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), (ghcN, (evaluate_in_ghc, target_Haskell)), (scalaN, (evaluate_in_scala, target_Scala))] #> fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> snd) [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) end diff --git a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML @@ -1,325 +1,323 @@ (* Title: HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Author: Steven Obua *) structure AM_GHC : ABSTRACT_MACHINE = struct open AbstractMachine; type program = string * Path.T * (int Inttab.table) fun count_patternvars PVar = 1 | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps fun update_arity arity code a = (case Inttab.lookup arity code of NONE => Inttab.update_new (code, a) arity | SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity) (* We have to find out the maximal arity of each constant *) fun collect_pattern_arity PVar arity = arity | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args)) local fun collect applevel (Var _) arity = arity | collect applevel (Const c) arity = update_arity arity c applevel | collect applevel (Abs m) arity = collect 0 m arity | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity) in fun collect_term_arity t arity = collect 0 t arity end fun nlift level n (Var m) = if m < level then Var m else Var (m+n) | nlift level n (Const c) = Const c | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b) | nlift level n (Abs b) = Abs (nlift (level+1) n b) fun rep n x = if n = 0 then [] else x::(rep (n-1) x) fun adjust_rules rules = let val arity = fold (fn (p, t) => fn arity => collect_term_arity t (collect_pattern_arity p arity)) rules Inttab.empty fun arity_of c = the (Inttab.lookup arity c) fun adjust_pattern PVar = PVar | adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C fun adjust_rule (PVar, _) = raise Compile ("pattern may not be a variable") | adjust_rule (rule as (p as PConst (c, args),t)) = let val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else () val args = map adjust_pattern args val len = length args val arity = arity_of c fun lift level n (Var m) = if m < level then Var m else Var (m+n) | lift level n (Const c) = Const c | lift level n (App (a,b)) = App (lift level n a, lift level n b) | lift level n (Abs b) = Abs (lift (level+1) n b) val lift = lift 0 fun adjust_term n t = if n=0 then t else adjust_term (n-1) (App (t, Var (n-1))) in if len = arity then rule else if arity >= len then (PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) (lift (arity-len) t)) else (raise Compile "internal error in adjust_rule") end in (arity, map adjust_rule rules) end fun print_term arity_of n = let fun str x = string_of_int x fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s fun print_apps d f [] = f | print_apps d f (a::args) = print_apps d ("app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args and print_call d (App (a, b)) args = print_call d a (b::args) | print_call d (Const c) args = (case arity_of c of NONE => print_apps d ("Const "^(str c)) args | SOME a => let val len = length args in if a <= len then let val s = "c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a)))) in print_apps d s (List.drop (args, a)) end else let fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n-1))) fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t) fun append_args [] t = t | append_args (c::cs) t = append_args cs (App (t, c)) in print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c))))) end end) | print_call d t args = print_apps d (print_term d t) args and print_term d (Var x) = if x < d then "b"^(str (d-x-1)) else "x"^(str (n-(x-d)-1)) | print_term d (Abs c) = "Abs (\\b"^(str d)^" -> "^(print_term (d + 1) c)^")" | print_term d t = print_call d t [] in print_term 0 end fun print_rule arity_of (p, t) = let fun str x = string_of_int x fun print_pattern top n PVar = (n+1, "x"^(str n)) | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)) | print_pattern top n (PConst (c, args)) = let val (n,s) = print_pattern_list (n, (if top then "c" else "C")^(str c)) args in (n, if top then s else "("^s^")") end and print_pattern_list r [] = r | print_pattern_list (n, p) (t::ts) = let val (n, t) = print_pattern false n t in print_pattern_list (n, p^" "^t) ts end val (n, pattern) = print_pattern true 0 p in pattern^" = "^(print_term arity_of n t) end fun group_rules rules = let fun add_rule (r as (PConst (c,_), _)) groups = let val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs) in Inttab.update (c, r::rs) groups end | add_rule _ _ = raise Compile "internal error group_rules" in fold_rev add_rule rules Inttab.empty end fun haskell_prog name rules = let val buffer = Unsynchronized.ref "" fun write s = (buffer := (!buffer)^s) fun writeln s = (write s; write "\n") fun writelist [] = () | writelist (s::ss) = (writeln s; writelist ss) fun str i = string_of_int i val (arity, rules) = adjust_rules rules val rules = group_rules rules val constants = Inttab.keys arity fun arity_of c = Inttab.lookup arity c fun rep_str s n = implode (rep n s) fun indexed s n = s^(str n) fun section n = if n = 0 then [] else (section (n-1))@[n-1] fun make_show c = let val args = section (the (arity_of c)) in " show ("^(indexed "C" c)^(implode (map (indexed " a") args))^") = " ^"\""^(indexed "C" c)^"\""^(implode (map (fn a => "++(show "^(indexed "a" a)^")") args)) end fun default_case c = let val args = implode (map (indexed " x") (section (the (arity_of c)))) in (indexed "c" c)^args^" = "^(indexed "C" c)^args end val _ = writelist [ "module "^name^" where", "", "data Term = Const Integer | App Term Term | Abs (Term -> Term)", " "^(implode (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)), "", "instance Show Term where"] val _ = writelist (map make_show constants) val _ = writelist [ " show (Const c) = \"c\"++(show c)", " show (App a b) = \"A\"++(show a)++(show b)", " show (Abs _) = \"L\"", ""] val _ = writelist [ "app (Abs a) b = a b", "app a b = App a b", "", "calc s c = writeFile s (show c)", ""] fun list_group c = (writelist (case Inttab.lookup rules c of NONE => [default_case c, ""] | SOME (rs as ((PConst (_, []), _)::rs')) => if not (null rs') then raise Compile "multiple declaration of constant" else (map (print_rule arity_of) rs) @ [""] | SOME rs => (map (print_rule arity_of) rs) @ [default_case c, ""])) val _ = map list_group constants in (arity, !buffer) end val guid_counter = Unsynchronized.ref 0 fun get_guid () = let val c = !guid_counter val _ = guid_counter := !guid_counter + 1 in string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c end fun tmp_file s = Path.expand (File.tmp_path (Path.basic s)); fun compile eqs = let val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else () val eqs = map (fn (_,b,c) => (b,c)) eqs val guid = get_guid () val module = "AMGHC_Prog_"^guid val (arity, source) = haskell_prog module eqs val module_file = tmp_file (module^".hs") val object_file = tmp_file (module^".o") val _ = File.write module_file source val _ = - Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ - Bash.string (File.platform_path module_file)) + Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ File.bash_platform_path module_file) val _ = if not (File.exists object_file) then raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')") else () in (guid, module_file, arity) end fun parse_result arity_of result = let val result = String.explode result fun shift NONE x = SOME x | shift (SOME y) x = SOME (y*10 + x) fun parse_int' x (#"0"::rest) = parse_int' (shift x 0) rest | parse_int' x (#"1"::rest) = parse_int' (shift x 1) rest | parse_int' x (#"2"::rest) = parse_int' (shift x 2) rest | parse_int' x (#"3"::rest) = parse_int' (shift x 3) rest | parse_int' x (#"4"::rest) = parse_int' (shift x 4) rest | parse_int' x (#"5"::rest) = parse_int' (shift x 5) rest | parse_int' x (#"6"::rest) = parse_int' (shift x 6) rest | parse_int' x (#"7"::rest) = parse_int' (shift x 7) rest | parse_int' x (#"8"::rest) = parse_int' (shift x 8) rest | parse_int' x (#"9"::rest) = parse_int' (shift x 9) rest | parse_int' x rest = (x, rest) fun parse_int rest = parse_int' NONE rest fun parse (#"C"::rest) = (case parse_int rest of (SOME c, rest) => let val (args, rest) = parse_list (the (arity_of c)) rest fun app_args [] t = t | app_args (x::xs) t = app_args xs (App (t, x)) in (app_args args (Const c), rest) end | (NONE, _) => raise Run "parse C") | parse (#"c"::rest) = (case parse_int rest of (SOME c, rest) => (Const c, rest) | _ => raise Run "parse c") | parse (#"A"::rest) = let val (a, rest) = parse rest val (b, rest) = parse rest in (App (a,b), rest) end | parse (#"L"::_) = raise Run "there may be no abstraction in the result" | parse _ = raise Run "invalid result" and parse_list n rest = if n = 0 then ([], rest) else let val (x, rest) = parse rest val (xs, rest) = parse_list (n-1) rest in (x::xs, rest) end val (parsed, rest) = parse result fun is_blank (#" "::rest) = is_blank rest | is_blank (#"\n"::rest) = is_blank rest | is_blank [] = true | is_blank _ = false in if is_blank rest then parsed else raise Run "non-blank suffix in result file" end fun run (guid, module_file, arity) t = let val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") fun arity_of c = Inttab.lookup arity c val callguid = get_guid() val module = "AMGHC_Prog_"^guid val call = module^"_Call_"^callguid val result_file = tmp_file (module^"_Result_"^callguid^".txt") val call_file = tmp_file (call^".hs") val term = print_term arity_of 0 t val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^ File.platform_path result_file^"\" ("^term^")" val _ = File.write call_file call_source val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^ - Bash.string (File.platform_path module_file) ^ " " ^ - Bash.string (File.platform_path call_file)) + File.bash_platform_path module_file ^ " " ^ File.bash_platform_path call_file) val result = File.read result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')") val t' = parse_result arity_of result val _ = File.rm call_file val _ = File.rm result_file in t' end end diff --git a/src/HOL/Tools/Quickcheck/narrowing_generators.ML b/src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML @@ -1,548 +1,548 @@ (* Title: HOL/Tools/Quickcheck/narrowing_generators.ML Author: Lukas Bulwahn, TU Muenchen Narrowing-based counterexample generation. *) signature NARROWING_GENERATORS = sig val allow_existentials : bool Config.T val finite_functions : bool Config.T val overlord : bool Config.T val ghc_options : string Config.T (* FIXME prefer settings, i.e. getenv (!?) *) val active : bool Config.T datatype counterexample = Universal_Counterexample of (term * counterexample) | Existential_Counterexample of (term * counterexample) list | Empty_Assignment val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context end structure Narrowing_Generators : NARROWING_GENERATORS = struct (* configurations *) val allow_existentials = Attrib.setup_config_bool \<^binding>\quickcheck_allow_existentials\ (K true) val finite_functions = Attrib.setup_config_bool \<^binding>\quickcheck_finite_functions\ (K true) val overlord = Attrib.setup_config_bool \<^binding>\quickcheck_narrowing_overlord\ (K false) val ghc_options = Attrib.setup_config_string \<^binding>\quickcheck_narrowing_ghc_options\ (K "") (* partial_term_of instances *) fun mk_partial_term_of (x, T) = Const (\<^const_name>\Quickcheck_Narrowing.partial_term_of_class.partial_term_of\, Term.itselfT T --> \<^typ>\narrowing_term\ --> \<^typ>\Code_Evaluation.term\) $ Logic.mk_type T $ x (** formal definition **) fun add_partial_term_of tyco raw_vs thy = let val vs = map (fn (v, _) => (v, \<^sort>\typerep\)) raw_vs val ty = Type (tyco, map TFree vs) val lhs = Const (\<^const_name>\partial_term_of\, Term.itselfT ty --> \<^typ>\narrowing_term\ --> \<^typ>\Code_Evaluation.term\) $ Free ("x", Term.itselfT ty) $ Free ("t", \<^typ>\narrowing_term\) val rhs = \<^term>\undefined :: Code_Evaluation.term\ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv" in thy |> Class.instantiation ([tyco], vs, \<^sort>\partial_term_of\) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq)) |> snd |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) end fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = let val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\partial_term_of\) andalso Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\typerep\ in if need_inst then add_partial_term_of tyco raw_vs thy else thy end (** code equations for datatypes **) fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = let val frees = map Free (Name.invent_names Name.context "a" (map (K \<^typ>\narrowing_term\) tys)) val narrowing_term = \<^term>\Quickcheck_Narrowing.Narrowing_constructor\ $ HOLogic.mk_number \<^typ>\integer\ i $ HOLogic.mk_list \<^typ>\narrowing_term\ (rev frees) val rhs = fold (fn u => fn t => \<^term>\Code_Evaluation.App\ $ t $ u) (map mk_partial_term_of (frees ~~ tys)) (\<^term>\Code_Evaluation.Const\ $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) val insts = map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), narrowing_term, rhs] val cty = Thm.global_ctyp_of thy ty in @{thm partial_term_of_anything} |> Thm.instantiate' [SOME cty] insts |> Thm.varifyT_global end fun add_partial_term_of_code tyco raw_vs raw_cs thy = let val algebra = Sign.classes_of thy val vs = map (fn (v, sort) => (v, curry (Sorts.inter_sort algebra) \<^sort>\typerep\ sort)) raw_vs val ty = Type (tyco, map TFree vs) val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs val const = Axclass.param_of_inst thy (\<^const_name>\partial_term_of\, tyco) val var_insts = map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), \<^term>\Quickcheck_Narrowing.Narrowing_variable p tt\, \<^term>\Code_Evaluation.Free (STR ''_'')\ $ HOLogic.mk_typerep ty] val var_eq = @{thm partial_term_of_anything} |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts |> Thm.varifyT_global val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs in thy |> Code.declare_default_eqns_global (map (rpair true) eqs) end fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\partial_term_of\ in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end (* narrowing generators *) (** narrowing specific names and types **) exception FUNCTION_TYPE val narrowingN = "narrowing" fun narrowingT T = \<^typ>\integer\ --> Type (\<^type_name>\Quickcheck_Narrowing.narrowing_cons\, [T]) fun mk_cons c T = Const (\<^const_name>\Quickcheck_Narrowing.cons\, T --> narrowingT T) $ Const (c, T) fun mk_apply (T, t) (U, u) = let val (_, U') = dest_funT U in (U', Const (\<^const_name>\Quickcheck_Narrowing.apply\, narrowingT U --> narrowingT T --> narrowingT U') $ u $ t) end fun mk_sum (t, u) = let val T = fastype_of t in Const (\<^const_name>\Quickcheck_Narrowing.sum\, T --> T --> T) $ t $ u end (** deriving narrowing instances **) fun mk_equations descr vs narrowings = let fun mk_call T = (T, Const (\<^const_name>\Quickcheck_Narrowing.narrowing_class.narrowing\, narrowingT T)) fun mk_aux_call fTs (k, _) (tyco, Ts) = let val T = Type (tyco, Ts) val _ = if not (null fTs) then raise FUNCTION_TYPE else () in (T, nth narrowings k) end fun mk_consexpr simpleT (c, xs) = let val Ts = map fst xs in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end fun mk_rhs exprs = foldr1 mk_sum exprs val rhss = Old_Datatype_Aux.interpret_construction descr vs { atyp = mk_call, dtyp = mk_aux_call } |> (map o apfst) Type |> map (fn (T, cs) => map (mk_consexpr T) cs) |> map mk_rhs val lhss = narrowings val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) in eqs end fun contains_recursive_type_under_function_types xs = exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = let val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..." val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames) in if not (contains_recursive_type_under_function_types descr) then thy |> Class.instantiation (tycos, vs, \<^sort>\narrowing\) |> Quickcheck_Common.define_functions (fn narrowings => mk_equations descr vs narrowings, NONE) prfx [] narrowingsN (map narrowingT (Ts @ Us)) |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) else thy end (* testing framework *) val target = "Haskell_Quickcheck" (** invocation of Haskell interpreter **) val narrowing_engine = File.read \<^file>\~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\ val pnf_narrowing_engine = File.read \<^file>\~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\ fun exec verbose code = ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context {line = 0, file = "generated code", verbose = verbose, debug = false} code) fun with_overlord_dir name f = let val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) val _ = Isabelle_System.mkdirs path in Exn.release (Exn.capture f path) end fun elapsed_time description e = let val ({elapsed, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds elapsed)) end fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = let val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie fun message s = if quiet then () else writeln s fun verbose_message s = if not quiet andalso verbose then writeln s else () val current_size = Unsynchronized.ref 0 val current_result = Unsynchronized.ref Quickcheck.empty_result val tmp_prefix = "Quickcheck_Narrowing" val ghc_options = Config.get ctxt ghc_options val with_tmp_dir = if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir fun run in_path = let fun mk_code_file module = let val (paths, base) = split_last module in Path.appends (in_path :: map Path.basic (paths @ [suffix ".hs" base])) end; val generatedN_suffix = suffix ".hs" Code_Target.generatedN; val includes = AList.delete (op =) [generatedN_suffix] code_modules |> (map o apfst) mk_code_file val code = the (AList.lookup (op =) code_modules [generatedN_suffix]) val code_file = mk_code_file [Code_Target.generatedN] val narrowing_engine_file = mk_code_file ["Narrowing_Engine"] val main_file = mk_code_file ["Main"] val main = "module Main where {\n\n" ^ "import System.IO;\n" ^ "import System.Environment;\n" ^ "import Narrowing_Engine;\n" ^ "import " ^ Code_Target.generatedN ^ " ;\n\n" ^ "main = getArgs >>= \\[potential, size] -> " ^ "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ Code_Target.generatedN ^ ".value ())\n\n}\n" val _ = map (uncurry File.write) (includes @ [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine), (code_file, code), (main_file, main)]) val executable = Path.append in_path (Path.basic "isabelle_quickcheck_narrowing") val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^ (space_implode " " - (map (Bash.string o File.platform_path) + (map File.bash_platform_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ - " -o " ^ Bash.string (File.platform_path executable) ^ ";" + " -o " ^ File.bash_platform_path executable ^ ";" val (_, compilation_time) = elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) val _ = Quickcheck.add_timing compilation_time current_result fun haskell_string_of_bool v = if v then "True" else "False" val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () fun with_size genuine_only k = if k > size then (NONE, !current_result) else let val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) (fn () => Isabelle_System.bash_output (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k)) val _ = Quickcheck.add_timing timing current_result in if response = "NONE\n" then with_size genuine_only (k + 1) else let val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response) val ml_code = "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))" val ctxt' = ctxt |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) |> Context.proof_map (exec false ml_code) val counterexample = get ctxt' () in if is_genuine counterexample then (counterexample, !current_result) else let val cex = Option.map (rpair []) (counterexample_of counterexample) val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)) val _ = message "Quickcheck continues to find a genuine counterexample..." in with_size true (k + 1) end end end in with_size genuine_only 0 end in with_tmp_dir tmp_prefix run end fun dynamic_value_strict opts cookie ctxt postproc t = let fun evaluator program _ vs_ty_t deps = Exn.interruptible_capture (value opts ctxt cookie) (Code_Target.compilation_text ctxt target program deps true vs_ty_t) in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end (** counterexample generator **) datatype counterexample = Universal_Counterexample of (term * counterexample) | Existential_Counterexample of (term * counterexample) list | Empty_Assignment fun map_counterexample _ Empty_Assignment = Empty_Assignment | map_counterexample f (Universal_Counterexample (t, c)) = Universal_Counterexample (f t, map_counterexample f c) | map_counterexample f (Existential_Counterexample cs) = Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs) structure Data = Proof_Data ( type T = (unit -> (bool * term list) option) * (unit -> counterexample option) val empty: T = (fn () => raise Fail "counterexample", fn () => raise Fail "existential_counterexample") fun init _ = empty ) val get_counterexample = #1 o Data.get; val get_existential_counterexample = #2 o Data.get; val put_counterexample = Data.map o @{apply 2(1)} o K val put_existential_counterexample = Data.map o @{apply 2(2)} o K fun finitize_functions (xTs, t) = let val (names, boundTs) = split_list xTs fun mk_eval_ffun dT rT = Const (\<^const_name>\Quickcheck_Narrowing.eval_ffun\, Type (\<^type_name>\Quickcheck_Narrowing.ffun\, [dT, rT]) --> dT --> rT) fun mk_eval_cfun dT rT = Const (\<^const_name>\Quickcheck_Narrowing.eval_cfun\, Type (\<^type_name>\Quickcheck_Narrowing.cfun\, [rT]) --> dT --> rT) fun eval_function (Type (\<^type_name>\fun\, [dT, rT])) = let val (rt', rT') = eval_function rT in (case dT of Type (\<^type_name>\fun\, _) => (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), Type (\<^type_name>\Quickcheck_Narrowing.cfun\, [rT'])) | _ => (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), Type (\<^type_name>\Quickcheck_Narrowing.ffun\, [dT, rT']))) end | eval_function (T as Type (\<^type_name>\prod\, [fT, sT])) = let val (ft', fT') = eval_function fT val (st', sT') = eval_function sT val T' = Type (\<^type_name>\prod\, [fT', sT']) val map_const = Const (\<^const_name>\map_prod\, (fT' --> fT) --> (sT' --> sT) --> T' --> T) fun apply_dummy T t = absdummy T (t (Bound 0)) in (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T') end | eval_function T = (I, T) val (tt, boundTs') = split_list (map eval_function boundTs) val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t) in (names ~~ boundTs', t') end fun dest_ffun (Type (\<^type_name>\Quickcheck_Narrowing.ffun\, [dT, rT])) = (dT, rT) fun eval_finite_functions (Const (\<^const_name>\Quickcheck_Narrowing.ffun.Constant\, T) $ value) = absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) | eval_finite_functions (Const (\<^const_name>\Quickcheck_Narrowing.ffun.Update\, T) $ a $ b $ f) = let val (T1, T2) = dest_ffun (body_type T) in Quickcheck_Common.mk_fun_upd T1 T2 (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) end | eval_finite_functions t = t (** tester **) val rewrs = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) (@{thms all_simps} @ @{thms ex_simps}) @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}, @{thm meta_eq_to_obj_eq [OF Ex1_def]}] fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t fun strip_quantifiers (Const (\<^const_name>\Ex\, _) $ Abs (x, T, t)) = apfst (cons (\<^const_name>\Ex\, (x, T))) (strip_quantifiers t) | strip_quantifiers (Const (\<^const_name>\All\, _) $ Abs (x, T, t)) = apfst (cons (\<^const_name>\All\, (x, T))) (strip_quantifiers t) | strip_quantifiers t = ([], t) fun contains_existentials t = exists (fn (Q, _) => Q = \<^const_name>\Ex\) (fst (strip_quantifiers t)) fun mk_property qs t = let fun enclose (\<^const_name>\Ex\, (x, T)) t = Const (\<^const_name>\Quickcheck_Narrowing.exists\, (T --> \<^typ>\property\) --> \<^typ>\property\) $ Abs (x, T, t) | enclose (\<^const_name>\All\, (x, T)) t = Const (\<^const_name>\Quickcheck_Narrowing.all\, (T --> \<^typ>\property\) --> \<^typ>\property\) $ Abs (x, T, t) in fold_rev enclose qs (\<^term>\Quickcheck_Narrowing.Property\ $ t) end fun mk_case_term ctxt p ((\<^const_name>\Ex\, (x, T)) :: qs') (Existential_Counterexample cs) = Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) => (t, mk_case_term ctxt (p - 1) qs' c)) cs) | mk_case_term ctxt p ((\<^const_name>\All\, _) :: qs') (Universal_Counterexample (t, c)) = if p = 0 then t else mk_case_term ctxt (p - 1) qs' c val post_process = perhaps (try Quickcheck_Common.post_process_term) o eval_finite_functions fun mk_terms ctxt qs result = let val ps = filter (fn (_, (\<^const_name>\All\, _)) => true | _ => false) (map_index I qs) in map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps |> map (apsnd post_process) end fun test_term ctxt catch_code_errors (t, _) = let fun dest_result (Quickcheck.Result r) = r val opts = ((Config.get ctxt Quickcheck.genuine_only, (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)), Config.get ctxt Quickcheck.size) val thy = Proof_Context.theory_of ctxt val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t val pnf_t = make_pnf_term thy t' in if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then let fun wrap f (qs, t) = let val (qs1, qs2) = split_list qs in apfst (map2 pair qs1) (f (qs2, t)) end val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I val (qs, prop_t) = finitize (strip_quantifiers pnf_t) val act = if catch_code_errors then try else (fn f => SOME o f) val execute = dynamic_value_strict (true, opts) ((K true, fn _ => error ""), (get_existential_counterexample, put_existential_counterexample, "Narrowing_Generators.put_existential_counterexample")) ctxt (apfst o Option.map o map_counterexample) in (case act execute (mk_property qs prop_t) of SOME (counterexample, result) => Quickcheck.Result {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = #timings (dest_result result), reports = #reports (dest_result result)} | NONE => (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; Quickcheck.empty_result)) end else let val frees = Term.add_frees t [] val t' = fold_rev absfree frees t fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t)) val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I fun ensure_testable t = Const (\<^const_name>\Quickcheck_Narrowing.ensure_testable\, fastype_of t --> fastype_of t) $ t fun is_genuine (SOME (true, _)) = true | is_genuine _ = false val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process)) val act = if catch_code_errors then try else (fn f => SOME o f) val execute = dynamic_value_strict (false, opts) ((is_genuine, counterexample_of), (get_counterexample, put_counterexample, "Narrowing_Generators.put_counterexample")) ctxt (apfst o Option.map o apsnd o map) in (case act execute (ensure_testable (finitize t')) of SOME (counterexample, result) => Quickcheck.Result {counterexample = counterexample_of counterexample, evaluation_terms = Option.map (K []) counterexample, timings = #timings (dest_result result), reports = #reports (dest_result result)} | NONE => (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; Quickcheck.empty_result)) end end fun test_goals ctxt catch_code_errors insts goals = if not (getenv "ISABELLE_GHC" = "") then let val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..." val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals in Quickcheck_Common.collect_results (test_term ctxt catch_code_errors) (maps (map snd) correct_inst_goals) [] end else (if Config.get ctxt Quickcheck.quiet then () else writeln ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set " ^ "this variable to your GHC Haskell compiler in your settings file. " ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false."); [Quickcheck.empty_result]) (* setup *) val active = Attrib.setup_config_bool \<^binding>\quickcheck_narrowing_active\ (K false) val _ = Theory.setup (Code.datatype_interpretation ensure_partial_term_of #> Code.datatype_interpretation ensure_partial_term_of_code #> Quickcheck_Common.datatype_interpretation \<^plugin>\quickcheck_narrowing\ (\<^sort>\narrowing\, instantiate_narrowing_datatype) #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))) end diff --git a/src/HOL/Tools/SMT/smt_solver.ML b/src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML +++ b/src/HOL/Tools/SMT/smt_solver.ML @@ -1,315 +1,315 @@ (* Title: HOL/Tools/SMT/smt_solver.ML Author: Sascha Boehme, TU Muenchen SMT solvers registry and SMT tactic. *) signature SMT_SOLVER = sig (*configuration*) datatype outcome = Unsat | Sat | Unknown | Time_Out type parsed_proof = {outcome: SMT_Failure.failure option, fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option, atp_proof: unit -> (term, string) ATP_Proof.atp_step list} type solver_config = {name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, default_max_relevant: int, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof) option, replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option} (*registry*) val add_solver: solver_config -> theory -> theory val default_max_relevant: Proof.context -> string -> int (*filter*) val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list -> int -> Time.time -> parsed_proof (*tactic*) val smt_tac: Proof.context -> thm list -> int -> tactic val smt_tac': Proof.context -> thm list -> int -> tactic end; structure SMT_Solver: SMT_SOLVER = struct (* interface to external solvers *) local fun make_command command options problem_path proof_path = Bash.strings (command () @ options) ^ " " ^ - Bash.string (File.platform_path problem_path) ^ + File.bash_platform_path problem_path ^ " > " ^ File.bash_path proof_path ^ " 2>&1" fun with_trace ctxt msg f x = let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () in f x end fun run ctxt name mk_cmd input = (case SMT_Config.certificates_of ctxt of NONE => if not (SMT_Config.is_available ctxt name) then error ("The SMT solver " ^ quote name ^ " is not installed") else if Config.get ctxt SMT_Config.debug_files = "" then with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input else let val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) val in_path = Path.ext "smt_in" base_path val out_path = Path.ext "smt_out" base_path in Cache_IO.raw_run mk_cmd input in_path out_path end | SOME certs => (case Cache_IO.lookup certs input of (NONE, key) => if Config.get ctxt SMT_Config.read_only_certificates then error ("Bad certificate cache: missing certificate") else Cache_IO.run_and_cache certs key mk_cmd input | (SOME output, _) => with_trace ctxt ("Using cached certificate from " ^ Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output)) (* Z3 returns 1 if "get-proof" or "get-model" fails. veriT returns 255. *) val normal_return_codes = [0, 1, 255] fun run_solver ctxt name mk_cmd input = let fun pretty tag lines = Pretty.string_of (Pretty.big_list tag (map Pretty.str lines)) val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) = Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err val output = drop_suffix (equal "") res val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)] val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)] val _ = member (op =) normal_return_codes return_code orelse raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) in output end fun trace_assms ctxt = SMT_Config.trace_msg ctxt (Pretty.string_of o Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) = let fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) in SMT_Config.trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "Names:" [ Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () end in fun invoke name command smt_options ithms ctxt = let val options = SMT_Config.solver_options_of ctxt val comments = [space_implode " " options] val (str, replay_data as {context = ctxt', ...}) = ithms |> tap (trace_assms ctxt) |> SMT_Translate.translate ctxt smt_options comments ||> tap trace_replay_data in (run_solver ctxt' name (make_command command options) str, replay_data) end end (* configuration *) datatype outcome = Unsat | Sat | Unknown | Time_Out type parsed_proof = {outcome: SMT_Failure.failure option, fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option, atp_proof: unit -> (term, string) ATP_Proof.atp_step list} type solver_config = {name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, default_max_relevant: int, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof) option, replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option} (* check well-sortedness *) val has_topsort = Term.exists_type (Term.exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)) (* top sorts cause problems with atomization *) fun check_topsort ctxt thm = if has_topsort (Thm.prop_of thm) then (SMT_Normalize.drop_fact_warning ctxt thm; TrueI) else thm (* registry *) type solver_info = { command: unit -> string list, smt_options: (string * string) list, default_max_relevant: int, parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof, replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm} structure Solvers = Generic_Data ( type T = solver_info Symtab.table val empty = Symtab.empty val extend = I fun merge data = Symtab.merge (K true) data ) local fun parse_proof outcome parse_proof0 outer_ctxt replay_data xfacts prems concl output = (case outcome output of (Unsat, lines) => (case parse_proof0 of SOME pp => pp outer_ctxt replay_data xfacts prems concl lines | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []}) | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out) | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat))) fun replay outcome replay0 oracle outer_ctxt (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output = (case outcome output of (Unsat, lines) => if Config.get ctxt SMT_Config.oracle then oracle () else (case replay0 of SOME replay => replay outer_ctxt replay_data lines | NONE => error "No proof reconstruction for solver -- \ \declare [[smt_oracle]] to allow oracle") | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out) | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat))) val cfalse = Thm.cterm_of \<^context> \<^prop>\False\ in fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome, parse_proof = parse_proof0, replay = replay0} : solver_config) = let fun solver oracle = { command = command, smt_options = smt_options, default_max_relevant = default_max_relevant, parse_proof = parse_proof (outcome name) parse_proof0, replay = replay (outcome name) replay0 oracle} val info = {name = name, class = class, avail = avail, options = options} in Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, oracle) => Context.theory_map (Solvers.map (Symtab.update_new (name, solver oracle)))) #> Context.theory_map (SMT_Config.add_solver info) end end fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) fun name_and_info_of ctxt = let val name = SMT_Config.solver_of ctxt in (name, get_info ctxt name) end val default_max_relevant = #default_max_relevant oo get_info fun apply_solver_and_replay ctxt thms0 = let val thms = map (check_topsort ctxt) thms0 val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt val (output, replay_data) = invoke name command smt_options (SMT_Normalize.normalize ctxt thms) ctxt in replay ctxt replay_data output end (* filter *) fun smt_filter ctxt0 goal xfacts i time_limit = let val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit) val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal fun negate ct = Thm.dest_comb ct ||> Thm.apply \<^cterm>\Not\ |-> Thm.apply val cprop = (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of SOME ct => ct | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal")) val conjecture = Thm.assume cprop val facts = map snd xfacts val thms = conjecture :: prems @ facts val thms' = map (check_topsort ctxt) thms val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt val (output, replay_data) = invoke name command smt_options (SMT_Normalize.normalize ctxt thms') ctxt in parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output end handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = NONE, atp_proof = K []} (* SMT tactic *) local fun str_of ctxt fail = "Solver " ^ SMT_Config.solver_of ctxt ^ ": " ^ SMT_Failure.string_of_failure fail fun safe_solve ctxt facts = SOME (apply_solver_and_replay ctxt facts) handle SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) => error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^ SMT_Failure.string_of_failure fail ^ " (setting the " ^ "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)") | SMT_Failure.SMT fail => error (str_of ctxt fail) fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1 | resolve _ NONE = no_tac fun tac prove ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) THEN' resolve_tac ctxt @{thms ccontr} THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve ctxt' (prove ctxt' (rules @ prems))) ctxt in val smt_tac = tac safe_solve val smt_tac' = tac (SOME oo apply_solver_and_replay) end 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,178 +1,181 @@ (* 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 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 fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_lines: Path.T -> string list val read_pages: Path.T -> string list val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit val generate: Path.T -> string -> unit val output: BinIO.outstream -> string -> unit val write_list: Path.T -> string list -> unit val append_list: Path.T -> string list -> unit val write_buffer: Path.T -> Buffer.T -> 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_Syntax.string o standard_path; val bash_paths = Bash_Syntax.strings o map standard_path; +val bash_platform_path = Bash_Syntax.string o platform_path; + (* full_path *) fun full_path dir path = let val path' = Path.expand path; val _ = Path.is_current path' andalso error "Bad file specification"; val path'' = Path.append dir path'; in if Path.is_absolute path'' then path'' else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path'' end; (* tmp_path *) fun tmp_path path = Path.append (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 => 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 *) (* scalable iterator: . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine . optional terminator at end-of-input *) fun fold_chunks terminator f path a = open_input (fn file => let fun read buf x = (case Byte.bytesToString (BinIO.input file) of "" => (case Buffer.content buf of "" => x | line => f line x) | input => (case String.fields (fn c => c = terminator) input of [rest] => read (Buffer.add rest buf) x | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x))) and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x | read_lines (line :: more) x = read_lines more (f line x); in read Buffer.empty a end) path; fun fold_lines f = fold_chunks #"\n" f; fun fold_pages f = fold_chunks #"\f" f; fun read_lines path = rev (fold_lines cons path []); fun read_pages path = rev (fold_pages cons path []); val read = open_input (Byte.bytesToString o BinIO.inputAll); (* output *) fun output file txt = BinIO.output (file, Byte.stringToBytes txt); 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 path txt = write_list path [txt]; fun append path txt = append_list path [txt]; fun generate path txt = if try read path = SOME txt then () else write path txt; fun write_buffer path buf = open_output (Buffer.output buf o output) path; (* 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/Tools/ghc.ML b/src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML +++ b/src/Pure/Tools/ghc.ML @@ -1,91 +1,91 @@ (* Title: Pure/Tools/ghc.ML Author: Makarius Support for GHC: Glasgow Haskell Compiler. *) signature GHC = sig val print_codepoint: UTF8.codepoint -> string val print_symbol: Symbol.symbol -> string val print_string: string -> string val project_template: {depends: string list, modules: string list} -> string val new_project: Path.T -> {name: string, depends: string list, modules: string list} -> unit end; structure GHC: GHC = struct (** string literals **) fun print_codepoint c = (case c of 34 => "\\\"" | 39 => "\\'" | 92 => "\\\\" | 7 => "\\a" | 8 => "\\b" | 9 => "\\t" | 10 => "\\n" | 11 => "\\v" | 12 => "\\f" | 13 => "\\r" | c => if c >= 32 andalso c < 127 then chr c else "\\" ^ string_of_int c ^ "\\&"); fun print_symbol sym = (case Symbol.decode sym of Symbol.Char s => print_codepoint (ord s) | Symbol.UTF8 s => UTF8.decode_permissive s |> map print_codepoint |> implode | Symbol.Sym s => "\\092<" ^ s ^ ">" | Symbol.Control s => "\\092<^" ^ s ^ ">" | _ => translate_string (print_codepoint o ord) sym); val print_string = quote o implode o map print_symbol o Symbol.explode; (** project setup **) fun project_template {depends, modules} = \<^verbatim>\{-# START_FILE {{name}}.cabal #-} name: {{name}} version: 0.1.0.0 homepage: default license: BSD3 author: default maintainer: default category: default build-type: Simple cabal-version: >=1.10 executable {{name}} hs-source-dirs: src main-is: Main.hs default-language: Haskell2010 build-depends: \ ^ commas ("base >= 4.7 && < 5" :: depends) ^ \<^verbatim>\ other-modules: \ ^ commas modules ^ \<^verbatim>\ {-# START_FILE Setup.hs #-} import Distribution.Simple main = defaultMain {-# START_FILE src/Main.hs #-} module Main where main :: IO () main = return () \; fun new_project dir {name, depends, modules} = let val template_path = Path.append dir (Path.basic name |> Path.ext "hsfiles"); val _ = File.write template_path (project_template {depends = depends, modules = modules}); val {rc, err, ...} = Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ - " --bare " ^ Bash.string (File.platform_path template_path)); + " --bare " ^ File.bash_platform_path template_path); in if rc = 0 then () else error err end; end;