src/Tools/Code/code_thingol.ML
changeset 31890 e943b039f0ac
parent 31889 fb2c8a687529
child 31892 a2139b503981
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 17:33:30 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 18:23:50 2009 +0200
     1.3 @@ -197,6 +197,17 @@
     1.4  
     1.5  val unfold_pat_abs = unfoldr split_pat_abs;
     1.6  
     1.7 +fun unfold_abs_eta [] t = ([], t)
     1.8 +  | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
     1.9 +      let
    1.10 +        val (vs_tys, t') = unfold_abs_eta tys t;
    1.11 +      in (v_ty :: vs_tys, t') end
    1.12 +  | unfold_abs_eta (_ :: tys) t =
    1.13 +      let
    1.14 +        val ctxt = fold_varnames Name.declare t Name.context;
    1.15 +        val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
    1.16 +      in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
    1.17 +
    1.18  fun eta_expand k (c as (_, (_, tys)), ts) =
    1.19    let
    1.20      val j = length ts;
    1.21 @@ -624,11 +635,12 @@
    1.22      val t = nth ts t_pos;
    1.23      val ty = nth tys t_pos;
    1.24      val ts_clause = nth_drop t_pos ts;
    1.25 +    val undefineds = Code.undefineds thy;
    1.26      fun mk_clause (co, num_co_args) t =
    1.27        let
    1.28          val (vs, body) = Term.strip_abs_eta num_co_args t;
    1.29          val not_undefined = case body
    1.30 -         of (Const (c, _)) => not (Code.is_undefined thy c)
    1.31 +         of (Const (c, _)) => not (member (op =) undefineds c)
    1.32            | _ => true;
    1.33          val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
    1.34        in (not_undefined, (pat, body)) end;
    1.35 @@ -661,36 +673,42 @@
    1.36      #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
    1.37    end
    1.38  
    1.39 -(*and translate_case' thy algbr funcgr thm case_scheme (c_ty, ts) =
    1.40 +(*and translate_case' thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
    1.41    let
    1.42 -    fun casify ts tys =
    1.43 +    fun casify naming ts tys =
    1.44        let
    1.45          val t = nth ts t_pos;
    1.46          val ty = nth tys t_pos;
    1.47          val ts_clause = nth_drop t_pos ts;
    1.48 -        fun strip_abs_eta t [] = t
    1.49 -          | strip_abs_eta ((`|=>
    1.50 +        val tyss_clause = map (fst o unfold_fun) (nth_drop t_pos tys);
    1.51 +
    1.52 +        val undefineds = map_filter (lookup_const naming) (*Code.undefineds thy*) [];
    1.53  
    1.54 -        fun mk_clause (co, num_co_args) t =
    1.55 +        fun mk_clause co (tys, t) =
    1.56            let
    1.57 -            val (vs, body) = Term.strip_abs_eta num_co_args t;
    1.58 +            val (vs, t') = unfold_abs_eta tys t;
    1.59 +            val is_undefined = case t
    1.60 +             of Const (c, _) => member (op =) undefineds c
    1.61 +              | _ => false;
    1.62 +          in if is_undefined then NONE else (_, t) end;
    1.63 +
    1.64              val not_undefined = case body
    1.65               of (Const (c, _)) => not (Code.is_undefined thy c)
    1.66                | _ => true;
    1.67              val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
    1.68            in (not_undefined, (pat, body)) end;
    1.69  
    1.70 -        val clauses = if null case_pats then let val ([v_ty], body) =
    1.71 -            Term.strip_abs_eta 1 (the_single ts_clause)
    1.72 -          in [(true, (Free v_ty, body))] end
    1.73 -          else map (uncurry mk_clause)
    1.74 -            (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
    1.75 +        val clauses = if null case_pats then let val ([(v, _)], t) =
    1.76 +            unfold_abs_eta (the_single tyss_clause) (the_single ts_clause) 
    1.77 +          in [(IVar v, t)] end
    1.78 +          else map2 mk_clause case_pats (tyss_clause ~~ ts_clause);
    1.79  
    1.80        in ((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses) end;
    1.81    in
    1.82      translate_const thy algbr funcgr thm c_ty
    1.83      ##>> fold_map (translate_term thy algbr funcgr thm) ts
    1.84 -    #>> (fn (t as IConst (c, (_, tys)), ts) => ICase (casify ts tys, t `$$ ts))
    1.85 +    #-> (fn (t as IConst (c, (_, tys)), ts) =>
    1.86 +      `(fn (naming, _) => pair (ICase (casify naming ts tys, t `$$ ts))))
    1.87    end*)
    1.88  
    1.89  and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =