src/Tools/Code/code_thingol.ML
changeset 32873 333945c9ac6a
parent 32872 019201eb7e07
child 32895 6f3cdb4a9e11
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Oct 05 08:36:33 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Oct 05 15:04:45 2009 +0200
     1.3 @@ -533,62 +533,62 @@
     1.4  
     1.5  (* translation *)
     1.6  
     1.7 -fun ensure_tyco thy algbr funcgr tyco =
     1.8 +fun ensure_tyco thy algbr eqngr tyco =
     1.9    let
    1.10      val stmt_datatype =
    1.11        let
    1.12          val (vs, cos) = Code.get_datatype thy tyco;
    1.13        in
    1.14 -        fold_map (translate_tyvar_sort thy algbr funcgr) vs
    1.15 +        fold_map (translate_tyvar_sort thy algbr eqngr) vs
    1.16          ##>> fold_map (fn (c, tys) =>
    1.17 -          ensure_const thy algbr funcgr c
    1.18 -          ##>> fold_map (translate_typ thy algbr funcgr) tys) cos
    1.19 +          ensure_const thy algbr eqngr c
    1.20 +          ##>> fold_map (translate_typ thy algbr eqngr) tys) cos
    1.21          #>> (fn info => Datatype (tyco, info))
    1.22        end;
    1.23    in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
    1.24 -and ensure_const thy algbr funcgr c =
    1.25 +and ensure_const thy algbr eqngr c =
    1.26    let
    1.27      fun stmt_datatypecons tyco =
    1.28 -      ensure_tyco thy algbr funcgr tyco
    1.29 +      ensure_tyco thy algbr eqngr tyco
    1.30        #>> (fn tyco => Datatypecons (c, tyco));
    1.31      fun stmt_classparam class =
    1.32 -      ensure_class thy algbr funcgr class
    1.33 +      ensure_class thy algbr eqngr class
    1.34        #>> (fn class => Classparam (c, class));
    1.35      fun stmt_fun raw_eqns =
    1.36        let
    1.37          val eqns = burrow_fst (clean_thms thy) raw_eqns;
    1.38 -        val ((vs, ty), _) = Code.typscheme_rhss_eqns thy c (map fst eqns);
    1.39 +        val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns);
    1.40        in
    1.41 -        fold_map (translate_tyvar_sort thy algbr funcgr) vs
    1.42 -        ##>> translate_typ thy algbr funcgr ty
    1.43 -        ##>> fold_map (translate_eqn thy algbr funcgr) eqns
    1.44 +        fold_map (translate_tyvar_sort thy algbr eqngr) vs
    1.45 +        ##>> translate_typ thy algbr eqngr ty
    1.46 +        ##>> fold_map (translate_eqn thy algbr eqngr) eqns
    1.47          #>> (fn info => Fun (c, info))
    1.48        end;
    1.49      val stmt_const = case Code.get_datatype_of_constr thy c
    1.50       of SOME tyco => stmt_datatypecons tyco
    1.51        | NONE => (case AxClass.class_of_param thy c
    1.52           of SOME class => stmt_classparam class
    1.53 -          | NONE => stmt_fun (Code_Preproc.eqns funcgr c))
    1.54 +          | NONE => stmt_fun (Code_Preproc.eqns eqngr c))
    1.55    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    1.56 -and ensure_class thy (algbr as (_, algebra)) funcgr class =
    1.57 +and ensure_class thy (algbr as (_, algebra)) eqngr class =
    1.58    let
    1.59      val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.60      val cs = #params (AxClass.get_info thy class);
    1.61      val stmt_class =
    1.62 -      fold_map (fn superclass => ensure_class thy algbr funcgr superclass
    1.63 -        ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
    1.64 -      ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
    1.65 -        ##>> translate_typ thy algbr funcgr ty) cs
    1.66 +      fold_map (fn superclass => ensure_class thy algbr eqngr superclass
    1.67 +        ##>> ensure_classrel thy algbr eqngr (class, superclass)) superclasses
    1.68 +      ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr c
    1.69 +        ##>> translate_typ thy algbr eqngr ty) cs
    1.70        #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
    1.71    in ensure_stmt lookup_class (declare_class thy) stmt_class class end
    1.72 -and ensure_classrel thy algbr funcgr (subclass, superclass) =
    1.73 +and ensure_classrel thy algbr eqngr (subclass, superclass) =
    1.74    let
    1.75      val stmt_classrel =
    1.76 -      ensure_class thy algbr funcgr subclass
    1.77 -      ##>> ensure_class thy algbr funcgr superclass
    1.78 +      ensure_class thy algbr eqngr subclass
    1.79 +      ##>> ensure_class thy algbr eqngr superclass
    1.80        #>> Classrel;
    1.81    in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
    1.82 -and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
    1.83 +and ensure_inst thy (algbr as (_, algebra)) eqngr (class, tyco) =
    1.84    let
    1.85      val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.86      val classparams = these (try (#params o AxClass.get_info thy) class);
    1.87 @@ -599,9 +599,9 @@
    1.88      val arity_typ = Type (tyco, map TFree vs);
    1.89      val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
    1.90      fun translate_superarity superclass =
    1.91 -      ensure_class thy algbr funcgr superclass
    1.92 -      ##>> ensure_classrel thy algbr funcgr (class, superclass)
    1.93 -      ##>> translate_dicts thy algbr funcgr NONE (arity_typ, [superclass])
    1.94 +      ensure_class thy algbr eqngr superclass
    1.95 +      ##>> ensure_classrel thy algbr eqngr (class, superclass)
    1.96 +      ##>> translate_dicts thy algbr eqngr NONE (arity_typ, [superclass])
    1.97        #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
    1.98              (superclass, (classrel, (inst, dss))));
    1.99      fun translate_classparam_inst (c, ty) =
   1.100 @@ -611,73 +611,73 @@
   1.101          val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   1.102            o Logic.dest_equals o Thm.prop_of) thm;
   1.103        in
   1.104 -        ensure_const thy algbr funcgr c
   1.105 -        ##>> translate_const thy algbr funcgr (SOME thm) c_ty
   1.106 +        ensure_const thy algbr eqngr c
   1.107 +        ##>> translate_const thy algbr eqngr (SOME thm) c_ty
   1.108          #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
   1.109        end;
   1.110      val stmt_inst =
   1.111 -      ensure_class thy algbr funcgr class
   1.112 -      ##>> ensure_tyco thy algbr funcgr tyco
   1.113 -      ##>> fold_map (translate_tyvar_sort thy algbr funcgr) vs
   1.114 +      ensure_class thy algbr eqngr class
   1.115 +      ##>> ensure_tyco thy algbr eqngr tyco
   1.116 +      ##>> fold_map (translate_tyvar_sort thy algbr eqngr) vs
   1.117        ##>> fold_map translate_superarity superclasses
   1.118        ##>> fold_map translate_classparam_inst classparams
   1.119        #>> (fn ((((class, tyco), arity), superarities), classparams) =>
   1.120               Classinst ((class, (tyco, arity)), (superarities, classparams)));
   1.121    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
   1.122 -and translate_typ thy algbr funcgr (TFree (v, _)) =
   1.123 +and translate_typ thy algbr eqngr (TFree (v, _)) =
   1.124        pair (ITyVar (unprefix "'" v))
   1.125 -  | translate_typ thy algbr funcgr (Type (tyco, tys)) =
   1.126 -      ensure_tyco thy algbr funcgr tyco
   1.127 -      ##>> fold_map (translate_typ thy algbr funcgr) tys
   1.128 +  | translate_typ thy algbr eqngr (Type (tyco, tys)) =
   1.129 +      ensure_tyco thy algbr eqngr tyco
   1.130 +      ##>> fold_map (translate_typ thy algbr eqngr) tys
   1.131        #>> (fn (tyco, tys) => tyco `%% tys)
   1.132 -and translate_term thy algbr funcgr thm (Const (c, ty)) =
   1.133 -      translate_app thy algbr funcgr thm ((c, ty), [])
   1.134 -  | translate_term thy algbr funcgr thm (Free (v, _)) =
   1.135 +and translate_term thy algbr eqngr thm (Const (c, ty)) =
   1.136 +      translate_app thy algbr eqngr thm ((c, ty), [])
   1.137 +  | translate_term thy algbr eqngr thm (Free (v, _)) =
   1.138        pair (IVar (SOME v))
   1.139 -  | translate_term thy algbr funcgr thm (Abs (v, ty, t)) =
   1.140 +  | translate_term thy algbr eqngr thm (Abs (v, ty, t)) =
   1.141        let
   1.142          val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
   1.143          val v'' = if member (op =) (Term.add_free_names t' []) v'
   1.144            then SOME v' else NONE
   1.145        in
   1.146 -        translate_typ thy algbr funcgr ty
   1.147 -        ##>> translate_term thy algbr funcgr thm t'
   1.148 +        translate_typ thy algbr eqngr ty
   1.149 +        ##>> translate_term thy algbr eqngr thm t'
   1.150          #>> (fn (ty, t) => (v'', ty) `|=> t)
   1.151        end
   1.152 -  | translate_term thy algbr funcgr thm (t as _ $ _) =
   1.153 +  | translate_term thy algbr eqngr thm (t as _ $ _) =
   1.154        case strip_comb t
   1.155         of (Const (c, ty), ts) =>
   1.156 -            translate_app thy algbr funcgr thm ((c, ty), ts)
   1.157 +            translate_app thy algbr eqngr thm ((c, ty), ts)
   1.158          | (t', ts) =>
   1.159 -            translate_term thy algbr funcgr thm t'
   1.160 -            ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.161 +            translate_term thy algbr eqngr thm t'
   1.162 +            ##>> fold_map (translate_term thy algbr eqngr thm) ts
   1.163              #>> (fn (t, ts) => t `$$ ts)
   1.164 -and translate_eqn thy algbr funcgr (thm, proper) =
   1.165 +and translate_eqn thy algbr eqngr (thm, proper) =
   1.166    let
   1.167      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   1.168        o Logic.unvarify o prop_of) thm;
   1.169    in
   1.170 -    fold_map (translate_term thy algbr funcgr (SOME thm)) args
   1.171 -    ##>> translate_term thy algbr funcgr (SOME thm) rhs
   1.172 +    fold_map (translate_term thy algbr eqngr (SOME thm)) args
   1.173 +    ##>> translate_term thy algbr eqngr (SOME thm) rhs
   1.174      #>> rpair (thm, proper)
   1.175    end
   1.176 -and translate_const thy algbr funcgr thm (c, ty) =
   1.177 +and translate_const thy algbr eqngr thm (c, ty) =
   1.178    let
   1.179      val tys = Sign.const_typargs thy (c, ty);
   1.180 -    val sorts = (map snd o fst o Code_Preproc.typ funcgr) c;
   1.181 +    val sorts = Code_Preproc.sortargs eqngr c;
   1.182      val tys_args = (fst o Term.strip_type) ty;
   1.183    in
   1.184 -    ensure_const thy algbr funcgr c
   1.185 -    ##>> fold_map (translate_typ thy algbr funcgr) tys
   1.186 -    ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
   1.187 -    ##>> fold_map (translate_typ thy algbr funcgr) tys_args
   1.188 +    ensure_const thy algbr eqngr c
   1.189 +    ##>> fold_map (translate_typ thy algbr eqngr) tys
   1.190 +    ##>> fold_map (translate_dicts thy algbr eqngr thm) (tys ~~ sorts)
   1.191 +    ##>> fold_map (translate_typ thy algbr eqngr) tys_args
   1.192      #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
   1.193    end
   1.194 -and translate_app_const thy algbr funcgr thm (c_ty, ts) =
   1.195 -  translate_const thy algbr funcgr thm c_ty
   1.196 -  ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.197 +and translate_app_const thy algbr eqngr thm (c_ty, ts) =
   1.198 +  translate_const thy algbr eqngr thm c_ty
   1.199 +  ##>> fold_map (translate_term thy algbr eqngr thm) ts
   1.200    #>> (fn (t, ts) => t `$$ ts)
   1.201 -and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   1.202 +and translate_case thy algbr eqngr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   1.203    let
   1.204      fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
   1.205      val tys = arg_types num_args (snd c_ty);
   1.206 @@ -721,14 +721,14 @@
   1.207                (constrs ~~ ts_clause);
   1.208        in ((t, ty), clauses) end;
   1.209    in
   1.210 -    translate_const thy algbr funcgr thm c_ty
   1.211 -    ##>> fold_map (fn (constr, n) => translate_const thy algbr funcgr thm constr #>> rpair n) constrs
   1.212 -    ##>> translate_typ thy algbr funcgr ty
   1.213 -    ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.214 +    translate_const thy algbr eqngr thm c_ty
   1.215 +    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs
   1.216 +    ##>> translate_typ thy algbr eqngr ty
   1.217 +    ##>> fold_map (translate_term thy algbr eqngr thm) ts
   1.218      #-> (fn (((t, constrs), ty), ts) =>
   1.219        `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
   1.220    end
   1.221 -and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   1.222 +and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   1.223    if length ts < num_args then
   1.224      let
   1.225        val k = length ts;
   1.226 @@ -736,24 +736,24 @@
   1.227        val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
   1.228        val vs = Name.names ctxt "a" tys;
   1.229      in
   1.230 -      fold_map (translate_typ thy algbr funcgr) tys
   1.231 -      ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
   1.232 +      fold_map (translate_typ thy algbr eqngr) tys
   1.233 +      ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs)
   1.234        #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
   1.235      end
   1.236    else if length ts > num_args then
   1.237 -    translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
   1.238 -    ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
   1.239 +    translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts))
   1.240 +    ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts))
   1.241      #>> (fn (t, ts) => t `$$ ts)
   1.242    else
   1.243 -    translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
   1.244 -and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
   1.245 +    translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
   1.246 +and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) =
   1.247    case Code.get_case_scheme thy c
   1.248 -   of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
   1.249 -    | NONE => translate_app_const thy algbr funcgr thm c_ty_ts
   1.250 -and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   1.251 -  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   1.252 +   of SOME case_scheme => translate_app_case thy algbr eqngr thm case_scheme c_ty_ts
   1.253 +    | NONE => translate_app_const thy algbr eqngr thm c_ty_ts
   1.254 +and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
   1.255 +  fold_map (ensure_class thy algbr eqngr) (proj_sort sort)
   1.256    #>> (fn sort => (unprefix "'" v, sort))
   1.257 -and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   1.258 +and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr thm (ty, sort) =
   1.259    let
   1.260      datatype typarg =
   1.261          Global of (class * string) * typarg list list
   1.262 @@ -773,11 +773,11 @@
   1.263         type_variable = type_variable} (ty, proj_sort sort)
   1.264        handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
   1.265      fun mk_dict (Global (inst, yss)) =
   1.266 -          ensure_inst thy algbr funcgr inst
   1.267 +          ensure_inst thy algbr eqngr inst
   1.268            ##>> (fold_map o fold_map) mk_dict yss
   1.269            #>> (fn (inst, dss) => DictConst (inst, dss))
   1.270        | mk_dict (Local (classrels, (v, (n, sort)))) =
   1.271 -          fold_map (ensure_classrel thy algbr funcgr) classrels
   1.272 +          fold_map (ensure_classrel thy algbr eqngr) classrels
   1.273            #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
   1.274    in fold_map mk_dict typargs end;
   1.275  
   1.276 @@ -800,9 +800,9 @@
   1.277  
   1.278  val cached_program = Program.get;
   1.279  
   1.280 -fun invoke_generation thy (algebra, funcgr) f name =
   1.281 +fun invoke_generation thy (algebra, eqngr) f name =
   1.282    Program.change_yield thy (fn naming_program => (NONE, naming_program)
   1.283 -    |> f thy algebra funcgr name
   1.284 +    |> f thy algebra eqngr name
   1.285      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
   1.286  
   1.287  
   1.288 @@ -814,8 +814,8 @@
   1.289        let
   1.290          val cs_all = Graph.all_succs program cs;
   1.291        in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
   1.292 -    fun generate_consts thy algebra funcgr =
   1.293 -      fold_map (ensure_const thy algebra funcgr);
   1.294 +    fun generate_consts thy algebra eqngr =
   1.295 +      fold_map (ensure_const thy algebra eqngr);
   1.296    in
   1.297      invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs
   1.298      |-> project_consts
   1.299 @@ -824,15 +824,15 @@
   1.300  
   1.301  (* value evaluation *)
   1.302  
   1.303 -fun ensure_value thy algbr funcgr t =
   1.304 +fun ensure_value thy algbr eqngr t =
   1.305    let
   1.306      val ty = fastype_of t;
   1.307      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   1.308        o dest_TFree))) t [];
   1.309      val stmt_value =
   1.310 -      fold_map (translate_tyvar_sort thy algbr funcgr) vs
   1.311 -      ##>> translate_typ thy algbr funcgr ty
   1.312 -      ##>> translate_term thy algbr funcgr NONE t
   1.313 +      fold_map (translate_tyvar_sort thy algbr eqngr) vs
   1.314 +      ##>> translate_typ thy algbr eqngr ty
   1.315 +      ##>> translate_term thy algbr eqngr NONE t
   1.316        #>> (fn ((vs, ty), t) => Fun
   1.317          (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
   1.318      fun term_value (dep, (naming, program1)) =
   1.319 @@ -850,10 +850,10 @@
   1.320      #> term_value
   1.321    end;
   1.322  
   1.323 -fun base_evaluator thy evaluator algebra funcgr vs t =
   1.324 +fun base_evaluator thy evaluator algebra eqngr vs t =
   1.325    let
   1.326      val (((naming, program), (((vs', ty'), t'), deps)), _) =
   1.327 -      invoke_generation thy (algebra, funcgr) ensure_value t;
   1.328 +      invoke_generation thy (algebra, eqngr) ensure_value t;
   1.329      val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
   1.330    in evaluator naming program ((vs'', (vs', ty')), t') deps end;
   1.331