src/HOLCF/domain/interface.ML
author wenzelm
Wed May 12 17:26:56 1999 +0200 (1999-05-12)
changeset 6642 732af87c0650
parent 4709 d24168720303
child 12030 46d57d0290a2
permissions -rw-r--r--
strip_quotes replaced by unenclose;
oheimb@2445
     1
(*  Title:      HOLCF/domain/interface.ML
oheimb@2445
     2
    ID:         $Id$
oheimb@2445
     3
    Author : David von Oheimb
oheimb@2445
     4
    Copyright 1995, 1996 TU Muenchen
oheimb@2445
     5
oheimb@2445
     6
parser for domain section
regensbu@1274
     7
*)
regensbu@1274
     8
regensbu@1274
     9
local 
regensbu@1274
    10
  open ThyParse;
regensbu@1274
    11
  open Domain_Library;
regensbu@1274
    12
oheimb@4030
    13
(* --- generation of bindings for axioms and theorems in .thy.ML - *)
regensbu@1274
    14
oheimb@4043
    15
  fun get      dname name   = "get_thm thy " ^ quote (dname^"."^name);
oheimb@4043
    16
  fun gen_vals dname name   = "val "^ name ^ " = get_thm" ^ 
wenzelm@4709
    17
			(if hd (rev (Symbol.explode name)) = "s" then "s" else "")^
oheimb@4043
    18
			" thy " ^ quote (dname^"."^name)^";";
oheimb@4043
    19
  fun gen_vall       name l = "val "^name^" = "^ mk_list l^";";
oheimb@4043
    20
  val rews = "iso_rews @ when_rews @\n\
oheimb@4043
    21
 	   \  con_rews @ sel_rews @ dis_rews @ dist_les @ dist_eqs @\n\
oheimb@4043
    22
	   \  copy_rews";
regensbu@1274
    23
