added extend_trrules_i;
authorwenzelm
Mon Jun 26 14:32:26 1995 +0200 (1995-06-26)
changeset 115896804ce95516
parent 1157 da78c293e8dc
child 1159 998a5c3451bf
added extend_trrules_i;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jun 23 11:59:06 1995 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Jun 26 14:32:26 1995 +0200
     1.3 @@ -13,10 +13,10 @@
     1.4    include SYN_TRANS0
     1.5    include MIXFIX0
     1.6    include PRINTER0
     1.7 -  type xrule
     1.8 -  val |-> : (string * string) * (string * string) -> xrule
     1.9 -  val <-| : (string * string) * (string * string) -> xrule
    1.10 -  val <-> : (string * string) * (string * string) -> xrule
    1.11 +  datatype 'a trrule =
    1.12 +    op |-> of 'a * 'a |
    1.13 +    op <-| of 'a * 'a |
    1.14 +    op <-> of 'a * 'a
    1.15  end;
    1.16  
    1.17  signature SYNTAX =
    1.18 @@ -29,10 +29,10 @@
    1.19    include MIXFIX1
    1.20    include PRINTER0
    1.21    sharing type ast = Parser.SynExt.Ast.ast
    1.22 -  type xrule
    1.23 -  val |-> : (string * string) * (string * string) -> xrule
    1.24 -  val <-| : (string * string) * (string * string) -> xrule
    1.25 -  val <-> : (string * string) * (string * string) -> xrule
    1.26 +  datatype 'a trrule =
    1.27 +    op |-> of 'a * 'a |
    1.28 +    op <-| of 'a * 'a |
    1.29 +    op <-> of 'a * 'a
    1.30    type syntax
    1.31    val extend_log_types: syntax -> string list -> syntax
    1.32    val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
    1.33 @@ -43,7 +43,8 @@
    1.34      (string * (term list -> term)) list *
    1.35      (string * (term list -> term)) list *
    1.36      (string * (ast list -> ast)) list -> syntax
    1.37 -  val extend_trrules: syntax -> xrule list -> syntax
    1.38 +  val extend_trrules: syntax -> (string * string) trrule list -> syntax
    1.39 +  val extend_trrules_i: syntax -> ast trrule list -> syntax
    1.40    val merge_syntaxes: syntax -> syntax -> syntax
    1.41    val type_syn: syntax
    1.42    val pure_syn: syntax
    1.43 @@ -344,14 +345,33 @@
    1.44  fun simple_read_typ str = read_typ type_syn (K []) str;
    1.45  
    1.46  
    1.47 -(* read translation rules *)
    1.48  
    1.49 -datatype 'a rule =
    1.50 +(** prepare translation rules **)
    1.51 +
    1.52 +datatype 'a trrule =
    1.53    op |-> of 'a * 'a |
    1.54    op <-| of 'a * 'a |
    1.55    op <-> of 'a * 'a;
    1.56  
    1.57 -type xrule = (string * string) rule;
    1.58 +fun map_rule f (x |-> y) = (f x |-> f y)
    1.59 +  | map_rule f (x <-| y) = (f x <-| f y)
    1.60 +  | map_rule f (x <-> y) = (f x <-> f y);
    1.61 +
    1.62 +fun right_rule (pat1 |-> pat2) = Some (pat1, pat2)
    1.63 +  | right_rule (pat1 <-| pat2) = None
    1.64 +  | right_rule (pat1 <-> pat2) = Some (pat1, pat2);
    1.65 +
    1.66 +fun left_rule (pat1 |-> pat2) = None
    1.67 +  | left_rule (pat1 <-| pat2) = Some (pat2, pat1)
    1.68 +  | left_rule (pat1 <-> pat2) = Some (pat2, pat1);
    1.69 +
    1.70 +
    1.71 +fun check_rule (rule as (lhs, rhs)) =
    1.72 +  (case rule_error rule of
    1.73 +    Some msg =>
    1.74 +      error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
    1.75 +        str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
    1.76 +  | None => rule);
    1.77  
    1.78  
    1.79  fun read_pattern syn (root, str) =
    1.80 @@ -371,33 +391,11 @@
    1.81        quote str);
    1.82  
    1.83  
    1.84 -fun check_rule (rule as (lhs, rhs)) =
    1.85 -  (case rule_error rule of
    1.86 -    Some msg =>
    1.87 -      error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
    1.88 -        str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
    1.89 -  | None => rule);
    1.90 -
    1.91 -
    1.92 -fun read_xrules syn xrules =
    1.93 -  let
    1.94 -    fun map_rule f (x |-> y) = (f x |-> f y)
    1.95 -      | map_rule f (x <-| y) = (f x <-| f y)
    1.96 -      | map_rule f (x <-> y) = (f x <-> f y);
    1.97 -
    1.98 -    fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
    1.99 -      | right_rule (xpat1 <-| xpat2) = None
   1.100 -      | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
   1.101 -
   1.102 -    fun left_rule (xpat1 |-> xpat2) = None
   1.103 -      | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
   1.104 -      | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
   1.105 -
   1.106 -    val rules = map (map_rule (read_pattern syn)) xrules;
   1.107 -  in
   1.108 +fun prep_rules rd_pat raw_rules =
   1.109 +  let val rules = map (map_rule rd_pat) raw_rules in
   1.110      (map check_rule (mapfilter right_rule rules),
   1.111        map check_rule (mapfilter left_rule rules))
   1.112 -  end;
   1.113 +  end
   1.114  
   1.115  
   1.116  
   1.117 @@ -441,7 +439,10 @@
   1.118  
   1.119  val extend_trfuns = ext_syntax syn_ext_trfuns;
   1.120  
   1.121 -fun extend_trrules syn xrules =
   1.122 -  ext_syntax syn_ext_rules syn (read_xrules syn xrules);
   1.123 +fun extend_trrules syn rules =
   1.124 +  ext_syntax syn_ext_rules syn (prep_rules (read_pattern syn) rules);
   1.125 +
   1.126 +fun extend_trrules_i syn rules =
   1.127 +  ext_syntax syn_ext_rules syn (prep_rules I rules);
   1.128  
   1.129  end;