1signature Parse_support = 2sig 3 type pretype = Pretype.pretype 4 type preterm = Preterm.preterm 5 type term = Term.term 6 7 type env = Parse_supportENV.env 8 type preterm_in_env = preterm Parse_supportENV.PSM 9 type bvar_in_env = env -> (preterm -> preterm) * env 10 type overload_info = term_grammar.overload_info 11 12 val gen_overloaded_const : overload_info -> locn.locn -> string -> 13 preterm_in_env 14 val make_preterm : preterm_in_env -> preterm Pretype.in_env 15 val make_aq : locn.locn -> term -> preterm_in_env 16 val make_binding_occ : locn.locn -> string -> bvar_in_env 17 val make_aq_binding_occ : locn.locn -> term -> bvar_in_env 18 val make_atom : overload_info -> locn.locn -> 19 string -> preterm_in_env 20 val make_qconst : locn.locn -> string * string -> preterm_in_env 21 val list_make_comb : locn.locn -> preterm_in_env list -> preterm_in_env 22 val bind_term : locn.locn -> bvar_in_env list -> 23 preterm_in_env -> preterm_in_env 24 val make_vstruct : overload_info -> locn.locn -> bvar_in_env list -> 25 pretype option -> bvar_in_env 26 val make_constrained : locn.locn -> preterm_in_env -> pretype -> 27 preterm_in_env 28 val make_let : overload_info -> locn.locn -> 29 (bvar_in_env list * preterm_in_env) list -> 30 preterm_in_env -> preterm_in_env 31 val make_set_abs : overload_info -> locn.locn -> 32 preterm_in_env * preterm_in_env -> 33 preterm_in_env 34 35 val make_case_arrow : overload_info -> locn.locn -> 36 preterm_in_env -> preterm_in_env -> 37 preterm_in_env 38 39 val binder_restrictions : unit -> (string * string) list 40 val associate_restriction : locn.locn -> string * string -> unit 41 val delete_restriction : locn.locn -> string -> unit 42 43end 44