src/Pure/Isar/expression.ML
author haftmann
Tue Oct 28 12:28:14 2008 +0100 (2008-10-28)
changeset 28701 ca5840b1f7b3
parent 28697 140bfb63f893
child 28795 6891e273c33b
permissions -rw-r--r--
making SMLNJ happy
     1 (*  Title:      Pure/Isar/expression.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen
     4 
     5 Locale expressions --- experimental.
     6 *)
     7 
     8 signature EXPRESSION =
     9 sig
    10 
    11 type map
    12 type 'morph expr
    13 
    14 type expression = (string * map) expr * (Name.binding * string option * mixfix) list
    15 type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
    16 
    17 val parse_expr: OuterParse.token list -> expression * OuterParse.token list
    18 val debug_parameters: expression -> Proof.context -> Proof.context
    19 val debug_context: expression -> Proof.context -> Proof.context
    20 
    21 end;
    22 
    23 
    24 structure Expression: EXPRESSION =
    25 struct
    26 
    27 (* Locale expressions *)
    28 
    29 datatype map =
    30   Positional of string option list |
    31   Named of (string * string) list;
    32 
    33 datatype 'morph expr = Expr of (string * 'morph) list;
    34 
    35 type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
    36 type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
    37 
    38 
    39 (** Parsing and printing **)
    40 
    41 local
    42 
    43 structure P = OuterParse;
    44 
    45 val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    46    P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
    47 fun plus1_unless test scan =
    48   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    49 
    50 val prefix = P.name --| P.$$$ ":";
    51 val named = P.name -- (P.$$$ "=" |-- P.term);
    52 val position = P.maybe P.term;
    53 val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    54   Scan.repeat1 position >> Positional;
    55 
    56 in
    57 
    58 val parse_expr =
    59   let
    60     fun expr2 x = P.xname x;
    61     fun expr1 x = (Scan.optional prefix "" -- expr2 --
    62       Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    63     fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
    64   in expr0 -- P.for_fixes end;
    65 
    66 end;
    67 
    68 (*
    69 fun pretty_expr thy (Locale loc) =
    70       [Pretty.str "Locale", Pretty.brk 1, Pretty.str (Locale.extern thy loc)]
    71   | pretty_expr thy (Instance (expr, (prfx, Positional insts))) =
    72       let
    73         val insts' = (* chop trailing NONEs *)
    74       
    75   | pretty_expr thy (Instance (expr, (prfx, Named insts))) =
    76 *)
    77 
    78 
    79 (** Processing of locale expression **)
    80 
    81 fun intern thy (Expr instances) = Expr (map (apfst (Locale.intern thy)) instances);
    82 
    83 
    84 (* Parameters of expression (not expression_i).
    85    Sanity check of instantiations.
    86    Positional instantiations are extended to match full length of parameter list. *)
    87 
    88 fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) =
    89   let
    90     fun reject_dups message xs =
    91       let val dups = duplicates (op =) xs
    92       in
    93         if null dups then () else error (message ^ commas dups)
    94       end;
    95 
    96     fun params2 loc =
    97           (Locale.parameters_of thy loc |> map (fn ((p, _), mx) => (p, mx)), loc) ;
    98     fun params1 (loc, (prfx, Positional insts)) =
    99           let
   100             val (ps, loc') = params2 loc;
   101 	    val d = length ps - length insts;
   102 	    val insts' =
   103 	      if d < 0 then error ("More arguments than parameters in instantiation.")
   104 (* FIXME print expr *)
   105 	      else insts @ replicate d NONE;
   106             val ps' = (ps ~~ insts') |>
   107               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
   108           in
   109             (ps', (loc', (prfx, Positional insts')))
   110           end
   111       | params1 (loc, (prfx, Named insts)) =
   112           let
   113             val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   114               (map fst insts);
   115 (* FIXME print expr *)
   116 
   117             val (ps, loc') = params2 loc;
   118             val ps' = fold (fn (p, _) => fn ps =>
   119               if AList.defined (op =) ps p then AList.delete (op =) p ps
   120               else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
   121 (* FIXME print expr *)
   122 (* FIXME AList lacks a version of delete that signals the absence of the deleted item *)
   123           in
   124             (ps', (loc', (prfx, Named insts)))
   125           end;
   126     fun params0 (Expr is) =
   127           let
   128             val (is', ps') = fold_map (fn i => fn ps =>
   129               let
   130                 val (ps', i') = params1 i;
   131                 val ps'' = AList.join (op =) (fn p => fn (mx1, mx2) =>
   132                   if mx1 = mx2 then mx1
   133                   else error ("Conflicting syntax for parameter" ^ quote p ^ " in expression.")) (ps, ps')
   134 (* FIXME print Expr is *)
   135               in (i', ps'') end) is []
   136           in
   137             (ps', Expr is')
   138           end;
   139 
   140     val (parms, expr') = params0 expr;
   141 
   142     val parms' = map fst parms;
   143     val fixed' = map (#1 #> Name.name_of) fixed;
   144     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   145     val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
   146 
   147   in (expr', (parms, fixed)) end;
   148 
   149 fun debug_parameters raw_expr ctxt =
   150   let
   151     val thy = ProofContext.theory_of ctxt;
   152     val expr = apfst (intern thy) raw_expr;
   153     val (expr', (parms, fixed)) = parameters thy expr;
   154   in ctxt end;
   155 
   156 
   157 fun debug_context (raw_expr, fixed) ctxt =
   158   let
   159     val thy = ProofContext.theory_of ctxt;
   160     val expr = intern thy raw_expr;
   161     val (expr', (parms, fixed)) = parameters thy (expr, fixed);
   162 
   163     fun declare_parameters (parms, fixed) ctxt =
   164       let
   165       val (parms', ctxt') =
   166         ProofContext.add_fixes (map (fn (p, mx) => (Name.binding p, NONE, mx)) parms) ctxt;
   167       val (fixed', ctxt'') =
   168         ProofContext.add_fixes fixed ctxt';
   169       in
   170         (parms' @ fixed', ctxt'')
   171       end;
   172 
   173     fun rough_inst loc prfx insts ctxt =
   174       let
   175         (* locale data *)
   176         val (parm_names, parm_types) = loc |> Locale.parameters_of thy |>
   177           map fst |> split_list;
   178 
   179         (* type parameters *)
   180         val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   181 
   182         (* parameter instantiations *)
   183         val insts' = case insts of
   184           Positional insts => (insts ~~ parm_names) |> map (fn
   185             (NONE, p) => Syntax.parse_term ctxt p |
   186             (SOME t, _) => Syntax.parse_term ctxt t) |
   187           Named insts => parm_names |> map (fn
   188             p => case AList.lookup (op =) insts p of
   189               SOME t => Syntax.parse_term ctxt t |
   190               NONE => Syntax.parse_term ctxt p);
   191 
   192 	(* type inference and contexts *)
   193         val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   194         val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   195 	val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   196 	val res = Syntax.check_terms ctxt arg;
   197 	val ctxt' = ctxt |> fold Variable.auto_fixes res;
   198 
   199 	(* instantiation *)
   200 	val (type_parms'', res') = chop (length type_parms) res;
   201         val insts'' = (parm_names ~~ res') |> map_filter
   202           (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   203             inst => SOME inst);
   204 	val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   205 	val inst = Symtab.make insts'';
   206       in
   207         (Element.inst_morphism thy (instT, inst) $>
   208           Morphism.name_morphism (Name.qualified prfx), ctxt')
   209       end;
   210 
   211     fun add_declarations loc morph ctxt =
   212       let
   213         (* locale data *)
   214         val parms = loc |> Locale.parameters_of thy;
   215         val (typ_decls, term_decls) = Locale.declarations_of thy loc;
   216 
   217         (* declarations from locale *)
   218 	val ctxt'' = ctxt |>
   219 	  fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |>
   220 	  fold_rev (fn decl => Context.proof_map (decl morph)) term_decls;
   221       in
   222         ctxt''
   223       end;
   224 
   225     val Expr [(loc1, (prfx1, insts1))] = expr';
   226     val ctxt0 = ProofContext.init thy;
   227     val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
   228     val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
   229     val ctxt'' = add_declarations loc1 morph1 ctxt';
   230   in ctxt'' end;
   231 
   232 
   233 end;