src/Pure/sign.ML
changeset 22696 00fc658c4fe5
parent 22683 0e9a65ddfe9d
child 22709 9ab51bac6287
     1.1 --- a/src/Pure/sign.ML	Sun Apr 15 14:31:53 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 15 14:31:54 2007 +0200
     1.3 @@ -170,14 +170,9 @@
     1.4    val read_typ_abbrev: theory -> string -> typ
     1.5    val read_tyname: theory -> string -> typ
     1.6    val read_const: theory -> string -> term
     1.7 -  val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
     1.8 -    (indexname -> sort option) -> Name.context -> bool
     1.9 -    -> (term list * typ) list -> term list * (indexname * typ) list
    1.10 -  val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
    1.11 -    (indexname -> sort option) -> Name.context -> bool
    1.12 -    -> term list * typ -> term * (indexname * typ) list
    1.13    val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
    1.14 -    Proof.context -> (indexname -> typ option) * (indexname -> sort option) ->
    1.15 +    (string -> string option) -> Proof.context ->
    1.16 +    (indexname -> typ option) * (indexname -> sort option) ->
    1.17      Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
    1.18    val read_def_terms:
    1.19      theory * (indexname -> typ option) * (indexname -> sort option) ->
    1.20 @@ -194,7 +189,6 @@
    1.21  structure Sign: SIGN =
    1.22  struct
    1.23  
    1.24 -
    1.25  (** datatype sign **)
    1.26  
    1.27  datatype sign = Sign of
    1.28 @@ -512,7 +506,7 @@
    1.29    let
    1.30      val thy = ProofContext.theory_of ctxt;
    1.31      val _ = Context.check_thy thy;
    1.32 -    val S = intern_sort thy (Syntax.read_sort ctxt syn str);
    1.33 +    val S = Syntax.read_sort ctxt syn (intern_sort thy) str;
    1.34    in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
    1.35  
    1.36  fun read_sort thy str = read_sort' (syn_of thy) (ProofContext.init thy) str;
    1.37 @@ -530,14 +524,34 @@
    1.38  
    1.39  (* types *)
    1.40  
    1.41 +fun get_sort tsig def_sort raw_env =
    1.42 +  let
    1.43 +    fun eq ((xi, S), (xi', S')) =
    1.44 +      Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
    1.45 +    val env = distinct eq raw_env;
    1.46 +    val _ = (case duplicates (eq_fst (op =)) env of [] => ()
    1.47 +      | dups => error ("Inconsistent sort constraints for type variable(s) "
    1.48 +          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
    1.49 +
    1.50 +    fun get xi =
    1.51 +      (case (AList.lookup (op =) env xi, def_sort xi) of
    1.52 +        (NONE, NONE) => Type.defaultS tsig
    1.53 +      | (NONE, SOME S) => S
    1.54 +      | (SOME S, NONE) => S
    1.55 +      | (SOME S, SOME S') =>
    1.56 +          if Type.eq_sort tsig (S, S') then S'
    1.57 +          else error ("Sort constraint inconsistent with default for type variable " ^
    1.58 +            quote (Term.string_of_vname' xi)));
    1.59 +  in get end;
    1.60 +
    1.61  local
    1.62  
    1.63  fun gen_read_typ' cert syn ctxt def_sort str =
    1.64    let
    1.65      val thy = ProofContext.theory_of ctxt;
    1.66      val _ = Context.check_thy thy;
    1.67 -    val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
    1.68 -    val T = intern_tycons thy (Syntax.read_typ ctxt syn get_sort (intern_sort thy) str);
    1.69 +    val T = intern_tycons thy
    1.70 +      (Syntax.read_typ ctxt syn (get_sort (tsig_of thy) def_sort) (intern_sort thy) str);
    1.71    in cert thy T handle TYPE (msg, _, _) => error msg end
    1.72    handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
    1.73  
    1.74 @@ -570,27 +584,40 @@
    1.75  
    1.76  
    1.77  
    1.78 -(** infer_types **)         (*exception ERROR*)
    1.79 +(* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
    1.80  
    1.81  (*
    1.82    def_type: partial map from indexnames to types (constrains Frees and Vars)
    1.83    def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
    1.84    used: context of already used type variables
    1.85    freeze: if true then generated parameters are turned into TFrees, else TVars
    1.86 -
    1.87 -  termss: lists of alternative parses (only one combination should be type-correct)
    1.88 -  typs: expected types
    1.89  *)
    1.90  
    1.91 -fun infer_types_simult pp thy consts def_type def_sort used freeze args =
    1.92 +fun read_def_terms' pp is_logtype syn consts fixed ctxt (def_type, def_sort) used freeze sTs =
    1.93    let
    1.94 +    val thy = ProofContext.theory_of ctxt;
    1.95 +    val tsig = tsig_of thy;
    1.96 +
    1.97 +    (*read terms -- potentially ambiguous*)
    1.98 +    val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
    1.99 +    fun map_free x =
   1.100 +      (case fixed x of
   1.101 +        NONE => if is_some (def_type (x, ~1)) then SOME x else NONE
   1.102 +      | some => some);
   1.103 +    val read =
   1.104 +      Syntax.read_term (get_sort tsig def_sort) map_const map_free
   1.105 +        (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn;
   1.106 +
   1.107 +    val args = sTs |> map (fn (s, raw_T) =>
   1.108 +      let val T = certify_typ thy raw_T handle TYPE (msg, _, _) => error msg
   1.109 +      in (read T s, T) end);
   1.110 +
   1.111 +    (*brute-force disambiguation via type-inference*)
   1.112      val termss = fold_rev (multiply o fst) args [[]];
   1.113 -    val typs =
   1.114 -      map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   1.115 +    val typs = map snd args;
   1.116  
   1.117 -    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   1.118 -        (try (Consts.the_constraint consts)) def_type def_sort (Consts.intern consts)
   1.119 -        (intern_tycons thy) (intern_sort thy) used freeze typs ts)
   1.120 +    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) tsig
   1.121 +        (try (Consts.the_constraint consts)) def_type used freeze (ts ~~ typs) |>> map fst)
   1.122        handle TYPE (msg, _, _) => Exn (ERROR msg);
   1.123  
   1.124      val err_results = map infer termss;
   1.125 @@ -604,37 +631,23 @@
   1.126          \Retry with smaller Syntax.ambiguity_level for more information."
   1.127        else "";
   1.128    in
   1.129 -    if null results then (cat_error (ambig_msg ()) (cat_lines errs))
   1.130 +    if null results then cat_error (ambig_msg ()) (cat_lines errs)
   1.131      else if length results = 1 then
   1.132        (if ambiguity > ! Syntax.ambiguity_level then
   1.133          warning "Fortunately, only one parse tree is type correct.\n\
   1.134            \You may still want to disambiguate your grammar or your input."
   1.135        else (); hd results)
   1.136 -    else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
   1.137 -      cat_lines (map (Pretty.string_of_term pp) (maps fst results))))
   1.138 +    else cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
   1.139 +      cat_lines (map (Pretty.string_of_term pp) (maps fst results)))
   1.140    end;
   1.141  
   1.142 -fun infer_types pp thy consts def_type def_sort used freeze tsT =
   1.143 -  apfst hd (infer_types_simult pp thy consts def_type def_sort used freeze [tsT]);
   1.144 -
   1.145 -
   1.146 -(* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
   1.147 -
   1.148 -fun read_def_terms' pp is_logtype syn consts ctxt (types, sorts) used freeze sTs =
   1.149 -  let
   1.150 -    val thy = ProofContext.theory_of ctxt;
   1.151 -    fun read (s, T) =
   1.152 -      let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
   1.153 -      in (Syntax.read ctxt is_logtype syn T' s, T') end;
   1.154 -  in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
   1.155 -
   1.156  fun read_def_terms (thy, types, sorts) used freeze sTs =
   1.157    let
   1.158      val pp = pp thy;
   1.159      val consts = consts_of thy;
   1.160      val cert_consts = Consts.certify pp (tsig_of thy) consts;
   1.161      val (ts, inst) =
   1.162 -      read_def_terms' pp (is_logtype thy) (syn_of thy) consts
   1.163 +      read_def_terms' pp (is_logtype thy) (syn_of thy) consts (K NONE)
   1.164          (ProofContext.init thy) (types, sorts) (Name.make_context used) freeze sTs;
   1.165    in (map cert_consts ts, inst) end;
   1.166