Quelle ml_antiquotations.ML Sprache: SML

(*  Title:      Pure/ML/ml_antiquotations.ML
    Author:     Makarius

Miscellaneous ML antiquotations.
*)

signature ML_ANTIQUOTATIONS =
sig
  val make_judgment: Proof.context -> term -> term
  val dest_judgment: Proof.context -> term -> term
end;

structure ML_Antiquotations: ML_ANTIQUOTATIONS =
struct

(* ML support *)

val _ = Theory.setup
(ML_Antiquotation.inline \<^binding>\<open>undefined\<close>
    (Scan.succeed "(raise General.Match)") #>

  ML_Antiquotation.inline \<^binding>\<open>assert\<close>
    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>

  ML_Antiquotation.declaration_embedded \<^binding>\<open>print\<close>
    (Scan.lift (Scan.optional Parse.embedded "Output.writeln"))
      (fn src => fn output => fn ctxt =>
        let
          val struct_name = ML_Context.struct_name ctxt;
          val (_, pos) = Token.name_of_src src;
          val (a, ctxt') = ML_Context.variant "output" ctxt;
          val env =
            "val " ^ a ^ ": string -> unit =\n\
            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
            ML_Syntax.print_position pos ^ "));\n";
          val body =
            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
        in (K (env, body), ctxt') end) #>

  ML_Antiquotation.value \<^binding>\<open>rat\<close>
    (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
      Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
        "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #>

  ML_Antiquotation.conditional \<^binding>\<open>if_linux\<close> (fn _ => ML_System.platform_is_linux) #>
  ML_Antiquotation.conditional \<^binding>\<open>if_macos\<close> (fn _ => ML_System.platform_is_macos) #>
  ML_Antiquotation.conditional \<^binding>\<open>if_windows\<close> (fn _ => ML_System.platform_is_windows) #>
  ML_Antiquotation.conditional \<^binding>\<open>if_unix\<close> (fn _ => ML_System.platform_is_unix));

(* formal entities *)

val _ = Theory.setup
(ML_Antiquotation.value_embedded \<^binding>\<open>system_option\<close>
    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
      (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>

  ML_Antiquotation.value_embedded \<^binding>\<open>theory\<close>
    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
      (Theory.check {long = false} ctxt (name, pos);
       "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
        ML_Syntax.print_string name))
    || Scan.succeed "Proof_Context.theory_of ML_context") #>

  ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
      (Theory.check {long = false} ctxt (name, pos);
       "Proof_Context.get_global {long = false} (Proof_Context.theory_of ML_context) " ^
        ML_Syntax.print_string name))) #>

  ML_Antiquotation.inline \<^binding>\<open>context\<close>
    (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>typ\<close>
    (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>term\<close>
    (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>prop\<close>
    (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>

  ML_Antiquotation.value_embedded \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
    "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>

  ML_Antiquotation.value_embedded \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>

  ML_Antiquotation.value_embedded \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>oracle_name\<close>
    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
      ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos)))));

(* type classes *)

fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) =>
  Proof_Context.read_class ctxt s
  |> syn ? Lexicon.mark_class
  |> ML_Syntax.print_string);

val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>class\<close> (class false) #>
  ML_Antiquotation.inline_embedded \<^binding>\<open>class_syntax\<close> (class true) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>sort\<close>
    (Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) =>
      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));

(* type constructors *)

fun type_name kind check = Args.context -- Scan.lift (Parse.token Parse.embedded)
  >> (fn (ctxt, tok) =>
    let
      val s = Token.inner_syntax_of tok;
      val (_, pos) = Input.source_content (Token.input_of tok);
      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
      val res =
        (case try check (c, decl) of
          SOME res => res
        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
    in ML_Syntax.print_string res end);

val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>type_name\<close>
    (type_name "logical type" (fn (c, Type.Logical_Type _) => c)) #>
  ML_Antiquotation.inline_embedded \<^binding>\<open>type_abbrev\<close>
    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
  ML_Antiquotation.inline_embedded \<^binding>\<open>nonterminal\<close>
    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
  ML_Antiquotation.inline_embedded \<^binding>\<open>type_syntax\<close>
    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));

