src/Tools/Code/code_thingol.ML
changeset 31892 a2139b503981
parent 31890 e943b039f0ac
child 31935 3896169e6ff9
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 18:24:03 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 19:31:50 2009 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4        let
     1.5          val (vs_tys, t') = unfold_abs_eta tys t;
     1.6        in (v_ty :: vs_tys, t') end
     1.7 -  | unfold_abs_eta (_ :: tys) t =
     1.8 +  | unfold_abs_eta tys t =
     1.9        let
    1.10          val ctxt = fold_varnames Name.declare t Name.context;
    1.11          val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
    1.12 @@ -631,86 +631,38 @@
    1.13    #>> (fn (t, ts) => t `$$ ts)
    1.14  and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
    1.15    let
    1.16 -    val (tys, _) = (chop num_args o fst o strip_type o snd) c_ty;
    1.17 -    val t = nth ts t_pos;
    1.18 +    fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
    1.19 +    val tys = arg_types num_args (snd c_ty);
    1.20      val ty = nth tys t_pos;
    1.21 -    val ts_clause = nth_drop t_pos ts;
    1.22 -    val undefineds = Code.undefineds thy;
    1.23 -    fun mk_clause (co, num_co_args) t =
    1.24 +    fun mk_constr c t = let val n = Code.no_args thy c
    1.25 +      in ((c, arg_types (Code.no_args thy c) (fastype_of t) ---> ty), n) end;
    1.26 +    val constrs = if null case_pats then []
    1.27 +      else map2 mk_constr case_pats (nth_drop t_pos ts);
    1.28 +    fun casify naming constrs ty ts =
    1.29        let
    1.30 -        val (vs, body) = Term.strip_abs_eta num_co_args t;
    1.31 -        val not_undefined = case body
    1.32 -         of (Const (c, _)) => not (member (op =) undefineds c)
    1.33 -          | _ => true;
    1.34 -        val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
    1.35 -      in (not_undefined, (pat, body)) end;
    1.36 -    val clauses = if null case_pats then let val ([v_ty], body) =
    1.37 -        Term.strip_abs_eta 1 (the_single ts_clause)
    1.38 -      in [(true, (Free v_ty, body))] end
    1.39 -      else map (uncurry mk_clause)
    1.40 -        (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
    1.41 -    fun retermify ty (_, (IVar v, body)) =
    1.42 -          (v, ty) `|=> body
    1.43 -      | retermify _ (_, (pat, body)) =
    1.44 +        val t = nth ts t_pos;
    1.45 +        val ts_clause = nth_drop t_pos ts;
    1.46 +        val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
    1.47 +        fun mk_clause ((constr as IConst (_, (_, tys)), n), t) =
    1.48            let
    1.49 -            val (IConst (_, (_, tys)), ts) = unfold_app pat;
    1.50 -            val vs = map2 (fn IVar v => fn ty => (v, ty)) ts tys;
    1.51 -          in vs `|==> body end;
    1.52 -    fun mk_icase const t ty clauses =
    1.53 -      let
    1.54 -        val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
    1.55 -      in
    1.56 -        ICase (((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses),
    1.57 -          const `$$ (ts1 @ t :: ts2))
    1.58 -      end;
    1.59 +            val (vs, t') = unfold_abs_eta (curry Library.take n tys) t;
    1.60 +            val is_undefined = case t
    1.61 +             of IConst (c, _) => member (op =) undefineds c
    1.62 +              | _ => false;
    1.63 +          in if is_undefined then NONE else SOME (constr `$$ map (IVar o fst) vs, t') end;
    1.64 +        val clauses = if null case_pats then let val ([(v, _)], t) =
    1.65 +            unfold_abs_eta [ty] (the_single ts_clause)
    1.66 +          in [(IVar v, t)] end
    1.67 +          else map_filter mk_clause (constrs ~~ ts_clause);
    1.68 +      in ((t, ty), clauses) end;
    1.69    in
    1.70      translate_const thy algbr funcgr thm c_ty
    1.71 -    ##>> translate_term thy algbr funcgr thm t
    1.72 +    ##>> fold_map (fn (constr, n) => translate_const thy algbr funcgr thm constr #>> rpair n) constrs
    1.73      ##>> translate_typ thy algbr funcgr ty
    1.74 -    ##>> fold_map (fn (b, (pat, body)) => translate_term thy algbr funcgr thm pat
    1.75 -      ##>> translate_term thy algbr funcgr thm body
    1.76 -      #>> pair b) clauses
    1.77 -    #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
    1.78 +    ##>> fold_map (translate_term thy algbr funcgr thm) ts
    1.79 +    #-> (fn (((t, constrs), ty), ts) =>
    1.80 +      `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
    1.81    end
    1.82 -
    1.83 -(*and translate_case' thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
    1.84 -  let
    1.85 -    fun casify naming ts tys =
    1.86 -      let
    1.87 -        val t = nth ts t_pos;
    1.88 -        val ty = nth tys t_pos;
    1.89 -        val ts_clause = nth_drop t_pos ts;
    1.90 -        val tyss_clause = map (fst o unfold_fun) (nth_drop t_pos tys);
    1.91 -
    1.92 -        val undefineds = map_filter (lookup_const naming) (*Code.undefineds thy*) [];
    1.93 -
    1.94 -        fun mk_clause co (tys, t) =
    1.95 -          let
    1.96 -            val (vs, t') = unfold_abs_eta tys t;
    1.97 -            val is_undefined = case t
    1.98 -             of Const (c, _) => member (op =) undefineds c
    1.99 -              | _ => false;
   1.100 -          in if is_undefined then NONE else (_, t) end;
   1.101 -
   1.102 -            val not_undefined = case body
   1.103 -             of (Const (c, _)) => not (Code.is_undefined thy c)
   1.104 -              | _ => true;
   1.105 -            val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
   1.106 -          in (not_undefined, (pat, body)) end;
   1.107 -
   1.108 -        val clauses = if null case_pats then let val ([(v, _)], t) =
   1.109 -            unfold_abs_eta (the_single tyss_clause) (the_single ts_clause) 
   1.110 -          in [(IVar v, t)] end
   1.111 -          else map2 mk_clause case_pats (tyss_clause ~~ ts_clause);
   1.112 -
   1.113 -      in ((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses) end;
   1.114 -  in
   1.115 -    translate_const thy algbr funcgr thm c_ty
   1.116 -    ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.117 -    #-> (fn (t as IConst (c, (_, tys)), ts) =>
   1.118 -      `(fn (naming, _) => pair (ICase (casify naming ts tys, t `$$ ts))))
   1.119 -  end*)
   1.120 -
   1.121  and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   1.122    if length ts < num_args then
   1.123      let