src/Tools/Code/code_thingol.ML
changeset 35226 b987b803616d
parent 34895 19fd499cddff
child 35299 4f4d5bf4ea08
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Feb 19 11:06:21 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Feb 19 11:06:21 2010 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5    datatype stmt =
     1.6        NoStmt
     1.7 -    | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
     1.8 +    | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.9      | Datatype of string * ((vname * sort) list * (string * itype list) list)
    1.10      | Datatypecons of string * string
    1.11      | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.12 @@ -256,8 +256,8 @@
    1.13      | thyname :: _ => thyname;
    1.14    fun thyname_of_const thy c = case AxClass.class_of_param thy c
    1.15     of SOME class => thyname_of_class thy class
    1.16 -    | NONE => (case Code.get_datatype_of_constr thy c
    1.17 -       of SOME dtco => Codegen.thyname_of_type thy dtco
    1.18 +    | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
    1.19 +       of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
    1.20          | NONE => Codegen.thyname_of_const thy c);
    1.21    fun purify_base "==>" = "follows"
    1.22      | purify_base "op &" = "and"
    1.23 @@ -400,7 +400,7 @@
    1.24  type typscheme = (vname * sort) list * itype;
    1.25  datatype stmt =
    1.26      NoStmt
    1.27 -  | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
    1.28 +  | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    1.29    | Datatype of string * ((vname * sort) list * (string * itype list) list)
    1.30    | Datatypecons of string * string
    1.31    | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.32 @@ -523,14 +523,18 @@
    1.33          |> pair name
    1.34    end;
    1.35  
    1.36 -fun not_wellsorted thy thm ty sort e =
    1.37 +fun translation_error thy some_thm msg sub_msg =
    1.38 +  let
    1.39 +    val err_thm = case some_thm
    1.40 +     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
    1.41 +  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
    1.42 +
    1.43 +fun not_wellsorted thy some_thm ty sort e =
    1.44    let
    1.45      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
    1.46 -    val err_thm = case thm
    1.47 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
    1.48      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
    1.49        ^ Syntax.string_of_sort_global thy sort;
    1.50 -  in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
    1.51 +  in translation_error thy some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
    1.52  
    1.53  
    1.54  (* translation *)
    1.55 @@ -558,16 +562,15 @@
    1.56        #>> (fn class => Classparam (c, class));
    1.57      fun stmt_fun cert =
    1.58        let
    1.59 -        val ((vs, ty), raw_eqns) = Code.equations_thms_cert thy cert;
    1.60 -        val eqns = map snd raw_eqns;
    1.61 +        val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
    1.62        in
    1.63          fold_map (translate_tyvar_sort thy algbr eqngr) vs
    1.64          ##>> translate_typ thy algbr eqngr ty
    1.65          ##>> fold_map (translate_eqn thy algbr eqngr) eqns
    1.66          #>> (fn info => Fun (c, info))
    1.67        end;
    1.68 -    val stmt_const = case Code.get_datatype_of_constr thy c
    1.69 -     of SOME tyco => stmt_datatypecons tyco
    1.70 +    val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
    1.71 +     of SOME (tyco, _) => stmt_datatypecons tyco
    1.72        | NONE => (case AxClass.class_of_param thy c
    1.73           of SOME class => stmt_classparam class
    1.74            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
    1.75 @@ -614,7 +617,7 @@
    1.76            o Logic.dest_equals o Thm.prop_of) thm;
    1.77        in
    1.78          ensure_const thy algbr eqngr c
    1.79 -        ##>> translate_const thy algbr eqngr (SOME thm) c_ty
    1.80 +        ##>> translate_const thy algbr eqngr NONE (SOME thm) c_ty
    1.81          #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
    1.82        end;
    1.83      val stmt_inst =
    1.84 @@ -632,54 +635,54 @@
    1.85        ensure_tyco thy algbr eqngr tyco
    1.86        ##>> fold_map (translate_typ thy algbr eqngr) tys
    1.87        #>> (fn (tyco, tys) => tyco `%% tys)
    1.88 -and translate_term thy algbr eqngr thm (Const (c, ty)) =
    1.89 -      translate_app thy algbr eqngr thm ((c, ty), [])
    1.90 -  | translate_term thy algbr eqngr thm (Free (v, _)) =
    1.91 +and translate_term thy algbr eqngr some_abs some_thm (Const (c, ty)) =
    1.92 +      translate_app thy algbr eqngr some_abs some_thm ((c, ty), [])
    1.93 +  | translate_term thy algbr eqngr some_abs some_thm (Free (v, _)) =
    1.94        pair (IVar (SOME v))
    1.95 -  | translate_term thy algbr eqngr thm (Abs (v, ty, t)) =
    1.96 +  | translate_term thy algbr eqngr some_abs some_thm (Abs (v, ty, t)) =
    1.97        let
    1.98          val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
    1.99          val v'' = if member (op =) (Term.add_free_names t' []) v'
   1.100            then SOME v' else NONE
   1.101        in
   1.102          translate_typ thy algbr eqngr ty
   1.103 -        ##>> translate_term thy algbr eqngr thm t'
   1.104 +        ##>> translate_term thy algbr eqngr some_abs some_thm t'
   1.105          #>> (fn (ty, t) => (v'', ty) `|=> t)
   1.106        end
   1.107 -  | translate_term thy algbr eqngr thm (t as _ $ _) =
   1.108 +  | translate_term thy algbr eqngr some_abs some_thm (t as _ $ _) =
   1.109        case strip_comb t
   1.110         of (Const (c, ty), ts) =>
   1.111 -            translate_app thy algbr eqngr thm ((c, ty), ts)
   1.112 +            translate_app thy algbr eqngr some_abs some_thm ((c, ty), ts)
   1.113          | (t', ts) =>
   1.114 -            translate_term thy algbr eqngr thm t'
   1.115 -            ##>> fold_map (translate_term thy algbr eqngr thm) ts
   1.116 +            translate_term thy algbr eqngr some_abs some_thm t'
   1.117 +            ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
   1.118              #>> (fn (t, ts) => t `$$ ts)
   1.119 -and translate_eqn thy algbr eqngr (thm, proper) =
   1.120 +and translate_eqn thy algbr eqngr ((some_abs, (args, rhs)), (some_thm, proper)) =
   1.121 +  fold_map (translate_term thy algbr eqngr some_abs some_thm) args
   1.122 +  ##>> translate_term thy algbr eqngr some_abs some_thm rhs
   1.123 +  #>> rpair (some_thm, proper)
   1.124 +and translate_const thy algbr eqngr some_abs some_thm (c, ty) =
   1.125    let
   1.126 -    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   1.127 -      o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
   1.128 -  in
   1.129 -    fold_map (translate_term thy algbr eqngr (SOME thm)) args
   1.130 -    ##>> translate_term thy algbr eqngr (SOME thm) rhs
   1.131 -    #>> rpair (thm, proper)
   1.132 -  end
   1.133 -and translate_const thy algbr eqngr thm (c, ty) =
   1.134 -  let
   1.135 +    val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
   1.136 +        andalso Code.is_abstr thy c
   1.137 +        then translation_error thy some_thm
   1.138 +          "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
   1.139 +      else ()
   1.140      val tys = Sign.const_typargs thy (c, ty);
   1.141      val sorts = Code_Preproc.sortargs eqngr c;
   1.142      val tys_args = (fst o Term.strip_type) ty;
   1.143    in
   1.144      ensure_const thy algbr eqngr c
   1.145      ##>> fold_map (translate_typ thy algbr eqngr) tys
   1.146 -    ##>> fold_map (translate_dicts thy algbr eqngr thm) (tys ~~ sorts)
   1.147 +    ##>> fold_map (translate_dicts thy algbr eqngr some_thm) (tys ~~ sorts)
   1.148      ##>> fold_map (translate_typ thy algbr eqngr) tys_args
   1.149      #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
   1.150    end
   1.151 -and translate_app_const thy algbr eqngr thm (c_ty, ts) =
   1.152 -  translate_const thy algbr eqngr thm c_ty
   1.153 -  ##>> fold_map (translate_term thy algbr eqngr thm) ts
   1.154 +and translate_app_const thy algbr eqngr some_abs some_thm (c_ty, ts) =
   1.155 +  translate_const thy algbr eqngr some_abs some_thm c_ty
   1.156 +  ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
   1.157    #>> (fn (t, ts) => t `$$ ts)
   1.158 -and translate_case thy algbr eqngr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   1.159 +and translate_case thy algbr eqngr some_abs some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   1.160    let
   1.161      fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
   1.162      val tys = arg_types num_args (snd c_ty);
   1.163 @@ -723,14 +726,14 @@
   1.164                (constrs ~~ ts_clause);
   1.165        in ((t, ty), clauses) end;
   1.166    in
   1.167 -    translate_const thy algbr eqngr thm c_ty
   1.168 -    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs
   1.169 +    translate_const thy algbr eqngr some_abs some_thm c_ty
   1.170 +    ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr some_abs some_thm constr #>> rpair n) constrs
   1.171      ##>> translate_typ thy algbr eqngr ty
   1.172 -    ##>> fold_map (translate_term thy algbr eqngr thm) ts
   1.173 +    ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
   1.174      #-> (fn (((t, constrs), ty), ts) =>
   1.175        `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
   1.176    end
   1.177 -and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   1.178 +and translate_app_case thy algbr eqngr some_abs some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   1.179    if length ts < num_args then
   1.180      let
   1.181        val k = length ts;
   1.182 @@ -739,23 +742,23 @@
   1.183        val vs = Name.names ctxt "a" tys;
   1.184      in
   1.185        fold_map (translate_typ thy algbr eqngr) tys
   1.186 -      ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs)
   1.187 +      ##>> translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts @ map Free vs)
   1.188        #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
   1.189      end
   1.190    else if length ts > num_args then
   1.191 -    translate_case thy algbr eqngr thm case_scheme ((c, ty), take num_args ts)
   1.192 -    ##>> fold_map (translate_term thy algbr eqngr thm) (drop num_args ts)
   1.193 +    translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), take num_args ts)
   1.194 +    ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) (drop num_args ts)
   1.195      #>> (fn (t, ts) => t `$$ ts)
   1.196    else
   1.197 -    translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
   1.198 -and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) =
   1.199 +    translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts)
   1.200 +and translate_app thy algbr eqngr some_abs some_thm (c_ty_ts as ((c, _), _)) =
   1.201    case Code.get_case_scheme thy c
   1.202 -   of SOME case_scheme => translate_app_case thy algbr eqngr thm case_scheme c_ty_ts
   1.203 -    | NONE => translate_app_const thy algbr eqngr thm c_ty_ts
   1.204 +   of SOME case_scheme => translate_app_case thy algbr eqngr some_abs some_thm case_scheme c_ty_ts
   1.205 +    | NONE => translate_app_const thy algbr eqngr some_abs some_thm c_ty_ts
   1.206  and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
   1.207    fold_map (ensure_class thy algbr eqngr) (proj_sort sort)
   1.208    #>> (fn sort => (unprefix "'" v, sort))
   1.209 -and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr thm (ty, sort) =
   1.210 +and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr some_thm (ty, sort) =
   1.211    let
   1.212      datatype typarg =
   1.213          Global of (class * string) * typarg list list
   1.214 @@ -773,7 +776,7 @@
   1.215      val typargs = Sorts.of_sort_derivation algebra
   1.216        {class_relation = class_relation, type_constructor = type_constructor,
   1.217         type_variable = type_variable} (ty, proj_sort sort)
   1.218 -      handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
   1.219 +      handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
   1.220      fun mk_dict (Global (inst, yss)) =
   1.221            ensure_inst thy algbr eqngr inst
   1.222            ##>> (fold_map o fold_map) mk_dict yss
   1.223 @@ -824,9 +827,9 @@
   1.224      val stmt_value =
   1.225        fold_map (translate_tyvar_sort thy algbr eqngr) vs
   1.226        ##>> translate_typ thy algbr eqngr ty
   1.227 -      ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
   1.228 +      ##>> translate_term thy algbr eqngr NONE NONE (Code.subst_signatures thy t)
   1.229        #>> (fn ((vs, ty), t) => Fun
   1.230 -        (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
   1.231 +        (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
   1.232      fun term_value (dep, (naming, program1)) =
   1.233        let
   1.234          val Fun (_, (vs_ty, [(([], t), _)])) =