(* constants *)

fun const_name check = Args.context -- Scan.lift (Parse.token Parse.embedded)
  >> (fn (ctxt, tok) =>
    let
      val s = Token.inner_syntax_of tok;
      val (_, pos) = Input.source_content (Token.input_of tok);
      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
      val res = check (Proof_Context.consts_of ctxt, c)
        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
    in ML_Syntax.print_string res end);

val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>const_name\<close>
    (const_name (fn (consts, c) => (Consts.the_const_type consts c; c))) #>
  ML_Antiquotation.inline_embedded \<^binding>\<open>const_abbrev\<close>
    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
  ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close>
    (const_name (fn (_, c) => Lexicon.mark_const c)) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
      ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #>

  ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close>
    (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax) -- Scan.optional
        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
      >> (fn ((ctxt, (raw_c, pos)), Ts) =>
        let
          val Const (c, _) =
            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
          val consts = Proof_Context.consts_of ctxt;
          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
          val _ = length Ts <> n andalso
            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
              quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos);
          val const = Const (c, Consts.instance consts (c, Ts));
        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));

(* object-logic judgment *)

fun make_judgment ctxt =
  let val const = Object_Logic.judgment_const ctxt
  in fn t => Const const $ t end;

fun dest_judgment ctxt =
  let
    val is_judgment = Object_Logic.is_judgment ctxt;
    val drop_judgment = Object_Logic.drop_judgment ctxt;
  in
    fn t =>
      if is_judgment t then drop_judgment t
      else raise TERM ("dest_judgment", [t])
  end;

val _ = Theory.setup
(ML_Antiquotation.value \<^binding>\<open>make_judgment\<close>
   (Scan.succeed "ML_Antiquotations.make_judgment ML_context") #>
  ML_Antiquotation.value \<^binding>\<open>dest_judgment\<close>
   (Scan.succeed "ML_Antiquotations.dest_judgment ML_context"));

(* type/term constructors *)

local

val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;

val parse_name_args =
  Parse.input Parse.name -- Scan.repeat Parse.embedded_ml;

val parse_for_args =
  Scan.optional (Parse.$$$ "for" |-- Parse.!!! (Scan.repeat1 Parse.embedded_ml)) [];

fun parse_body b =
  if b then Parse.$$$ "=>" |-- Parse.!!! (Parse.embedded_ml >> single) else Scan.succeed [];

fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_"
  | is_dummy _ = false;

val ml = ML_Lex.tokenize_no_range;
val ml_range = ML_Lex.tokenize_range;
val ml_dummy = ml "_";
fun ml_enclose range x = ml "(" @ x @ ml_range range ")";
fun ml_parens x = ml "(" @ x @ ml ")";
fun ml_bracks x = ml "[" @ x @ ml "]";
fun ml_commas xs = flat (separate (ml ", ") xs);
val ml_list = ml_bracks o ml_commas;
val ml_string = ml o ML_Syntax.print_string;
fun ml_pair (x, y) = ml_parens (ml_commas [x, y]);

