tuned;
authorwenzelm
Thu Jun 02 18:29:55 2005 +0200 (2005-06-02)
changeset 161950eb3c15298cd
parent 16194 3d192ab9907b
child 16196 abff174ba569
tuned;
src/Pure/General/url.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/General/url.ML	Thu Jun 02 18:29:54 2005 +0200
     1.2 +++ b/src/Pure/General/url.ML	Thu Jun 02 18:29:55 2005 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Basic URLs.  See RFC 1738.
     1.8 +Basic URLs, see RFC 1738.
     1.9  *)
    1.10  
    1.11  signature URL =
    1.12 @@ -52,22 +52,21 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
    1.17 +val scan_host =
    1.18 +  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
    1.19    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    1.20  
    1.21 -val scan_host1 = gen_host Scan.any1;
    1.22  val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
    1.23 -val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
    1.24 +val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
    1.25  
    1.26  val scan_url =
    1.27    Scan.unless (Scan.this_string "file:" ||
    1.28      Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    1.29    Scan.this_string "file:///" |-- scan_path_root >> File ||
    1.30    Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
    1.31 -  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
    1.32 -  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
    1.33 -  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
    1.34 -  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *)
    1.35 +  Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
    1.36 +  Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
    1.37 +  Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    1.38  
    1.39  in
    1.40  
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Jun 02 18:29:54 2005 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jun 02 18:29:55 2005 +0200
     2.3 @@ -64,9 +64,8 @@
     2.4    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     2.5    val load_thy: string -> bool -> bool -> Path.T -> unit
     2.6    val isar: bool -> bool -> unit Toplevel.isar
     2.7 -  val scan: string -> OuterLex.token list  
     2.8 -  val read: OuterLex.token list -> 
     2.9 -		(string * OuterLex.token list * Toplevel.transition) list
    2.10 +  val scan: string -> OuterLex.token list
    2.11 +  val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
    2.12  end;
    2.13  
    2.14  structure OuterSyntax : OUTER_SYNTAX  =
    2.15 @@ -268,13 +267,16 @@
    2.16    |> toplevel_source term false true get_parser;
    2.17  
    2.18  
    2.19 -(* scan text,  read tokens with trace (for Proof General) *)
    2.20 +(* scan text *)
    2.21  
    2.22  fun scan str =
    2.23 - Source.of_string str
    2.24 - |> Symbol.source false
    2.25 - |> T.source true get_lexicons Position.none
    2.26 - |> Source.exhaust
    2.27 +  Source.of_string str
    2.28 +  |> Symbol.source false
    2.29 +  |> T.source true get_lexicons Position.none
    2.30 +  |> Source.exhaust;
    2.31 +
    2.32 +
    2.33 +(* read tokens with trace *)
    2.34  
    2.35  fun read toks =
    2.36    Source.of_list toks
    2.37 @@ -283,6 +285,7 @@
    2.38    |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
    2.39  
    2.40  
    2.41 +
    2.42  (** read theory **)
    2.43  
    2.44  (* check_text *)
     3.1 --- a/src/Pure/Proof/extraction.ML	Thu Jun 02 18:29:54 2005 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Thu Jun 02 18:29:55 2005 +0200
     3.3 @@ -123,14 +123,10 @@
     3.4  
     3.5  val chtype = change_type o SOME;
     3.6  
     3.7 -fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
     3.8 +fun extr_name s vs = NameSpace.append "extr" (space_implode "_" (s :: vs));
     3.9 +fun corr_name s vs = extr_name s vs ^ "_correctness";
    3.10  
    3.11 -fun corr_name s vs =
    3.12 -  add_prefix "extr" (space_implode "_" (s :: vs)) ^ "_correctness";
    3.13 -
    3.14 -fun extr_name s vs = add_prefix "extr" (space_implode "_" (s :: vs));
    3.15 -
    3.16 -fun msg d s = priority (implode (replicate d " ") ^ s);
    3.17 +fun msg d s = priority (Symbol.spaces d ^ s);
    3.18  
    3.19  fun vars_of t = rev (foldl_aterms
    3.20    (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
    3.21 @@ -279,7 +275,7 @@
    3.22  val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
    3.23  
    3.24  fun thaw (T as TFree (a, S)) =
    3.25 -      if ":" mem explode a then TVar (unpack_ixn a, S) else T
    3.26 +      if exists_string (equal ":") a then TVar (unpack_ixn a, S) else T
    3.27    | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
    3.28    | thaw T = T;
    3.29  
     4.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Jun 02 18:29:54 2005 +0200
     4.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Jun 02 18:29:55 2005 +0200
     4.3 @@ -37,10 +37,10 @@
     4.4  
     4.5  (** constants for theorems and axioms **)
     4.6  
     4.7 -fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
     4.8 -
     4.9 -fun add_proof_atom_consts names sg = Sign.add_consts_i
    4.10 -  (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
    4.11 +fun add_proof_atom_consts names sg =
    4.12 +  sg
    4.13 +  |> Sign.add_path "//"
    4.14 +  |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
    4.15  
    4.16  (** constants for application and abstraction **)
    4.17  
    4.18 @@ -184,12 +184,12 @@
    4.19    [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
    4.20  
    4.21  fun term_of _ (PThm ((name, _), _, _, NONE)) =
    4.22 -      Const (add_prefix "thm" name, proofT)
    4.23 +      Const (NameSpace.append "thm" name, proofT)
    4.24    | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
    4.25 -      mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
    4.26 -  | term_of _ (PAxm (name, _, NONE)) = Const (add_prefix "axm" name, proofT)
    4.27 +      mk_tyapp (Const (NameSpace.append "thm" name, proofT), Ts)
    4.28 +  | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
    4.29    | term_of _ (PAxm (name, _, SOME Ts)) =
    4.30 -      mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
    4.31 +      mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
    4.32    | term_of _ (PBound i) = Bound i
    4.33    | term_of Ts (Abst (s, opT, prf)) = 
    4.34        let val T = getOpt (opT,dummyT)
    4.35 @@ -223,7 +223,7 @@
    4.36      val sg = sign_of thy |>
    4.37        add_proof_syntax |>
    4.38        add_proof_atom_consts
    4.39 -        (map (add_prefix "axm") axm_names @ map (add_prefix "thm") thm_names)
    4.40 +        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
    4.41    in
    4.42      (cterm_of sg (term_of_proof prf'),
    4.43       proof_of_term thy tab true o Thm.term_of)
    4.44 @@ -237,7 +237,7 @@
    4.45      val sg = sign_of thy |>
    4.46        add_proof_syntax |>
    4.47        add_proof_atom_consts
    4.48 -        (map (add_prefix "axm") axm_names @ map (add_prefix "thm") thm_names)
    4.49 +        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
    4.50    in
    4.51      (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
    4.52    end;
    4.53 @@ -255,7 +255,7 @@
    4.54      val sg' = sg |>
    4.55        add_proof_syntax |>
    4.56        add_proof_atom_consts
    4.57 -        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
    4.58 +        (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
    4.59    in
    4.60      Sign.pretty_term sg' (term_of_proof prf)
    4.61    end;
     5.1 --- a/src/Pure/type_infer.ML	Thu Jun 02 18:29:54 2005 +0200
     5.2 +++ b/src/Pure/type_infer.ML	Thu Jun 02 18:29:55 2005 +0200
     5.3 @@ -88,13 +88,13 @@
     5.4    | deref (Link (ref T)) = deref T
     5.5    | deref T = T;
     5.6  
     5.7 -fun foldl_pretyps f (x, PConst (_, T)) = f (x, T)
     5.8 -  | foldl_pretyps f (x, PFree (_, T)) = f (x, T)
     5.9 -  | foldl_pretyps f (x, PVar (_, T)) = f (x, T)
    5.10 -  | foldl_pretyps _ (x, PBound _) = x
    5.11 -  | foldl_pretyps f (x, PAbs (_, T, t)) = foldl_pretyps f (f (x, T), t)
    5.12 -  | foldl_pretyps f (x, PAppl (t, u)) = foldl_pretyps f (foldl_pretyps f (x, t), u)
    5.13 -  | foldl_pretyps f (x, Constraint (t, T)) = f (foldl_pretyps f (x, t), T);
    5.14 +fun fold_pretyps f (PConst (_, T)) x = f T x
    5.15 +  | fold_pretyps f (PFree (_, T)) x = f T x
    5.16 +  | fold_pretyps f (PVar (_, T)) x = f T x
    5.17 +  | fold_pretyps _ (PBound _) x = x
    5.18 +  | fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x)
    5.19 +  | fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x)
    5.20 +  | fold_pretyps f (Constraint (t, T)) x = f T (fold_pretyps f t x);
    5.21  
    5.22  
    5.23  
    5.24 @@ -110,16 +110,16 @@
    5.25  
    5.26  fun pretyp_of is_param (params, typ) =
    5.27    let
    5.28 -    fun add_parms (ps, TVar (xi as (x, _), S)) =
    5.29 -          if is_param xi andalso is_none (assoc (ps, xi))
    5.30 +    fun add_parms (TVar (xi as (x, _), S)) ps =
    5.31 +          if is_param xi andalso is_none (assoc_string_int (ps, xi))
    5.32            then (xi, mk_param S) :: ps else ps
    5.33 -      | add_parms (ps, TFree _) = ps
    5.34 -      | add_parms (ps, Type (_, Ts)) = Library.foldl add_parms (ps, Ts);
    5.35 +      | add_parms (TFree _) ps = ps
    5.36 +      | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
    5.37  
    5.38 -    val params' = add_parms (params, typ);
    5.39 +    val params' = add_parms typ params;
    5.40  
    5.41      fun pre_of (TVar (v as (xi, _))) =
    5.42 -          (case assoc (params', xi) of
    5.43 +          (case assoc_string_int (params', xi) of
    5.44              NONE => PTVar v
    5.45            | SOME p => p)
    5.46        | pre_of (TFree ("'_dummy_", S)) = mk_param S
    5.47 @@ -137,7 +137,7 @@
    5.48  fun preterm_of const_type is_param ((vparams, params), tm) =
    5.49    let
    5.50      fun add_vparm (ps, xi) =
    5.51 -      if is_none (assoc (ps, xi)) then
    5.52 +      if is_none (assoc_string_int (ps, xi)) then
    5.53          (xi, mk_param []) :: ps
    5.54        else ps;
    5.55  
    5.56 @@ -149,7 +149,7 @@
    5.57        | add_vparms (ps, _) = ps;
    5.58  
    5.59      val vparams' = add_vparms (vparams, tm);
    5.60 -    fun var_param xi = valOf (assoc (vparams', xi));
    5.61 +    fun var_param xi = the (assoc_string_int (vparams', xi));
    5.62  
    5.63  
    5.64      val preT_of = pretyp_of is_param;
    5.65 @@ -192,23 +192,23 @@
    5.66  
    5.67  (* add_parms *)
    5.68  
    5.69 -fun add_parmsT (rs, PType (_, Ts)) = Library.foldl add_parmsT (rs, Ts)
    5.70 -  | add_parmsT (rs, Link (r as ref (Param _))) = r ins rs
    5.71 -  | add_parmsT (rs, Link (ref T)) = add_parmsT (rs, T)
    5.72 -  | add_parmsT (rs, _) = rs;
    5.73 +fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs
    5.74 +  | add_parmsT (Link (r as ref (Param _))) rs = r ins rs
    5.75 +  | add_parmsT (Link (ref T)) rs = add_parmsT T rs
    5.76 +  | add_parmsT _ rs = rs;
    5.77  
    5.78 -val add_parms = foldl_pretyps add_parmsT;
    5.79 +val add_parms = fold_pretyps add_parmsT;
    5.80  
    5.81  
    5.82  (* add_names *)
    5.83  
    5.84 -fun add_namesT (xs, PType (_, Ts)) = Library.foldl add_namesT (xs, Ts)
    5.85 -  | add_namesT (xs, PTFree (x, _)) = x ins xs
    5.86 -  | add_namesT (xs, PTVar ((x, _), _)) = x ins xs
    5.87 -  | add_namesT (xs, Link (ref T)) = add_namesT (xs, T)
    5.88 -  | add_namesT (xs, Param _) = xs;
    5.89 +fun add_namesT (PType (_, Ts)) xs = fold add_namesT Ts xs
    5.90 +  | add_namesT (PTFree (x, _)) xs = x ins_string xs
    5.91 +  | add_namesT (PTVar ((x, _), _)) xs = x ins_string xs
    5.92 +  | add_namesT (Link (ref T)) xs = add_namesT T xs
    5.93 +  | add_namesT (Param _) xs = xs;
    5.94  
    5.95 -val add_names = foldl_pretyps add_namesT;
    5.96 +val add_names = fold_pretyps add_namesT;
    5.97  
    5.98  
    5.99  (* simple_typ/term_of *)
   5.100 @@ -237,11 +237,11 @@
   5.101      fun elim (r as ref (Param S), x) = r := mk_var (x, S)
   5.102        | elim _ = ();
   5.103  
   5.104 -    val used' = Library.foldl add_names (Library.foldl add_namesT (used, Ts), ts);
   5.105 -    val parms = rev (Library.foldl add_parms (Library.foldl add_parmsT ([], Ts), ts));
   5.106 +    val used' = fold add_names ts (fold add_namesT Ts used);
   5.107 +    val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
   5.108      val names = Term.invent_names used' (prfx ^ "'a") (length parms);
   5.109    in
   5.110 -    seq2 elim (parms, names);
   5.111 +    ListPair.app elim (parms, names);
   5.112      (map simple_typ_of Ts, map simple_term_of ts)
   5.113    end;
   5.114  
   5.115 @@ -269,7 +269,7 @@
   5.116            else r := mk_param (Sorts.inter_sort classes (S', S))
   5.117        | meet (Link (ref T), S) = meet (T, S)
   5.118        | meet (PType (a, Ts), S) =
   5.119 -          seq2 meet (Ts, Sorts.mg_domain (classes, arities) a S
   5.120 +          ListPair.app meet (Ts, Sorts.mg_domain (classes, arities) a S
   5.121              handle Sorts.DOMAIN ac => raise NO_UNIFIER (no_domain ac))
   5.122        | meet (PTFree (x, S'), S) =
   5.123            if Sorts.sort_le classes (S', S) then ()
   5.124 @@ -304,7 +304,7 @@
   5.125        | unif (PType (a, Ts), PType (b, Us)) =
   5.126            if a <> b then
   5.127              raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b)
   5.128 -          else seq2 unif (Ts, Us)
   5.129 +          else ListPair.app unif (Ts, Us)
   5.130        | unif (T, U) = if T = U then () else raise NO_UNIFIER "";
   5.131  
   5.132    in unif end;
   5.133 @@ -457,7 +457,7 @@
   5.134            ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
   5.135  
   5.136      fun get xi =
   5.137 -      (case (assoc (env, xi), def_sort xi) of
   5.138 +      (case (assoc_string_int (env, xi), def_sort xi) of
   5.139          (NONE, NONE) => Type.defaultS tsig
   5.140        | (NONE, SOME S) => S
   5.141        | (SOME S, NONE) => S
   5.142 @@ -472,8 +472,8 @@
   5.143  
   5.144  fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
   5.145    let
   5.146 -    fun get_type xi = getOpt (def_type xi, dummyT);
   5.147 -    fun is_free x = isSome (def_type (x, ~1));
   5.148 +    fun get_type xi = if_none (def_type xi) dummyT;
   5.149 +    fun is_free x = is_some (def_type (x, ~1));
   5.150      val raw_env = Syntax.raw_term_sorts tm;
   5.151      val sort_of = get_sort tsig def_sort map_sort raw_env;
   5.152  
   5.153 @@ -509,8 +509,8 @@
   5.154  
   5.155    tsig: type signature
   5.156    const_type: name mapping and signature lookup
   5.157 -  def_type: partial map from indexnames to types (constrains Frees, Vars)
   5.158 -  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   5.159 +  def_type: partial map from indexnames to types (constrains Frees and Vars)
   5.160 +  def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
   5.161    used: list of already used type variables
   5.162    freeze: if true then generated parameters are turned into TFrees, else TVars*)
   5.163  
   5.164 @@ -519,7 +519,7 @@
   5.165    let
   5.166      val {classes, arities, ...} = Type.rep_tsig tsig;
   5.167      val pat_Ts' = map (Type.cert_typ tsig) pat_Ts;
   5.168 -    val is_const = isSome o const_type;
   5.169 +    val is_const = is_some o const_type;
   5.170      val raw_ts' =
   5.171        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
   5.172      val (ts, Ts, unifier) = basic_infer_types pp const_type