src/HOL/Tools/Nunchaku/nunchaku_problem.ML
author blanchet
Fri, 08 Sep 2017 00:02:21 +0200
changeset 66622 0916eb2dbaca
parent 66618 048524a4f537
child 66623 8fc868e9e1bf
permissions -rw-r--r--
properly parenthesize copy types in Nunchaku
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Nunchaku/Tools/nunchaku_problem.ML
66614
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 64429
diff changeset
     2
    Author:     Jasmin Blanchette, VU Amsterdam
1f1c5d85d232 moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents: 64429
diff changeset
     3
    Copyright   2015, 2016, 2017
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     4
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     5
Abstract syntax tree for Nunchaku problems.
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     6
*)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     7
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     8
signature NUNCHAKU_PROBLEM =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     9
sig
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    10
  eqtype ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    11
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    12
  datatype ty =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    13
    NType of ident * ty list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    14
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    15
  datatype tm =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    16
    NAtom of int * ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    17
  | NConst of ident * ty list * ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    18
  | NAbs of tm * tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    19
  | NMatch of tm * (ident * tm list * tm) list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    20
  | NApp of tm * tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    21
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
    22
  type nun_copy_spec =
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    23
    {abs_ty: ty,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    24
     rep_ty: ty,
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
    25
     subset: tm option,
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
    26
     quotient: tm option,
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    27
     abs: tm,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    28
     rep: tm}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    29
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    30
  type nun_ctr_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    31
    {ctr: tm,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    32
     arg_tys: ty list}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    33
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    34
  type nun_co_data_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    35
    {ty: ty,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    36
     ctrs: nun_ctr_spec list}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    37
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    38
  type nun_const_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    39
    {const: tm,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    40
     props: tm list}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    41
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    42
  type nun_consts_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    43
    {consts: tm list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    44
     props: tm list}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    45
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    46
  datatype nun_command =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    47
    NTVal of ty * (int option * int option)
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
    48
  | NCopy of nun_copy_spec
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    49
  | NData of nun_co_data_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    50
  | NCodata of nun_co_data_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    51
  | NVal of tm * ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    52
  | NPred of bool * nun_const_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    53
  | NCopred of nun_const_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    54
  | NRec of nun_const_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    55
  | NSpec of nun_consts_spec
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    56
  | NAxiom of tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    57
  | NGoal of tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    58
  | NEval of tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    59
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    60
  type nun_problem =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    61
    {commandss: nun_command list list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    62
     sound: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    63
     complete: bool}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    64
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    65
  type name_pool =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    66
    {nice_of_ugly: string Symtab.table,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    67
     ugly_of_nice: string Symtab.table}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    68
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    69
  val nun_abstract: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    70
  val nun_and: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    71
  val nun_anon_fun_prefix: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    72
  val nun_arrow: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    73
  val nun_asserting: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    74
  val nun_assign: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    75
  val nun_at: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    76
  val nun_axiom: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    77
  val nun_bar: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    78
  val nun_choice: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    79
  val nun_codata: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    80
  val nun_colon: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    81
  val nun_comma: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    82
  val nun_concrete: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    83
  val nun_conj: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    84
  val nun_copred: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    85
  val nun_copy: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    86
  val nun_data: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    87
  val nun_disj: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    88
  val nun_dollar: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    89
  val nun_dot: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    90
  val nun_dummy: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    91
  val nun_else: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    92
  val nun_end: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    93
  val nun_equals: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    94
  val nun_eval: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    95
  val nun_exists: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    96
  val nun_false: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    97
  val nun_forall: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    98
  val nun_goal: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    99
  val nun_hash: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   100
  val nun_if: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   101
  val nun_implies: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   102
  val nun_irrelevant: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   103
  val nun_lambda: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   104
  val nun_lbrace: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   105
  val nun_lbracket: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   106
  val nun_lparen: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   107
  val nun_match: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   108
  val nun_mu: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   109
  val nun_not: string