fun type_antiquotation binding {function} =
  ML_Context.add_antiquotation_embedded binding
    (fn range => fn input => fn ctxt =>
      let
        val ((s, type_args), fn_body) = input
          |> Parse.read_embedded ctxt keywords (parse_name_args -- parse_body function);
        val pos = Input.pos_of s;

        val Type (c, Ts) =
          Proof_Context.read_type_name {proper = true, strict = true} ctxt
            (Syntax.implode_input s);
        val n = length Ts;
        val _ =
          length type_args = n orelse
            error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^
              " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos);

        val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt;
        val (decls2, ctxt2) = ML_Context.expand_antiquotes_list fn_body ctxt1;
        fun decl' ctxt' =
          let
            val (ml_args_env, ml_args_body) = split_list (decls1 ctxt');
            val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt');
            val ml1 =
              ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body));
            val ml2 =
              if function then
                ml_enclose range
                 (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
                  ml "| T => " @ ml_range range "raise" @
                  ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])")
              else ml1;
          in (flat (ml_args_env @ ml_fn_env), ml2) end;
      in (decl', ctxt2) end);

fun const_antiquotation binding {pattern, function} =
  ML_Context.add_antiquotation_embedded binding
    (fn range => fn input => fn ctxt =>
      let
        val (((s, type_args), term_args), fn_body) = input
          |> Parse.read_embedded ctxt keywords
              (parse_name_args -- parse_for_args -- parse_body function);

        val Const (c, T) =
          Proof_Context.read_const {proper = true, strict = true} ctxt
            (Syntax.implode_input s);

        val consts = Proof_Context.consts_of ctxt;
        val type_paths = Consts.type_arguments consts c;
        val type_params = map Term.dest_TVar (Consts.typargs consts (c, T));

        val n = length type_params;
        val m = length (Term.binder_types T);

        fun err msg =
          error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^
            Position.here (Input.pos_of s));
        val _ =
          length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)");
        val _ =
          length term_args > m andalso Term.is_Type (Term.body_type T) andalso
            err (" cannot have more than " ^ string_of_int m ^ " argument(s)");

        val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt;
        val (decls2, ctxt2) = ML_Context.expand_antiquotes_list term_args ctxt1;
        val (decls3, ctxt3) = ML_Context.expand_antiquotes_list fn_body ctxt2;
        fun decl' ctxt' =
          let
            val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt');
            val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt');
            val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt');

            val relevant = map is_dummy type_args ~~ type_paths;
            fun relevant_path is =
              not pattern orelse
                let val p = rev is
                in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end;

            val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1);
            fun ml_typ is (Type (d, Us)) =
                  if relevant_path is then
                    ml "Term.Type " @
                    ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us))
                  else ml_dummy
              | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy
              | ml_typ _ (TFree _) = raise Match;

            fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T)
              | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u);

            val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env);
            val ml1 = ml_enclose range (ml_app (rev ml_args_body2));
            val ml2 =
              if function then
                ml_enclose range
                 (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
                  ml "| t => " @ ml_range range "raise" @
                  ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])")
              else ml1;
          in (ml_env, ml2) end;
      in (decl', ctxt3) end);

val _ = Theory.setup
(type_antiquotation \<^binding>\<open>Type\<close> {function = false} #>
  type_antiquotation \<^binding>\<open>Type_fn\<close> {function = true} #>
  const_antiquotation \<^binding>\<open>Const\<close> {pattern = false, function = false} #>
  const_antiquotation \<^binding>\<open>Const_\<close> {pattern = true, function = false} #>
  const_antiquotation \<^binding>\<open>Const_fn\<close> {pattern = true, function = true});

in end;

(* exception handling *)

local

val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range;
val tokenize_range_text = map Antiquote.Text oo ML_Lex.tokenize_range;

val bg_expr = tokenize_text "(fn () =>";
val en_expr = tokenize_text ")";
fun make_expr a = bg_expr @ a @ en_expr;

fun make_handler range a =
  tokenize_range_text range "(fn" @ a @
  tokenize_range_text range "| exn => Exn.reraise exn)";

fun report_special tok = (ML_Lex.pos_of tok, Markup.keyword3);

fun print_special tok =
  let val (pos, markup) = report_special tok
  in Markup.markup markup (ML_Lex.content_of tok) ^ Position.here pos end;

val is_catch = ML_Lex.is_ident_with (fn x => x = "catch");
val is_finally = ML_Lex.is_ident_with (fn x => x = "finally");
fun is_special t = is_catch t orelse is_finally t;
val is_special_text = fn Antiquote.Text t => is_special t | _ => false;

fun parse_try ctxt input =
  let
    val ants = ML_Lex.read_source input;
    val specials = ants
      |> map_filter (fn Antiquote.Text t => if is_special t then SOME t else NONE | _ => NONE);
    val _ = Context_Position.reports ctxt (map report_special specials);
  in
    (case specials of
      [] => ("Isabelle_Thread.try", [make_expr ants])
    | [s] =>
        let val (a, b) = ants |> chop_prefix (not o is_special_text) ||> tl in
          if is_finally s
          then ("Isabelle_Thread.try_finally", [make_expr a, make_expr b])
          else ("Isabelle_Thread.try_catch", [make_expr a, make_handler (ML_Lex.range_of s) b])
        end
    | _ => error ("Too many special keywords: " ^ commas (map print_special specials)))
  end;

fun parse_can (_: Proof.context) input =
  ("Isabelle_Thread.can", [make_expr (ML_Lex.read_source input)]);

in

val _ = Theory.setup
  (ML_Antiquotation.special_form \<^binding>\<open>try\<close> parse_try #>
   ML_Antiquotation.special_form \<^binding>\<open>can\<close> parse_can);

end;

(* special form for option type *)

val _ = Theory.setup
  (ML_Context.add_antiquotation_embedded \<^binding>\<open>if_none\<close>
    (fn _ => fn input => fn ctxt =>
      let
        val tokenize = ML_Lex.tokenize_no_range;

        val (decl, ctxt') = ML_Context.read_antiquotes input ctxt;
        fun decl' ctxt'' =
          let
            val (ml_env, ml_body) = decl ctxt'';
            val ml_body' = tokenize "(fn SOME x => x | NONE => " @ ml_body @ tokenize ")";
          in (ml_env, ml_body') end;
      in (decl', ctxt') end));

(* basic combinators *)

local

val parameter = Parse.position Parse.nat >> (fn (n, pos) =>
  if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos));

fun indices n = map string_of_int (1 upto n);

fun empty n = replicate_string n " []";
fun dummy n = replicate_string n " _";
fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n));
fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n));

