Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: nunchaku_problem.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Tools/Nunchaku/nunchaku_problem.ML
    Author:     Jasmin Blanchette, VU Amsterdam
    Copyright   2015, 2016, 2017

Abstract syntax tree for Nunchaku problems.
*)

signature NUNCHAKU_PROBLEM =
sig
  eqtype ident

  datatype ty =
    NType of ident * ty list

  datatype tm =
    NAtom of int * ty
  | NConst of ident * ty list * ty
  | NAbs of tm * tm
  | NMatch of tm * (ident * tm list * tm) list
  | NApp of tm * tm

  type nun_copy_spec =
    {abs_ty: ty,
     rep_ty: ty,
     subset: tm option,
     quotient: tm option,
     abs: tm,
     rep: tm}

  type nun_ctr_spec =
    {ctr: tm,
     arg_tys: ty list}

  type nun_co_data_spec =
    {ty: ty,
     ctrs: nun_ctr_spec list}

  type nun_const_spec =
    {const: tm,
     props: tm list}

  type nun_consts_spec =
    {consts: tm list,
     props: tm list}

  datatype nun_command =
    NTVal of ty * (int option * int option)
  | NCopy of nun_copy_spec
  | NData of nun_co_data_spec list
  | NCodata of nun_co_data_spec list
  | NVal of tm * ty
  | NPred of bool * nun_const_spec list
  | NCopred of nun_const_spec list
  | NRec of nun_const_spec list
  | NSpec of nun_consts_spec
  | NAxiom of tm
  | NGoal of tm
  | NEval of tm

  type nun_problem =
    {commandss: nun_command list list,
     sound: bool,
     complete: bool}

  type name_pool =
    {nice_of_ugly: string Symtab.table,
     ugly_of_nice: string Symtab.table}

  val nun_abstract: string
  val nun_and: string
  val nun_arrow: string
  val nun_asserting: string
  val nun_assign: string
  val nun_at: string
  val nun_axiom: string
  val nun_bar: string
  val nun_choice: string
  val nun_codata: string
  val nun_colon: string
  val nun_comma: string
  val nun_concrete: string
  val nun_conj: string
  val nun_copred: string
  val nun_copy: string
  val nun_data: string
  val nun_disj: string
  val nun_dollar: string
  val nun_dollar_anon_fun_prefix: string
  val nun_dot: string
  val nun_dummy: string
  val nun_else: string
  val nun_end: string
  val nun_equals: string
  val nun_eval: string
  val nun_exists: string
  val nun_false: string
  val nun_forall: string
  val nun_goal: string
  val nun_hash: string
  val nun_if: string
  val nun_implies: string
  val nun_irrelevant: string
  val nun_lambda: string
  val nun_lbrace: string
  val nun_lbracket: string
  val nun_lparen: string
  val nun_match: string
  val nun_mu: string
  val nun_not: string
  val nun_partial_quotient: string
  val nun_pred: string
  val nun_prop: string
  val nun_quotient: string
  val nun_rbrace: string
  val nun_rbracket: string
  val nun_rec: string
  val nun_rparen: string
  val nun_semicolon: string
  val nun_spec: string
  val nun_subset: string
  val nun_then: string
  val nun_true: string
  val nun_type: string
  val nun_unparsable: string
  val nun_unique: string
  val nun_unique_unsafe: string
  val nun_val: string
  val nun_wf: string
  val nun_with: string
  val nun__witness_of: string

  val ident_of_str: string -> ident
  val str_of_ident: ident -> string
  val encode_args: string list -> string
  val nun_const_of_str: string list -> string -> ident
  val nun_tconst_of_str: string list -> string -> ident
  val nun_free_of_str: string -> ident
  val nun_tfree_of_str: string -> ident
  val nun_var_of_str: string -> ident
  val str_of_nun_const: ident -> string list * string
  val str_of_nun_tconst: ident -> string list * string
  val str_of_nun_free: ident -> string
  val str_of_nun_tfree: ident -> string
  val str_of_nun_var: ident -> string

  val dummy_ty: ty
  val prop_ty: ty
  val mk_arrow_ty: ty * ty -> ty
  val mk_arrows_ty: ty list * ty -> ty
  val nabss: tm list * tm -> tm
  val napps: tm * tm list -> tm

  val ty_of: tm -> ty
  val safe_ty_of: tm -> ty

  val fold_map_ty_idents: (string -> 'a -> string * 'a) -> ty -> 'a -> ty * 'a
  val fold_map_tm_idents: (string -> 'a -> string * 'a) -> tm -> 'a -> tm * 'a
  val fold_map_nun_command_idents: (string -> 'a -> string * 'a) -> nun_command -> 'a ->
    nun_command * 'a
  val fold_map_nun_problem_idents: (string -> 'a -> string * 'a) -> nun_problem -> 'a ->
    nun_problem * 'a

  val allocate_nice: name_pool -> string * string -> string * name_pool

  val rcomb_tms: tm list -> tm -> tm
  val abs_tms: tm list -> tm -> tm
  val eta_expandN_tm: int -> tm -> tm
  val eta_expand_builtin_tm: tm -> tm

  val str_of_ty: ty -> string
  val str_of_tm: tm -> string
  val str_of_tmty: tm -> string

  val nice_nun_problem: nun_problem -> nun_problem * name_pool
  val str_of_nun_problem: nun_problem -> string
