fixed OCaml bug
authorhaftmann
Wed Aug 15 08:57:45 2007 +0200 (2007-08-15)
changeset 24284f5afd33f5d02
parent 24283 8ca96f4e49cd
child 24285 066bb557570f
fixed OCaml bug
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_target.ML	Wed Aug 15 08:57:42 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Wed Aug 15 08:57:45 2007 +0200
     1.3 @@ -36,8 +36,8 @@
     1.4    val assert_serializer: theory -> string -> string;
     1.5  
     1.6    val eval_verbose: bool ref;
     1.7 -  val eval_term: theory -> (theory -> string -> string) -> CodeThingol.code
     1.8 -    -> (string * 'a option ref) * CodeThingol.iterm -> string list -> 'a;
     1.9 +  val eval_term: theory -> (string * 'a option ref) -> CodeThingol.code
    1.10 +    ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.11    val code_width: int ref;
    1.12  
    1.13    val setup: theory -> theory;
    1.14 @@ -189,7 +189,7 @@
    1.15      val vars' = CodeName.intro_vars (the_list v) vars;
    1.16      val vars'' = CodeName.intro_vars vs vars';
    1.17      val v' = Option.map (CodeName.lookup_var vars') v;
    1.18 -    val pat' = Option.map (pr_term vars'' fxy) pat;
    1.19 +    val pat' = Option.map (pr_term true vars'' fxy) pat;
    1.20    in (pr_bind' ((v', pat'), ty), vars'') end;
    1.21  
    1.22  
    1.23 @@ -383,7 +383,7 @@
    1.24        | pr_bind' ((SOME v, NONE), _) = str v
    1.25        | pr_bind' ((NONE, SOME p), _) = p
    1.26        | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
    1.27 -    and pr_bind fxy = gen_pr_bind pr_bind' (pr_term false) fxy
    1.28 +    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
    1.29      and pr_case vars fxy (cases as ((_, [_]), _)) =
    1.30            let
    1.31              val (binds, t') = CodeThingol.unfold_let (ICase cases);
    1.32 @@ -448,7 +448,6 @@
    1.33                      concat (
    1.34                        [str definer, (str o deresolv) name]
    1.35                        @ (if null ts andalso null vs
    1.36 -                           andalso not (ty = ITyVar "_")(*for evaluation*)
    1.37                           then [str ":", pr_typ NOBR ty]
    1.38                           else
    1.39                             pr_tyvars vs
    1.40 @@ -653,7 +652,7 @@
    1.41        | pr_bind' ((SOME v, NONE), _) = str v
    1.42        | pr_bind' ((NONE, SOME p), _) = p
    1.43        | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
    1.44 -    and pr_bind fxy = gen_pr_bind pr_bind' (pr_term false) fxy
    1.45 +    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
    1.46      and pr_case vars fxy (cases as ((_, [_]), _)) =
    1.47            let
    1.48              val (binds, t') = CodeThingol.unfold_let (ICase cases);
    1.49 @@ -687,12 +686,11 @@
    1.50                | fillup_parm x (i, NONE) = x ^ string_of_int i;
    1.51              fun fish_parms vars eqs =
    1.52                let
    1.53 -                val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
    1.54 -                val x = Name.variant (map_filter I fished1) "x";
    1.55 -                val fished2 = map_index (fillup_parm x) fished1;
    1.56 -                val fished3 = fold_rev (fn x => fn xs => Name.variant xs x :: xs) fished2 [];
    1.57 -                val vars' = CodeName.intro_vars fished3 vars;
    1.58 -              in map (CodeName.lookup_var vars') fished3 end;
    1.59 +                val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
    1.60 +                val x = Name.variant (map_filter I raw_fished) "x";
    1.61 +                val fished = map_index (fillup_parm x) raw_fished;
    1.62 +                val vars' = CodeName.intro_vars fished vars;
    1.63 +              in map (CodeName.lookup_var vars') fished end;
    1.64              fun pr_eq (ts, t) =
    1.65                let
    1.66                  val consts = map_filter
    1.67 @@ -1146,7 +1144,7 @@
    1.68      and pr_app' lhs vars ((c, _), ts) =
    1.69        (str o deresolv) c :: map (pr_term lhs vars BR) ts
    1.70      and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
    1.71 -    and pr_bind fxy = pr_bind_haskell (pr_term false) fxy
    1.72 +    and pr_bind fxy = pr_bind_haskell pr_term fxy
    1.73      and pr_case vars fxy (cases as ((_, [_]), _)) =
    1.74            let
    1.75              val (binds, t) = CodeThingol.unfold_let (ICase cases);
    1.76 @@ -1302,7 +1300,7 @@
    1.77    let
    1.78      fun pretty pr vars fxy [(t, _)] =
    1.79        let
    1.80 -        val pr_bind = pr_bind_haskell pr;
    1.81 +        val pr_bind = pr_bind_haskell (K pr);
    1.82          fun pr_mbind (NONE, t) vars =
    1.83                (semicolon [pr vars NOBR t], vars)
    1.84            | pr_mbind (SOME (bind, true), t) vars = vars
    1.85 @@ -1618,12 +1616,12 @@
    1.86        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
    1.87    end;
    1.88  
    1.89 -fun eval_term thy labelled_name code ((ref_name, reff), t) args =
    1.90 +fun eval_term thy (ref_name, reff) code (t, ty) args =
    1.91    let
    1.92      val val_name = "Isabelle_Eval.EVAL.EVAL";
    1.93      val val_name' = "Isabelle_Eval.EVAL";
    1.94      val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
    1.95 -    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name;
    1.96 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] CodeName.labelled_name;
    1.97      fun eval code = (
    1.98        reff := NONE;
    1.99        seri (SOME [val_name]) code;
   1.100 @@ -1636,7 +1634,7 @@
   1.101        );
   1.102    in
   1.103      code
   1.104 -    |> CodeThingol.add_eval_def (val_name, t)
   1.105 +    |> CodeThingol.add_eval_def (val_name, (t, ty))
   1.106      |> eval
   1.107    end;
   1.108