Type inference for elements through syntax module.
authorballarin
Wed Nov 19 17:04:29 2008 +0100 (2008-11-19)
changeset 288525ddea758679b
parent 28851 368aca388dd9
child 28853 69eb69659bf3
Type inference for elements through syntax module.
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Nov 19 17:03:13 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Nov 19 17:04:29 2008 +0100
     1.3 @@ -312,26 +312,61 @@
     1.4  
     1.5  (*** Locale processing ***)
     1.6  
     1.7 -(** Prepare locale elements **)
     1.8 +(** Parsing **)
     1.9 +
    1.10 +fun parse_elem prep_typ prep_term ctxt elem =
    1.11 +  Element.map_ctxt {name = I, var = I, typ = prep_typ ctxt,
    1.12 +    term = prep_term ctxt, fact = I, attrib = I} elem;
    1.13 +
    1.14 +fun parse_concl prep_term ctxt concl =
    1.15 +  (map o map) (fn (t, ps) =>
    1.16 +    (prep_term ctxt, map (prep_term ctxt) ps)) concl;
    1.17 +
    1.18 +
    1.19 +(** Type checking **)
    1.20 +
    1.21 +fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map (Logic.mk_type #> rpair [])) fixes
    1.22 +  | extract_elem (Constrains csts) = map (#2 #> single #> map (Logic.mk_type #> rpair [])) csts
    1.23 +  | extract_elem (Assumes asms) = map #2 asms
    1.24 +  | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [(t, ps)]) defs
    1.25 +  | extract_elem (Notes _) = [];
    1.26  
    1.27 -local
    1.28 +fun restore_elem (Fixes fixes, propps) =
    1.29 +      (fixes ~~ propps) |> map (fn ((x, _, mx), propp) =>
    1.30 +        (x, propp |> map (fst #> Logic.dest_type) |> try hd, mx)) |> Fixes
    1.31 +  | restore_elem (Constrains csts, propps) =
    1.32 +      (csts ~~ propps) |> map (fn ((x, _), propp) =>
    1.33 +        (x, propp |> map (fst #> Logic.dest_type) |> hd)) |> Constrains
    1.34 +  | restore_elem (Assumes asms, propps) =
    1.35 +      (asms ~~ propps) |> map (fn ((b, _), propp) => (b, propp)) |> Assumes
    1.36 +  | restore_elem (Defines defs, propps) =
    1.37 +      (defs ~~ propps) |> map (fn ((b, _), [propp]) => (b, propp)) |> Defines
    1.38 +  | restore_elem (Notes notes, _) = Notes notes;
    1.39 +
    1.40 +fun check_autofix_elems elems concl ctxt =
    1.41 +  let
    1.42 +    val termss = elems |> map extract_elem;
    1.43 +    val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ flat termss); 
    1.44 +(*    val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *)
    1.45 +val _ = "check" |> warning;
    1.46 +val _ = PolyML.makestring all_terms' |> warning;
    1.47 +    val (concl', terms') = chop (length concl) all_terms';
    1.48 +    val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) terms' ctxt;
    1.49 +  in (terms' |> unflat termss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end;
    1.50 +
    1.51 +
    1.52 +(** Prepare locale elements **)
    1.53  
    1.54  fun declare_elem prep_vars (Fixes fixes) ctxt =
    1.55        let val (vars, _) = prep_vars fixes ctxt
    1.56 -      in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
    1.57 +      in ctxt |> ProofContext.add_fixes_i vars |> snd end
    1.58    | declare_elem prep_vars (Constrains csts) ctxt =
    1.59 -      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
    1.60 -      in ([], ctxt') end
    1.61 -  | declare_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
    1.62 -  | declare_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
    1.63 -  | declare_elem _ (Notes _) ctxt = ([], ctxt);
    1.64 +      ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd
    1.65 +  | declare_elem _ (Assumes asms) ctxt = ctxt
    1.66 +  | declare_elem _ (Defines defs) ctxt = ctxt
    1.67 +  | declare_elem _ (Notes _) ctxt = ctxt;
    1.68  
    1.69 -in
    1.70 -
    1.71 -fun declare_elems prep_vars raw_elems ctxt =
    1.72 -  fold_map (declare_elem prep_vars) raw_elems ctxt;
    1.73 -
    1.74 -end;
    1.75 +(** Finish locale elements, extract specification text **)
    1.76  
    1.77  local
    1.78  
    1.79 @@ -367,18 +402,18 @@
    1.80        (spec, fold (bind_def ctxt o #1 o #2) defs binds)
    1.81    | eval_text _ (Notes _) text = text;
    1.82  
    1.83 -fun closeup _ false elem = elem
    1.84 -  | closeup ctxt true elem =
    1.85 +fun closeup _ _ false elem = elem
    1.86 +  | closeup ctxt parms true elem =
    1.87        let
    1.88          fun close_frees t =
    1.89            let
    1.90              val rev_frees =
    1.91                Term.fold_aterms (fn Free (x, T) =>
    1.92 -                if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
    1.93 +                if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
    1.94            in Term.list_all_free (rev rev_frees, t) end;
    1.95  
    1.96          fun no_binds [] = []
    1.97 -          | no_binds _ = error "Illegal term bindings in locale element";
    1.98 +          | no_binds _ = error "Illegal term bindings in context element";
    1.99        in
   1.100          (case elem of
   1.101            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   1.102 @@ -388,19 +423,17 @@
   1.103          | e => e)
   1.104        end;
   1.105  
   1.106 -fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
   1.107 +fun finish_ext_elem parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   1.108        let val x = Name.name_of binding
   1.109        in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   1.110 -  | finish_ext_elem _ _ (Constrains _, _) = Constrains []
   1.111 -  | finish_ext_elem _ close (Assumes asms, propp) =
   1.112 -      close (Assumes (map #1 asms ~~ propp))
   1.113 -  | finish_ext_elem _ close (Defines defs, propp) =
   1.114 -      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
   1.115 -  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
   1.116 +  | finish_ext_elem _ _ (Constrains _) = Constrains []
   1.117 +  | finish_ext_elem _ close (Assumes asms) = close (Assumes asms)
   1.118 +  | finish_ext_elem _ close (Defines defs) = close (Defines defs)
   1.119 +  | finish_ext_elem _ _ (Notes facts) = Notes facts;
   1.120  
   1.121 -fun finish_elem ctxt parms do_close (elem, propp) text =
   1.122 +fun finish_elem ctxt parms do_close elem text =
   1.123    let
   1.124 -    val elem' = finish_ext_elem parms (closeup ctxt do_close) (elem, propp);
   1.125 +    val elem' = finish_ext_elem parms (closeup ctxt parms do_close) elem;
   1.126      val text' = eval_text ctxt elem' text;
   1.127    in (elem', text') end
   1.128    
   1.129 @@ -414,62 +447,40 @@
   1.130  
   1.131  local
   1.132  
   1.133 -fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   1.134 +(* nice, but for now not needed
   1.135 +fun fold_suffixes f [] y = f [] y
   1.136 +  | fold_suffixes f (x :: xs) y = f (x :: xs) (f xs y);
   1.137  
   1.138 -fun frozen_tvars ctxt Ts =
   1.139 -  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
   1.140 -  |> map (fn ((xi, S), T) => (xi, (S, T)));
   1.141 -
   1.142 -fun unify_frozen ctxt maxidx Ts Us =
   1.143 -  let
   1.144 -    fun paramify NONE i = (NONE, i)
   1.145 -      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
   1.146 +fun fold_prefixes f xs y = fold_suffixes (f o rev) (rev xs) y;
   1.147 +*)
   1.148  
   1.149 -    val (Ts', maxidx') = fold_map paramify Ts maxidx;
   1.150 -    val (Us', maxidx'') = fold_map paramify Us maxidx';
   1.151 -    val thy = ProofContext.theory_of ctxt;
   1.152 -
   1.153 -    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
   1.154 -          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   1.155 -      | unify _ env = env;
   1.156 -    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   1.157 -    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   1.158 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   1.159 -  in map (Option.map (Envir.norm_type unifier')) Vs end;
   1.160 -
   1.161 -fun prep_elems prep_vars prepp do_close context raw_elems raw_concl =
   1.162 +fun prep_elems parse_typ parse_prop prep_vars do_close context raw_elems raw_concl =
   1.163    let
   1.164 -    val (raw_propps, raw_ctxt) = declare_elems prep_vars raw_elems context;
   1.165 -      (* raw_ctxt is context enriched by syntax from raw_elems *)
   1.166 +    fun prep_elem raw_elem (elems, ctxt) =
   1.167 +      let
   1.168 +        val ctxt' = declare_elem prep_vars raw_elem ctxt;
   1.169 +        val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
   1.170 +        (* FIXME term bindings *)
   1.171 +        val (_, _, ctxt'') = check_autofix_elems elems' [] ctxt';
   1.172 +      in (elems', ctxt'') end;
   1.173  
   1.174 -    fun prep_prop raw_propp (raw_ctxt, raw_concl) =
   1.175 +    fun prep_concl raw_concl (elems, ctxt) =
   1.176        let
   1.177 -        (* process patterns (conclusion and external elements) *)
   1.178 -        val (ctxt, all_propp) = prepp (raw_ctxt, raw_concl @ raw_propp);
   1.179 -        (* add type information from conclusion and external elements to context *)
   1.180 -        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
   1.181 -        (* resolve schematic variables (patterns) in conclusion and external elements. *)
   1.182 -        val all_propp' = map2 (curry (op ~~))
   1.183 -          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
   1.184 -        val (concl, propp) = chop (length raw_concl) all_propp';
   1.185 -      in (propp, (ctxt, concl)) end
   1.186 +        val concl = (map o map) (fn (t, ps) =>
   1.187 +          (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl;
   1.188 +      in check_autofix_elems elems concl ctxt end;
   1.189  
   1.190 -    val (propps, (ctxt, concl)) = fold_burrow prep_prop raw_propps (raw_ctxt, raw_concl);
   1.191 +    val (elems, concl, ctxt) = fold prep_elem raw_elems ([], context) |>
   1.192 +      prep_concl raw_concl;
   1.193  
   1.194 -    (* Infer parameter types *) 
   1.195 +    (* Retrieve parameter types *) 
   1.196      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   1.197 -      _ => fn ps => ps) raw_elems [];
   1.198 -    val typing = unify_frozen ctxt 0
   1.199 -      (map (Variable.default_type raw_ctxt) xs)
   1.200 -      (map (Variable.default_type ctxt) xs);
   1.201 -    val parms = param_types (xs ~~ typing);
   1.202 +      _ => fn ps => ps) elems [];
   1.203 +    val (Ts, _) = fold_map ProofContext.inferred_param xs ctxt; 
   1.204 +    val parms = xs ~~ Ts;
   1.205  
   1.206 -    (* CB: extract information from assumes and defines elements
   1.207 -       (fixes, constrains and notes in raw_elemss don't have an effect on
   1.208 -       text and elemss), compute final form of context elements. *)
   1.209 -   val (elems, text) = finish_elems ctxt parms do_close
   1.210 -      (raw_elems ~~ propps) ((([], []), ([], [])), ([], [], []));
   1.211 -    (* CB: text has the following structure:
   1.212 +    val (elems', text) = finish_elems ctxt parms do_close elems ((([], []), ([], [])), ([], [], []));
   1.213 +    (* text has the following structure:
   1.214             (((exts, exts'), (ints, ints')), (xs, env, defs))
   1.215         where
   1.216           exts: external assumptions (terms in external assumes elements)
   1.217 @@ -489,12 +500,13 @@
   1.218             from proppss in Assumes and Defines
   1.219           - Facts unchanged
   1.220         *)
   1.221 -   in ((parms, elems, concl), text) end
   1.222 +
   1.223 +  in ((parms, elems', concl), text) end
   1.224  
   1.225  in
   1.226  
   1.227 -fun read_elems x = prep_elems ProofContext.read_vars ProofContext.read_propp_schematic x;
   1.228 -fun cert_elems x = prep_elems ProofContext.cert_vars ProofContext.cert_propp_schematic x;
   1.229 +fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars x;
   1.230 +fun cert_elems x = prep_elems (K I) (K I) ProofContext.cert_vars x;
   1.231  
   1.232  end;
   1.233  
   1.234 @@ -536,10 +548,9 @@
   1.235  
   1.236  fun read_context imprt body ctxt =
   1.237    #1 (prep_context_statement intern_expr read_elems true imprt body [] ctxt);
   1.238 -(*
   1.239  fun cert_context imprt body ctxt =
   1.240    #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt);
   1.241 -*)
   1.242 +
   1.243  end;
   1.244  
   1.245