end;

structure Nunchaku_Problem : NUNCHAKU_PROBLEM =
struct

open Nunchaku_Util;

type ident = string;

datatype ty =
  NType of ident * ty list;

datatype tm =
  NAtom of int * ty
| NConst of ident * ty list * ty
| NAbs of tm * tm
| NMatch of tm * (ident * tm list * tm) list
| NApp of tm * tm;

type nun_copy_spec =
  {abs_ty: ty,
   rep_ty: ty,
   subset: tm option,
   quotient: tm option,
   abs: tm,
   rep: tm};

type nun_ctr_spec =
  {ctr: tm,
   arg_tys: ty list};

type nun_co_data_spec =
  {ty: ty,
   ctrs: nun_ctr_spec list};

type nun_const_spec =
  {const: tm,
   props: tm list};

type nun_consts_spec =
  {consts: tm list,
   props: tm list};

datatype nun_command =
  NTVal of ty * (int option * int option)
| NCopy of nun_copy_spec
| NData of nun_co_data_spec list
| NCodata of nun_co_data_spec list
| NVal of tm * ty
| NPred of bool * nun_const_spec list
| NCopred of nun_const_spec list
| NRec of nun_const_spec list
| NSpec of nun_consts_spec
| NAxiom of tm
| NGoal of tm
| NEval of tm;

type nun_problem =
  {commandss: nun_command list list,
   sound: bool,
   complete: bool};

type name_pool =
  {nice_of_ugly: string Symtab.table,
   ugly_of_nice: string Symtab.table};

val nun_abstract = "abstract";
val nun_and = "and";
val nun_arrow = "->";
val nun_asserting = "asserting";
val nun_assign = ":=";
val nun_at = "@";
val nun_axiom = "axiom";
val nun_bar = "|";
val nun_choice = "choice";
val nun_codata = "codata";
val nun_colon = ":";
val nun_comma = ",";
val nun_concrete = "concrete";
val nun_conj = "&&";
val nun_copred = "copred";
val nun_copy = "copy";
val nun_data = "data";
val nun_disj = "||";
val nun_dollar = "$";
val nun_dollar_anon_fun_prefix = "$anon_fun_";
val nun_dot = ".";
val nun_dummy = "_";
val nun_else = "else";
val nun_end = "end";
val nun_equals = "=";
val nun_eval = "eval";
val nun_exists = "exists";
val nun_false = "false";
val nun_forall = "forall";
val nun_goal = "goal";
val nun_hash = "#";
val nun_if = "if";
val nun_implies = "=>";
val nun_irrelevant = "?__";
val nun_lambda = "fun";
val nun_lbrace = "{";
val nun_lbracket = "[";
val nun_lparen = "(";
val nun_match = "match";
val nun_mu = "mu";
val nun_not = "~";
val nun_partial_quotient = "partial_quotient";
val nun_pred = "pred";
val nun_prop = "prop";
val nun_quotient = "quotient";
val nun_rbrace = "}";
val nun_rbracket = "]";
val nun_rec = "rec";
val nun_rparen = ")";
val nun_semicolon = ";";
val nun_spec = "spec";
val nun_subset = "subset";
val nun_then = "then";
val nun_true = "true";
val nun_type = "type";
val nun_unique = "unique";
val nun_unique_unsafe = "unique_unsafe";
val nun_unparsable = "?__unparsable";
val nun_val = "val";
val nun_wf = "wf";
val nun_with = "with";
val nun__witness_of = "_witness_of";

val nun_parens = enclose nun_lparen nun_rparen;

fun nun_parens_if_space s = s |> String.isSubstring " " s ? nun_parens;

fun str_of_nun_arg_list str_of_arg =
  map (prefix " " o nun_parens_if_space o str_of_arg) #> space_implode "";

fun str_of_nun_and_list str_of_elem =
  map str_of_elem #> space_implode ("\n" ^ nun_and ^ " ");

val is_nun_const_quantifier = member (op =) [nun_forall, nun_exists];
val is_nun_const_connective = member (op =) [nun_conj, nun_disj, nun_implies];

val nun_builtin_arity =
  [(nun_asserting, 2),
   (nun_conj, 2),
   (nun_disj, 2),
   (nun_equals, 2),
   (nun_exists, 1),
   (nun_false, 0),
   (nun_forall, 1),
   (nun_if, 3),
   (nun_implies, 2),
   (nun_not, 1),
   (nun_true, 0)];

val arity_of_nun_builtin = AList.lookup (op =) nun_builtin_arity #> the_default 0;

val nun_const_prefix = "c.";
val nun_free_prefix = "f.";
val nun_var_prefix = "v.";
val nun_tconst_prefix = "C.";
val nun_tfree_prefix = "F.";
val nun_custom_id_suffix = "_";

val ident_of_str = I : string -> ident;
val str_of_ident = I : ident -> string;

val encode_args = enclose "(" ")" o commas;

