# HG changeset patch
# User haftmann
# Date 1224863322 -7200
# Node ID 1a9fabb515cd3f9df5043dd3a32c0a022c78977d
# Parent  150a8a1eae1a7657f440535f786d5de9f1df3424
"fun" gained a more uniform status

diff -r 150a8a1eae1a -r 1a9fabb515cd src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Fri Oct 24 17:48:40 2008 +0200
+++ b/src/Tools/code/code_thingol.ML	Fri Oct 24 17:48:42 2008 +0200
@@ -7,8 +7,6 @@
 *)
 
 infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
 infix 4 `$;
 infix 4 `$$;
 infixr 3 `|->;
@@ -31,8 +29,6 @@
     | `|-> of (vname * itype) * iterm
     | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
         (*((term, type), [(selector pattern, body term )]), primitive term)*)
-  val `-> : itype * itype -> itype;
-  val `--> : itype list * itype -> itype;
   val `$$ : iterm * iterm list -> iterm;
   val `|--> : (vname * itype) list * iterm -> iterm;
   type typscheme = (vname * sort) list * itype;
@@ -160,15 +156,9 @@
     instance (class, tyco)  inst
  *)
 
-fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
-val op `--> = Library.foldr (op `->);
 val op `$$ = Library.foldl (op `$);
 val op `|--> = Library.foldr (op `|->);
 
-val unfold_fun = unfoldr
-  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
-    | _ => NONE);
-
 val unfold_app = unfoldl
   (fn op `$ t => SOME t
     | _ => NONE);
@@ -256,19 +246,7 @@
   | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
 
 
-(** naming policies **)
-
-(* identifier categories *)
-
-val suffix_class = "class";
-val suffix_classrel = "classrel"
-val suffix_tyco = "tyco";
-val suffix_instance = "inst";
-val suffix_const = "const";
-
-fun add_suffix nsp NONE = NONE
-  | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
-
+(** namings **)
 
 (* policies *)
 
@@ -300,7 +278,8 @@
 fun namify_classrel thy = namify thy (fn (class1, class2) => 
   NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
   (*order fits nicely with composed projections*)
-fun namify_tyco thy = namify thy NameSpace.base thyname_of_tyco;
+fun namify_tyco thy "fun" = "Pure.fun"
+  | namify_tyco thy tyco = namify thy NameSpace.base thyname_of_tyco tyco;
 fun namify_instance thy = namify thy (fn (class, tyco) => 
   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
 fun namify_const thy = namify thy NameSpace.base thyname_of_const;
@@ -308,7 +287,7 @@
 end; (* local *)
 
 
-(* naming data with lookup and declare *)
+(* data *)
 
 structure StringPairTab = Code_Name.StringPairTab;
 
@@ -364,6 +343,22 @@
   mapp (add_variant update (thing, namify thy thing))
   #> `(fn naming => the (lookup naming thing));
 
+
+(* lookup and declare *)
+
+local
+
+val suffix_class = "class";
+val suffix_classrel = "classrel"
+val suffix_tyco = "tyco";
+val suffix_instance = "inst";
+val suffix_const = "const";
+
+fun add_suffix nsp NONE = NONE
+  | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
+
+in
+
 val lookup_class = add_suffix suffix_class
   oo Symtab.lookup o fst o #class o dest_Naming;
 val lookup_classrel = add_suffix suffix_classrel
@@ -386,6 +381,12 @@
 fun declare_const thy = declare thy map_const
   lookup_const Symtab.update_new namify_const;
 
+val unfold_fun = unfoldr
+  (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
+    | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
+
+end; (* local *)
+
 
 (** statements, abstract programs **)
 
@@ -492,7 +493,7 @@
       fold_map (fn superclass => ensure_class thy algbr funcgr superclass
         ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
       ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
-        ##>> exprgen_typ thy algbr funcgr ty) cs
+        ##>> translate_typ thy algbr funcgr ty) cs
       #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
   in ensure_stmt lookup_class (declare_class thy) stmt_class class end
 and ensure_classrel thy algbr funcgr (subclass, superclass) =
@@ -502,32 +503,30 @@
       ##>> ensure_class thy algbr funcgr superclass
       #>> Classrel;
   in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
-and ensure_tyco thy algbr funcgr "fun" =
-      pair "fun"
-  | ensure_tyco thy algbr funcgr tyco =
+and ensure_tyco thy algbr funcgr tyco =
+  let
+    val stmt_datatype =
       let
-        val stmt_datatype =
-          let
-            val (vs, cos) = Code.get_datatype thy tyco;
-          in
-            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-            ##>> fold_map (fn (c, tys) =>
-              ensure_const thy algbr funcgr c
-              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
-            #>> (fn info => Datatype (tyco, info))
-          end;
-      in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
-and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
+        val (vs, cos) = Code.get_datatype thy tyco;
+      in
+        fold_map (translate_tyvar_sort thy algbr funcgr) vs
+        ##>> fold_map (fn (c, tys) =>
+          ensure_const thy algbr funcgr c
+          ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
+        #>> (fn info => Datatype (tyco, info))
+      end;
+  in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
+and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
-and exprgen_typ thy algbr funcgr (TFree v_sort) =
-      exprgen_tyvar_sort thy algbr funcgr v_sort
+and translate_typ thy algbr funcgr (TFree v_sort) =
+      translate_tyvar_sort thy algbr funcgr v_sort
       #>> (fn (v, sort) => ITyVar v)
-  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
+  | translate_typ thy algbr funcgr (Type (tyco, tys)) =
       ensure_tyco thy algbr funcgr tyco
-      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
+      ##>> fold_map (translate_typ thy algbr funcgr) tys
       #>> (fn (tyco, tys) => tyco `%% tys)
-and exprgen_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
+and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   let
     val pp = Syntax.pp_global thy;
     datatype typarg =
@@ -555,13 +554,13 @@
           fold_map (ensure_classrel thy algbr funcgr) classrels
           #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   in fold_map mk_dict typargs end
-and exprgen_eq thy algbr funcgr (thm, linear) =
+and translate_eq thy algbr funcgr (thm, linear) =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
       o Logic.unvarify o prop_of) thm;
   in
-    fold_map (exprgen_term thy algbr funcgr (SOME thm)) args
-    ##>> exprgen_term thy algbr funcgr (SOME thm) rhs
+    fold_map (translate_term thy algbr funcgr (SOME thm)) args
+    ##>> translate_term thy algbr funcgr (SOME thm) rhs
     #>> rpair (thm, linear)
   end
 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
@@ -574,13 +573,13 @@
       Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
     val arity_typ = Type (tyco, map TFree vs);
     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
-    fun exprgen_superarity superclass =
+    fun translate_superarity superclass =
       ensure_class thy algbr funcgr superclass
       ##>> ensure_classrel thy algbr funcgr (class, superclass)
-      ##>> exprgen_dicts thy algbr funcgr NONE (arity_typ, [superclass])
+      ##>> translate_dicts thy algbr funcgr NONE (arity_typ, [superclass])
       #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
             (superclass, (classrel, (inst, dss))));
-    fun exprgen_classparam_inst (c, ty) =
+    fun translate_classparam_inst (c, ty) =
       let
         val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
         val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
@@ -588,15 +587,15 @@
           o Logic.dest_equals o Thm.prop_of) thm;
       in
         ensure_const thy algbr funcgr c