64429
582f54f6b29b adapted Nunchaku integration to keyword renaming
blanchet
parents: 64411
diff changeset
   110
  val nun_partial_quotient: string
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   111
  val nun_pred: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   112
  val nun_prop: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   113
  val nun_quotient: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   114
  val nun_rbrace: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   115
  val nun_rbracket: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   116
  val nun_rec: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   117
  val nun_rparen: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   118
  val nun_semicolon: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   119
  val nun_spec: string
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   120
  val nun_subset: string
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   121
  val nun_then: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   122
  val nun_true: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   123
  val nun_type: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   124
  val nun_unparsable: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   125
  val nun_unique: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   126
  val nun_unique_unsafe: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   127
  val nun_val: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   128
  val nun_wf: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   129
  val nun_with: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   130
  val nun__witness_of: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   131
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   132
  val ident_of_str: string -> ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   133
  val str_of_ident: ident -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   134
  val encode_args: string list -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   135
  val nun_const_of_str: string list -> string -> ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   136
  val nun_tconst_of_str: string list -> string -> ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   137
  val nun_free_of_str: string -> ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   138
  val nun_tfree_of_str: string -> ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   139
  val nun_var_of_str: string -> ident
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   140
  val str_of_nun_const: ident -> string list * string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   141
  val str_of_nun_tconst: ident -> string list * string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   142
  val str_of_nun_free: ident -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   143
  val str_of_nun_tfree: ident -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   144
  val str_of_nun_var: ident -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   145
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   146
  val dummy_ty: ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   147
  val prop_ty: ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   148
  val mk_arrow_ty: ty * ty -> ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   149
  val mk_arrows_ty: ty list * ty -> ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   150
  val nabss: tm list * tm -> tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   151
  val napps: tm * tm list -> tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   152
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   153
  val ty_of: tm -> ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   154
  val safe_ty_of: tm -> ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   155
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   156
  val fold_map_ty_idents: (string -> 'a -> string * 'a) -> ty -> 'a -> ty * 'a
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   157
  val fold_map_tm_idents: (string -> 'a -> string * 'a) -> tm -> 'a -> tm * 'a
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   158
  val fold_map_nun_command_idents: (string -> 'a -> string * 'a) -> nun_command -> 'a ->
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   159
    nun_command * 'a
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   160
  val fold_map_nun_problem_idents: (string -> 'a -> string * 'a) -> nun_problem -> 'a ->
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   161
    nun_problem * 'a
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   162
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   163
  val allocate_nice: name_pool -> string * string -> string * name_pool
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   164
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   165
  val rcomb_tms: tm list -> tm -> tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   166
  val abs_tms: tm list -> tm -> tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   167
  val eta_expandN_tm: int -> tm -> tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   168
  val eta_expand_builtin_tm: tm -> tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   169
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   170
  val str_of_ty: ty -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   171
  val str_of_tm: tm -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   172
  val str_of_tmty: tm -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   173
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   174
  val nice_nun_problem: nun_problem -> nun_problem * name_pool
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   175
  val str_of_nun_problem: nun_problem -> string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   176
end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   177
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   178
structure Nunchaku_Problem : NUNCHAKU_PROBLEM =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   179
struct
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   180
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   181
open Nunchaku_Util;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   182
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   183
type ident = string;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   184
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   185
datatype ty =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   186
  NType of ident * ty list;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   187
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   188
datatype tm =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   189
  NAtom of int * ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   190
| NConst of ident * ty list * ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   191
| NAbs of tm * tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   192
| NMatch of tm * (ident * tm list * tm) list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   193
| NApp of tm * tm;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   194
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   195
type nun_copy_spec =
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   196
  {abs_ty: ty,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   197
   rep_ty: ty,
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   198
   subset: tm option,
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   199
   quotient: tm option,
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   200
   abs: tm,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   201
   rep: tm};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   202
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   203
type nun_ctr_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   204
  {ctr: tm,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   205
   arg_tys: ty list};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   206
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   207
type nun_co_data_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   208
  {ty: ty,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   209
   ctrs: nun_ctr_spec list};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   210
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   211
type nun_const_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   212
  {const: tm,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   213
   props: tm list};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   214
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   215
type nun_consts_spec =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   216
  {consts: tm list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   217
   props: tm list};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   218
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   219
datatype nun_command =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   220
  NTVal of ty * (int option * int option)
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   221
| NCopy of nun_copy_spec
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   222
| NData of nun_co_data_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   223
| NCodata of nun_co_data_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   224
| NVal of tm * ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   225
| NPred of bool * nun_const_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   226
| NCopred of nun_const_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   227
| NRec of nun_const_spec list
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   228
| NSpec of nun_consts_spec
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   229
| NAxiom of tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   230
| NGoal of tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   231
| NEval of tm;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   232
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   233
type nun_problem =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   234
  {commandss: nun_command list list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   235
   sound: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   236
   complete: bool};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   237
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   238
type name_pool =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   239
  {nice_of_ugly: string Symtab.table,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   240
   ugly_of_nice: string Symtab.table};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   241
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   242
val nun_abstract = "abstract";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   243
val nun_and = "and";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   244
val nun_anon_fun_prefix = "anon_fun_";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   245
val nun_arrow = "->";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   246
val nun_asserting = "asserting";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   247
val nun_assign = ":=";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   248
val nun_at = "@";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   249
val nun_axiom = "axiom";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   250
val nun_bar = "|";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   251
val nun_choice = "choice";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   252
val nun_codata = "codata";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   253
val nun_colon = ":";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   254
val nun_comma = ",";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   255
val nun_concrete = "concrete";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   256
val nun_conj = "&&";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   257
val nun_copred = "copred";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   258
val nun_copy = "copy";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   259
val nun_data = "data";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   260
val nun_disj = "||";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   261
val nun_dollar = "$";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   262
val nun_dot = ".";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   263
val nun_dummy = "_";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   264
val nun_else = "else";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   265
val nun_end = "end";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   266
val nun_equals = "=";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   267
val nun_eval = "eval";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   268
val nun_exists = "exists";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   269
val nun_false = "false";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   270
val nun_forall = "forall";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   271
val nun_goal = "goal";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   272
val nun_hash = "#";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   273
val nun_if = "if";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   274
val nun_implies = "=>";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   275
val nun_irrelevant = "?__";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   276
val nun_lambda = "fun";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   277
val nun_lbrace = "{";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   278
val nun_lbracket = "[";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   279
val nun_lparen = "(";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   280
val nun_match = "match";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   281
val nun_mu = "mu";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   282
val nun_not = "~";
64429
582f54f6b29b adapted Nunchaku integration to keyword renaming
blanchet
parents: 64411
diff changeset
   283
