an intermediate step towards a refined translation of cases
authorhaftmann
Tue Jun 30 18:23:50 2009 +0200 (2009-06-30)
changeset 31890e943b039f0ac
parent 31889 fb2c8a687529
child 31891 3404c8cb9e14
an intermediate step towards a refined translation of cases
src/Pure/Isar/code.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 30 17:33:30 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 30 18:23:50 2009 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    val these_eqns: theory -> string -> (thm * bool) list
     1.5    val all_eqns: theory -> (thm * bool) list
     1.6    val get_case_scheme: theory -> string -> (int * (int * string list)) option
     1.7 -  val is_undefined: theory -> string -> bool
     1.8 +  val undefineds: theory -> string list
     1.9    val print_codesetup: theory -> unit
    1.10  end;
    1.11  
    1.12 @@ -898,7 +898,7 @@
    1.13  
    1.14  fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
    1.15  
    1.16 -val is_undefined = Symtab.defined o snd o the_cases o the_exec;
    1.17 +val undefineds = Symtab.keys o snd o the_cases o the_exec;
    1.18  
    1.19  structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
    1.20  
     2.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 17:33:30 2009 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 18:23:50 2009 +0200
     2.3 @@ -197,6 +197,17 @@
     2.4  
     2.5  val unfold_pat_abs = unfoldr split_pat_abs;
     2.6  
     2.7 +fun unfold_abs_eta [] t = ([], t)
     2.8 +  | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
     2.9 +      let
    2.10 +        val (vs_tys, t') = unfold_abs_eta tys t;
    2.11 +      in (v_ty :: vs_tys, t') end
    2.12 +  | unfold_abs_eta (_ :: tys) t =
    2.13 +      let
    2.14 +        val ctxt = fold_varnames Name.declare t Name.context;
    2.15 +        val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
    2.16 +      in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
    2.17 +
    2.18  fun eta_expand k (c as (_, (_, tys)), ts) =
    2.19    let
    2.20      val j = length ts;
    2.21 @@ -624,11 +635,12 @@
    2.22      val t = nth ts t_pos;
    2.23      val ty = nth tys t_pos;
    2.24      val ts_clause = nth_drop t_pos ts;
    2.25 +    val undefineds = Code.undefineds thy;
    2.26      fun mk_clause (co, num_co_args) t =
    2.27        let
    2.28          val (vs, body) = Term.strip_abs_eta num_co_args t;
    2.29          val not_undefined = case body
    2.30 -         of (Const (c, _)) => not (Code.is_undefined thy c)
    2.31 +         of (Const (c, _)) => not (member (op =) undefineds c)
    2.32            | _ => true;
    2.33          val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
    2.34        in (not_undefined, (pat, body)) end;
    2.35 @@ -661,36 +673,42 @@
    2.36      #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
    2.37    end
    2.38  
    2.39 -(*and translate_case' thy algbr funcgr thm case_scheme (c_ty, ts) =
    2.40 +(*and translate_case' thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
    2.41    let
    2.42 -    fun casify ts tys =
    2.43 +    fun casify naming ts tys =
    2.44        let
    2.45          val t = nth ts t_pos;
    2.46          val ty = nth tys t_pos;
    2.47          val ts_clause = nth_drop t_pos ts;
    2.48 -        fun strip_abs_eta t [] = t
    2.49 -          | strip_abs_eta ((`|=>
    2.50 +        val tyss_clause = map (fst o unfold_fun) (nth_drop t_pos tys);
    2.51 +
    2.52 +        val undefineds = map_filter (lookup_const naming) (*Code.undefineds thy*) [];
    2.53  
    2.54 -        fun mk_clause (co, num_co_args) t =
    2.55 +        fun mk_clause co (tys, t) =
    2.56            let
    2.57 -            val (vs, body) = Term.strip_abs_eta num_co_args t;
    2.58 +            val (vs, t') = unfold_abs_eta tys t;
    2.59 +            val is_undefined = case t
    2.60 +             of Const (c, _) => member (op =) undefineds c
    2.61 +              | _ => false;
    2.62 +          in if is_undefined then NONE else (_, t) end;
    2.63 +
    2.64              val not_undefined = case body
    2.65               of (Const (c, _)) => not (Code.is_undefined thy c)
    2.66                | _ => true;
    2.67              val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
    2.68            in (not_undefined, (pat, body)) end;
    2.69  
    2.70 -        val clauses = if null case_pats then let val ([v_ty], body) =
    2.71 -            Term.strip_abs_eta 1 (the_single ts_clause)
    2.72 -          in [(true, (Free v_ty, body))] end
    2.73 -          else map (uncurry mk_clause)
    2.74 -            (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
    2.75 +        val clauses = if null case_pats then let val ([(v, _)], t) =
    2.76 +            unfold_abs_eta (the_single tyss_clause) (the_single ts_clause) 
    2.77 +          in [(IVar v, t)] end
    2.78 +          else map2 mk_clause case_pats (tyss_clause ~~ ts_clause);
    2.79  
    2.80        in ((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses) end;
    2.81    in
    2.82      translate_const thy algbr funcgr thm c_ty
    2.83      ##>> fold_map (translate_term thy algbr funcgr thm) ts
    2.84 -    #>> (fn (t as IConst (c, (_, tys)), ts) => ICase (casify ts tys, t `$$ ts))
    2.85 +    #-> (fn (t as IConst (c, (_, tys)), ts) =>
    2.86 +      `(fn (naming, _) => pair (ICase (casify naming ts tys, t `$$ ts))))
    2.87    end*)
    2.88  
    2.89  and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =