src/Pure/Isar/expression.ML
changeset 28697 140bfb63f893
child 28701 ca5840b1f7b3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Oct 27 16:23:54 2008 +0100
     1.3 @@ -0,0 +1,233 @@
     1.4 +(*  Title:      Pure/Isar/expression.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Clemens Ballarin, TU Muenchen
     1.7 +
     1.8 +Locale expressions --- experimental.
     1.9 +*)
    1.10 +
    1.11 +signature EXPRESSION =
    1.12 +sig
    1.13 +
    1.14 +type map
    1.15 +type 'morph expr
    1.16 +
    1.17 +type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    1.18 +type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    1.19 +
    1.20 +val parse_expr: OuterParse.token list -> expression * OuterParse.token list
    1.21 +val debug_parameters: expression -> Proof.context -> Proof.context
    1.22 +val debug_context: expression -> Proof.context -> Proof.context
    1.23 +
    1.24 +end;
    1.25 +
    1.26 +
    1.27 +structure Expression: EXPRESSION =
    1.28 +struct
    1.29 +
    1.30 +(* Locale expressions *)
    1.31 +
    1.32 +datatype map =
    1.33 +  Positional of string option list |
    1.34 +  Named of (string * string) list;
    1.35 +
    1.36 +datatype 'morph expr = Expr of (string * 'morph) list;
    1.37 +
    1.38 +type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
    1.39 +type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
    1.40 +
    1.41 +
    1.42 +(** Parsing and printing **)
    1.43 +
    1.44 +local
    1.45 +
    1.46 +structure P = OuterParse;
    1.47 +
    1.48 +val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    1.49 +   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
    1.50 +fun plus1_unless test scan =
    1.51 +  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    1.52 +
    1.53 +val prefix = P.name --| P.$$$ ":";
    1.54 +val named = P.name -- (P.$$$ "=" |-- P.term);
    1.55 +val position = P.maybe P.term;
    1.56 +val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    1.57 +  Scan.repeat1 position >> Positional;
    1.58 +
    1.59 +in
    1.60 +
    1.61 +val parse_expr =
    1.62 +  let
    1.63 +    fun expr2 x = P.xname x;
    1.64 +    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    1.65 +      Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    1.66 +    fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
    1.67 +  in expr0 -- P.for_fixes end;
    1.68 +
    1.69 +end;
    1.70 +
    1.71 +(*
    1.72 +fun pretty_expr thy (Locale loc) =
    1.73 +      [Pretty.str "Locale", Pretty.brk 1, Pretty.str (Locale.extern thy loc)]
    1.74 +  | pretty_expr thy (Instance (expr, (prfx, Positional insts))) =
    1.75 +      let
    1.76 +        val insts' = (* chop trailing NONEs *)
    1.77 +      
    1.78 +  | pretty_expr thy (Instance (expr, (prfx, Named insts))) =
    1.79 +*)
    1.80 +
    1.81 +
    1.82 +(** Processing of locale expression **)
    1.83 +
    1.84 +fun intern thy (Expr instances) = Expr (map (apfst (Locale.intern thy)) instances);
    1.85 +
    1.86 +
    1.87 +(* Parameters of expression (not expression_i).
    1.88 +   Sanity check of instantiations.
    1.89 +   Positional instantiations are extended to match full length of parameter list. *)
    1.90 +
    1.91 +fun parameters thy (expr, fixed) =
    1.92 +  let
    1.93 +    fun reject_dups message xs =
    1.94 +      let val dups = duplicates (op =) xs
    1.95 +      in
    1.96 +        if null dups then () else error (message ^ commas dups)
    1.97 +      end;
    1.98 +
    1.99 +    fun params2 loc =
   1.100 +          (Locale.parameters_of thy loc |> map (fn ((p, _), mx) => (p, mx)), loc) ;
   1.101 +    fun params1 (loc, (prfx, Positional insts)) =
   1.102 +          let
   1.103 +            val (ps, loc') = params2 loc;
   1.104 +	    val d = length ps - length insts;
   1.105 +	    val insts' =
   1.106 +	      if d < 0 then error ("More arguments than parameters in instantiation.")
   1.107 +(* FIXME print expr *)
   1.108 +	      else insts @ replicate d NONE;
   1.109 +            val ps' = (ps ~~ insts') |>
   1.110 +              map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
   1.111 +          in
   1.112 +            (ps', (loc', (prfx, Positional insts')))
   1.113 +          end
   1.114 +      | params1 (loc, (prfx, Named insts)) =
   1.115 +          let
   1.116 +            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   1.117 +              (map fst insts);
   1.118 +(* FIXME print expr *)
   1.119 +
   1.120 +            val (ps, loc') = params2 loc;
   1.121 +            val ps' = fold (fn (p, _) => fn ps =>
   1.122 +              if AList.defined (op =) ps p then AList.delete (op =) p ps
   1.123 +              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
   1.124 +(* FIXME print expr *)
   1.125 +(* FIXME AList lacks a version of delete that signals the absence of the deleted item *)
   1.126 +          in
   1.127 +            (ps', (loc', (prfx, Named insts)))
   1.128 +          end;
   1.129 +    fun params0 (Expr is) =
   1.130 +          let
   1.131 +            val (is', ps') = fold_map (fn i => fn ps =>
   1.132 +              let
   1.133 +                val (ps', i') = params1 i;
   1.134 +                val ps'' = AList.join (op =) (fn p => fn (mx1, mx2) =>
   1.135 +                  if mx1 = mx2 then mx1
   1.136 +                  else error ("Conflicting syntax for parameter" ^ quote p ^ " in expression.")) (ps, ps')
   1.137 +(* FIXME print Expr is *)
   1.138 +              in (i', ps'') end) is []
   1.139 +          in
   1.140 +            (ps', Expr is')
   1.141 +          end;
   1.142 +
   1.143 +    val (parms, expr') = params0 expr;
   1.144 +
   1.145 +    val parms' = map fst parms;
   1.146 +    val fixed' = map (#1 #> Name.name_of) fixed;
   1.147 +    val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   1.148 +    val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
   1.149 +
   1.150 +  in (expr', (parms, fixed)) end;
   1.151 +
   1.152 +fun debug_parameters raw_expr ctxt =
   1.153 +  let
   1.154 +    val thy = ProofContext.theory_of ctxt;
   1.155 +    val expr = apfst (intern thy) raw_expr;
   1.156 +    val (expr', (parms, fixed)) = parameters thy expr;
   1.157 +  in ctxt end;
   1.158 +
   1.159 +
   1.160 +fun debug_context (raw_expr, fixed) ctxt =
   1.161 +  let
   1.162 +    val thy = ProofContext.theory_of ctxt;
   1.163 +    val expr = intern thy raw_expr;
   1.164 +    val (expr', (parms, fixed)) = parameters thy (expr, fixed);
   1.165 +
   1.166 +    fun declare_parameters (parms, fixed) ctxt =
   1.167 +      let
   1.168 +      val (parms', ctxt') =
   1.169 +        ProofContext.add_fixes (map (fn (p, mx) => (Name.binding p, NONE, mx)) parms) ctxt;
   1.170 +      val (fixed', ctxt'') =
   1.171 +        ProofContext.add_fixes fixed ctxt';
   1.172 +      in
   1.173 +        (parms' @ fixed', ctxt'')
   1.174 +      end;
   1.175 +
   1.176 +    fun rough_inst loc prfx insts ctxt =
   1.177 +      let
   1.178 +        (* locale data *)
   1.179 +        val (parm_names, parm_types) = loc |> Locale.parameters_of thy |>
   1.180 +          map fst |> split_list;
   1.181 +
   1.182 +        (* type parameters *)
   1.183 +        val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   1.184 +
   1.185 +        (* parameter instantiations *)
   1.186 +        val insts' = case insts of
   1.187 +          Positional insts => (insts ~~ parm_names) |> map (fn
   1.188 +            (NONE, p) => Syntax.parse_term ctxt p |
   1.189 +            (SOME t, _) => Syntax.parse_term ctxt t) |
   1.190 +          Named insts => parm_names |> map (fn
   1.191 +            p => case AList.lookup (op =) insts p of
   1.192 +              SOME t => Syntax.parse_term ctxt t |
   1.193 +              NONE => Syntax.parse_term ctxt p);
   1.194 +
   1.195 +	(* type inference and contexts *)
   1.196 +        val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   1.197 +        val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   1.198 +	val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   1.199 +	val res = Syntax.check_terms ctxt arg;
   1.200 +	val ctxt' = ctxt |> fold Variable.auto_fixes res;
   1.201 +
   1.202 +	(* instantiation *)
   1.203 +	val (type_parms'', res') = chop (length type_parms) res;
   1.204 +        val insts'' = (parm_names ~~ res') |> map_filter
   1.205 +          (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   1.206 +            inst => SOME inst);
   1.207 +	val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   1.208 +	val inst = Symtab.make insts'';
   1.209 +      in
   1.210 +        (Element.inst_morphism thy (instT, inst) $>
   1.211 +          Morphism.name_morphism (Name.qualified prfx), ctxt')
   1.212 +      end;
   1.213 +
   1.214 +    fun add_declarations loc morph ctxt =
   1.215 +      let
   1.216 +        (* locale data *)
   1.217 +        val parms = loc |> Locale.parameters_of thy;
   1.218 +        val (typ_decls, term_decls) = Locale.declarations_of thy loc;
   1.219 +
   1.220 +        (* declarations from locale *)
   1.221 +	val ctxt'' = ctxt |>
   1.222 +	  fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |>
   1.223 +	  fold_rev (fn decl => Context.proof_map (decl morph)) term_decls;
   1.224 +      in
   1.225 +        ctxt''
   1.226 +      end;
   1.227 +
   1.228 +    val Expr [(loc1, (prfx1, insts1))] = expr';
   1.229 +    val ctxt0 = ProofContext.init thy;
   1.230 +    val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
   1.231 +    val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   1.232 +    val ctxt'' = add_declarations loc1 morph1 ctxt';
   1.233 +  in ctxt'' end;
   1.234 +
   1.235 +
   1.236 +end;