val nun_partial_quotient = "partial_quotient";
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   284
val nun_pred = "pred";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   285
val nun_prop = "prop";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   286
val nun_quotient = "quotient";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   287
val nun_rbrace = "}";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   288
val nun_rbracket = "]";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   289
val nun_rec = "rec";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   290
val nun_rparen = ")";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   291
val nun_semicolon = ";";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   292
val nun_spec = "spec";
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   293
val nun_subset = "subset";
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   294
val nun_then = "then";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   295
val nun_true = "true";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   296
val nun_type = "type";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   297
val nun_unique = "unique";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   298
val nun_unique_unsafe = "unique_unsafe";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   299
val nun_unparsable = "?__unparsable";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   300
val nun_val = "val";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   301
val nun_wf = "wf";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   302
val nun_with = "with";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   303
val nun__witness_of = "_witness_of";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   304
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   305
val nun_parens = enclose nun_lparen nun_rparen;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   306
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   307
fun nun_parens_if_space s = s |> String.isSubstring " " s ? nun_parens;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   308
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   309
fun str_of_nun_arg_list str_of_arg =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   310
  map (prefix " " o nun_parens_if_space o str_of_arg) #> space_implode "";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   311
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   312
fun str_of_nun_and_list str_of_elem =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   313
  map str_of_elem #> space_implode ("\n" ^ nun_and ^ " ");
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   314
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   315
val is_nun_const_quantifier = member (op =) [nun_forall, nun_exists];
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   316
val is_nun_const_connective = member (op =) [nun_conj, nun_disj, nun_implies];
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   317
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   318
val nun_builtin_arity =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   319
  [(nun_asserting, 2),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   320
   (nun_conj, 2),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   321
   (nun_disj, 2),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   322
   (nun_equals, 2),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   323
   (nun_exists, 1),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   324
   (nun_false, 0),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   325
   (nun_forall, 1),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   326
   (nun_if, 3),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   327
   (nun_implies, 2),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   328
   (nun_not, 1),
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   329
   (nun_true, 0)];
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   330
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   331
val arity_of_nun_builtin = AList.lookup (op =) nun_builtin_arity #> the_default 0;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   332
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   333
val nun_const_prefix = "c.";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   334
val nun_free_prefix = "f.";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   335
val nun_var_prefix = "v.";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   336
val nun_tconst_prefix = "C.";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   337
val nun_tfree_prefix = "F.";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   338
val nun_custom_id_suffix = "_";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   339
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   340
val ident_of_str = I : string -> ident;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   341
val str_of_ident = I : ident -> string;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   342
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   343
val encode_args = enclose "(" ")" o commas;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   344
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   345
fun decode_args s =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   346
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   347
    fun delta #"(" = 1
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   348
      | delta #")" = ~1
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   349
      | delta _ = 0;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   350
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   351
    fun dec 0 (#"(" :: #")" :: cs) _ = ([], String.implode cs)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   352
      | dec 0 (#"(" :: cs) [] = dec 1 cs [[]]
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   353
      | dec 0 cs _ = ([], String.implode cs)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   354
      | dec _ [] _ = raise Fail ("ill-formed arguments in " ^ quote s)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   355
      | dec 1 (#")" :: cs) args = (rev (map (String.implode o rev) args), String.implode cs)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   356
      | dec 1 (#"," :: cs) args = dec 1 cs ([] :: args)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   357
      | dec n (c :: cs) (arg :: args) = dec (n + delta c) cs ((c :: arg) :: args);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   358
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   359
    dec 0 (String.explode s) []
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   360
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   361
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   362
fun nun_const_of_str args =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   363
  suffix nun_custom_id_suffix #> prefix nun_const_prefix #> prefix (encode_args args);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   364
fun nun_tconst_of_str args =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   365
  suffix nun_custom_id_suffix #> prefix nun_tconst_prefix #> prefix (encode_args args);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   366
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   367
val nun_free_of_str = suffix nun_custom_id_suffix #> prefix nun_free_prefix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   368
val nun_tfree_of_str = suffix nun_custom_id_suffix #> prefix nun_tfree_prefix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   369
val nun_var_of_str = suffix nun_custom_id_suffix #> prefix nun_var_prefix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   370
val str_of_nun_const = decode_args ##> unprefix nun_const_prefix ##> unsuffix nun_custom_id_suffix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   371
val str_of_nun_tconst = decode_args ##> unprefix nun_tconst_prefix ##> unsuffix nun_custom_id_suffix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   372
val str_of_nun_free = unprefix nun_free_prefix #> unsuffix nun_custom_id_suffix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   373
val str_of_nun_tfree = unprefix nun_tfree_prefix #> unsuffix nun_custom_id_suffix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   374
val str_of_nun_var = unprefix nun_var_prefix #> unsuffix nun_custom_id_suffix;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   375
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   376
fun index_name s 0 = s
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   377
  | index_name s j =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   378
    let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   379
      val n = size s;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   380
      val m = n - 1;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   381
    in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   382
      String.substring (s, 0, m) ^ string_of_int j ^ String.substring (s, m, n - m)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   383
    end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   384
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   385
val dummy_ty = NType (nun_dummy, []);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   386
val prop_ty = NType (nun_prop, []);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   387
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   388
fun mk_arrow_ty (dom, ran) = NType (nun_arrow, [dom, ran]);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   389
val mk_arrows_ty = Library.foldr mk_arrow_ty;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   390
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   391
val nabss = Library.foldr NAbs;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   392
val napps = Library.foldl NApp;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   393
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   394
fun domain_ty (NType (_, [ty, _])) = ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   395
  | domain_ty ty = ty;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   396
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   397
fun range_ty (NType (_, [_, ty])) = ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   398
  | range_ty ty = ty;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   399
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   400
fun domain_tys 0 _ = []
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   401
  | domain_tys n ty = domain_ty ty :: domain_tys (n - 1) (range_ty ty);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   402
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   403
fun ty_of (NAtom (_, ty)) = ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   404
  | ty_of (NConst (_, _, ty)) = ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   405
  | ty_of (NAbs (var, body)) = mk_arrow_ty (ty_of var, ty_of body)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   406
  | ty_of (NMatch (_, (_, _, body1) :: _)) = ty_of body1
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   407
  | ty_of (NApp (const, _)) = range_ty (ty_of const);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   408
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   409
val safe_ty_of = try ty_of #> the_default dummy_ty;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   410
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   411
fun strip_nun_binders binder (app as NApp (NConst (id, _, _), NAbs (var, body))) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   412
    if id = binder then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   413
      strip_nun_binders binder body
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   414
      |>> cons var
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   415
    else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   416
      ([], app)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   417
  | strip_nun_binders _ tm = ([], tm);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   418
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   419
fun fold_map_option _ NONE = pair NONE
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   420
  | fold_map_option f (SOME x) = f x #>> SOME;
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   421
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   422
fun fold_map_ty_idents f (NType (id, tys)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   423
    f id
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   424
    ##>> fold_map (fold_map_ty_idents f) tys
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   425
    #>> NType;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   426
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   427
fun fold_map_match_branch_idents f (id, vars, body) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   428
    f id
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   429
    ##>> fold_map (fold_map_tm_idents f) vars
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   430
    ##>> fold_map_tm_idents f body
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   431
    #>> Scan.triple1
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   432
and fold_map_tm_idents f (NAtom (j, ty)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   433
    fold_map_ty_idents f ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   434
    #>> curry NAtom j
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   435
  | fold_map_tm_idents f (NConst (id, tys, ty)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   436
    f id
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   437
    ##>> fold_map (fold_map_ty_idents f) tys
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   438
    ##>> fold_map_ty_idents f ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   439
    #>> (Scan.triple1 #> NConst)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   440
  | fold_map_tm_idents f (NAbs (var, body)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   441
    fold_map_tm_idents f var
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   442
    ##>> fold_map_tm_idents f body
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   443
    #>> NAbs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   444
  | fold_map_tm_idents f (NMatch (obj, branches)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   445
    fold_map_tm_idents f obj
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   446
    ##>> fold_map (fold_map_match_branch_idents f) branches
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   447
    #>> NMatch
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   448
  | fold_map_tm_idents f (NApp (const, arg)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   449
    fold_map_tm_idents f const
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   450
    ##>> fold_map_tm_idents f arg
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   451
    #>> NApp;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   452
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   453
fun fold_map_nun_copy_spec_idents f {abs_ty, rep_ty, subset, quotient, abs, rep} =
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   454
  fold_map_ty_idents f abs_ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   455
  ##>> fold_map_ty_idents f rep_ty
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   456
  ##>> fold_map_option (fold_map_tm_idents f) subset
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   457
  ##>> fold_map_option (fold_map_tm_idents f) quotient
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   458
  ##>> fold_map_tm_idents f abs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   459
  ##>> fold_map_tm_idents f rep
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   460
  #>> (fn (((((abs_ty, rep_ty), subset), quotient), abs), rep) =>
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   461
    {abs_ty = abs_ty, rep_ty = rep_ty, subset = subset, quotient = quotient, abs = abs, rep = rep});
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   462
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   463
fun fold_map_nun_ctr_spec_idents f {ctr, arg_tys} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   464
  fold_map_tm_idents f ctr
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   465
  ##>> fold_map (fold_map_ty_idents f) arg_tys
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   466
  #>> (fn (ctr, arg_tys) => {ctr = ctr, arg_tys = arg_tys});
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   467
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   468
fun fold_map_nun_co_data_spec_idents f {ty, ctrs} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   469
  fold_map_ty_idents f ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   470
  ##>> fold_map (fold_map_nun_ctr_spec_idents f) ctrs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   471
  #>> (fn (ty, ctrs) => {ty = ty, ctrs = ctrs});
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   472
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   473
fun fold_map_nun_const_spec_idents f {const, props} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   474
  fold_map_tm_idents f const
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   475
  ##>> fold_map (fold_map_tm_idents f) props
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   476
  #>> (fn (const, props) => {const = const, props = props});
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   477
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   478
fun fold_map_nun_consts_spec_idents f {consts, props} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   479
  fold_map (fold_map_tm_idents f) consts
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   480
  ##>> fold_map (fold_map_tm_idents f) props
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   481
  #>> (fn (consts, props) => {consts = consts, props = props});
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   482
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   483
fun fold_map_nun_command_idents f (NTVal (ty, cards)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   484
    fold_map_ty_idents f ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   485
    #>> (rpair cards #> NTVal)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   486
  | fold_map_nun_command_idents f (NCopy spec) =
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   487
    fold_map_nun_copy_spec_idents f spec
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   488
    #>> NCopy
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   489
  | fold_map_nun_command_idents f (NData specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   490
    fold_map (fold_map_nun_co_data_spec_idents f) specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   491
    #>> NData
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   492
  | fold_map_nun_command_idents f (NCodata specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   493
    fold_map (fold_map_nun_co_data_spec_idents f) specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   494
    #>> NCodata
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   495
  | fold_map_nun_command_idents f (NVal (tm, ty)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   496
    fold_map_tm_idents f tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   497
    ##>> fold_map_ty_idents f ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   498
    #>> NVal
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   499
  | fold_map_nun_command_idents f (NPred (wf, specs)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   500
    fold_map (fold_map_nun_const_spec_idents f) specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   501
    #>> curry NPred wf
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   502
  | fold_map_nun_command_idents f (NCopred specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   503
    fold_map (fold_map_nun_const_spec_idents f) specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   504
    #>> NCopred
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   505
  | fold_map_nun_command_idents f (NRec specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   506
    fold_map (fold_map_nun_const_spec_idents f) specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   507
    #>> NRec
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   508
  | fold_map_nun_command_idents f (NSpec spec) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   509
    fold_map_nun_consts_spec_idents f spec
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   510
    #>> NSpec
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   511
  | fold_map_nun_command_idents f (NAxiom tm) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   512
    fold_map_tm_idents f tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   513
    #>> NAxiom
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   514
  | fold_map_nun_command_idents f (NGoal tm) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   515
    fold_map_tm_idents f tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   516
    #>> NGoal
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   517
  | fold_map_nun_command_idents f (NEval tm) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   518
    fold_map_tm_idents f tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   519
    #>> NEval;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   520
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   521
fun fold_map_nun_problem_idents f ({commandss, sound, complete} : nun_problem) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   522
  fold_map (fold_map (fold_map_nun_command_idents f)) commandss
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   523
  #>> (fn commandss' => {commandss = commandss', sound = sound, complete = complete});
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   524
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   525
fun dest_rassoc_args oper arg0 rest =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   526
  (case rest of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   527
    NApp (NApp (oper', arg1), rest') =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   528
    if oper' = oper then arg0 :: dest_rassoc_args oper arg1 rest' else [arg0, rest]
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   529
  | _ => [arg0, rest]);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   530
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   531
val rcomb_tms = fold (fn arg => fn func => NApp (func, arg));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   532
val abs_tms = fold_rev (curry NAbs);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   533
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   534
fun fresh_var_names_wrt_tm n tm =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   535
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   536
    fun max_var_br (_, vars, body) = fold max_var (body :: vars)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   537
    and max_var (NAtom _) = I
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   538
      | max_var (NConst (id, _, _)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   539
        (fn max => if String.isPrefix nun_var_prefix id andalso size id > size max then id else max)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   540
      | max_var (NApp (func, arg)) = fold max_var [func, arg]
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   541
      | max_var (NAbs (var, body)) = fold max_var [var, body]
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   542
      | max_var (NMatch (obj, branches)) = max_var obj #> fold max_var_br branches;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   543
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   544
    val dummy_name = nun_var_of_str Name.uu;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   545
    val max_name = max_var tm dummy_name;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   546
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   547
    map (index_name max_name) (1 upto n)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   548
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   549
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   550
fun eta_expandN_tm 0 tm = tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   551
  | eta_expandN_tm n tm =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   552
    let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   553
      val var_names = fresh_var_names_wrt_tm n tm;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   554
      val arg_tys = domain_tys n (ty_of tm);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   555
      val vars = map2 (fn id => fn ty => NConst (id, [], ty)) var_names arg_tys;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   556
    in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   557
      abs_tms vars (rcomb_tms vars tm)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   558
    end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   559
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   560
val eta_expand_builtin_tm =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   561
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   562
    fun expand_quant_arg (NAbs (var, body)) = NAbs (var, expand_quant_arg body)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   563
      | expand_quant_arg (NMatch (obj, branches)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   564
        NMatch (obj, map (@{apply 3(3)} expand_quant_arg) branches)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   565
      | expand_quant_arg (tm as NApp (_, NAbs _)) = tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   566
      | expand_quant_arg (NApp (quant, arg)) = NApp (quant, eta_expandN_tm 1 arg)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   567
      | expand_quant_arg tm = tm;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   568
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   569
    fun expand args (NApp (func, arg)) = expand (expand [] arg :: args) func
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   570
      | expand args (func as NConst (id, _, _)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   571
        let val missing = Int.max (0, arity_of_nun_builtin id - length args) in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   572
          rcomb_tms args func
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   573
          |> eta_expandN_tm missing
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   574
          |> is_nun_const_quantifier id ? expand_quant_arg
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   575
        end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   576
      | expand args (func as NAtom _) = rcomb_tms args func
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   577
      | expand args (NAbs (var, body)) = rcomb_tms args (NAbs (var, expand [] body))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   578
      | expand args (NMatch (obj, branches)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   579
        rcomb_tms args (NMatch (obj, map (@{apply 3(3)} (expand [])) branches));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   580
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   581
    expand []
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   582
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   583
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   584
val str_of_ty =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   585
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   586
    fun str_of maybe_parens (NType (id, tys)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   587
      if id = nun_arrow then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   588
        (case tys of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   589
          [ty, ty'] => maybe_parens (str_of nun_parens ty ^ " " ^ nun_arrow ^ " " ^ str_of I ty'))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   590
      else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   591
        id ^ str_of_nun_arg_list (str_of I) tys
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   592
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   593
    str_of I
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   594
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   595
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   596
val (str_of_tmty, str_of_tm) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   597
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   598
    fun is_triv_head (NConst (id, _, _)) = (arity_of_nun_builtin id = 0)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   599
      | is_triv_head (NAtom _) = true
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   600
      | is_triv_head (NApp (const, _)) = is_triv_head const
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   601
      | is_triv_head (NAbs _) = false
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   602
      | is_triv_head (NMatch _) = false;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   603
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   604
    fun str_of_at_const id tys =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   605
      nun_at ^ str_of_ident id ^ str_of_nun_arg_list str_of_ty tys;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   606
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   607
    fun str_of_app ty_opt const arg =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   608
      let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   609
        val ty_opt' =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   610
          try (Option.map (fn ty => mk_arrow_ty (ty_of arg, ty))) ty_opt
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   611
          |> the_default NONE;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   612
      in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   613
        (str_of ty_opt' const |> (case const of NAbs _ => nun_parens | _ => I)) ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   614
        str_of_nun_arg_list (str_of NONE) [arg]
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   615
      end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   616
    and str_of_br ty_opt (id, vars, body) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   617
      " " ^ nun_bar ^ " " ^ id ^ space_implode "" (map (prefix " " o str_of NONE) vars) ^ " " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   618
      nun_arrow ^ " " ^ str_of ty_opt body
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   619
    and str_of_tmty tm =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   620
      let val ty = ty_of tm in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   621
        str_of (SOME ty) tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   622
      end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   623
    and str_of _ (NAtom (j, _)) = nun_dollar ^ string_of_int j
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   624
      | str_of _ (NConst (id, [], _)) = str_of_ident id
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   625
      | str_of (SOME ty0) (NConst (id, tys, ty)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   626
        if ty = ty0 then str_of_ident id else str_of_at_const id tys
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   627
      | str_of _ (NConst (id, tys, _)) = str_of_at_const id tys
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   628
      | str_of ty_opt (NAbs (var, body)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   629
        nun_lambda ^ " " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   630
        (case ty_opt of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   631
          SOME ty => str_of (SOME (domain_ty ty))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   632
        | NONE => nun_parens o str_of_tmty) var ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   633
        nun_dot ^ " " ^ str_of (Option.map range_ty ty_opt) body
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   634
      | str_of ty_opt (NMatch (obj, branches)) =
66618
048524a4f537 got rid of unsound and needless beta-reduction in Nunchaku frontend
blanchet
parents: 66614
diff changeset
   635
        nun_match ^ " " ^ str_of NONE obj ^ " " ^ nun_with ^
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   636
        space_implode "" (map (str_of_br ty_opt) branches) ^ " " ^ nun_end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   637
      | str_of ty_opt (app as NApp (func, argN)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   638
        (case (func, argN) of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   639
          (NApp (oper as NConst (id, _, _), arg1), arg2) =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   640
          if id = nun_asserting then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   641
            str_of ty_opt arg1 ^ " " ^ nun_asserting ^ " " ^ str_of (SOME prop_ty) arg2
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   642
            |> nun_parens
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   643
          else if id = nun_equals then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   644
            (str_of NONE arg1 |> not (is_triv_head arg1) ? nun_parens) ^ " " ^ id ^ " " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   645
            (str_of (try ty_of arg2) arg2 |> not (is_triv_head arg2) ? nun_parens)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   646
          else if is_nun_const_connective id then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   647
            let val args = dest_rassoc_args oper arg1 arg2 in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   648
              space_implode (" " ^ id ^ " ")
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   649
                (map (fn arg => str_of NONE arg |> not (is_triv_head arg) ? nun_parens) args)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   650
            end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   651
          else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   652
            str_of_app ty_opt func argN
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   653
        | (NApp (NApp (NConst (id, _, _), arg1), arg2), arg3) =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   654
          if id = nun_if then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   655
            nun_if ^ " " ^ str_of NONE arg1 ^ " " ^ nun_then ^ " " ^ str_of NONE arg2 ^ " " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   656
            nun_else ^ " " ^ str_of NONE arg3
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   657
            |> nun_parens
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   658
          else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   659
            str_of_app ty_opt func argN
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   660
        | (NConst (id, _, _), NAbs _) =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   661
          if is_nun_const_quantifier id then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   662
            let val (vars, body) = strip_nun_binders id app in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   663
              id ^ " " ^ space_implode " " (map (nun_parens o str_of_tmty) vars) ^ nun_dot ^ " " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   664
              str_of NONE body
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   665
            end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   666
          else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   667
            str_of_app ty_opt func argN
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   668
        | _ => str_of_app ty_opt func argN);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   669
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   670
    (str_of_tmty, str_of NONE)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   671
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   672
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   673
val empty_name_pool = {nice_of_ugly = Symtab.empty, ugly_of_nice = Symtab.empty};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   674
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   675
val nice_of_ugly_suggestion =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   676
  unascii_of #> Long_Name.base_name #> ascii_of #> unsuffix nun_custom_id_suffix
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   677
  #> (fn s => if s = "" orelse not (Char.isAlpha (String.sub (s, 0))) then "x" ^ s else s);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   678
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   679
fun allocate_nice ({nice_of_ugly, ugly_of_nice} : name_pool) (ugly, nice_sugg0) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   680
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   681
    fun alloc j =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   682
      let val nice_sugg = index_name nice_sugg0 j in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   683
        (case Symtab.lookup ugly_of_nice nice_sugg of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   684
          NONE =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   685
          (nice_sugg,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   686
           {nice_of_ugly = Symtab.update_new (ugly, nice_sugg) nice_of_ugly,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   687
            ugly_of_nice = Symtab.update_new (nice_sugg, ugly) ugly_of_nice})
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   688
        | SOME _ => alloc (j + 1))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   689
      end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   690
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   691
    alloc 0
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   692
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   693
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   694
fun nice_ident ugly (pool as {nice_of_ugly, ...}) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   695
  if String.isSuffix nun_custom_id_suffix ugly then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   696
    (case Symtab.lookup nice_of_ugly ugly of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   697
      NONE => allocate_nice pool (ugly, nice_of_ugly_suggestion ugly)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   698
    | SOME nice => (nice, pool))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   699
  else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   700
    (ugly, pool);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   701
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   702
fun nice_nun_problem problem =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   703
  fold_map_nun_problem_idents nice_ident problem empty_name_pool;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   704
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   705
fun str_of_tval (NType (id, tys)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   706
  str_of_ident id ^ " " ^ nun_colon ^ " " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   707
  fold (K (prefix (nun_type ^ " " ^ nun_arrow ^ " "))) tys nun_type;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   708
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   709
fun is_triv_subset (NAbs (_, body)) = is_triv_subset body
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   710
  | is_triv_subset (NConst (id, _, _)) = (id = nun_true)
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   711
  | is_triv_subset _ = false;
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   712
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   713
fun str_of_nun_copy_spec {abs_ty, rep_ty, subset, quotient, abs, rep} =
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   714
  str_of_ty abs_ty ^ " " ^ nun_assign ^ " " ^ str_of_ty rep_ty ^
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   715
  (case subset of
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   716
    NONE => ""
66622
0916eb2dbaca properly parenthesize copy types in Nunchaku
blanchet
parents: 66618
diff changeset
   717
  | SOME s =>
0916eb2dbaca properly parenthesize copy types in Nunchaku
blanchet
parents: 66618
diff changeset
   718
    if is_triv_subset s then ""
0916eb2dbaca properly parenthesize copy types in Nunchaku
blanchet
parents: 66618
diff changeset
   719
    else "\n  " ^ nun_subset ^ " " ^ nun_parens_if_space (str_of_tm s)) ^
64429
582f54f6b29b adapted Nunchaku integration to keyword renaming
blanchet
parents: 64411
diff changeset
   720
  (* TODO: use nun_quotient when possible *)
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   721
  (case quotient of
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   722
    NONE => ""
64429
582f54f6b29b adapted Nunchaku integration to keyword renaming
blanchet
parents: 64411
diff changeset
   723
  | SOME q => "\n  " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   724
  "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   725
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   726
fun str_of_nun_ctr_spec {ctr, arg_tys} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   727
  str_of_tm ctr ^ str_of_nun_arg_list str_of_ty arg_tys;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   728
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   729
fun str_of_nun_co_data_spec {ty, ctrs} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   730
  str_of_ty ty ^ " " ^ nun_assign ^ "\n  " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   731
  space_implode ("\n" ^ nun_bar ^ " ") (map str_of_nun_ctr_spec ctrs);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   732
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   733
fun str_of_nun_const_spec {const, props} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   734
  str_of_tmty const ^ " " ^ nun_assign ^ "\n  " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   735
  space_implode (nun_semicolon ^ "\n  ") (map str_of_tm props);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   736
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   737
fun str_of_nun_consts_spec {consts, props} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   738
  space_implode (" " ^ nun_and ^ "\n     ") (map str_of_tmty consts) ^ " " ^ nun_assign ^ "\n  " ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   739
  space_implode (nun_semicolon ^ "\n  ") (map str_of_tm props);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   740
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   741
fun str_of_nun_cards_suffix (NONE, NONE) = ""
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   742
  | str_of_nun_cards_suffix (c1, c2) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   743
    let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   744
      val s1 = Option.map (prefix "min_card " o signed_string_of_int) c1;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   745
      val s2 = Option.map (prefix "max_card " o signed_string_of_int) c2;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   746
    in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   747
      enclose " [" "]" (space_implode ", " (map_filter I [s1, s2]))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   748
    end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   749
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   750
fun str_of_nun_command (NTVal (ty, cards)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   751
    nun_val ^ " " ^ str_of_tval ty ^ str_of_nun_cards_suffix cards
64411
0af9926e1303 adapted Nunchaku's input syntax to new design decisions
blanchet
parents: 64389
diff changeset
   752
  | str_of_nun_command (NCopy spec) = nun_copy ^ " " ^ str_of_nun_copy_spec spec
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   753
  | str_of_nun_command (NData specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   754
    nun_data ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   755
  | str_of_nun_command (NCodata specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   756
    nun_codata ^ " " ^ str_of_nun_and_list str_of_nun_co_data_spec specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   757
  | str_of_nun_command (NVal (tm, ty)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   758
    nun_val ^ " " ^ str_of_tm tm ^ " " ^ nun_colon ^ " " ^ str_of_ty ty
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   759
  | str_of_nun_command (NPred (wf, specs)) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   760
    nun_pred ^ " " ^ (if wf then nun_lbracket ^ nun_wf ^ nun_rbracket ^ " " else "") ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   761
    str_of_nun_and_list str_of_nun_const_spec specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   762
  | str_of_nun_command (NCopred specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   763
    nun_copred ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   764
  | str_of_nun_command (NRec specs) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   765
    nun_rec ^ " " ^ str_of_nun_and_list str_of_nun_const_spec specs
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   766
  | str_of_nun_command (NSpec spec) = nun_spec ^ " " ^ str_of_nun_consts_spec spec
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   767
  | str_of_nun_command (NAxiom tm) = nun_axiom ^ " " ^ str_of_tm tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   768
  | str_of_nun_command (NGoal tm) = nun_goal ^ " " ^ str_of_tm tm
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   769
  | str_of_nun_command (NEval tm) = nun_hash ^ " " ^ nun_eval ^ " " ^ str_of_tm tm;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   770
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   771
fun str_of_nun_problem {commandss, sound, complete} =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   772
  map (cat_lines o map (suffix nun_dot o str_of_nun_command)) commandss
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   773
  |> space_implode "\n\n" |> suffix "\n"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   774
  |> prefix (nun_hash ^ " " ^ (if sound then "sound" else "unsound") ^ "\n")
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   775
  |> prefix (nun_hash ^ " " ^ (if complete then "complete" else "incomplete") ^ "\n");
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   776
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   777
end;