-        ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty
+        ##>> translate_const thy algbr funcgr (SOME thm) c_ty
         #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
       end;
     val stmt_inst =
       ensure_class thy algbr funcgr class
       ##>> ensure_tyco thy algbr funcgr tyco
-      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-      ##>> fold_map exprgen_superarity superclasses
-      ##>> fold_map exprgen_classparam_inst classparams
+      ##>> fold_map (translate_tyvar_sort thy algbr funcgr) vs
+      ##>> fold_map translate_superarity superclasses
+      ##>> fold_map translate_classparam_inst classparams
       #>> (fn ((((class, tyco), arity), superarities), classparams) =>
              Classinst ((class, (tyco, arity)), (superarities, classparams)));
   in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
@@ -615,9 +614,9 @@
           then raw_thms
           else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
       in
-        fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-        ##>> exprgen_typ thy algbr funcgr ty
-        ##>> fold_map (exprgen_eq thy algbr funcgr) thms
+        fold_map (translate_tyvar_sort thy algbr funcgr) vs
+        ##>> translate_typ thy algbr funcgr ty
+        ##>> fold_map (translate_eq thy algbr funcgr) thms
         #>> (fn info => Fun (c, info))
       end;
     val stmt_const = case Code.get_datatype_of_constr thy c
@@ -626,42 +625,42 @@
          of SOME class => stmt_classparam class
           | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
   in ensure_stmt lookup_const (declare_const thy) stmt_const c end