oheimb@4043
    24
  fun gen_struct num ((dname,_), cons') = let
regensbu@1274
    25
    val axioms1 = ["abs_iso", "rep_iso", "when_def"];
oheimb@1637
    26
		   (* con_defs , sel_defs, dis_defs *) 
oheimb@4043
    27
    val axioms2 = ["copy_def", "reach", "take_def", "finite_def"];
oheimb@4043
    28
    val theorems = ["iso_rews", "exhaust", "casedist", "when_rews", "con_rews", 
oheimb@4043
    29
		    "sel_rews", "dis_rews", "dist_les", "dist_eqs", "inverts", 
oheimb@4043
    30
		    "injects", "copy_rews"];
regensbu@1274
    31
    in
regensbu@1274
    32
      "structure "^dname^" = struct\n"^
oheimb@4043
    33
      cat_lines (map (gen_vals dname) axioms1)^"\n"^
oheimb@4043
    34
      gen_vall "con_defs"       (map (fn (con,_,_) => 
oheimb@4043
    35
		get dname (strip_esc con^"_def")) cons')^"\n"^
oheimb@4043
    36
      gen_vall "sel_defs" (flat (map (fn (_,_,args) => map (fn (_,sel,_) => 
oheimb@4043
    37
		get dname (sel^"_def")) args)    cons'))^"\n"^
oheimb@4043
    38
      gen_vall "dis_defs"       (map (fn (con,_,_) => 
oheimb@4043
    39
		get dname (dis_name_ con^"_def")) cons')^"\n"^
oheimb@4043
    40
      cat_lines (map (gen_vals dname) axioms2)^"\n"^
oheimb@4043
    41
      cat_lines (map (gen_vals dname) theorems)^"\n"^
oheimb@4043
    42
      (if num > 1 then "val rews = " ^rews ^";\n" else "")
regensbu@1274
    43
    end;
regensbu@1274
    44
oheimb@4008
    45
  fun mk_domain eqs'' = let
oheimb@4008
    46
    val num    = length eqs'';
oheimb@4008
    47
    val dtnvs  = map fst eqs'';
regensbu@1274
    48
    val dnames = map fst dtnvs;
regensbu@1274
    49
    val comp_dname = implode (separate "_" dnames);
paulson@2267
    50
    val conss' = ListPair.map 
oheimb@4043
    51
	(fn (dnam,cons'') => let fun sel n m = upd_second 
oheimb@4043
    52
			     (fn None   => dnam^"_sel_"^(string_of_int n)^
oheimb@4043
    53
						    "_"^(string_of_int m)
oheimb@4043
    54
			       | Some s => s)
paulson@2267
    55
	      fun fill_sels n con = upd_third (mapn (sel n) 1) con;
paulson@2267
    56
	  in mapn fill_sels 1 cons'' end)
oheimb@4008
    57
	(dnames, map snd eqs'');
regensbu@1274
    58
    val eqs' = dtnvs~~conss';
regensbu@1274
    59
oheimb@1637
    60
(* ----- string for calling add_domain -------------------------------------- *)
regensbu@1284
    61
oheimb@1637
    62
    val thy_ext_string = let
paulson@2240
    63
      fun mk_conslist cons' = 
oheimb@4030
    64
	  mk_list (map (fn (c,syn,ts)=> "\n"^
oheimb@4008
    65
		    mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
oheimb@4008
    66
		    mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
oheimb@4043
    67
    in "val thy = thy |> Domain_Extender.add_domain "
oheimb@4030
    68
       ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => "\n"^
oheimb@4008
    69
				   mk_pair (mk_pair (quote n, mk_list vs), 
oheimb@4008
    70
					    mk_conslist cs)) eqs'))
oheimb@4030
    71
       ^ ";\n"
oheimb@1637
    72
    end;
oheimb@1637
    73
oheimb@4122
    74
(* ----- string for producing the structures -------------------------------- *)
oheimb@1637
    75
oheimb@1637
    76
    val val_gen_string =  let
oheimb@1637
    77
      val comp_axioms   = [(* copy, *) "reach", "take_def", "finite_def"
oheimb@1637
    78
			   (*, "bisim_def" *)];
oheimb@4043
    79
      val comp_theorems = ["take_rews", "take_lemmas", "finites", 
oheimb@4043
    80
			   "finite_ind", "ind", "coind"];
oheimb@1637
    81
      fun collect sep name = if num = 1 then name else
oheimb@4043
    82
		   implode (separate sep (map (fn s => s^"."^name) dnames));
regensbu@1274
    83
    in
oheimb@4030
    84
	implode (separate "end; (* struct *)\n" 
oheimb@4043
    85
			  (map (gen_struct num) eqs')) ^
oheimb@4043
    86
	(if num > 1 then "end; (* struct *)\n\
oheimb@4043
    87
		         \structure "^comp_dname^" = struct\n" ^
oheimb@4043
    88
			 gen_vals comp_dname "copy_def" ^"\n" ^
oheimb@4043
    89
			 cat_lines (map (fn name => gen_vall (name^"s")
oheimb@4043
    90
			 (map (fn dn => dn^"."^name) dnames)) comp_axioms)^"\n"
oheimb@4043
    91
		    else "") ^
oheimb@4043
    92
	gen_vals comp_dname "bisim_def" ^"\n"^
oheimb@4043
    93
        cat_lines (map (gen_vals comp_dname) comp_theorems)^"\n"^
oheimb@4043
    94
	"val rews = "^(if num>1 then collect" @ " "rews"else rews)^ 
oheimb@4030
    95
		    " @ take_rews;\n\
oheimb@4030
    96
      \end; (* struct *)\n"
oheimb@1637
    97
    end;
oheimb@4043
    98
  in (thy_ext_string^
oheimb@4030
    99
      val_gen_string^
oheimb@4030
   100
      "val thy = thy",
oheimb@4030
   101
      "") end;
oheimb@1637
   102
oheimb@4030
   103
(* ----- parser for domain declaration equation ----------------------------- *)
regensbu@1274
   104
wenzelm@6642
   105
  val name' = name >> unenclose;
wenzelm@6642
   106
  val type_var' = type_var >> unenclose;
oheimb@4008
   107
  fun esc_quote s = let fun esc [] = []
oheimb@4008
   108
			|   esc ("\""::xs) = esc xs
oheimb@4008
   109
			|   esc ("[" ::xs) = "{"::esc xs
oheimb@4008
   110
			|   esc ("]" ::xs) = "}"::esc xs
oheimb@4008
   111
			|   esc (x   ::xs) = x  ::esc xs
wenzelm@4709
   112
		    in implode (esc (Symbol.explode s)) end;
oheimb@4122
   113
  val tvar = (type_var' ^^ 
oheimb@4122
   114
	      optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
oheimb@4008
   115
  fun type_args l = (tvar >> (fn x => [x])
oheimb@4008
   116
                 ||  "(" $$-- !! (list1 tvar --$$ ")")
oheimb@4008
   117
                 ||  empty >> K []) l
oheimb@4008
   118
  fun con_typ l   = (type_args -- name' >> (fn (x,y) => (y,x))) l
oheimb@4008
   119
                      (* here ident may be used instead of name' 
oheimb@4008
   120
                         to avoid ambiguity with standard mixfix option *)
regensbu@1274
   121
  val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
oheimb@2445
   122
			  -- (optional ((name' >> Some) --$$ "::") None)
oheimb@4122
   123
			  -- typ --$$ ")" 
oheimb@4122
   124
		    >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
oheimb@4008
   125
		 || typ >> (fn x => (false,None,x)) 
oheimb@2445
   126
  val domain_cons = name' -- !! (repeat domain_arg) 
oheimb@4122
   127
		    -- ThyParse.opt_mixfix
oheimb@1637
   128
		    >> (fn ((con,args),syn) => (con,syn,args));
regensbu@1274
   129
in
oheimb@4043
   130
  val domain_decl = (enum1 "and" (con_typ --$$ "="  -- !! 
oheimb@4043
   131
				 (enum1 "|" domain_cons))) >> mk_domain;
wenzelm@3622
   132
  val _ = ThySyn.add_syntax
oheimb@4122
   133
    ["lazy", "and"]
oheimb@4122
   134
    [("domain", domain_decl)]
regensbu@1274
   135
wenzelm@3622
   136
end; (* local *)