fun decode_args s =
  let
    fun delta #"(" = 1
      | delta #")" = ~1
      | delta _ = 0;

    fun dec 0 (#"(" :: #")" :: cs) _ = ([], String.implode cs)
      | dec 0 (#"(" :: cs) [] = dec 1 cs [[]]
      | dec 0 cs _ = ([], String.implode cs)
      | dec _ [] _ = raise Fail ("ill-formed arguments in " ^ quote s)
      | dec 1 (#")" :: cs) args = (rev (map (String.implode o rev) args), String.implode cs)
      | dec 1 (#"," :: cs) args = dec 1 cs ([] :: args)
      | dec n (c :: cs) (arg :: args) = dec (n + delta c) cs ((c :: arg) :: args);
  in
    dec 0 (String.explode s) []
  end;

fun nun_const_of_str args =
  suffix nun_custom_id_suffix #> prefix nun_const_prefix #> prefix (encode_args args);
fun nun_tconst_of_str args =
  suffix nun_custom_id_suffix #> prefix nun_tconst_prefix #> prefix (encode_args args);

val nun_free_of_str = suffix nun_custom_id_suffix #> prefix nun_free_prefix;
val nun_tfree_of_str = suffix nun_custom_id_suffix #> prefix nun_tfree_prefix;
val nun_var_of_str = suffix nun_custom_id_suffix #> prefix nun_var_prefix;
val str_of_nun_const = decode_args ##> unprefix nun_const_prefix ##> unsuffix nun_custom_id_suffix;
val str_of_nun_tconst = decode_args ##> unprefix nun_tconst_prefix ##> unsuffix nun_custom_id_suffix;
val str_of_nun_free = unprefix nun_free_prefix #> unsuffix nun_custom_id_suffix;
val str_of_nun_tfree = unprefix nun_tfree_prefix #> unsuffix nun_custom_id_suffix;
val str_of_nun_var = unprefix nun_var_prefix #> unsuffix nun_custom_id_suffix;

fun index_name s 0 = s
  | index_name s j =
    let
      val n = size s;
      val m = n - 1;
    in
      String.substring (s, 0, m) ^ string_of_int j ^ String.substring (s, m, n - m)
    end;

val dummy_ty = NType (nun_dummy, []);
val prop_ty = NType (nun_prop, []);

fun mk_arrow_ty (dom, ran) = NType (nun_arrow, [dom, ran]);
val mk_arrows_ty = Library.foldr mk_arrow_ty;

val nabss = Library.foldr NAbs;
val napps = Library.foldl NApp;

fun domain_ty (NType (_, [ty, _])) = ty
  | domain_ty ty = ty;

fun range_ty (NType (_, [_, ty])) = ty
  | range_ty ty = ty;

fun domain_tys 0 _ = []
  | domain_tys n ty = domain_ty ty :: domain_tys (n - 1) (range_ty ty);

fun ty_of (NAtom (_, ty)) = ty
  | ty_of (NConst (_, _, ty)) = ty
  | ty_of (NAbs (var, body)) = mk_arrow_ty (ty_of var, ty_of body)
  | ty_of (NMatch (_, (_, _, body1) :: _)) = ty_of body1
  | ty_of (NApp (const, _)) = range_ty (ty_of const);

val safe_ty_of = try ty_of #> the_default dummy_ty;

fun strip_nun_binders binder (app as NApp (NConst (id, _, _), NAbs (var, body))) =
    if id = binder then
      strip_nun_binders binder body
      |>> cons var
    else
      ([], app)
  | strip_nun_binders _ tm = ([], tm);

fun fold_map_option _ NONE = pair NONE
  | fold_map_option f (SOME x) = f x #>> SOME;

fun fold_map_ty_idents f (NType (id, tys)) =
    f id
    ##>> fold_map (fold_map_ty_idents f) tys
    #>> NType;

fun fold_map_match_branch_idents f (id, vars, body) =
    f id
    ##>> fold_map (fold_map_tm_idents f) vars
    ##>> fold_map_tm_idents f body
    #>> Scan.triple1
and fold_map_tm_idents f (NAtom (j, ty)) =
    fold_map_ty_idents f ty
    #>> curry NAtom j
  | fold_map_tm_idents f (NConst (id, tys, ty)) =
    f id
    ##>> fold_map (fold_map_ty_idents f) tys
    ##>> fold_map_ty_idents f ty
    #>> (Scan.triple1 #> NConst)
  | fold_map_tm_idents f (NAbs (var, body)) =
    fold_map_tm_idents f var
    ##>> fold_map_tm_idents f body
    #>> NAbs
  | fold_map_tm_idents f (NMatch (obj, branches)) =
    fold_map_tm_idents f obj
    ##>> fold_map (fold_map_match_branch_idents f) branches
    #>> NMatch
  | fold_map_tm_idents f (NApp (const, arg)) =
    fold_map_tm_idents f const
    ##>> fold_map_tm_idents f arg
    #>> NApp;

fun fold_map_nun_copy_spec_idents f {abs_ty, rep_ty, subset, quotient, abs, rep} =
  fold_map_ty_idents f abs_ty
  ##>> fold_map_ty_idents f rep_ty
  ##>> fold_map_option (fold_map_tm_idents f) subset
  ##>> fold_map_option (fold_map_tm_idents f) quotient
  ##>> fold_map_tm_idents f abs
  ##>> fold_map_tm_idents f rep
  #>> (fn (((((abs_ty, rep_ty), subset), quotient), abs), rep) =>
    {abs_ty = abs_ty, rep_ty = rep_ty, subset = subset, quotient = quotient, abs = abs, rep = rep});

fun fold_map_nun_ctr_spec_idents f {ctr, arg_tys} =
  fold_map_tm_idents f ctr
  ##>> fold_map (fold_map_ty_idents f) arg_tys
  #>> (fn (ctr, arg_tys) => {ctr = ctr, arg_tys = arg_tys});

fun fold_map_nun_co_data_spec_idents f {ty, ctrs} =
  fold_map_ty_idents f ty
  ##>> fold_map (fold_map_nun_ctr_spec_idents f) ctrs
  #>> (fn (ty, ctrs) => {ty = ty, ctrs = ctrs});

fun fold_map_nun_const_spec_idents f {const, props} =
  fold_map_tm_idents f const
  ##>> fold_map (fold_map_tm_idents f) props
  #>> (fn (const, props) => {const = const, props = props});

fun fold_map_nun_consts_spec_idents f {consts, props} =
  fold_map (fold_map_tm_idents f) consts
  ##>> fold_map (fold_map_tm_idents f) props
  #>> (fn (consts, props) => {consts = consts, props = props});

fun fold_map_nun_command_idents f (NTVal (ty, cards)) =
    fold_map_ty_idents f ty
    #>> (rpair cards #> NTVal)
  | fold_map_nun_command_idents f (NCopy spec) =
    fold_map_nun_copy_spec_idents f spec
    #>> NCopy
  | fold_map_nun_command_idents f (NData specs) =
    fold_map (fold_map_nun_co_data_spec_idents f) specs
    #>> NData
  | fold_map_nun_command_idents f (NCodata specs) =
    fold_map (fold_map_nun_co_data_spec_idents f) specs
    #>> NCodata
  | fold_map_nun_command_idents f (NVal (tm, ty)) =
    fold_map_tm_idents f tm
    ##>> fold_map_ty_idents f ty
    #>> NVal
  | fold_map_nun_command_idents f (NPred (wf, specs)) =
    fold_map (fold_map_nun_const_spec_idents f) specs
    #>> curry NPred wf
  | fold_map_nun_command_idents f (NCopred specs) =
    fold_map (fold_map_nun_const_spec_idents f) specs
    #>> NCopred
  | fold_map_nun_command_idents f (NRec specs) =
    fold_map (fold_map_nun_const_spec_idents f) specs
    #>> NRec
  | fold_map_nun_command_idents f (NSpec spec) =
    fold_map_nun_consts_spec_idents f spec
    #>> NSpec
  | fold_map_nun_command_idents f (NAxiom tm) =
    fold_map_tm_idents f tm
    #>> NAxiom
  | fold_map_nun_command_idents f (NGoal tm) =
    fold_map_tm_idents f tm
    #>> NGoal
  | fold_map_nun_command_idents f (NEval tm) =
    fold_map_tm_idents f tm
    #>> NEval;

fun fold_map_nun_problem_idents f ({commandss, sound, complete} : nun_problem) =
  fold_map (fold_map (fold_map_nun_command_idents f)) commandss
  #>> (fn commandss' => {commandss = commandss', sound = sound, complete = complete});

fun dest_rassoc_args oper arg0 rest =
  (case rest of
    NApp (NApp (oper', arg1), rest') =>
    if oper' = oper then arg0 :: dest_rassoc_args oper arg1 rest' else [arg0, rest]
  | _ => [arg0, rest]);

val rcomb_tms = fold (fn arg => fn func => NApp (func, arg));
val abs_tms = fold_rev (curry NAbs);

fun fresh_var_names_wrt_tm n tm =
  let
    fun max_var_br (_, vars, body) = fold max_var (body :: vars)
    and max_var (NAtom _) = I
      | max_var (NConst (id, _, _)) =
        (fn max => if String.isPrefix nun_var_prefix id andalso size id > size max then id else max)
      | max_var (NApp (func, arg)) = fold max_var [func, arg]
      | max_var (NAbs (var, body)) = fold max_var [var, body]
      | max_var (NMatch (obj, branches)) = max_var obj #> fold max_var_br branches;

    val dummy_name = nun_var_of_str Name.uu;
    val max_name = max_var tm dummy_name;
  in
    map (index_name max_name) (1 upto n)
  end;

fun eta_expandN_tm 0 tm = tm
  | eta_expandN_tm n tm =
    let
      val var_names = fresh_var_names_wrt_tm n tm;
      val arg_tys = domain_tys n (ty_of tm);
      val vars = map2 (fn id => fn ty => NConst (id, [], ty)) var_names arg_tys;
    in
      abs_tms vars (rcomb_tms vars tm)
    end;

val eta_expand_builtin_tm =
  let
    fun expand_quant_arg (NAbs (var, body)) = NAbs (var, expand_quant_arg body)
      | expand_quant_arg (NMatch (obj, branches)) =
        NMatch (obj, map (@{apply 3(3)} expand_quant_arg) branches)
      | expand_quant_arg (tm as NApp (_, NAbs _)) = tm
      | expand_quant_arg (NApp (quant, arg)) = NApp (quant, eta_expandN_tm 1 arg)
      | expand_quant_arg tm = tm;

    fun expand args (NApp (func, arg)) = expand (expand [] arg :: args) func
      | expand args (func as NConst (id, _, _)) =
        let val missing = Int.max (0, arity_of_nun_builtin id - length args) in
          rcomb_tms args func
          |> eta_expandN_tm missing
          |> is_nun_const_quantifier id ? expand_quant_arg
        end
      | expand args (func as NAtom _) = rcomb_tms args func
      | expand args (NAbs (var, body)) = rcomb_tms args (NAbs (var, expand [] body))
      | expand args (NMatch (obj, branches)) =
        rcomb_tms args (NMatch (obj, map (@{apply 3(3)} (expand [])) branches));
  in
    expand []
  end;

val str_of_ty =
  let
    fun str_of maybe_parens (NType (id, tys)) =
      if id = nun_arrow then
        (case tys of
          [ty, ty'] => maybe_parens (str_of nun_parens ty ^ " " ^ nun_arrow ^ " " ^ str_of I ty'))
      else
        id ^ str_of_nun_arg_list (str_of I) tys
  in
    str_of I
  end;

val (str_of_tmty, str_of_tm) =
  let
    fun is_triv_head (NConst (id, _, _)) = (arity_of_nun_builtin id = 0)
      | is_triv_head (NAtom _) = true
      | is_triv_head (NApp (const, _)) = is_triv_head const
      | is_triv_head (NAbs _) = false
      | is_triv_head (NMatch _) = false;

    fun str_of_at_const id tys =
      nun_at ^ str_of_ident id ^ str_of_nun_arg_list str_of_ty tys;

    fun str_of_app ty_opt const arg =
      let
        val ty_opt' =
          try (Option.map (fn ty => mk_arrow_ty (ty_of arg, ty))) ty_opt
          |> the_default NONE;
      in
        (str_of ty_opt' const |> (case const of NAbs _ => nun_parens | _ => I)) ^
        str_of_nun_arg_list (str_of NONE) [arg]
      end
    and str_of_br ty_opt (id, vars, body) =
      " " ^ nun_bar ^ " " ^ id ^ space_implode "" (map (prefix " " o str_of NONE) vars) ^ " " ^
      nun_arrow ^ " " ^ str_of ty_opt body
    and str_of_tmty tm =
      let val ty = ty_of tm in
        str_of (SOME ty) tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty
      end
    and str_of _ (NAtom (j, _)) = nun_dollar ^ string_of_int j
      | str_of _ (NConst (id, [], _)) = str_of_ident id
      | str_of (SOME ty0) (NConst (id, tys, ty)) =
        if ty = ty0 then str_of_ident id else str_of_at_const id tys
      | str_of _ (NConst (id, tys, _)) = str_of_at_const id tys
      | str_of ty_opt (NAbs (var, body)) =
        nun_lambda ^ " " ^
        (case ty_opt of
          SOME ty => str_of (SOME (domain_ty ty))
        | NONE => nun_parens o str_of_tmty) var ^
        nun_dot ^ " " ^ str_of (Option.map range_ty ty_opt) body
      | str_of ty_opt (NMatch (obj, branches)) =
        nun_match ^ " " ^ str_of NONE obj ^ " " ^ nun_with ^
        space_implode "" (map (str_of_br ty_opt) branches) ^ " " ^ nun_end
      | str_of ty_opt (app as NApp (func, argN)) =
        (case (func, argN) of
          (NApp (oper as NConst (id, _, _), arg1), arg2) =>
          if id = nun_asserting then
            str_of ty_opt arg1 ^ " " ^ nun_asserting ^ " " ^ str_of (SOME prop_ty) arg2
            |> nun_parens
          else if id = nun_equals then
            (str_of NONE arg1 |> not (is_triv_head arg1) ? nun_parens) ^ " " ^ id ^ " " ^
            (str_of (try ty_of arg2) arg2 |> not (is_triv_head arg2) ? nun_parens)
          else if is_nun_const_connective id then
            let val args = dest_rassoc_args oper arg1 arg2 in
              space_implode (" " ^ id ^ " ")
                (map (fn arg => str_of NONE arg |> not (is_triv_head arg) ? nun_parens) args)
            end
          else
            str_of_app ty_opt func argN
        | (NApp (NApp (NConst (id, _, _), arg1), arg2), arg3) =>
          if id = nun_if then
            nun_if ^ " " ^ str_of NONE arg1 ^ " " ^ nun_then ^ " " ^ str_of NONE arg2 ^ " " ^
            nun_else ^ " " ^ str_of NONE arg3
            |> nun_parens
          else
            str_of_app ty_opt func argN
        | (NConst (id, _, _), NAbs _) =>
          if is_nun_const_quantifier id then
            let val (vars, body) = strip_nun_binders id app in
              id ^ " " ^ space_implode " " (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^
              str_of NONE body
            end
          else
            str_of_app ty_opt func argN
        | _ => str_of_app ty_opt func argN);
  in
    (str_of_tmty, str_of NONE)
  end;

val empty_name_pool = {nice_of_ugly = Symtab.empty, ugly_of_nice = Symtab.empty};

val nice_of_ugly_suggestion =
  unascii_of #> Long_Name.base_name #> ascii_of #> unsuffix nun_custom_id_suffix
  #> (fn s => if s = "" orelse not (Char.isAlpha (String.sub (s, 0))) then "x" ^ s else s);

fun allocate_nice ({nice_of_ugly, ugly_of_nice} : name_pool) (ugly, nice_sugg0) =
  let
    fun alloc j =
      let val nice_sugg = index_name nice_sugg0 j in
        (case Symtab.lookup ugly_of_nice nice_sugg of
          NONE =>
          (nice_sugg,
           {nice_of_ugly = Symtab.update_new (ugly, nice_sugg) nice_of_ugly,
            ugly_of_nice = Symtab.update_new (nice_sugg, ugly) ugly_of_nice})
        | SOME _ => alloc (j + 1))
      end;
  in
    alloc 0
  end;

fun nice_ident ugly (pool as {nice_of_ugly, ...}) =
  if String.isSuffix nun_custom_id_suffix ugly then
    (case Symtab.lookup nice_of_ugly ugly of
      NONE => allocate_nice pool (ugly, nice_of_ugly_suggestion ugly)
    | SOME nice => (nice, pool))
  else
    (ugly, pool);

fun nice_nun_problem problem =
  fold_map_nun_problem_idents nice_ident problem empty_name_pool;

fun str_of_tval (NType (id, tys)) =
  str_of_ident id ^ " " ^ nun_colon ^ " " ^
  fold (K (prefix (nun_type ^ " " ^ nun_arrow ^ " "))) tys nun_type;

fun is_triv_subset (NAbs (_, body)) = is_triv_subset body
  | is_triv_subset (NConst (id, _, _)) = (id = nun_true)
  | is_triv_subset _ = false;

fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =
  str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
  (case subset of
    NONE => ""
  | SOME s =>
    if is_triv_subset s then ""
    else "\n " ^ nun_subset ^ " " ^ nun_parens_if_space (str_of_tm s)) ^
  (* TODO: use nun_quotient when possible *)
  (case quotient of
    NONE => ""
  | SOME q => "\n " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^
  "\n " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n " ^ nun_concrete ^ " " ^ str_of_tm rep;

fun str_of_nun_ctr_spec {ctr, arg_tys} =
  str_of_tm ctr ^ str_of_nun_arg_list str_of_ty arg_tys;

fun str_of_nun_co_data_spec {ty, ctrs} =
  str_of_ty ty ^ " " ^ nun_assign ^ "\n " ^
  space_implode ("\n" ^ nun_bar ^ " ") (map str_of_nun_ctr_spec ctrs);

fun str_of_nun_const_spec {const, props} =
  str_of_tmty const ^ " " ^ nun_assign ^ "\n " ^
  space_implode (nun_semicolon ^ "\n ") (map str_of_tm props);

fun str_of_nun_consts_spec {consts, props} =
  space_implode (" " ^ nun_and ^ "\n ") (map str_of_tmty consts) ^ " " ^ nun_assign ^ "\n " ^
  space_implode (nun_semicolon ^ "\n ") (map str_of_tm props);

fun str_of_nun_cards_suffix (NONE, NONE) = ""
  | str_of_nun_cards_suffix (c1, c2) =
    let
      val s1 = Option.map (prefix "min_card " o signed_string_of_int) c1;
      val s2 = Option.map (prefix "max_card " o signed_string_of_int) c2;
    in
      enclose " [" "]" (space_implode "; " (map_filter I [s1, s2]))
    end;

fun str_of_nun_command (NTVal (ty, cards)) =
    nun_val ^ " " ^ str_of_tval ty ^ str_of_nun_cards_suffix cards
  | str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_copy_spec spec
  | str_of_nun_command (NData specs) =
    nun_data ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
  | str_of_nun_command (NCodata specs) =
    nun_codata ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
  | str_of_nun_command (NVal (tm, ty)) =
    nun_val ^ " " ^ str_of_tm tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty
  | str_of_nun_command (NPred (wf, specs)) =
    nun_pred ^ " " ^ (if wf then nun_lbracket ^ nun_wf ^ nun_rbracket ^ " " else "") ^
    str_of_nun_and_list str_of_nun_const_spec specs
  | str_of_nun_command (NCopred specs) =
    nun_copred ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs
  | str_of_nun_command (NRec specs) =
    nun_rec ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs
  | str_of_nun_command (NSpec spec) = nun_spec ^ " " ^ str_of_nun_consts_spec spec
  | str_of_nun_command (NAxiom tm) = nun_axiom ^ " " ^ str_of_tm tm
  | str_of_nun_command (NGoal tm) = nun_goal ^ " " ^ str_of_tm tm
  | str_of_nun_command (NEval tm) = nun_hash ^ " " ^ nun_eval ^ " " ^ str_of_tm tm;

fun str_of_nun_problem {commandss, sound, complete} =
  map (cat_lines o map (suffix nun_dot o str_of_nun_command)) commandss
  |> space_implode "\n\n" |> suffix "\n"
  |> prefix (nun_hash ^ " " ^ (if sound then "sound" else "unsound") ^ "\n")
  |> prefix (nun_hash ^ " " ^ (if complete then "complete" else "incomplete") ^ "\n");

end;

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.