val tuple = enclose "(" ")" o commas;
fun tuple_empty n = tuple (replicate n "[]");
fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n));
fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)"
fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n));

in

val _ = Theory.setup
(ML_Antiquotation.value \<^binding>\<open>map\<close>
    (Scan.lift parameter >> (fn n =>
      "fn f =>\n\
      \  let\n\
      \    fun map _" ^ empty n ^ " = []\n\
      \      | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\
      \      | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^
      " in map f end")) #>
  ML_Antiquotation.value \<^binding>\<open>fold\<close>
    (Scan.lift parameter >> (fn n =>
      "fn f =>\n\
      \  let\n\
      \    fun fold _" ^ empty n ^ " a = a\n\
      \      | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\
      \      | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
      " in fold f end")) #>
  ML_Antiquotation.value \<^binding>\<open>fold_map\<close>
    (Scan.lift parameter >> (fn n =>
      "fn f =>\n\
      \  let\n\
      \    fun fold_map _" ^ empty n ^ " a = ([], a)\n\
      \      | fold_map f" ^ cons n ^ " a =\n\
      \          let\n\
      \            val (x, a') = f" ^ vars "x" n ^ " a\n\
      \            val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\
      \          in (x :: xs, a'') end\n\
      \      | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
      " in fold_map f end")) #>
  ML_Antiquotation.value \<^binding>\<open>split_list\<close>
    (Scan.lift parameter >> (fn n =>
      "fn list =>\n\
      \  let\n\
      \    fun split_list [] =" ^ tuple_empty n ^ "\n\
      \      | split_list" ^ tuple_cons n ^ " =\n\
      \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
      \          in " ^ cons_tuple n ^ "end\n\
      \  in split_list list end")) #>
  ML_Antiquotation.value \<^binding>\<open>apply\<close>
    (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
      (fn (n, opt_index) =>
        let
          val cond =
            (case opt_index of
              NONE => K true
            | SOME (index, index_pos) =>
                if 1 <= index andalso index <= n then equal (string_of_int index)
                else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos));
        in
          "fn f => fn " ^ tuple_vars "x" n ^ " => " ^
            tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n))
        end)));

end;

(* outer syntax *)

val _ = Theory.setup
(ML_Antiquotation.value_embedded \<^binding>\<open>keyword\<close>
    (Args.context --
      Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true)))
      >> (fn (ctxt, (name, pos)) =>
        if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
          (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
           "Parse.$$$ " ^ ML_Syntax.print_string name)
        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
  ML_Antiquotation.value_embedded \<^binding>\<open>command_keyword\<close>
    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
      (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
        SOME markup =>
         (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
          ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
      | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));

end;

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.