src/Tools/Code/code_thingol.ML
changeset 31888 626c075fd457
parent 31874 f172346ba805
child 31889 fb2c8a687529
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 16:43:27 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 16:43:28 2009 +0200
     1.3 @@ -25,11 +25,11 @@
     1.4        IConst of const
     1.5      | IVar of vname
     1.6      | `$ of iterm * iterm
     1.7 -    | `|=> of (vname * itype) * iterm
     1.8 +    | `|=> of (vname option * itype) * iterm
     1.9      | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    1.10          (*((term, type), [(selector pattern, body term )]), primitive term)*)
    1.11    val `$$ : iterm * iterm list -> iterm;
    1.12 -  val `|==> : (vname * itype) list * iterm -> iterm;
    1.13 +  val `|==> : (vname option * itype) list * iterm -> iterm;
    1.14    type typscheme = (vname * sort) list * itype;
    1.15  end;
    1.16  
    1.17 @@ -40,7 +40,7 @@
    1.18    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
    1.19    val unfold_fun: itype -> itype list * itype
    1.20    val unfold_app: iterm -> iterm * iterm list
    1.21 -  val unfold_abs: iterm -> (vname * itype) list * iterm
    1.22 +  val unfold_abs: iterm -> (vname option * itype) list * iterm
    1.23    val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
    1.24    val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
    1.25    val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option
    1.26 @@ -127,7 +127,7 @@
    1.27      IConst of const
    1.28    | IVar of vname
    1.29    | `$ of iterm * iterm
    1.30 -  | `|=> of (vname * itype) * iterm
    1.31 +  | `|=> of (vname option * itype) * iterm
    1.32    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    1.33      (*see also signature*)
    1.34  
    1.35 @@ -168,7 +168,7 @@
    1.36  fun fold_varnames f =
    1.37    let
    1.38      fun add (IVar v) = f v
    1.39 -      | add ((v, _) `|=> _) = f v
    1.40 +      | add ((SOME v, _) `|=> _) = f v
    1.41        | add _ = I;
    1.42    in fold_aiterms add end;
    1.43  
    1.44 @@ -177,19 +177,22 @@
    1.45      fun add _ (IConst _) = I
    1.46        | add vs (IVar v) = if not (member (op =) vs v) then f v else I
    1.47        | add vs (t1 `$ t2) = add vs t1 #> add vs t2
    1.48 -      | add vs ((v, _) `|=> t) = add (insert (op =) v vs) t
    1.49 -      | add vs (ICase (_, t)) = add vs t;
    1.50 +      | add vs ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
    1.51 +      | add vs ((NONE, _) `|=> t) = add vs t
    1.52 +      | add vs (ICase (((t, _), ds), _)) = add vs t #> fold (add_case vs) ds
    1.53 +    and add_case vs (p, t) = add (fold_varnames (insert (op =)) p vs) t;
    1.54    in add [] end;
    1.55  
    1.56  fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
    1.57  
    1.58 -val split_pat_abs = (fn (v, ty) `|=> t => (case t
    1.59 -   of ICase (((IVar w, _), [(p, t')]), _) =>
    1.60 -        if v = w andalso (exists_var p v orelse not (exists_var t' v))
    1.61 -        then SOME ((SOME p, ty), t')
    1.62 -        else SOME ((SOME (IVar v), ty), t)
    1.63 -    | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t))
    1.64 -  | _ => NONE);
    1.65 +fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((NONE, ty), t)
    1.66 +  | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
    1.67 +     of ICase (((IVar w, _), [(p, t')]), _) =>
    1.68 +          if v = w andalso (exists_var p v orelse not (exists_var t' v))
    1.69 +          then ((SOME p, ty), t')
    1.70 +          else ((SOME (IVar v), ty), t)
    1.71 +      | _ => ((SOME (IVar v), ty), t))
    1.72 +  | split_pat_abs _ = NONE;
    1.73  
    1.74  val unfold_pat_abs = unfoldr split_pat_abs;
    1.75  
    1.76 @@ -199,7 +202,7 @@
    1.77      val l = k - j;
    1.78      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
    1.79      val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
    1.80 -  in vs_tys `|==> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
    1.81 +  in (map o apfst) SOME vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
    1.82  
    1.83  fun contains_dictvar t =
    1.84    let
    1.85 @@ -573,10 +576,12 @@
    1.86    | translate_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
    1.87        let
    1.88          val (v, t) = Syntax.variant_abs abs;
    1.89 +        val v' = if member (op =) (Term.add_free_names t []) v
    1.90 +          then SOME v else NONE
    1.91        in
    1.92          translate_typ thy algbr funcgr ty
    1.93          ##>> translate_term thy algbr funcgr thm t
    1.94 -        #>> (fn (ty, t) => (v, ty) `|=> t)
    1.95 +        #>> (fn (ty, t) => (v', ty) `|=> t)
    1.96        end
    1.97    | translate_term thy algbr funcgr thm (t as _ $ _) =
    1.98        case strip_comb t
    1.99 @@ -631,11 +636,11 @@
   1.100        else map (uncurry mk_clause)
   1.101          (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
   1.102      fun retermify ty (_, (IVar x, body)) =
   1.103 -          (x, ty) `|=> body
   1.104 +          (SOME x, ty) `|=> body
   1.105        | retermify _ (_, (pat, body)) =
   1.106            let
   1.107              val (IConst (_, (_, tys)), ts) = unfold_app pat;
   1.108 -            val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
   1.109 +            val vs = map2 (fn IVar x => fn ty => (SOME x, ty)) ts tys;
   1.110            in vs `|==> body end;
   1.111      fun mk_icase const t ty clauses =
   1.112        let
   1.113 @@ -663,7 +668,7 @@
   1.114      in
   1.115        fold_map (translate_typ thy algbr funcgr) tys
   1.116        ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
   1.117 -      #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|==> t)
   1.118 +      #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
   1.119      end
   1.120    else if length ts > num_args then
   1.121      translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))