src/HOLCF/domain/syntax.ML
author oheimb
Mon Oct 27 11:34:33 1997 +0100 (1997-10-27)
changeset 4008 2444085532c6
parent 3793 6e807b50b6c1
child 4122 f63c283cefaf
permissions -rw-r--r--
adapted domain and ax_ops package for name spaces
oheimb@2453
     1
(*  Title:      HOLCF/domain/syntax.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
syntax generator for domain section
regensbu@1274
     7
*)
regensbu@1274
     8
regensbu@1274
     9
structure Domain_Syntax = struct 
regensbu@1274
    10
regensbu@1274
    11
local 
regensbu@1274
    12
regensbu@1274
    13
open Domain_Library;
regensbu@1274
    14
infixr 5 -->; infixr 6 ~>;
oheimb@1637
    15
fun calc_syntax dtypeprod ((dname, typevars), (cons':
oheimb@1637
    16
			   (string * ThyOps.cmixfix * (bool*string*typ) list) list)) =
regensbu@1274
    17
let
regensbu@1274
    18
(* ----- constants concerning the isomorphism ------------------------------------- *)
regensbu@1274
    19
regensbu@1274
    20
local
regensbu@1274
    21
  fun opt_lazy (lazy,_,t) = if lazy then Type("u",[t]) else t
oheimb@1637
    22
  fun prod     (_,_,args) = if args = [] then Type("one",[])
oheimb@1637
    23
				         else foldr'(mk_typ "**") (map opt_lazy args);
oheimb@1637
    24
  fun freetvar s = if (mk_tvar s) mem typevars then freetvar ("t"^s) else mk_tvar s;
oheimb@1637
    25
  fun when_type (_   ,_,args) = foldr (op ~>)       (map third args,freetvar "t");
regensbu@1274
    26
in
regensbu@1274
    27
  val dtype  = Type(dname,typevars);
regensbu@1274
    28
  val dtype2 = foldr' (mk_typ "++") (map prod cons');
oheimb@4008
    29
  val dnam = Sign.base_name dname;
