src/Tools/Code/code_thingol.ML
changeset 31935 3896169e6ff9
parent 31892 a2139b503981
child 31957 a9742afd403e
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Jul 03 16:51:07 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Jul 03 16:51:07 2009 +0200
     1.3 @@ -49,9 +49,8 @@
     1.4    val eta_expand: int -> const * iterm list -> iterm
     1.5    val contains_dictvar: iterm -> bool
     1.6    val locally_monomorphic: iterm -> bool
     1.7 -  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
     1.8 +  val add_constnames: iterm -> string list -> string list
     1.9    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
    1.10 -  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
    1.11  
    1.12    type naming
    1.13    val empty_naming: naming
    1.14 @@ -153,38 +152,30 @@
    1.15    of (IConst c, ts) => SOME (c, ts)
    1.16     | _ => NONE;
    1.17  
    1.18 -fun fold_aiterms f (t as IConst _) = f t
    1.19 -  | fold_aiterms f (t as IVar _) = f t
    1.20 -  | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
    1.21 -  | fold_aiterms f (t as _ `|=> t') = f t #> fold_aiterms f t'
    1.22 -  | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
    1.23 -
    1.24 -fun fold_constnames f =
    1.25 -  let
    1.26 -    fun add (IConst (c, _)) = f c
    1.27 -      | add _ = I;
    1.28 -  in fold_aiterms add end;
    1.29 +fun add_constnames (IConst (c, _)) = insert (op =) c
    1.30 +  | add_constnames (IVar _) = I
    1.31 +  | add_constnames (t1 `$ t2) = add_constnames t1 #> add_constnames t2
    1.32 +  | add_constnames (_ `|=> t) = add_constnames t
    1.33 +  | add_constnames (ICase (((t, _), ds), _)) = add_constnames t
    1.34 +      #> fold (fn (pat, body) => add_constnames pat #> add_constnames body) ds;
    1.35  
    1.36  fun fold_varnames f =
    1.37    let
    1.38 -    fun add (IVar (SOME v)) = f v
    1.39 -      | add ((SOME v, _) `|=> _) = f v
    1.40 -      | add _ = I;
    1.41 -  in fold_aiterms add end;
    1.42 +    fun fold_aux add f =
    1.43 +      let
    1.44 +        fun fold_term _ (IConst _) = I
    1.45 +          | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
    1.46 +          | fold_term _ (IVar NONE) = I
    1.47 +          | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
    1.48 +          | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
    1.49 +          | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
    1.50 +          | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
    1.51 +        and fold_case vs (p, t) = fold_term (add p vs) t;
    1.52 +      in fold_term [] end;
    1.53 +    fun add t = fold_aux add (insert (op =)) t;
    1.54 +  in fold_aux add f end;
    1.55  
    1.56 -fun fold_unbound_varnames f =
    1.57 -  let
    1.58 -    fun add _ (IConst _) = I
    1.59 -      | add vs (IVar (SOME v)) = if not (member (op =) vs v) then f v else I
    1.60 -      | add _ (IVar NONE) = I
    1.61 -      | add vs (t1 `$ t2) = add vs t1 #> add vs t2
    1.62 -      | add vs ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
    1.63 -      | add vs ((NONE, _) `|=> t) = add vs t
    1.64 -      | add vs (ICase (((t, _), ds), _)) = add vs t #> fold (add_case vs) ds
    1.65 -    and add_case vs (p, t) = add (fold_varnames (insert (op =)) p vs) t;
    1.66 -  in add [] end;
    1.67 -
    1.68 -fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
    1.69 +fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
    1.70  
    1.71  fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
    1.72    | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
    1.73 @@ -219,12 +210,14 @@
    1.74  
    1.75  fun contains_dictvar t =
    1.76    let
    1.77 -    fun contains (DictConst (_, dss)) = (fold o fold) contains dss
    1.78 -      | contains (DictVar _) = K true;
    1.79 -  in
    1.80 -    fold_aiterms
    1.81 -      (fn IConst (_, ((_, dss), _)) => (fold o fold) contains dss | _ => I) t false
    1.82 -  end;
    1.83 +    fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss
    1.84 +      | cont_dict (DictVar _) = true;
    1.85 +    fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
    1.86 +      | cont_term (IVar _) = false
    1.87 +      | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
    1.88 +      | cont_term (_ `|=> t) = cont_term t
    1.89 +      | cont_term (ICase (_, t)) = cont_term t;
    1.90 +  in cont_term t end;
    1.91    
    1.92  fun locally_monomorphic (IConst _) = false
    1.93    | locally_monomorphic (IVar _) = true
    1.94 @@ -640,20 +633,37 @@
    1.95        else map2 mk_constr case_pats (nth_drop t_pos ts);
    1.96      fun casify naming constrs ty ts =
    1.97        let
    1.98 +        val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
    1.99 +        fun collapse_clause vs_map ts body =
   1.100 +          let
   1.101 +          in case body
   1.102 +           of IConst (c, _) => if member (op =) undefineds c
   1.103 +                then []
   1.104 +                else [(ts, body)]
   1.105 +            | ICase (((IVar (SOME v), _), subclauses), _) =>
   1.106 +                if forall (fn (pat', body') => exists_var pat' v
   1.107 +                  orelse not (exists_var body' v)) subclauses
   1.108 +                then case AList.lookup (op =) vs_map v
   1.109 +                 of SOME i => maps (fn (pat', body') =>
   1.110 +                      collapse_clause (AList.delete (op =) v vs_map)
   1.111 +                        (nth_map i (K pat') ts) body') subclauses
   1.112 +                  | NONE => [(ts, body)]
   1.113 +                else [(ts, body)]
   1.114 +            | _ => [(ts, body)]
   1.115 +          end;
   1.116 +        fun mk_clause mk tys t =
   1.117 +          let
   1.118 +            val (vs, body) = unfold_abs_eta tys t;
   1.119 +            val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
   1.120 +            val ts = map (IVar o fst) vs;
   1.121 +          in map mk (collapse_clause vs_map ts body) end;
   1.122          val t = nth ts t_pos;
   1.123          val ts_clause = nth_drop t_pos ts;
   1.124 -        val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
   1.125 -        fun mk_clause ((constr as IConst (_, (_, tys)), n), t) =
   1.126 -          let
   1.127 -            val (vs, t') = unfold_abs_eta (curry Library.take n tys) t;
   1.128 -            val is_undefined = case t
   1.129 -             of IConst (c, _) => member (op =) undefineds c
   1.130 -              | _ => false;
   1.131 -          in if is_undefined then NONE else SOME (constr `$$ map (IVar o fst) vs, t') end;
   1.132 -        val clauses = if null case_pats then let val ([(v, _)], t) =
   1.133 -            unfold_abs_eta [ty] (the_single ts_clause)
   1.134 -          in [(IVar v, t)] end
   1.135 -          else map_filter mk_clause (constrs ~~ ts_clause);
   1.136 +        val clauses = if null case_pats
   1.137 +          then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
   1.138 +          else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
   1.139 +            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t)
   1.140 +              (constrs ~~ ts_clause);
   1.141        in ((t, ty), clauses) end;
   1.142    in
   1.143      translate_const thy algbr funcgr thm c_ty