src/Tools/Code/code_thingol.ML
changeset 48072 ace701efe203
parent 48003 1d11af40b106
child 48074 c6d514717d7b
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -18,19 +18,18 @@
     1.4        Dict of string list * plain_dict
     1.5    and plain_dict = 
     1.6        Dict_Const of string * dict list list
     1.7 -    | Dict_Var of vname * (int * int)
     1.8 +    | Dict_Var of vname * (int * int);
     1.9    datatype itype =
    1.10        `%% of string * itype list
    1.11      | ITyVar of vname;
    1.12 -  type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
    1.13 -    (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
    1.14 +  type const = { name: string, typargs: itype list, dicts: dict list list,
    1.15 +    dom: itype list, range: itype, annotate: bool };
    1.16    datatype iterm =
    1.17        IConst of const
    1.18      | IVar of vname option
    1.19      | `$ of iterm * iterm
    1.20      | `|=> of (vname option * itype) * iterm
    1.21 -    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    1.22 -        (*((term, type), [(selector pattern, body term )]), primitive term)*)
    1.23 +    | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
    1.24    val `$$ : iterm * iterm list -> iterm;
    1.25    val `|==> : (vname option * itype) list * iterm -> iterm;
    1.26    type typscheme = (vname * sort) list * itype;
    1.27 @@ -77,10 +76,10 @@
    1.28      | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.29      | Classrel of class * class
    1.30      | Classparam of string * class
    1.31 -    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
    1.32 -          * ((class * (string * (string * dict list list))) list (*super instances*)
    1.33 -        * (((string * const) * (thm * bool)) list (*class parameter instances*)
    1.34 -          * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
    1.35 +    | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
    1.36 +        superinsts: (class * (string * (string * dict list list))) list,
    1.37 +        inst_params: ((string * const) * (thm * bool)) list,
    1.38 +        superinst_params: ((string * const) * (thm * bool)) list };
    1.39    type program = stmt Graph.T
    1.40    val empty_funs: program -> string list
    1.41    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
    1.42 @@ -126,7 +125,7 @@
    1.43    case dest x
    1.44     of NONE => ([], x)
    1.45      | SOME (x1, x2) =>
    1.46 -        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
    1.47 +        let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
    1.48  
    1.49  
    1.50  (** language core - types, terms **)
    1.51 @@ -137,21 +136,21 @@
    1.52      Dict of string list * plain_dict
    1.53  and plain_dict = 
    1.54      Dict_Const of string * dict list list
    1.55 -  | Dict_Var of vname * (int * int)
    1.56 +  | Dict_Var of vname * (int * int);
    1.57  
    1.58  datatype itype =
    1.59      `%% of string * itype list
    1.60    | ITyVar of vname;
    1.61  
    1.62 -type const = string * (((itype list * dict list list) *
    1.63 -  (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
    1.64 +type const = { name: string, typargs: itype list, dicts: dict list list,
    1.65 +  dom: itype list, range: itype, annotate: bool };
    1.66  
    1.67  datatype iterm =
    1.68      IConst of const
    1.69    | IVar of vname option
    1.70    | `$ of iterm * iterm
    1.71    | `|=> of (vname option * itype) * iterm
    1.72 -  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    1.73 +  | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
    1.74      (*see also signature*)
    1.75  
    1.76  fun is_IVar (IVar _) = true
    1.77 @@ -172,7 +171,7 @@
    1.78      | _ => NONE);
    1.79  
    1.80  val split_let = 
    1.81 -  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
    1.82 +  (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
    1.83      | _ => NONE);
    1.84  
    1.85  val unfold_let = unfoldr split_let;
    1.86 @@ -188,16 +187,16 @@
    1.87        | fold' (IVar _) = I
    1.88        | fold' (t1 `$ t2) = fold' t1 #> fold' t2
    1.89        | fold' (_ `|=> t) = fold' t
    1.90 -      | fold' (ICase (((t, _), ds), _)) = fold' t
    1.91 -          #> fold (fn (pat, body) => fold' pat #> fold' body) ds
    1.92 +      | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
    1.93 +          #> fold (fn (p, body) => fold' p #> fold' body) clauses
    1.94    in fold' end;
    1.95  
    1.96 -val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
    1.97 +val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
    1.98  
    1.99  fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
   1.100    | add_tycos (ITyVar _) = I;
   1.101  
   1.102 -val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
   1.103 +val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
   1.104  
   1.105  fun fold_varnames f =
   1.106    let
   1.107 @@ -209,7 +208,7 @@
   1.108            | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
   1.109            | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
   1.110            | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
   1.111 -          | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
   1.112 +          | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_case vs) clauses
   1.113          and fold_case vs (p, t) = fold_term (add p vs) t;
   1.114        in fold_term [] end;
   1.115      fun add t = fold_aux add (insert (op =)) t;
   1.116 @@ -219,9 +218,9 @@
   1.117  
   1.118  fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
   1.119    | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
   1.120 -     of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
   1.121 -          if v = w andalso (exists_var p v orelse not (exists_var t' v))
   1.122 -          then ((p, ty), t')
   1.123 +     of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
   1.124 +          if v = w andalso (exists_var p v orelse not (exists_var body v))
   1.125 +          then ((p, ty), body)
   1.126            else ((IVar (SOME v), ty), t)
   1.127        | _ => ((IVar (SOME v), ty), t))
   1.128    | split_pat_abs _ = NONE;
   1.129 @@ -239,27 +238,27 @@
   1.130          val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
   1.131        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
   1.132  
   1.133 -fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
   1.134 +fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
   1.135    let
   1.136      val j = length ts;
   1.137      val l = k - j;
   1.138      val _ = if l > length tys
   1.139 -      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
   1.140 +      then error ("Impossible eta-expansion for constant " ^ quote c) else ();
   1.141      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
   1.142      val vs_tys = (map o apfst) SOME
   1.143        (Name.invent_names ctxt "a" ((take l o drop j) tys));
   1.144 -  in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
   1.145 +  in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
   1.146  
   1.147  fun contains_dict_var t =
   1.148    let
   1.149      fun cont_dict (Dict (_, d)) = cont_plain_dict d
   1.150      and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
   1.151        | cont_plain_dict (Dict_Var _) = true;
   1.152 -    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
   1.153 +    fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
   1.154        | cont_term (IVar _) = false
   1.155        | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
   1.156        | cont_term (_ `|=> t) = cont_term t
   1.157 -      | cont_term (ICase (_, t)) = cont_term t;
   1.158 +      | cont_term (ICase { primitive = t, ... }) = cont_term t;
   1.159    in cont_term t end;
   1.160  
   1.161  
   1.162 @@ -427,11 +426,10 @@
   1.163    | Class of class * (vname * ((class * string) list * (string * itype) list))
   1.164    | Classrel of class * class
   1.165    | Classparam of string * class
   1.166 -  | Classinst of (class * (string * (vname * sort) list))
   1.167 -        * ((class * (string * (string * dict list list))) list
   1.168 -      * (((string * const) * (thm * bool)) list
   1.169 -        * ((string * const) * (thm * bool)) list))
   1.170 -      (*see also signature*);
   1.171 +  | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
   1.172 +      superinsts: (class * (string * (string * dict list list))) list,
   1.173 +      inst_params: ((string * const) * (thm * bool)) list,
   1.174 +      superinst_params: ((string * const) * (thm * bool)) list };
   1.175  
   1.176  type program = stmt Graph.T;
   1.177  
   1.178 @@ -444,9 +442,10 @@
   1.179        (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
   1.180    | map_terms_bottom_up f ((v, ty) `|=> t) = f
   1.181        ((v, ty) `|=> map_terms_bottom_up f t)
   1.182 -  | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
   1.183 -      (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
   1.184 -        (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
   1.185 +  | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
   1.186 +      (ICase { term = map_terms_bottom_up f t, typ = ty,
   1.187 +        clauses = (map o pairself) (map_terms_bottom_up f) clauses,
   1.188 +        primitive = map_terms_bottom_up f t0 });
   1.189  
   1.190  fun map_classparam_instances_as_term f =
   1.191    (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
   1.192 @@ -459,8 +458,11 @@
   1.193    | map_terms_stmt f (stmt as Class _) = stmt
   1.194    | map_terms_stmt f (stmt as Classrel _) = stmt
   1.195    | map_terms_stmt f (stmt as Classparam _) = stmt
   1.196 -  | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
   1.197 -      Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
   1.198 +  | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
   1.199 +      inst_params, superinst_params }) =
   1.200 +        Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
   1.201 +          inst_params = map_classparam_instances_as_term f inst_params,
   1.202 +          superinst_params = map_classparam_instances_as_term f superinst_params };
   1.203  
   1.204  fun is_cons program name = case Graph.get_node program name
   1.205   of Datatypecons _ => true
   1.206 @@ -484,7 +486,7 @@
   1.207            quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
   1.208          end
   1.209      | Classparam (c, _) => quote (Code.string_of_const thy c)
   1.210 -    | Classinst ((class, (tyco, _)), _) =>
   1.211 +    | Classinst { class, tyco, ... } =>
   1.212          let
   1.213            val Class (class, _) = Graph.get_node program class;
   1.214            val Datatype (tyco, _) = Graph.get_node program tyco;
   1.215 @@ -678,9 +680,9 @@
   1.216  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
   1.217    let
   1.218      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   1.219 -    val these_classparams = these o try (#params o AxClass.get_info thy);
   1.220 -    val classparams = these_classparams class;
   1.221 -    val further_classparams = maps these_classparams
   1.222 +    val these_class_params = these o try (#params o AxClass.get_info thy);
   1.223 +    val class_params = these_class_params class;
   1.224 +    val superclass_params = maps these_class_params
   1.225        ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
   1.226      val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   1.227      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   1.228 @@ -710,12 +712,11 @@
   1.229        ##>> ensure_tyco thy algbr eqngr permissive tyco
   1.230        ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
   1.231        ##>> fold_map translate_super_instance super_classes
   1.232 -      ##>> fold_map translate_classparam_instance classparams
   1.233 -      ##>> fold_map translate_classparam_instance further_classparams
   1.234 -      #>> (fn (((((class, tyco), arity_args), super_instances),
   1.235 -        classparam_instances), further_classparam_instances) =>
   1.236 -          Classinst ((class, (tyco, arity_args)), (super_instances,
   1.237 -            (classparam_instances, further_classparam_instances))));
   1.238 +      ##>> fold_map translate_classparam_instance class_params
   1.239 +      ##>> fold_map translate_classparam_instance superclass_params
   1.240 +      #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
   1.241 +          Classinst { class = class, tyco = tyco, vs = vs,
   1.242 +            superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
   1.243    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
   1.244  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
   1.245        pair (ITyVar (unprefix "'" v))
   1.246 @@ -759,17 +760,18 @@
   1.247          then translation_error thy permissive some_thm
   1.248            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
   1.249        else ()
   1.250 -    val (annotate, ty') = dest_tagged_type ty
   1.251 -    val arg_typs = Sign.const_typargs thy (c, ty');
   1.252 +    val (annotate, ty') = dest_tagged_type ty;
   1.253 +    val typargs = Sign.const_typargs thy (c, ty');
   1.254      val sorts = Code_Preproc.sortargs eqngr c;
   1.255 -    val (function_typs, body_typ) = Term.strip_type ty';
   1.256 +    val (dom, range) = Term.strip_type ty';
   1.257    in
   1.258      ensure_const thy algbr eqngr permissive c
   1.259 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
   1.260 -    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
   1.261 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
   1.262 -    #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
   1.263 -      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
   1.264 +    ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
   1.265 +    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
   1.266 +    ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
   1.267 +    #>> (fn (((c, typargs), dss), range :: dom) =>
   1.268 +      IConst { name = c, typargs = typargs, dicts = dss,
   1.269 +        dom = dom, range = range, annotate = annotate })
   1.270    end
   1.271  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   1.272    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
   1.273 @@ -788,22 +790,22 @@
   1.274      val constrs =
   1.275        if null case_pats then []
   1.276        else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
   1.277 -    fun casify naming constrs ty ts =
   1.278 +    fun casify naming constrs ty t_app ts =
   1.279        let
   1.280          val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
   1.281          fun collapse_clause vs_map ts body =
   1.282            let
   1.283            in case body
   1.284 -           of IConst (c, _) => if member (op =) undefineds c
   1.285 +           of IConst { name = c, ... } => if member (op =) undefineds c
   1.286                  then []
   1.287                  else [(ts, body)]
   1.288 -            | ICase (((IVar (SOME v), _), subclauses), _) =>
   1.289 +            | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
   1.290                  if forall (fn (pat', body') => exists_var pat' v
   1.291 -                  orelse not (exists_var body' v)) subclauses
   1.292 +                  orelse not (exists_var body' v)) clauses
   1.293                  then case AList.lookup (op =) vs_map v
   1.294                   of SOME i => maps (fn (pat', body') =>
   1.295                        collapse_clause (AList.delete (op =) v vs_map)
   1.296 -                        (nth_map i (K pat') ts) body') subclauses
   1.297 +                        (nth_map i (K pat') ts) body') clauses
   1.298                    | NONE => [(ts, body)]
   1.299                  else [(ts, body)]
   1.300              | _ => [(ts, body)]
   1.301 @@ -818,11 +820,11 @@
   1.302          val ts_clause = nth_drop t_pos ts;
   1.303          val clauses = if null case_pats
   1.304            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
   1.305 -          else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
   1.306 +          else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
   1.307              mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
   1.308                (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
   1.309                  (case_pats ~~ ts_clause)));
   1.310 -      in ((t, ty), clauses) end;
   1.311 +      in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
   1.312    in
   1.313      translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
   1.314      ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
   1.315 @@ -830,7 +832,7 @@
   1.316      ##>> translate_typ thy algbr eqngr permissive ty
   1.317      ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
   1.318      #-> (fn (((t, constrs), ty), ts) =>
   1.319 -      `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
   1.320 +      `(fn (_, (naming, _)) => casify naming constrs ty t ts))
   1.321    end
   1.322  and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
   1.323    if length ts < num_args then