src/HOLCF/ax_ops/thy_ops.ML
author paulson
Wed, 27 Nov 1996 10:40:45 +0100
changeset 2238 c72a23bbe762
parent 1810 0eef167ebe1b
child 3534 c245c88194ff
permissions -rw-r--r--
Eta-expanded some declarations that are illegal under value polymorphism
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     1
(*  TTITLEF/thy_ops.ML
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     2
    ID:         $Id$
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     3
    Author:     Tobias Mayr
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     4
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     5
Additional theory file section for HOLCF: ops 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     6
There's an elaborate but german description of this program,
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     7
write to mayrt@informatik.tu-muenchen.de.
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     8
For a short english description of the new sections
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
     9
write to regensbu@informatik.tu-muenchen.de. 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    10
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    11
TODO: maybe AST-representation with "op name" instead of _I_...
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    12
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    13
*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    14
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    15
signature THY_OPS =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    16
sig
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    17
 (* continuous mixfixes (extension of datatype Mixfix.mixfix) *)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    18
 datatype cmixfix =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    19
    Mixfix of Mixfix.mixfix |
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    20
    CInfixl of int | 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    21
    CInfixr of int |
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    22
    CMixfix of string * int list *int;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    23
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    24
 exception CINFIX of cmixfix;
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    25
 val cmixfix_to_mixfix : cmixfix ->  Mixfix.mixfix;
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    26
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    27
 (* theory extenders : *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    28
 val add_ops          : {curried: bool, total: bool, strict: bool} ->
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    29
                        (string * string * cmixfix) list -> theory -> theory;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    30
 val add_ops_i        : {curried: bool, total: bool, strict: bool} ->
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    31
                        (string * typ * cmixfix) list -> theory -> theory;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    32
 val ops_keywords  : string list;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    33
 val ops_sections  : (string * (ThyParse.token list -> 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    34
                        (string * string) * ThyParse.token list)) list;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    35
 val opt_cmixfix: ThyParse.token list -> (string * ThyParse.token list);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    36
 val const_name    : string -> cmixfix -> string;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    37
end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    38
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    39
structure ThyOps : THY_OPS =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    40
struct
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    41
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    42
open HOLCFlogic;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    43
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    44
(** library ******************************************************)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    45
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    46
(* abbreviations *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    47
val internal = fst; (* cinfix-ops will have diffrent internal/external names *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    48
val external = snd;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    49
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    50
fun apsnd_of_three f = fn (a,b,c) => (a,f b,c);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    51
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    52
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    53
(******** ops ********************)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    54
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    55
(* the extended copy of mixfix *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    56
datatype cmixfix =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    57
    Mixfix of Mixfix.mixfix |
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    58
    CInfixl of int |
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    59
    CInfixr of int |
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    60
    CMixfix of string * int list *int;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    61
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    62
exception CINFIX of cmixfix;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    63
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    64
fun cmixfix_to_mixfix (Mixfix x) = x
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    65
  | cmixfix_to_mixfix x = raise CINFIX x;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    66
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    67
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    68
(** theory extender : add_ops *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    69
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    70
(* generating the declarations of the new constants. *************
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    71
   cinfix names x are internally non infix (renamed by mk_internal_name) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    72
   and externally non continous infix function names (changed by op_to_fun).
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    73
   Thus the cinfix declaration is splitted in an 'oldstyle' decl,
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    74
   which is NoSyn (non infix) and is added by add_consts_i,
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    75
   and an syn(tactic) decl, which is an infix function (not operation)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    76
   added by add_syntax_i, so that it can appear in input strings, but 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    77
   not in terms.
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    78
   The interface between internal and external names is realized by 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    79
   transrules A x B <=> _x ' A ' B (generated by xrules_of) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    80
   The boolean argument 'curried' distinguishes between curried and
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    81
   tupeled syntax of operation application *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    82
   
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    83
local
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    84
 fun strip ("'" :: c :: cs) = c :: strip cs
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    85
   | strip ["'"] = []
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    86
   | strip (c :: cs) = c :: strip cs
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    87
   | strip [] = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    88
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    89
 val strip_esc = implode o strip o explode;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    90
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    91
 fun infix_name c = "op " ^ strip_esc c;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    92
in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    93
  val mk_internal_name = infix_name;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    94
(*
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    95
(* changing e.g. 'ab' to '_I_97_98'. 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    96
   Called by oldstyle, xrules_of, strictness_axms and totality_axms. *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    97
  fun mk_internal_name name =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    98
  let fun alphanum (s::ss) = "_"^(string_of_int (ord s))^(alphanum ss)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
    99
        | alphanum [] = "";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   100
  in 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   101
      "_I"^(alphanum o explode) name
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   102
  end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   103
*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   104
 (* extension of Pure/Syntax/mixfix.ML: SynExt.const_name *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   105
 fun const_name c (CInfixl _) = mk_internal_name c
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   106
   | const_name c (CInfixr _) = mk_internal_name c
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   107
   | const_name c (CMixfix _) = c
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   108
   | const_name c (Mixfix  x) = Syntax.const_name c x;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   109
end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   110
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   111
(* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   112
(*####*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   113
fun op_to_fun true  sign (Type("->" ,[larg,t]))=
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1284
diff changeset
   114
                                         Type("fun",[larg,op_to_fun true sign t])
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   115
  | op_to_fun false sign (Type("->",[args,res])) = let
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1284
diff changeset
   116
                fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1284
diff changeset
   117
                |   otf t                        = Type("fun",[t,res]);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1284
diff changeset
   118
                in otf args end
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   119
  | op_to_fun _     sign t = t(*error("Wrong type for cinfix/cmixfix : "^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   120
                              (Sign.string_of_typ sign t))*);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   121
(*####*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   122
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   123
(* oldstyle is called by add_ext_axioms(_i) *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   124
    (* the first part is just copying the homomorphic part of the structures *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   125
fun oldstyle ((name,typ,Mixfix(x))::tl) = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   126
         (name,typ,x)::(oldstyle tl)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   127
  | oldstyle ((name,typ,CInfixl(i))::tl) = 
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   128
         (mk_internal_name name,typ,Mixfix.NoSyn)::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   129
         (oldstyle tl)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   130
  | oldstyle ((name,typ,CInfixr(i))::tl) =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   131
         (mk_internal_name name,typ,Mixfix.NoSyn)::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   132
         (oldstyle tl) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   133
  | oldstyle ((name,typ,CMixfix(x))::tl) =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   134
         (name,typ,Mixfix.NoSyn)::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   135
         (oldstyle tl) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   136
  | oldstyle [] = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   137
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   138
(* generating the external purely syntactical infix functions. 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   139
   Called by add_ext_axioms(_i) *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   140
fun syn_decls curried sign ((name,typ,CInfixl(i))::tl) =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   141
     (name,op_to_fun curried sign typ,Mixfix.Infixl(i))::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   142
      (syn_decls curried sign tl)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   143
  | syn_decls curried sign ((name,typ,CInfixr(i))::tl) =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   144
     (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   145
      (syn_decls curried sign tl)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   146
  | syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   147
(*####
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   148
     ("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   149
####**)
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   150
     (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   151
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   152
      (syn_decls curried sign tl)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   153
  | syn_decls curried sign (_::tl) = syn_decls curried sign tl
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   154
  | syn_decls _ _ [] = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   155
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   156
fun translate name vars rhs = 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   157
    Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name)) 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   158
		 (map Variable vars)), 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   159
		rhs); 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   160
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   161
(* generating the translation rules. Called by add_ext_axioms(_i) *)
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
   162
local open Ast in 
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   163
fun xrules_of true ((name,typ,CInfixl(i))::tail) = 
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   164
    translate name ["A","B"]
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   165
     (mk_appl (Constant "@fapp") 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   166
      [(mk_appl (Constant "@fapp") 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   167
	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   168
    ::xrules_of true tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   169
  | xrules_of true ((name,typ,CInfixr(i))::tail) = 
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   170
    translate name ["A","B"]
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   171
     (mk_appl (Constant "@fapp") 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   172
      [(mk_appl (Constant "@fapp") 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   173
	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   174
    ::xrules_of true tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   175
(*####*)
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   176
  | xrules_of true ((name,typ,CMixfix(_))::tail) = 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   177
        let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   178
            |   argnames _ _ = [];
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   179
            val names = argnames (ord"A") typ;
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   180
        in if names = [] then [] else 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   181
	    [Syntax.<-> (mk_appl (Constant name) (map Variable names),
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   182
			 foldl (fn (t,arg) => 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   183
				(mk_appl (Constant "@fapp") [t,Variable arg]))
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   184
			 (Constant name,names))] 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   185
        end
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   186
    @xrules_of true tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   187
(*####*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   188
  | xrules_of false ((name,typ,CInfixl(i))::tail) = 
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   189
    translate name ["A","B"]
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   190
    (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   191
     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   192
    ::xrules_of false tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   193
  | xrules_of false ((name,typ,CInfixr(i))::tail) = 
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   194
    translate name ["A","B"]
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   195
    (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   196
     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   197
    ::xrules_of false tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   198
(*####*)
1810
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   199
  | xrules_of false ((name,typ,CMixfix(_))::tail) = 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   200
        let fun foldr' f l =
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   201
	      let fun itr []  = raise LIST "foldr'"
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   202
		    | itr [a] = a
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   203
		    | itr (a::l) = f(a, itr l)
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   204
	      in  itr l end;
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   205
	    fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   206
	    |   argnames n _ = [chr n];
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   207
	    val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   208
						 | _ => []);
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   209
        in if vars = [] then [] else 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   210
	    [Syntax.<-> 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   211
	     (mk_appl (Constant name) vars,
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   212
	      mk_appl (Constant "@fapp")
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   213
	      [Constant name, 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   214
	       case vars of [v] => v
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   215
	                 | args => mk_appl (Constant "@ctuple")
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   216
			             [hd args,
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   217
				      foldr' (fn (t,arg) => 
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   218
					      mk_appl (Constant "_args")
0eef167ebe1b Translation infixes <->, etc., no longer available at top-level
paulson
parents: 1512
diff changeset
   219
					      [t,arg]) (tl args)]])]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1284
diff changeset
   220
        end
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   221
    @xrules_of false tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   222
(*####*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   223
  | xrules_of c ((name,typ,Mixfix(_))::tail) = xrules_of c tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   224
  | xrules_of _ [] = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   225
end; 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   226
(**** producing the new axioms ****************)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   227
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   228
datatype arguments = Curried_args of ((typ*typ) list) |
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   229
                     Tupeled_args of (typ list);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   230
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   231
fun num_of_args (Curried_args l) = length l
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   232
  | num_of_args (Tupeled_args l) = length l;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   233
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   234
fun types_of (Curried_args l) = map fst l
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   235
  | types_of (Tupeled_args l) = l;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   236
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   237
fun mk_mkNotEqUU_vars (typ::tl) cnt = mkNotEqUU (Free("x"^(string_of_int cnt),typ))::
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   238
                            (mk_mkNotEqUU_vars tl (cnt+1))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   239
  | mk_mkNotEqUU_vars [] _ = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   240
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   241
local
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   242
 (* T1*...*Tn goes to [T1,...,Tn] *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   243
 fun args_of_tupel (Type("*",[left,right])) = left::(args_of_tupel right)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   244
   | args_of_tupel T = [T];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   245
 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   246
 (* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   247
    Bi is the Type of the function that is applied to an Ai type argument *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   248
 fun args_of_curried (typ as (Type("->",[S,T]))) = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   249
      (S,typ) :: args_of_curried T
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   250
   | args_of_curried _ = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   251
in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   252
 fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   253
   | args_of_op false (typ as (Type("->",[S,T]))) = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   254
      Tupeled_args(args_of_tupel S)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   255
   | args_of_op false _ = Tupeled_args([]);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   256
end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   257
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   258
(* generates for the type t the type of the fapp constant 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   259
   that will be applied to t *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   260
fun mk_fapp_typ (typ as Type("->",argl)) = Type("fun",[typ,Type("fun",argl)]) 
1284
e5b95ee2616b removed incompatibility with sml
regensbu
parents: 1274
diff changeset
   261
  | mk_fapp_typ t = (
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   262
                    error("Internal error:mk_fapp_typ: wrong argument\n"));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   263
                    
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   264
fun mk_arg_tupel_UU uu_pos [typ] n = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   265
     if n<>uu_pos then Free("x"^(string_of_int n),typ)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   266
                  else Const("UU",typ)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   267
  | mk_arg_tupel_UU uu_pos (typ::tail) n = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   268
     mkCPair
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   269
     (if n<>uu_pos then Free("x"^(string_of_int n),typ) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   270
                   else Const("UU",typ))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   271
     (mk_arg_tupel_UU uu_pos tail (n+1))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   272
  | mk_arg_tupel_UU _ [] _ = error("Internal error:mk_arg_tupel: empty list");
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   273
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   274
fun mk_app_UU cnt uu_pos fname (Curried_args((typ,ftyp)::tl)) = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   275
     Const("fapp",mk_fapp_typ ftyp) $
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   276
     (mk_app_UU (cnt-1) uu_pos fname (Curried_args tl))$ 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   277
     (if cnt = uu_pos then Const("UU",typ)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   278
                      else Free("x"^(string_of_int cnt),typ))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   279
  | mk_app_UU _ _ (name,typ) (Curried_args []) = Const(name,typ)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   280
  | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args []) = Const(name,typ)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   281
  | mk_app_UU cnt uu_pos (name,typ) (Tupeled_args list) = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   282
     Const("fapp",mk_fapp_typ typ) $ Const(name,typ) $ 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   283
     mk_arg_tupel_UU uu_pos list 0;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   284
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   285
fun mk_app cnt fname args = mk_app_UU cnt (~1) fname args;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   286
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   287
(* producing the strictness axioms *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   288
local
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   289
 fun s_axm_of curried name typ args num cnt = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   290
       if cnt = num then 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   291
        error("Internal error: s_axm_of: arg is no operation "^(external name))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   292
       else 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   293
       let val app = mk_app_UU (num-1) cnt (internal name,typ) args
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   294
           val equation = HOLogic.mk_eq(app,Const("UU",fastype_of app)) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   295
       in 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   296
        if cnt = num-1 then equation
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   297
        else And $ equation $
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   298
             s_axm_of curried name typ args num (cnt+1)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   299
       end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   300
in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   301
 fun strictness_axms curried ((rawname,typ,cmixfix)::tail) =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   302
  let val name = case cmixfix of
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   303
                      (CInfixl _) => (mk_internal_name rawname,rawname)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   304
                    | (CInfixr _) => (mk_internal_name rawname,rawname)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   305
                    |  _          => (rawname,rawname)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   306
      val args = args_of_op curried typ;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   307
      val num  = num_of_args args;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   308
  in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   309
      ((external name)^"_strict",
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   310
       if num <> 0
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   311
       then HOLogic.mk_Trueprop(s_axm_of curried name typ args num 0) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   312
       else HOLogic.mk_Trueprop(True)) :: strictness_axms curried tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   313
  end
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   314
   | strictness_axms _ [] = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   315
end; (*local*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   316
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   317
(* producing the totality axioms *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   318
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   319
fun totality_axms curried ((rawname,typ,cmixfix)::tail) =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   320
 let val name  = case cmixfix of
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   321
                     (CInfixl _) => (mk_internal_name rawname,rawname)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   322
                   | (CInfixr _) => (mk_internal_name rawname,rawname)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   323
                   | _           => (rawname,rawname)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   324
     val args  = args_of_op curried typ;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   325
     val prems = mk_mkNotEqUU_vars (if curried then rev (types_of args)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   326
                                           else (types_of args)) 0;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   327
     val term  = mk_app (num_of_args args - 1) (internal name,typ) args;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   328
 in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   329
     ((external name)^"_total", 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   330
      if num_of_args args <> 0 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   331
      then Logic.list_implies (prems,mkNotEqUU term)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   332
      else HOLogic.mk_Trueprop(True)) :: totality_axms curried tail
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   333
 end
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   334
  | totality_axms _ [] = [];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   335
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   336
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   337
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   338
(* the theory extenders ****************************)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   339
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   340
fun add_ops {curried,strict,total} raw_decls thy =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   341
  let val {sign,...} = rep_theory thy;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   342
      val decls = map (apsnd_of_three (typ_of o read_ctyp sign)) raw_decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   343
      val oldstyledecls = oldstyle decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   344
      val syndecls = syn_decls curried sign decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   345
      val xrules = xrules_of curried decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   346
      val s_axms = (if strict then strictness_axms curried decls else []);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   347
      val t_axms = (if total  then totality_axms   curried decls else []);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   348
  in 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   349
  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   350
                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   351
  end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   352
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   353
fun add_ops_i {curried,strict,total} decls thy =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   354
  let val {sign,...} = rep_theory thy;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   355
      val oldstyledecls = oldstyle decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   356
      val syndecls = syn_decls curried sign decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   357
      val xrules = xrules_of curried decls;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   358
      val s_axms = (if strict then strictness_axms curried decls else []);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   359
      val t_axms = (if total  then totality_axms   curried decls else []);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   360
  in 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   361
  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   362
                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   363
  end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   364
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   365
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   366
(* parser: ops_decls ********************************)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   367
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   368
local open ThyParse 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   369
in
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   370
(* the following is an adapted version of const_decls from thy_parse.ML *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   371
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   372
val names1 = list1 name;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   373
2238
c72a23bbe762 Eta-expanded some declarations that are illegal under value polymorphism
paulson
parents: 1810
diff changeset
   374
fun split_decls decls = flat (map (fn (xs, y) => map (rpair y) xs) decls);
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   375
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   376
fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   377
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   378
fun mk_strict_vals [] = ""
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   379
  | mk_strict_vals [name] =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   380
      "get_axiom thy \""^name^"_strict\"\n"
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   381
  | mk_strict_vals (name::tail) =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   382
      "get_axiom thy \""^name^"_strict\",\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   383
      mk_strict_vals tail;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   384
  
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   385
fun mk_total_vals [] = ""
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   386
  | mk_total_vals [name] = 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   387
      "get_axiom thy \""^name^"_total\"\n"
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   388
  | mk_total_vals (name::tail) =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   389
      "get_axiom thy \""^name^"_total\",\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   390
      mk_total_vals tail;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   391
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   392
fun mk_ops_decls (((curried,strict),total),list) =
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   393
          (* call for the theory extender *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   394
           ("|> ThyOps.add_ops \n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   395
            "{ curried = "^curried^" , strict = "^strict^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   396
               " , total = "^total^" } \n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   397
            (mk_big_list o map mk_triple2) list^";\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   398
            "val strict_axms = []; val total_axms = [];\nval thy = thy\n",
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   399
          (* additional declarations *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   400
            (if strict="true" then "val strict_axms = strict_axms @ [\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   401
               mk_strict_vals (map (strip_quotes o fst) list)^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   402
               "];\n"             
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   403
             else "")^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   404
            (if total="true" then "val total_axms = total_axms @ [\n"^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   405
               mk_total_vals (map (strip_quotes o fst) list)^
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   406
               "];\n"             
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   407
             else ""));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   408
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   409
(* mixfix annotations *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   410
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   411
fun cat_parens pre1 pre2 s = cat pre1 (parens (cat pre2 s));
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   412
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   413
val infxl = "infixl" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixl";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   414
val infxr = "infixr" $$-- !! nat >> cat_parens "ThyOps.Mixfix" "Infixr";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   415
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   416
val cinfxl = "cinfixl" $$-- !! nat >> cat "ThyOps.CInfixl";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   417
val cinfxr = "cinfixr" $$-- !! nat >> cat "ThyOps.CInfixr";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   418
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   419
val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   420
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   421
val cmixfx = "cmixfix" $$-- string -- !! (opt_pris -- optional nat "max_pri")
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   422
  >> (cat "ThyOps.CMixfix" o mk_triple2);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   423
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   424
val bindr = "binder" $$--
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   425
  !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   426
                || nat >> (fn n => (n,n))
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   427
     )          )
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   428
  >> (cat_parens "ThyOps.Mixfix" "Binder" o mk_triple2);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   429
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   430
val mixfx = string -- !! (opt_pris -- optional nat "max_pri")
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   431
  >> (cat_parens "ThyOps.Mixfix" "Mixfix" o mk_triple2);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   432
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   433
fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "ThyOps.Mixfix NoSyn";
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   434
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   435
val opt_cmixfix = opt_syn (mixfx || infxl || infxr || bindr || 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   436
                              cinfxl || cinfxr || cmixfx);
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   437
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   438
fun ops_decls toks= 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   439
               (optional ($$ "curried" >> K "true") "false" --
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   440
                optional ($$ "strict" >> K "true") "false" --
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   441
                optional ($$ "total" >> K "true") "false" -- 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   442
                (repeat1 (names1 --$$ "::" -- !! (string -- opt_cmixfix)) 
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   443
                 >> split_decls)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   444
                >> mk_ops_decls) toks
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   445
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   446
end;
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   447
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   448
(*** new keywords and sections: ******************************************)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   449
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   450
val ops_keywords = ["curried","strict","total","cinfixl","cinfixr","cmixfix"];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   451
     (* "::" is already a pure keyword *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   452
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   453
val ops_sections = [("ops"    , ops_decls) ];
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   454
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   455
end; (* the structure ThyOps *)
ea0668a1c0ba added 8bit pragmas
regensbu
parents:
diff changeset
   456