New-style locale expressions with instantiation (new file expression.ML).
authorballarin
Mon Oct 27 16:23:54 2008 +0100 (2008-10-27)
changeset 28697140bfb63f893
parent 28696 f1701105d651
child 28698 b1c4366e1212
New-style locale expressions with instantiation (new file expression.ML).
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Oct 27 16:20:52 2008 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Mon Oct 27 16:23:54 2008 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4    Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML	\
     1.5    Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML	\
     1.6    Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
     1.7 +  Isar/expression.ML							\
     1.8    Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML	\
     1.9    Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML		\
    1.10    Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
     2.1 --- a/src/Pure/Isar/ROOT.ML	Mon Oct 27 16:20:52 2008 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Mon Oct 27 16:23:54 2008 +0100
     2.3 @@ -54,6 +54,7 @@
     2.4  use "local_theory.ML";
     2.5  use "overloading.ML";
     2.6  use "locale.ML";
     2.7 +use "expression.ML";
     2.8  use "class.ML";
     2.9  use "theory_target.ML";
    2.10  use "instance.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/expression.ML	Mon Oct 27 16:23:54 2008 +0100
     3.3 @@ -0,0 +1,233 @@
     3.4 +(*  Title:      Pure/Isar/expression.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Clemens Ballarin, TU Muenchen
     3.7 +
     3.8 +Locale expressions --- experimental.
     3.9 +*)
    3.10 +
    3.11 +signature EXPRESSION =
    3.12 +sig
    3.13 +
    3.14 +type map
    3.15 +type 'morph expr
    3.16 +
    3.17 +type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    3.18 +type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    3.19 +
    3.20 +val parse_expr: OuterParse.token list -> expression * OuterParse.token list
    3.21 +val debug_parameters: expression -> Proof.context -> Proof.context
    3.22 +val debug_context: expression -> Proof.context -> Proof.context
    3.23 +
    3.24 +end;
    3.25 +
    3.26 +
    3.27 +structure Expression: EXPRESSION =
    3.28 +struct
    3.29 +
    3.30 +(* Locale expressions *)
    3.31 +
    3.32 +datatype map =
    3.33 +  Positional of string option list |
    3.34 +  Named of (string * string) list;
    3.35 +
    3.36 +datatype 'morph expr = Expr of (string * 'morph) list;
    3.37 +
    3.38 +type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
    3.39 +type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
    3.40 +
    3.41 +
    3.42 +(** Parsing and printing **)
    3.43 +
    3.44 +local
    3.45 +
    3.46 +structure P = OuterParse;
    3.47 +
    3.48 +val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    3.49 +   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
    3.50 +fun plus1_unless test scan =
    3.51 +  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    3.52 +
    3.53 +val prefix = P.name --| P.$$$ ":";
    3.54 +val named = P.name -- (P.$$$ "=" |-- P.term);
    3.55 +val position = P.maybe P.term;
    3.56 +val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    3.57 +  Scan.repeat1 position >> Positional;
    3.58 +
    3.59 +in
    3.60 +
    3.61 +val parse_expr =
    3.62 +  let
    3.63 +    fun expr2 x = P.xname x;
    3.64 +    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    3.65 +      Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    3.66 +    fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
    3.67 +  in expr0 -- P.for_fixes end;
    3.68 +
    3.69 +end;
    3.70 +
    3.71 +(*
    3.72 +fun pretty_expr thy (Locale loc) =
    3.73 +      [Pretty.str "Locale", Pretty.brk 1, Pretty.str (Locale.extern thy loc)]
    3.74 +  | pretty_expr thy (Instance (expr, (prfx, Positional insts))) =
    3.75 +      let
    3.76 +        val insts' = (* chop trailing NONEs *)
    3.77 +      
    3.78 +  | pretty_expr thy (Instance (expr, (prfx, Named insts))) =
    3.79 +*)
    3.80 +
    3.81 +
    3.82 +(** Processing of locale expression **)
    3.83 +
    3.84 +fun intern thy (Expr instances) = Expr (map (apfst (Locale.intern thy)) instances);
    3.85 +
    3.86 +
    3.87 +(* Parameters of expression (not expression_i).
    3.88 +   Sanity check of instantiations.
    3.89 +   Positional instantiations are extended to match full length of parameter list. *)
    3.90 +
    3.91 +fun parameters thy (expr, fixed) =
    3.92 +  let
    3.93 +    fun reject_dups message xs =
    3.94 +      let val dups = duplicates (op =) xs
    3.95 +      in
    3.96 +        if null dups then () else error (message ^ commas dups)
    3.97 +      end;
    3.98 +
    3.99 +    fun params2 loc =
   3.100 +          (Locale.parameters_of thy loc |> map (fn ((p, _), mx) => (p, mx)), loc) ;
   3.101 +    fun params1 (loc, (prfx, Positional insts)) =
   3.102 +          let
   3.103 +            val (ps, loc') = params2 loc;
   3.104 +	    val d = length ps - length insts;
   3.105 +	    val insts' =
   3.106 +	      if d < 0 then error ("More arguments than parameters in instantiation.")
   3.107 +(* FIXME print expr *)
   3.108 +	      else insts @ replicate d NONE;
   3.109 +            val ps' = (ps ~~ insts') |>
   3.110 +              map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
   3.111 +          in
   3.112 +            (ps', (loc', (prfx, Positional insts')))
   3.113 +          end
   3.114 +      | params1 (loc, (prfx, Named insts)) =
   3.115 +          let
   3.116 +            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   3.117 +              (map fst insts);
   3.118 +(* FIXME print expr *)
   3.119 +
   3.120 +            val (ps, loc') = params2 loc;
   3.121 +            val ps' = fold (fn (p, _) => fn ps =>
   3.122 +              if AList.defined (op =) ps p then AList.delete (op =) p ps
   3.123 +              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
   3.124 +(* FIXME print expr *)
   3.125 +(* FIXME AList lacks a version of delete that signals the absence of the deleted item *)
   3.126 +          in
   3.127 +            (ps', (loc', (prfx, Named insts)))
   3.128 +          end;
   3.129 +    fun params0 (Expr is) =
   3.130 +          let
   3.131 +            val (is', ps') = fold_map (fn i => fn ps =>
   3.132 +              let
   3.133 +                val (ps', i') = params1 i;
   3.134 +                val ps'' = AList.join (op =) (fn p => fn (mx1, mx2) =>
   3.135 +                  if mx1 = mx2 then mx1
   3.136 +                  else error ("Conflicting syntax for parameter" ^ quote p ^ " in expression.")) (ps, ps')
   3.137 +(* FIXME print Expr is *)
   3.138 +              in (i', ps'') end) is []
   3.139 +          in
   3.140 +            (ps', Expr is')
   3.141 +          end;
   3.142 +
   3.143 +    val (parms, expr') = params0 expr;
   3.144 +
   3.145 +    val parms' = map fst parms;
   3.146 +    val fixed' = map (#1 #> Name.name_of) fixed;
   3.147 +    val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   3.148 +    val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
   3.149 +
   3.150 +  in (expr', (parms, fixed)) end;
   3.151 +
   3.152 +fun debug_parameters raw_expr ctxt =
   3.153 +  let
   3.154 +    val thy = ProofContext.theory_of ctxt;
   3.155 +    val expr = apfst (intern thy) raw_expr;
   3.156 +    val (expr', (parms, fixed)) = parameters thy expr;
   3.157 +  in ctxt end;
   3.158 +
   3.159 +
   3.160 +fun debug_context (raw_expr, fixed) ctxt =
   3.161 +  let
   3.162 +    val thy = ProofContext.theory_of ctxt;
   3.163 +    val expr = intern thy raw_expr;
   3.164 +    val (expr', (parms, fixed)) = parameters thy (expr, fixed);
   3.165 +
   3.166 +    fun declare_parameters (parms, fixed) ctxt =
   3.167 +      let
   3.168 +      val (parms', ctxt') =
   3.169 +        ProofContext.add_fixes (map (fn (p, mx) => (Name.binding p, NONE, mx)) parms) ctxt;
   3.170 +      val (fixed', ctxt'') =
   3.171 +        ProofContext.add_fixes fixed ctxt';
   3.172 +      in
   3.173 +        (parms' @ fixed', ctxt'')
   3.174 +      end;
   3.175 +
   3.176 +    fun rough_inst loc prfx insts ctxt =
   3.177 +      let
   3.178 +        (* locale data *)
   3.179 +        val (parm_names, parm_types) = loc |> Locale.parameters_of thy |>
   3.180 +          map fst |> split_list;
   3.181 +
   3.182 +        (* type parameters *)
   3.183 +        val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   3.184 +
   3.185 +        (* parameter instantiations *)
   3.186 +        val insts' = case insts of
   3.187 +          Positional insts => (insts ~~ parm_names) |> map (fn
   3.188 +            (NONE, p) => Syntax.parse_term ctxt p |
   3.189 +            (SOME t, _) => Syntax.parse_term ctxt t) |
   3.190 +          Named insts => parm_names |> map (fn
   3.191 +            p => case AList.lookup (op =) insts p of
   3.192 +              SOME t => Syntax.parse_term ctxt t |
   3.193 +              NONE => Syntax.parse_term ctxt p);
   3.194 +
   3.195 +	(* type inference and contexts *)
   3.196 +        val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   3.197 +        val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   3.198 +	val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   3.199 +	val res = Syntax.check_terms ctxt arg;
   3.200 +	val ctxt' = ctxt |> fold Variable.auto_fixes res;
   3.201 +
   3.202 +	(* instantiation *)
   3.203 +	val (type_parms'', res') = chop (length type_parms) res;
   3.204 +        val insts'' = (parm_names ~~ res') |> map_filter
   3.205 +          (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   3.206 +            inst => SOME inst);
   3.207 +	val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   3.208 +	val inst = Symtab.make insts'';
   3.209 +      in
   3.210 +        (Element.inst_morphism thy (instT, inst) $>
   3.211 +          Morphism.name_morphism (Name.qualified prfx), ctxt')
   3.212 +      end;
   3.213 +
   3.214 +    fun add_declarations loc morph ctxt =
   3.215 +      let
   3.216 +        (* locale data *)
   3.217 +        val parms = loc |> Locale.parameters_of thy;
   3.218 +        val (typ_decls, term_decls) = Locale.declarations_of thy loc;
   3.219 +
   3.220 +        (* declarations from locale *)
   3.221 +	val ctxt'' = ctxt |>
   3.222 +	  fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |>
   3.223 +	  fold_rev (fn decl => Context.proof_map (decl morph)) term_decls;
   3.224 +      in
   3.225 +        ctxt''
   3.226 +      end;
   3.227 +
   3.228 +    val Expr [(loc1, (prfx1, insts1))] = expr';
   3.229 +    val ctxt0 = ProofContext.init thy;
   3.230 +    val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
   3.231 +    val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   3.232 +    val ctxt'' = add_declarations loc1 morph1 ctxt';
   3.233 +  in ctxt'' end;
   3.234 +
   3.235 +
   3.236 +end;