--- a/src/HOL/datatype.ML Mon Jun 17 16:51:47 1996 +0200
+++ b/src/HOL/datatype.ML Tue Jun 18 16:17:38 1996 +0200
@@ -224,8 +224,8 @@
val xrules =
let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
- in [("logic", "case x of " ^ first_part) <->
- ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
+ in [Syntax.<-> (("logic", "case x of " ^ first_part),
+ ("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
end;
(*type declarations for constructors*)
--- a/src/HOLCF/ax_ops/thy_ops.ML Mon Jun 17 16:51:47 1996 +0200
+++ b/src/HOLCF/ax_ops/thy_ops.ML Tue Jun 18 16:17:38 1996 +0200
@@ -153,53 +153,70 @@
| syn_decls curried sign (_::tl) = syn_decls curried sign tl
| syn_decls _ _ [] = [];
+fun translate name vars rhs =
+ Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name))
+ (map Variable vars)),
+ rhs);
+
(* generating the translation rules. Called by add_ext_axioms(_i) *)
local open Ast in
fun xrules_of true ((name,typ,CInfixl(i))::tail) =
- ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
- (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
- Constant (mk_internal_name name),Variable "A"]),Variable "B"]))
+ translate name ["A","B"]
+ (mk_appl (Constant "@fapp")
+ [(mk_appl (Constant "@fapp")
+ [Constant (mk_internal_name name),Variable "A"]),Variable "B"])
::xrules_of true tail
| xrules_of true ((name,typ,CInfixr(i))::tail) =
- ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
- (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
- Constant (mk_internal_name name),Variable "A"]),Variable "B"]))
+ translate name ["A","B"]
+ (mk_appl (Constant "@fapp")
+ [(mk_appl (Constant "@fapp")
+ [Constant (mk_internal_name name),Variable "A"]),Variable "B"])
::xrules_of true tail
(*####*)
- | xrules_of true ((name,typ,CMixfix(_))::tail) = let
- fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
- | argnames _ _ = [];
- val names = argnames (ord"A") typ;
- in if names = [] then [] else [mk_appl (Constant name) (map Variable names)<->
- foldl (fn (t,arg) => (mk_appl (Constant "@fapp") [t,Variable arg]))
- (Constant name,names)] end
+ | xrules_of true ((name,typ,CMixfix(_))::tail) =
+ let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
+ | argnames _ _ = [];
+ val names = argnames (ord"A") typ;
+ in if names = [] then [] else
+ [Syntax.<-> (mk_appl (Constant name) (map Variable names),
+ foldl (fn (t,arg) =>
+ (mk_appl (Constant "@fapp") [t,Variable arg]))
+ (Constant name,names))]
+ end
@xrules_of true tail
(*####*)
| xrules_of false ((name,typ,CInfixl(i))::tail) =
- ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
+ translate name ["A","B"]
(mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
- (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]))
+ (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
::xrules_of false tail
| xrules_of false ((name,typ,CInfixr(i))::tail) =
- ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
+ translate name ["A","B"]
(mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
- (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]))
+ (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
::xrules_of false tail
(*####*)
- | xrules_of false ((name,typ,CMixfix(_))::tail) = let
- fun foldr' f l =
- let fun itr [] = raise LIST "foldr'"
- | itr [a] = a
- | itr (a::l) = f(a, itr l)
- in itr l end;
- fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
- | argnames n _ = [chr n];
- val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
- | _ => []);
- in if vars = [] then [] else [mk_appl (Constant name) vars <->
- (mk_appl (Constant "@fapp") [Constant name, case vars of [v] => v
- | args => mk_appl (Constant "@ctuple") [hd args,foldr' (fn (t,arg) =>
- mk_appl (Constant "_args") [t,arg]) (tl args)]])]
+ | xrules_of false ((name,typ,CMixfix(_))::tail) =
+ let fun foldr' f l =
+ let fun itr [] = raise LIST "foldr'"
+ | itr [a] = a
+ | itr (a::l) = f(a, itr l)
+ in itr l end;
+ fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
+ | argnames n _ = [chr n];
+ val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
+ | _ => []);
+ in if vars = [] then [] else
+ [Syntax.<->
+ (mk_appl (Constant name) vars,
+ mk_appl (Constant "@fapp")
+ [Constant name,
+ case vars of [v] => v
+ | args => mk_appl (Constant "@ctuple")
+ [hd args,
+ foldr' (fn (t,arg) =>
+ mk_appl (Constant "_args")
+ [t,arg]) (tl args)]])]
end
@xrules_of false tail
(*####*)
--- a/src/Pure/Thy/thy_parse.ML Mon Jun 17 16:51:47 1996 +0200
+++ b/src/Pure/Thy/thy_parse.ML Tue Jun 18 16:17:38 1996 +0200
@@ -311,12 +311,15 @@
optional ("(" $$-- !! (name --$$ ")")) "\"logic\"" -- string >> mk_pair;
val trans_arrow =
- $$ "=>" >> K " |-> " ||
- $$ "<=" >> K " <-| " ||
- $$ "==" >> K " <-> ";
+ $$ "=>" >> K "Syntax.|-> " ||
+ $$ "<=" >> K "Syntax.<-| " ||
+ $$ "==" >> K "Syntax.<-> ";
-val trans_decls = repeat1 (trans_pat ^^ !! (trans_arrow ^^ trans_pat))
- >> mk_big_list;
+val trans_line =
+ trans_pat -- !! (trans_arrow -- trans_pat) >>
+ (fn (left, (arr, right)) => arr ^ "(" ^ left ^ ",\t" ^ right ^ ")");
+
+val trans_decls = repeat1 trans_line >> mk_big_list;
(* ML translations *)
--- a/src/Pure/sign.ML Mon Jun 17 16:51:47 1996 +0200
+++ b/src/Pure/sign.ML Tue Jun 18 16:17:38 1996 +0200
@@ -55,8 +55,8 @@
(string * (term list -> term)) list *
(string * (term list -> term)) list *
(string * (ast list -> ast)) list -> sg -> sg
- val add_trrules: (string * string) trrule list -> sg -> sg
- val add_trrules_i: ast trrule list -> sg -> sg
+ val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
+ val add_trrules_i: ast Syntax.trrule list -> sg -> sg
val add_name: string -> sg -> sg
val make_draft: sg -> sg
val merge: sg * sg -> sg