-and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
-      exprgen_app thy algbr funcgr thm ((c, ty), [])
-  | exprgen_term thy algbr funcgr thm (Free (v, _)) =
+and translate_term thy algbr funcgr thm (Const (c, ty)) =
+      translate_app thy algbr funcgr thm ((c, ty), [])
+  | translate_term thy algbr funcgr thm (Free (v, _)) =
       pair (IVar v)
-  | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
+  | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
       let
         val (v, t) = Syntax.variant_abs abs;
       in
-        exprgen_typ thy algbr funcgr ty
-        ##>> exprgen_term thy algbr funcgr thm t
+        translate_typ thy algbr funcgr ty
+        ##>> translate_term thy algbr funcgr thm t
         #>> (fn (ty, t) => (v, ty) `|-> t)
       end
-  | exprgen_term thy algbr funcgr thm (t as _ $ _) =
+  | translate_term thy algbr funcgr thm (t as _ $ _) =
       case strip_comb t
        of (Const (c, ty), ts) =>
-            exprgen_app thy algbr funcgr thm ((c, ty), ts)
+            translate_app thy algbr funcgr thm ((c, ty), ts)
         | (t', ts) =>
-            exprgen_term thy algbr funcgr thm t'
-            ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
+            translate_term thy algbr funcgr thm t'
+            ##>> fold_map (translate_term thy algbr funcgr thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and exprgen_const thy algbr funcgr thm (c, ty) =
+and translate_const thy algbr funcgr thm (c, ty) =
   let
     val tys = Sign.const_typargs thy (c, ty);
     val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
     val tys_args = (fst o Term.strip_type) ty;
   in
     ensure_const thy algbr funcgr c
-    ##>> fold_map (exprgen_dicts thy algbr funcgr thm) (tys ~~ sorts)
-    ##>> fold_map (exprgen_typ thy algbr funcgr) tys_args
+    ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
+    ##>> fold_map (translate_typ thy algbr funcgr) tys_args
     #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   end
-and exprgen_app_default thy algbr funcgr thm (c_ty, ts) =
-  exprgen_const thy algbr funcgr thm c_ty
-  ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
+and translate_app_default thy algbr funcgr thm (c_ty, ts) =
+  translate_const thy algbr funcgr thm c_ty
+  ##>> fold_map (translate_term thy algbr funcgr thm) ts
   #>> (fn (t, ts) => t `$$ ts)
-and exprgen_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
+and translate_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
   let
     val (tys, _) =
       (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
@@ -681,14 +680,14 @@
       | mk_ds cases = map_filter (uncurry mk_case)
           (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
   in
-    exprgen_term thy algbr funcgr thm dt
-    ##>> exprgen_typ thy algbr funcgr dty
-    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr thm pat
-          ##>> exprgen_term thy algbr funcgr thm body) (mk_ds cases)
-    ##>> exprgen_app_default thy algbr funcgr thm app
+    translate_term thy algbr funcgr thm dt
+    ##>> translate_typ thy algbr funcgr dty
+    ##>> fold_map (fn (pat, body) => translate_term thy algbr funcgr thm pat
+          ##>> translate_term thy algbr funcgr thm body) (mk_ds cases)
+    ##>> translate_app_default thy algbr funcgr thm app
     #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
   end
-and exprgen_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
+and translate_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
  of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
       if length ts < i then
         let
@@ -698,18 +697,18 @@
             (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
           val vs = Name.names ctxt "a" tys;
         in
-          fold_map (exprgen_typ thy algbr funcgr) tys
-          ##>> exprgen_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
+          fold_map (translate_typ thy algbr funcgr) tys
+          ##>> translate_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
           #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
         end
       else if length ts > i then
-        exprgen_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
-        ##>> fold_map (exprgen_term thy algbr funcgr thm) (Library.drop (i, ts))
+        translate_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
+        ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (i, ts))
         #>> (fn (t, ts) => t `$$ ts)
       else
-        exprgen_case thy algbr funcgr thm n cases ((c, ty), ts)
+        translate_case thy algbr funcgr thm n cases ((c, ty), ts)
       end
-  | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts);
+  | NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
 
 
 (** generated programs **)
@@ -763,9 +762,9 @@
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
     val stmt_value =
-      fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-      ##>> exprgen_typ thy algbr funcgr ty
-      ##>> exprgen_term thy algbr funcgr NONE t
+      fold_map (translate_tyvar_sort thy algbr funcgr) vs
+      ##>> translate_typ thy algbr funcgr ty
+      ##>> translate_term thy algbr funcgr NONE t
       #>> (fn ((vs, ty), t) => Fun
         (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
     fun term_value (dep, (naming, program1)) =