equal
deleted
inserted
replaced
25 end; |
25 end; |
26 |
26 |
27 signature SYN_TRANS1 = |
27 signature SYN_TRANS1 = |
28 sig |
28 sig |
29 include SYN_TRANS0 |
29 include SYN_TRANS0 |
|
30 val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term |
|
31 val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term |
30 val constrainAbsC: string |
32 val constrainAbsC: string |
31 val pure_trfuns: |
33 val pure_trfuns: |
32 (string * (Ast.ast list -> Ast.ast)) list * |
34 (string * (Ast.ast list -> Ast.ast)) list * |
33 (string * (term list -> term)) list * |
35 (string * (term list -> term)) list * |
34 (string * (term list -> term)) list * |
36 (string * (term list -> term)) list * |
169 | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); |
171 | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); |
170 |
172 |
171 |
173 |
172 |
174 |
173 (** print (ast) translations **) |
175 (** print (ast) translations **) |
|
176 |
|
177 (* types *) |
|
178 |
|
179 fun non_typed_tr' f _ _ ts = f ts; |
|
180 fun non_typed_tr'' f x _ _ ts = f x ts; |
|
181 |
174 |
182 |
175 (* application *) |
183 (* application *) |
176 |
184 |
177 fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) |
185 fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) |
178 | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; |
186 | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; |