Translation infixes <->, etc., no longer available at top-level
authorpaulson
Tue Jun 18 16:17:38 1996 +0200 (1996-06-18)
changeset 18100eef167ebe1b
parent 1809 8cb50df49570
child 1811 9083542fd861
Translation infixes <->, etc., no longer available at top-level
src/HOL/datatype.ML
src/HOLCF/ax_ops/thy_ops.ML
src/Pure/Thy/thy_parse.ML
src/Pure/sign.ML
     1.1 --- a/src/HOL/datatype.ML	Mon Jun 17 16:51:47 1996 +0200
     1.2 +++ b/src/HOL/datatype.ML	Tue Jun 18 16:17:38 1996 +0200
     1.3 @@ -224,8 +224,8 @@
     1.4        
     1.5        val xrules =
     1.6          let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
     1.7 -        in [("logic", "case x of " ^ first_part) <->
     1.8 -             ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
     1.9 +        in [Syntax.<-> (("logic", "case x of " ^ first_part),
    1.10 +			("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
    1.11          end;
    1.12  
    1.13       (*type declarations for constructors*)
     2.1 --- a/src/HOLCF/ax_ops/thy_ops.ML	Mon Jun 17 16:51:47 1996 +0200
     2.2 +++ b/src/HOLCF/ax_ops/thy_ops.ML	Tue Jun 18 16:17:38 1996 +0200
     2.3 @@ -153,53 +153,70 @@
     2.4    | syn_decls curried sign (_::tl) = syn_decls curried sign tl
     2.5    | syn_decls _ _ [] = [];
     2.6  
     2.7 +fun translate name vars rhs = 
     2.8 +    Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name)) 
     2.9 +		 (map Variable vars)), 
    2.10 +		rhs); 
    2.11 +
    2.12  (* generating the translation rules. Called by add_ext_axioms(_i) *)
    2.13  local open Ast in 
    2.14  fun xrules_of true ((name,typ,CInfixl(i))::tail) = 
    2.15 -    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
    2.16 -     (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
    2.17 -      Constant (mk_internal_name name),Variable "A"]),Variable "B"]))
    2.18 +    translate name ["A","B"]
    2.19 +     (mk_appl (Constant "@fapp") 
    2.20 +      [(mk_appl (Constant "@fapp") 
    2.21 +	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
    2.22      ::xrules_of true tail
    2.23    | xrules_of true ((name,typ,CInfixr(i))::tail) = 
    2.24 -    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
    2.25 -     (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
    2.26 -      Constant (mk_internal_name name),Variable "A"]),Variable "B"]))
    2.27 +    translate name ["A","B"]
    2.28 +     (mk_appl (Constant "@fapp") 
    2.29 +      [(mk_appl (Constant "@fapp") 
    2.30 +	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
    2.31      ::xrules_of true tail
    2.32  (*####*)
    2.33 -  | xrules_of true ((name,typ,CMixfix(_))::tail) = let
    2.34 -        fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
    2.35 -        |   argnames _ _ = [];
    2.36 -        val names = argnames (ord"A") typ;
    2.37 -        in if names = [] then [] else [mk_appl (Constant name) (map Variable names)<->
    2.38 -            foldl (fn (t,arg) => (mk_appl (Constant "@fapp") [t,Variable arg]))
    2.39 -                  (Constant name,names)] end
    2.40 +  | xrules_of true ((name,typ,CMixfix(_))::tail) = 
    2.41 +        let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
    2.42 +            |   argnames _ _ = [];
    2.43 +            val names = argnames (ord"A") typ;
    2.44 +        in if names = [] then [] else 
    2.45 +	    [Syntax.<-> (mk_appl (Constant name) (map Variable names),
    2.46 +			 foldl (fn (t,arg) => 
    2.47 +				(mk_appl (Constant "@fapp") [t,Variable arg]))
    2.48 +			 (Constant name,names))] 
    2.49 +        end
    2.50      @xrules_of true tail
    2.51  (*####*)
    2.52    | xrules_of false ((name,typ,CInfixl(i))::tail) = 
    2.53 -    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
    2.54 +    translate name ["A","B"]
    2.55      (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
    2.56 -     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]))
    2.57 +     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
    2.58      ::xrules_of false tail
    2.59    | xrules_of false ((name,typ,CInfixr(i))::tail) = 
    2.60 -    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
    2.61 +    translate name ["A","B"]
    2.62      (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
    2.63 -     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]))
    2.64 +     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
    2.65      ::xrules_of false tail
    2.66  (*####*)
    2.67 -  | xrules_of false ((name,typ,CMixfix(_))::tail) = let
    2.68 -        fun foldr' f l =
    2.69 -          let fun itr []  = raise LIST "foldr'"
    2.70 -                | itr [a] = a
    2.71 -                | itr (a::l) = f(a, itr l)
    2.72 -          in  itr l end;
    2.73 -        fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
    2.74 -        |   argnames n _ = [chr n];
    2.75 -        val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
    2.76 -                                             | _ => []);
    2.77 -        in if vars = [] then [] else [mk_appl (Constant name) vars <->
    2.78 -            (mk_appl (Constant "@fapp") [Constant name, case vars of [v] => v
    2.79 -                | args => mk_appl (Constant "@ctuple") [hd args,foldr' (fn (t,arg) => 
    2.80 -                                mk_appl (Constant "_args") [t,arg]) (tl args)]])]
    2.81 +  | xrules_of false ((name,typ,CMixfix(_))::tail) = 
    2.82 +        let fun foldr' f l =
    2.83 +	      let fun itr []  = raise LIST "foldr'"
    2.84 +		    | itr [a] = a
    2.85 +		    | itr (a::l) = f(a, itr l)
    2.86 +	      in  itr l end;
    2.87 +	    fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
    2.88 +	    |   argnames n _ = [chr n];
    2.89 +	    val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
    2.90 +						 | _ => []);
    2.91 +        in if vars = [] then [] else 
    2.92 +	    [Syntax.<-> 
    2.93 +	     (mk_appl (Constant name) vars,
    2.94 +	      mk_appl (Constant "@fapp")
    2.95 +	      [Constant name, 
    2.96 +	       case vars of [v] => v
    2.97 +	                 | args => mk_appl (Constant "@ctuple")
    2.98 +			             [hd args,
    2.99 +				      foldr' (fn (t,arg) => 
   2.100 +					      mk_appl (Constant "_args")
   2.101 +					      [t,arg]) (tl args)]])]
   2.102          end
   2.103      @xrules_of false tail
   2.104  (*####*)
     3.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Jun 17 16:51:47 1996 +0200
     3.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Jun 18 16:17:38 1996 +0200
     3.3 @@ -311,12 +311,15 @@
     3.4    optional ("(" $$-- !! (name --$$ ")")) "\"logic\"" -- string >> mk_pair;
     3.5  
     3.6  val trans_arrow =
     3.7 -  $$ "=>" >> K " |-> " ||
     3.8 -  $$ "<=" >> K " <-| " ||
     3.9 -  $$ "==" >> K " <-> ";
    3.10 +  $$ "=>" >> K "Syntax.|-> " ||
    3.11 +  $$ "<=" >> K "Syntax.<-| " ||
    3.12 +  $$ "==" >> K "Syntax.<-> ";
    3.13  
    3.14 -val trans_decls = repeat1 (trans_pat ^^ !! (trans_arrow ^^ trans_pat))
    3.15 -  >> mk_big_list;
    3.16 +val trans_line =
    3.17 +    trans_pat -- !! (trans_arrow -- trans_pat) >>
    3.18 +        (fn (left, (arr, right)) => arr ^ "(" ^ left ^ ",\t" ^ right ^ ")");
    3.19 +
    3.20 +val trans_decls = repeat1 trans_line >> mk_big_list;
    3.21  
    3.22  
    3.23  (* ML translations *)
     4.1 --- a/src/Pure/sign.ML	Mon Jun 17 16:51:47 1996 +0200
     4.2 +++ b/src/Pure/sign.ML	Tue Jun 18 16:17:38 1996 +0200
     4.3 @@ -55,8 +55,8 @@
     4.4      (string * (term list -> term)) list *
     4.5      (string * (term list -> term)) list *
     4.6      (string * (ast list -> ast)) list -> sg -> sg
     4.7 -  val add_trrules: (string * string) trrule list -> sg -> sg
     4.8 -  val add_trrules_i: ast trrule list -> sg -> sg
     4.9 +  val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    4.10 +  val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    4.11    val add_name: string -> sg -> sg
    4.12    val make_draft: sg -> sg
    4.13    val merge: sg * sg -> sg