src/Tools/code/code_thingol.ML
changeset 28688 1a9fabb515cd
parent 28663 bd8438543bf2
child 28706 3fef773ae6b1
     1.1 --- a/src/Tools/code/code_thingol.ML	Fri Oct 24 17:48:40 2008 +0200
     1.2 +++ b/src/Tools/code/code_thingol.ML	Fri Oct 24 17:48:42 2008 +0200
     1.3 @@ -7,8 +7,6 @@
     1.4  *)
     1.5  
     1.6  infix 8 `%%;
     1.7 -infixr 6 `->;
     1.8 -infixr 6 `-->;
     1.9  infix 4 `$;
    1.10  infix 4 `$$;
    1.11  infixr 3 `|->;
    1.12 @@ -31,8 +29,6 @@
    1.13      | `|-> of (vname * itype) * iterm
    1.14      | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    1.15          (*((term, type), [(selector pattern, body term )]), primitive term)*)
    1.16 -  val `-> : itype * itype -> itype;
    1.17 -  val `--> : itype list * itype -> itype;
    1.18    val `$$ : iterm * iterm list -> iterm;
    1.19    val `|--> : (vname * itype) list * iterm -> iterm;
    1.20    type typscheme = (vname * sort) list * itype;
    1.21 @@ -160,15 +156,9 @@
    1.22      instance (class, tyco)  inst
    1.23   *)
    1.24  
    1.25 -fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
    1.26 -val op `--> = Library.foldr (op `->);
    1.27  val op `$$ = Library.foldl (op `$);
    1.28  val op `|--> = Library.foldr (op `|->);
    1.29  
    1.30 -val unfold_fun = unfoldr
    1.31 -  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
    1.32 -    | _ => NONE);
    1.33 -
    1.34  val unfold_app = unfoldl
    1.35    (fn op `$ t => SOME t
    1.36      | _ => NONE);
    1.37 @@ -256,19 +246,7 @@
    1.38    | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
    1.39  
    1.40  
    1.41 -(** naming policies **)
    1.42 -
    1.43 -(* identifier categories *)
    1.44 -
    1.45 -val suffix_class = "class";
    1.46 -val suffix_classrel = "classrel"
    1.47 -val suffix_tyco = "tyco";
    1.48 -val suffix_instance = "inst";
    1.49 -val suffix_const = "const";
    1.50 -
    1.51 -fun add_suffix nsp NONE = NONE
    1.52 -  | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
    1.53 -
    1.54 +(** namings **)
    1.55  
    1.56  (* policies *)
    1.57  
    1.58 @@ -300,7 +278,8 @@
    1.59  fun namify_classrel thy = namify thy (fn (class1, class2) => 
    1.60    NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
    1.61    (*order fits nicely with composed projections*)
    1.62 -fun namify_tyco thy = namify thy NameSpace.base thyname_of_tyco;
    1.63 +fun namify_tyco thy "fun" = "Pure.fun"
    1.64 +  | namify_tyco thy tyco = namify thy NameSpace.base thyname_of_tyco tyco;
    1.65  fun namify_instance thy = namify thy (fn (class, tyco) => 
    1.66    NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
    1.67  fun namify_const thy = namify thy NameSpace.base thyname_of_const;
    1.68 @@ -308,7 +287,7 @@
    1.69  end; (* local *)
    1.70  
    1.71  
    1.72 -(* naming data with lookup and declare *)
    1.73 +(* data *)
    1.74  
    1.75  structure StringPairTab = Code_Name.StringPairTab;
    1.76  
    1.77 @@ -364,6 +343,22 @@
    1.78    mapp (add_variant update (thing, namify thy thing))
    1.79    #> `(fn naming => the (lookup naming thing));
    1.80  
    1.81 +
    1.82 +(* lookup and declare *)
    1.83 +
    1.84 +local
    1.85 +
    1.86 +val suffix_class = "class";
    1.87 +val suffix_classrel = "classrel"
    1.88 +val suffix_tyco = "tyco";
    1.89 +val suffix_instance = "inst";
    1.90 +val suffix_const = "const";
    1.91 +
    1.92 +fun add_suffix nsp NONE = NONE
    1.93 +  | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
    1.94 +
    1.95 +in
    1.96 +
    1.97  val lookup_class = add_suffix suffix_class
    1.98    oo Symtab.lookup o fst o #class o dest_Naming;
    1.99  val lookup_classrel = add_suffix suffix_classrel
   1.100 @@ -386,6 +381,12 @@
   1.101  fun declare_const thy = declare thy map_const
   1.102    lookup_const Symtab.update_new namify_const;
   1.103  
   1.104 +val unfold_fun = unfoldr
   1.105 +  (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
   1.106 +    | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
   1.107 +
   1.108 +end; (* local *)
   1.109 +
   1.110  
   1.111  (** statements, abstract programs **)
   1.112  
   1.113 @@ -492,7 +493,7 @@
   1.114        fold_map (fn superclass => ensure_class thy algbr funcgr superclass
   1.115          ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
   1.116        ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
   1.117 -        ##>> exprgen_typ thy algbr funcgr ty) cs
   1.118 +        ##>> translate_typ thy algbr funcgr ty) cs
   1.119        #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
   1.120    in ensure_stmt lookup_class (declare_class thy) stmt_class class end
   1.121  and ensure_classrel thy algbr funcgr (subclass, superclass) =
   1.122 @@ -502,32 +503,30 @@
   1.123        ##>> ensure_class thy algbr funcgr superclass
   1.124        #>> Classrel;
   1.125    in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
   1.126 -and ensure_tyco thy algbr funcgr "fun" =
   1.127 -      pair "fun"
   1.128 -  | ensure_tyco thy algbr funcgr tyco =
   1.129 +and ensure_tyco thy algbr funcgr tyco =
   1.130 +  let
   1.131 +    val stmt_datatype =
   1.132        let
   1.133 -        val stmt_datatype =
   1.134 -          let
   1.135 -            val (vs, cos) = Code.get_datatype thy tyco;
   1.136 -          in
   1.137 -            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.138 -            ##>> fold_map (fn (c, tys) =>
   1.139 -              ensure_const thy algbr funcgr c
   1.140 -              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
   1.141 -            #>> (fn info => Datatype (tyco, info))
   1.142 -          end;
   1.143 -      in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
   1.144 -and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   1.145 +        val (vs, cos) = Code.get_datatype thy tyco;
   1.146 +      in
   1.147 +        fold_map (translate_tyvar_sort thy algbr funcgr) vs
   1.148 +        ##>> fold_map (fn (c, tys) =>
   1.149 +          ensure_const thy algbr funcgr c
   1.150 +          ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
   1.151 +        #>> (fn info => Datatype (tyco, info))
   1.152 +      end;
   1.153 +  in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
   1.154 +and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   1.155    fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   1.156    #>> (fn sort => (unprefix "'" v, sort))
   1.157 -and exprgen_typ thy algbr funcgr (TFree v_sort) =
   1.158 -      exprgen_tyvar_sort thy algbr funcgr v_sort
   1.159 +and translate_typ thy algbr funcgr (TFree v_sort) =
   1.160 +      translate_tyvar_sort thy algbr funcgr v_sort
   1.161        #>> (fn (v, sort) => ITyVar v)
   1.162 -  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
   1.163 +  | translate_typ thy algbr funcgr (Type (tyco, tys)) =
   1.164        ensure_tyco thy algbr funcgr tyco
   1.165 -      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
   1.166 +      ##>> fold_map (translate_typ thy algbr funcgr) tys
   1.167        #>> (fn (tyco, tys) => tyco `%% tys)
   1.168 -and exprgen_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   1.169 +and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   1.170    let
   1.171      val pp = Syntax.pp_global thy;
   1.172      datatype typarg =
   1.173 @@ -555,13 +554,13 @@
   1.174            fold_map (ensure_classrel thy algbr funcgr) classrels
   1.175            #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   1.176    in fold_map mk_dict typargs end
   1.177 -and exprgen_eq thy algbr funcgr (thm, linear) =
   1.178 +and translate_eq thy algbr funcgr (thm, linear) =
   1.179    let
   1.180      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   1.181        o Logic.unvarify o prop_of) thm;
   1.182    in
   1.183 -    fold_map (exprgen_term thy algbr funcgr (SOME thm)) args
   1.184 -    ##>> exprgen_term thy algbr funcgr (SOME thm) rhs
   1.185 +    fold_map (translate_term thy algbr funcgr (SOME thm)) args
   1.186 +    ##>> translate_term thy algbr funcgr (SOME thm) rhs
   1.187      #>> rpair (thm, linear)
   1.188    end
   1.189  and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
   1.190 @@ -574,13 +573,13 @@
   1.191        Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   1.192      val arity_typ = Type (tyco, map TFree vs);
   1.193      val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
   1.194 -    fun exprgen_superarity superclass =
   1.195 +    fun translate_superarity superclass =
   1.196        ensure_class thy algbr funcgr superclass
   1.197        ##>> ensure_classrel thy algbr funcgr (class, superclass)
   1.198 -      ##>> exprgen_dicts thy algbr funcgr NONE (arity_typ, [superclass])
   1.199 +      ##>> translate_dicts thy algbr funcgr NONE (arity_typ, [superclass])
   1.200        #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   1.201              (superclass, (classrel, (inst, dss))));
   1.202 -    fun exprgen_classparam_inst (c, ty) =
   1.203 +    fun translate_classparam_inst (c, ty) =
   1.204        let
   1.205          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
   1.206          val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
   1.207 @@ -588,15 +587,15 @@
   1.208            o Logic.dest_equals o Thm.prop_of) thm;
   1.209        in
   1.210          ensure_const thy algbr funcgr c
   1.211 -        ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty
   1.212 +        ##>> translate_const thy algbr funcgr (SOME thm) c_ty
   1.213          #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
   1.214        end;
   1.215      val stmt_inst =
   1.216        ensure_class thy algbr funcgr class
   1.217        ##>> ensure_tyco thy algbr funcgr tyco
   1.218 -      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.219 -      ##>> fold_map exprgen_superarity superclasses
   1.220 -      ##>> fold_map exprgen_classparam_inst classparams
   1.221 +      ##>> fold_map (translate_tyvar_sort thy algbr funcgr) vs
   1.222 +      ##>> fold_map translate_superarity superclasses
   1.223 +      ##>> fold_map translate_classparam_inst classparams
   1.224        #>> (fn ((((class, tyco), arity), superarities), classparams) =>
   1.225               Classinst ((class, (tyco, arity)), (superarities, classparams)));
   1.226    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
   1.227 @@ -615,9 +614,9 @@
   1.228            then raw_thms
   1.229            else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
   1.230        in
   1.231 -        fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.232 -        ##>> exprgen_typ thy algbr funcgr ty
   1.233 -        ##>> fold_map (exprgen_eq thy algbr funcgr) thms
   1.234 +        fold_map (translate_tyvar_sort thy algbr funcgr) vs
   1.235 +        ##>> translate_typ thy algbr funcgr ty
   1.236 +        ##>> fold_map (translate_eq thy algbr funcgr) thms
   1.237          #>> (fn info => Fun (c, info))
   1.238        end;
   1.239      val stmt_const = case Code.get_datatype_of_constr thy c
   1.240 @@ -626,42 +625,42 @@
   1.241           of SOME class => stmt_classparam class
   1.242            | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
   1.243    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
   1.244 -and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
   1.245 -      exprgen_app thy algbr funcgr thm ((c, ty), [])
   1.246 -  | exprgen_term thy algbr funcgr thm (Free (v, _)) =
   1.247 +and translate_term thy algbr funcgr thm (Const (c, ty)) =
   1.248 +      translate_app thy algbr funcgr thm ((c, ty), [])
   1.249 +  | translate_term thy algbr funcgr thm (Free (v, _)) =
   1.250        pair (IVar v)
   1.251 -  | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
   1.252 +  | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
   1.253        let
   1.254          val (v, t) = Syntax.variant_abs abs;
   1.255        in
   1.256 -        exprgen_typ thy algbr funcgr ty
   1.257 -        ##>> exprgen_term thy algbr funcgr thm t
   1.258 +        translate_typ thy algbr funcgr ty
   1.259 +        ##>> translate_term thy algbr funcgr thm t
   1.260          #>> (fn (ty, t) => (v, ty) `|-> t)
   1.261        end
   1.262 -  | exprgen_term thy algbr funcgr thm (t as _ $ _) =
   1.263 +  | translate_term thy algbr funcgr thm (t as _ $ _) =
   1.264        case strip_comb t
   1.265         of (Const (c, ty), ts) =>
   1.266 -            exprgen_app thy algbr funcgr thm ((c, ty), ts)
   1.267 +            translate_app thy algbr funcgr thm ((c, ty), ts)
   1.268          | (t', ts) =>
   1.269 -            exprgen_term thy algbr funcgr thm t'
   1.270 -            ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
   1.271 +            translate_term thy algbr funcgr thm t'
   1.272 +            ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.273              #>> (fn (t, ts) => t `$$ ts)
   1.274 -and exprgen_const thy algbr funcgr thm (c, ty) =
   1.275 +and translate_const thy algbr funcgr thm (c, ty) =
   1.276    let
   1.277      val tys = Sign.const_typargs thy (c, ty);
   1.278      val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
   1.279      val tys_args = (fst o Term.strip_type) ty;
   1.280    in
   1.281      ensure_const thy algbr funcgr c
   1.282 -    ##>> fold_map (exprgen_dicts thy algbr funcgr thm) (tys ~~ sorts)
   1.283 -    ##>> fold_map (exprgen_typ thy algbr funcgr) tys_args
   1.284 +    ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
   1.285 +    ##>> fold_map (translate_typ thy algbr funcgr) tys_args
   1.286      #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   1.287    end
   1.288 -and exprgen_app_default thy algbr funcgr thm (c_ty, ts) =
   1.289 -  exprgen_const thy algbr funcgr thm c_ty
   1.290 -  ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
   1.291 +and translate_app_default thy algbr funcgr thm (c_ty, ts) =
   1.292 +  translate_const thy algbr funcgr thm c_ty
   1.293 +  ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.294    #>> (fn (t, ts) => t `$$ ts)
   1.295 -and exprgen_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
   1.296 +and translate_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
   1.297    let
   1.298      val (tys, _) =
   1.299        (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
   1.300 @@ -681,14 +680,14 @@
   1.301        | mk_ds cases = map_filter (uncurry mk_case)
   1.302            (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
   1.303    in
   1.304 -    exprgen_term thy algbr funcgr thm dt
   1.305 -    ##>> exprgen_typ thy algbr funcgr dty
   1.306 -    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr thm pat
   1.307 -          ##>> exprgen_term thy algbr funcgr thm body) (mk_ds cases)
   1.308 -    ##>> exprgen_app_default thy algbr funcgr thm app
   1.309 +    translate_term thy algbr funcgr thm dt
   1.310 +    ##>> translate_typ thy algbr funcgr dty
   1.311 +    ##>> fold_map (fn (pat, body) => translate_term thy algbr funcgr thm pat
   1.312 +          ##>> translate_term thy algbr funcgr thm body) (mk_ds cases)
   1.313 +    ##>> translate_app_default thy algbr funcgr thm app
   1.314      #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
   1.315    end
   1.316 -and exprgen_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
   1.317 +and translate_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
   1.318   of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
   1.319        if length ts < i then
   1.320          let
   1.321 @@ -698,18 +697,18 @@
   1.322              (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
   1.323            val vs = Name.names ctxt "a" tys;
   1.324          in
   1.325 -          fold_map (exprgen_typ thy algbr funcgr) tys
   1.326 -          ##>> exprgen_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
   1.327 +          fold_map (translate_typ thy algbr funcgr) tys
   1.328 +          ##>> translate_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
   1.329            #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   1.330          end
   1.331        else if length ts > i then
   1.332 -        exprgen_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
   1.333 -        ##>> fold_map (exprgen_term thy algbr funcgr thm) (Library.drop (i, ts))
   1.334 +        translate_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
   1.335 +        ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (i, ts))
   1.336          #>> (fn (t, ts) => t `$$ ts)
   1.337        else
   1.338 -        exprgen_case thy algbr funcgr thm n cases ((c, ty), ts)
   1.339 +        translate_case thy algbr funcgr thm n cases ((c, ty), ts)
   1.340        end
   1.341 -  | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts);
   1.342 +  | NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
   1.343  
   1.344  
   1.345  (** generated programs **)
   1.346 @@ -763,9 +762,9 @@
   1.347      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   1.348        o dest_TFree))) t [];
   1.349      val stmt_value =
   1.350 -      fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.351 -      ##>> exprgen_typ thy algbr funcgr ty
   1.352 -      ##>> exprgen_term thy algbr funcgr NONE t
   1.353 +      fold_map (translate_tyvar_sort thy algbr funcgr) vs
   1.354 +      ##>> translate_typ thy algbr funcgr ty
   1.355 +      ##>> translate_term thy algbr funcgr NONE t
   1.356        #>> (fn ((vs, ty), t) => Fun
   1.357          (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
   1.358      fun term_value (dep, (naming, program1)) =