oheimb@4008
    30
  val const_rep  = (dnam^"_rep" ,              dtype  ~> dtype2, NoSyn');
oheimb@4008
    31
  val const_abs  = (dnam^"_abs" ,              dtype2 ~> dtype , NoSyn');
oheimb@4008
    32
  val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
oheimb@4008
    33
					       	 dtype ~> freetvar "t"), NoSyn');
oheimb@4008
    34
  val const_copy = (dnam^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
regensbu@1274
    35
end;
regensbu@1274
    36
regensbu@1274
    37
(* ----- constants concerning the constructors, discriminators and selectors ------ *)
regensbu@1274
    38
regensbu@1274
    39
fun is_infix (ThyOps.CInfixl       _ ) = true
regensbu@1274
    40
|   is_infix (ThyOps.CInfixr       _ ) = true
regensbu@1274
    41
|   is_infix (ThyOps.Mixfix(Infixl _)) = true
regensbu@1274
    42
|   is_infix (ThyOps.Mixfix(Infixr _)) = true
regensbu@1274
    43
|   is_infix  _                        = false;
regensbu@1274
    44
regensbu@1274
    45
local
regensbu@1274
    46
  val escape = let
oheimb@1637
    47
	fun esc (c :: cs) = if c mem ["'","_","(",")","/"] then "'" :: c :: esc cs
oheimb@1637
    48
							   else        c :: esc cs
oheimb@1637
    49
	|   esc []        = []
oheimb@1637
    50
	in implode o esc o explode end;
regensbu@1274
    51
  fun con       (name,s,args) = (name,foldr (op ~>) (map third args,dtype),s);
regensbu@1274
    52
  fun dis       (con ,s,_   ) = (dis_name_ con, dtype~>Type("tr",[]),
oheimb@1637
    53
			 	 ThyOps.Mixfix(Mixfix("is'_"^
oheimb@1637
    54
				 (if is_infix s then Id else escape)con,[],max_pri)));
regensbu@1274
    55
  fun sel       (_   ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ~> typ,NoSyn'))args;
regensbu@1274
    56
in
regensbu@1274
    57
  val consts_con = map con cons';
regensbu@1274
    58
  val consts_dis = map dis cons';
regensbu@1274
    59
  val consts_sel = flat(map sel cons');
regensbu@1274
    60
end;
regensbu@1274
    61
regensbu@1274
    62
(* ----- constants concerning induction ------------------------------------------- *)
regensbu@1274
    63
oheimb@4008
    64
  val const_take   = (dnam^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
oheimb@4008
    65
  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
regensbu@1274
    66
regensbu@1274
    67
(* ----- case translation --------------------------------------------------------- *)
regensbu@1274
    68
regensbu@1274
    69
local open Syntax in
regensbu@1274
    70
  val case_trans = let 
oheimb@1637
    71
	fun c_ast con syn = Constant (ThyOps.const_name con syn);
oheimb@1637
    72
	fun expvar n      = Variable ("e"^(string_of_int n));
oheimb@1637
    73
	fun argvar n m _  = Variable ("a"^(string_of_int n)^"_"^(string_of_int m));
oheimb@1637
    74
	fun app s (l,r)   = mk_appl (Constant s) [l,r];
oheimb@1637
    75
	fun case1 n (con,syn,args) = mk_appl (Constant "@case1")
oheimb@1637
    76
		 [if is_infix syn
oheimb@1637
    77
		  then mk_appl (c_ast con syn) (mapn (argvar n) 1 args)
oheimb@1637
    78
		  else foldl (app "@fapp") (c_ast con syn, (mapn (argvar n) 1 args)),
oheimb@1637
    79
		  expvar n];
oheimb@1637
    80
	fun arg1 n (con,_,args) = if args = [] then expvar n 
oheimb@1637
    81
				  else mk_appl (Constant "LAM ") 
oheimb@1637
    82
		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
wenzelm@3534
    83
  in
wenzelm@3534
    84
    ParsePrintRule
wenzelm@3534
    85
      (mk_appl (Constant "@case") [Variable "x", foldr'
oheimb@1637
    86
				 (fn (c,cs) => mk_appl (Constant "@case2") [c,cs])
wenzelm@3534
    87
				 (mapn case1 1 cons')],
wenzelm@3534
    88
       mk_appl (Constant "@fapp") [foldl 
oheimb@1637
    89
				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
oheimb@4008
    90
				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
wenzelm@3534
    91
				 Variable "x"])
regensbu@1274
    92
  end;
regensbu@1274
    93
end;
regensbu@1274
    94
regensbu@1274
    95
in ([const_rep, const_abs, const_when, const_copy] @ 
regensbu@1274
    96
     consts_con @ consts_dis @ consts_sel @
regensbu@1274
    97
    [const_take, const_finite],
regensbu@1274
    98
    [case_trans])
regensbu@1274
    99
end; (* let *)
regensbu@1274
   100
regensbu@1274
   101
(* ----- putting all the syntax stuff together ------------------------------------ *)
regensbu@1274
   102
regensbu@1274
   103
in (* local *)
regensbu@1274
   104
oheimb@4008
   105
fun add_syntax (comp_dnam,eqs': ((string * typ list) *
oheimb@1637
   106
		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
regensbu@1274
   107
let
oheimb@4008
   108
  val dtypes  = map (Type      o fst) eqs';
regensbu@1274
   109
  val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
regensbu@1274
   110
  val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
oheimb@4008
   111
  val const_copy   = (comp_dnam^"_copy"  ,funprod ~> funprod       , NoSyn');
oheimb@4008
   112
  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
regensbu@1274
   113
  val ctt           = map (calc_syntax funprod) eqs';
regensbu@1274
   114
  val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
oheimb@4008
   115
in thy'' |> add_cur_ops_i (flat(map fst ctt))
oheimb@1637
   116
	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
wenzelm@3771
   117
	 |> Theory.add_trrules_i (flat(map snd ctt))
regensbu@1274
   118
end; (* let *)
regensbu@1274
   119
regensbu@1274
   120
end; (* local *)
regensbu@1274
   121
end; (* struct *)