src/HOLCF/Tools/domain/domain_syntax.ML
changeset 30190 479806475f3c
parent 29322 ae6f2b1559fa
child 30280 eb98b49ef835
equal deleted inserted replaced
30189:3633f560f4c3 30190:479806475f3c
     1 (*  Title:      HOLCF/Tools/domain/domain_syntax.ML
     1 (*  Title:      HOLCF/Tools/domain/domain_syntax.ML
     2     ID:         $Id$
       
     3     Author:     David von Oheimb
     2     Author:     David von Oheimb
     4 
     3 
     5 Syntax generator for domain command.
     4 Syntax generator for domain command.
     6 *)
     5 *)
     7 
     6 
    20   fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
    19   fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
    21   fun prod     (_,_,args) = if args = [] then oneT
    20   fun prod     (_,_,args) = if args = [] then oneT
    22 			    else foldr1 mk_sprodT (map opt_lazy args);
    21 			    else foldr1 mk_sprodT (map opt_lazy args);
    23   fun freetvar s = let val tvar = mk_TFree s in
    22   fun freetvar s = let val tvar = mk_TFree s in
    24 		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
    23 		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
    25   fun when_type (_   ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
    24   fun when_type (_   ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args);
    26 in
    25 in
    27   val dtype  = Type(dname,typevars);
    26   val dtype  = Type(dname,typevars);
    28   val dtype2 = foldr1 mk_ssumT (map prod cons');
    27   val dtype2 = foldr1 mk_ssumT (map prod cons');
    29   val dnam = Sign.base_name dname;
    28   val dnam = Sign.base_name dname;
    30   val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
    29   val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
    31   val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
    30   val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
    32   val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
    31   val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
    33   val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
    32   val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
    34 end;
    33 end;
    35 
    34 
    36 (* ----- constants concerning constructors, discriminators, and selectors --- *)
    35 (* ----- constants concerning constructors, discriminators, and selectors --- *)
    37 
    36 
    39   val escape = let
    38   val escape = let
    40 	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
    39 	fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs
    41 							 else      c::esc cs
    40 							 else      c::esc cs
    42 	|   esc []      = []
    41 	|   esc []      = []
    43 	in implode o esc o Symbol.explode end;
    42 	in implode o esc o Symbol.explode end;
    44   fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
    43   fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
    45   fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
    44   fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
    46 			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
    45 			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
    47 			(* strictly speaking, these constants have one argument,
    46 			(* strictly speaking, these constants have one argument,
    48 			   but the mixfix (without arguments) is introduced only
    47 			   but the mixfix (without arguments) is introduced only
    49 			   to generate parse rules for non-alphanumeric names*)
    48 			   to generate parse rules for non-alphanumeric names*)
    84     fun app s (l,r)  = mk_appl (Constant s) [l,r];
    83     fun app s (l,r)  = mk_appl (Constant s) [l,r];
    85     val cabs = app "_cabs";
    84     val cabs = app "_cabs";
    86     val capp = app "Rep_CFun";
    85     val capp = app "Rep_CFun";
    87     fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
    86     fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
    88     fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
    87     fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
    89     fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
    88     fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
    90     fun when1 n m = if n = m then arg1 n else K (Constant "UU");
    89     fun when1 n m = if n = m then arg1 n else K (Constant "UU");
    91 
    90 
    92     fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
    91     fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
    93     fun app_pat x = mk_appl (Constant "_pat") [x];
    92     fun app_pat x = mk_appl (Constant "_pat") [x];
    94     fun args_list [] = Constant "_noargs"
    93     fun args_list [] = Constant "_noargs"