23: # 861 "./lpsrc/flx_types.ipk" 24: type dir_t = 25: | DIR_open of ivs_list_t * qualified_name_t 26: | DIR_inject_module of qualified_name_t 27: | DIR_use of id_t * qualified_name_t 28: 29: type dcl_t = 30: [ 31: 32: (* data structures *) 33: | `DCL_axiom of params_t * axiom_method_t 34: | `DCL_lemma of params_t * axiom_method_t 35: | `DCL_reduce of simple_parameter_t list * expr_t * expr_t 36: | `DCL_function of params_t * typecode_t * property_t list * asm_t list 37: | `DCL_union of (id_t * int option * vs_list_t * typecode_t) list 38: | `DCL_struct of (id_t * typecode_t) list 39: | `DCL_cstruct of (id_t * typecode_t) list 40: | `DCL_cclass of class_member_t list 41: | `DCL_typeclass of asm_t list 42: | `DCL_match_check of pattern_t * (string * int) 43: | `DCL_match_handler of pattern_t * (string * int) * asm_t list 44: | `DCL_glr of typecode_t * (reduced_production_t * expr_t) 45: 46: (* variables *) 47: | `DCL_val of typecode_t 48: | `DCL_var of typecode_t 49: | `DCL_lazy of typecode_t * expr_t 50: | `DCL_ref of typecode_t 51: | `DCL_type_alias of typecode_t 52: | `DCL_inherit of qualified_name_t 53: | `DCL_inherit_fun of qualified_name_t 54: 55: (* module system *) 56: | `DCL_module of asm_t list 57: | `DCL_class of asm_t list 58: | `DCL_instance of qualified_name_t * asm_t list 59: 60: (* binding structures [prolog] *) 61: | `DCL_newtype of typecode_t 62: | `DCL_abs of type_qual_t list * c_t * named_req_expr_t 63: | `DCL_const of typecode_t * c_t * named_req_expr_t 64: | `DCL_fun of property_t list * typecode_t list * typecode_t * c_t * named_req_expr_t * prec_t 65: | `DCL_callback of property_t list * typecode_t list * typecode_t * named_req_expr_t 66: | `DCL_insert of c_t * ikind_t * named_req_expr_t 67: | `DCL_regdef of regexp_t 68: | `DCL_regmatch of (regexp_t * expr_t) list 69: | `DCL_reglex of (regexp_t * expr_t) list 70: ] 71: 72: and access_t = [`Private | `Public ] 73: 74: and asm_t = 75: [ 76: | `Exe of range_srcref * exe_t 77: | `Dcl of range_srcref * id_t * int option * access_t * vs_list_t * dcl_t 78: | `Iface of range_srcref * iface_t 79: | `Dir of dir_t 80: ] 81: 82: and iface_t = 83: [ 84: | `IFACE_export_fun of suffixed_name_t * string 85: | `IFACE_export_type of typecode_t * string 86: ] 87: 88: (** value typing *) 89: type 't b0typecode_t' = 90: [ 91: | `BTYP_inst of bid_t * 't list 92: | `BTYP_tuple of 't list 93: | `BTYP_record of (string * 't) list 94: | `BTYP_variant of (string * 't) list 95: | `BTYP_unitsum of int 96: | `BTYP_sum of 't list 97: | `BTYP_function of 't * 't 98: | `BTYP_cfunction of 't * 't 99: | `BTYP_pointer of 't 100: | `BTYP_lvalue of 't 101: | `BTYP_array of 't * 't 102: | `BTYP_void 103: | `BTYP_fix of int 104: | `BTYP_intersect of 't list (** intersection type *) 105: ] 106: 107: type 't btpattern_t' = { 108: pattern: 't; 109: pattern_vars: IntSet.t; (* pattern type variables, including 'any' vars *) 110: assignments : (int * 't) list (* assignments for 'as' vars *) 111: } 112: 113: 114: (** meta typing *) 115: type 't b1typecode_t' = 116: [ 117: | `BTYP_var of int * 't 118: | `BTYP_apply of 't * 't 119: | `BTYP_typefun of (int * 't) list * 't * 't 120: | `BTYP_type of int 121: | `BTYP_type_tuple of 't list 122: | `BTYP_type_match of 't * ('t btpattern_t' * 't) list 123: 124: (* type sets *) 125: | `BTYP_typeset of 't list (** open union *) 126: | `BTYP_typesetunion of 't list (** open union *) 127: | `BTYP_typesetintersection of 't list (** open union *) 128: 129: (* Barry Jay pattern calculus *) 130: | `BTYP_case of 't * IntSet.t * 't 131: 132: | `BTYP_lift of 't (* lift type to metatype *) 133: ] 134: 135: (** general typing *) 136: type 't btypecode_t' = 137: [ 138: | 't b0typecode_t' 139: | 't b1typecode_t' 140: ] 141: 142: type b0typecode_t = 't b0typecode_t' as 't 143: type btypecode_t = 't btypecode_t' as 't 144: type btpattern_t = btypecode_t btpattern_t' 145: 146: type entry_kind_t = { 147: base_sym:int; (* the function *) 148: spec_vs:(string * int) list; (* the type variables of the specialisation *) 149: sub_ts:btypecode_t list (* types to replace the old type variables 150: expressed in terms of the new ones 151: *) 152: } 153: 154: and entry_set_t = 155: [ 156: | `FunctionEntry of entry_kind_t list 157: | `NonFunctionEntry of entry_kind_t 158: ] 159: 160: and module_rep_t = 161: | Simple_module of bid_t * typecode_t list * name_map_t * dir_t list 162: 163: and name_map_t = (string, entry_set_t) Hashtbl.t 164: 165: 166: type biface_t = 167: [ 168: | `BIFACE_export_fun of range_srcref * bid_t * string 169: | `BIFACE_export_type of range_srcref * btypecode_t * string 170: ] 171: 172: type regular_args_t = 173: int list * (* alphabet *) 174: int * (* state count *) 175: (int, tbexpr_t) Hashtbl.t * (* state->expression map *) 176: (int * int, int) Hashtbl.t (* transition matrix *) 177: 178: and bexe_t = 179: [ 180: | `BEXE_label of range_srcref * string 181: | `BEXE_comment of range_srcref * string (* for documenting generated code *) 182: | `BEXE_halt of range_srcref * string (* for internal use only *) 183: | `BEXE_goto of range_srcref * string (* for internal use only *) 184: | `BEXE_ifgoto of range_srcref * tbexpr_t * string (* for internal use only *) 185: | `BEXE_ifnotgoto of range_srcref * tbexpr_t * string (* for internal use only *) 186: | `BEXE_call of range_srcref * tbexpr_t * tbexpr_t 187: | `BEXE_call_direct of range_srcref * bid_t * btypecode_t list * tbexpr_t 188: | `BEXE_call_method_direct of range_srcref * tbexpr_t * bid_t * btypecode_t list * tbexpr_t 189: | `BEXE_call_method_stack of range_srcref * tbexpr_t * bid_t * btypecode_t list * tbexpr_t 190: | `BEXE_call_stack of range_srcref * bid_t * btypecode_t list * tbexpr_t 191: | `BEXE_call_prim of range_srcref * bid_t * btypecode_t list * tbexpr_t 192: | `BEXE_jump of range_srcref * tbexpr_t * tbexpr_t 193: | `BEXE_jump_direct of range_srcref * bid_t * btypecode_t list * tbexpr_t 194: | `BEXE_loop of range_srcref * int * tbexpr_t 195: | `BEXE_svc of range_srcref * bid_t 196: | `BEXE_fun_return of range_srcref * tbexpr_t 197: | `BEXE_yield of range_srcref * tbexpr_t 198: | `BEXE_proc_return of range_srcref 199: | `BEXE_nop of range_srcref * string 200: | `BEXE_code of range_srcref * c_t 201: | `BEXE_nonreturn_code of range_srcref * c_t 202: | `BEXE_assign of range_srcref * tbexpr_t * tbexpr_t 203: | `BEXE_init of range_srcref * bid_t * tbexpr_t 204: | `BEXE_begin 205: | `BEXE_end 206: | `BEXE_assert of range_srcref * tbexpr_t 207: | `BEXE_assert2 of range_srcref * range_srcref * tbexpr_t option * tbexpr_t 208: | `BEXE_axiom_check of range_srcref * tbexpr_t 209: 210: | `BEXE_apply_ctor of range_srcref * bid_t * bid_t * btypecode_t list * bid_t * tbexpr_t 211: | `BEXE_apply_ctor_stack of range_srcref * bid_t * bid_t * btypecode_t list * bid_t * tbexpr_t 212: (* For classes! Note this case works as so: 213: * arg0 denotes a variable to store the closure pointer in 214: * arg1 and 2 denote the closure to be created, 215: * arg3 and 4 s a procedure call executed in the 216: context of the closure to initialise the frame. 217: * The expression just returns the initialised closure. 218: * This is rougly equivalent to (in Ocaml notation): 219: 220: let frame = closure (arg1,arg2) in 221: closure(arg3,arg2).call(arg4).run(); 222: closure 223: 224: except that the second closure create takes 225: the first as its parent. This combinator is 226: needed to intervene in the construction of 227: the display (list of environment pointers) 228: to ensure that the first closure is passed 229: as a display variable to the second, so that 230: the class constructor can refer to the class object 231: as its parent, that is, so references to member variables 232: resolve correctly to the instance object. 233: 234: NOTE: the stack version applies to the constructor procedure 235: NOT the class, which is always heaped 236: *) 237: ] 238: 239: and bexpr_t = 240: [ 241: | `BEXPR_parse of tbexpr_t * int list 242: | `BEXPR_deref of tbexpr_t 243: | `BEXPR_name of bid_t * btypecode_t list 244: | `BEXPR_ref of bid_t * btypecode_t list 245: | `BEXPR_new of tbexpr_t 246: | `BEXPR_literal of literal_t 247: | `BEXPR_apply of tbexpr_t * tbexpr_t 248: | `BEXPR_apply_prim of bid_t * btypecode_t list * tbexpr_t 249: | `BEXPR_apply_direct of bid_t * btypecode_t list * tbexpr_t 250: | `BEXPR_apply_stack of bid_t * btypecode_t list * tbexpr_t 251: | `BEXPR_apply_method_direct of tbexpr_t * bid_t * btypecode_t list * tbexpr_t 252: | `BEXPR_apply_method_stack of tbexpr_t * bid_t * btypecode_t list * tbexpr_t 253: | `BEXPR_apply_struct of bid_t * btypecode_t list * tbexpr_t 254: 255: | `BEXPR_tuple of tbexpr_t list 256: | `BEXPR_record of (string * tbexpr_t) list 257: | `BEXPR_variant of string * tbexpr_t 258: | `BEXPR_get_n of int * tbexpr_t (* tuple projection *) 259: | `BEXPR_get_named of int * tbexpr_t (* struct/class projection *) 260: | `BEXPR_closure of bid_t * btypecode_t list 261: | `BEXPR_method_closure of tbexpr_t * bid_t * btypecode_t list 262: | `BEXPR_case of int * btypecode_t 263: | `BEXPR_match_case of int * tbexpr_t 264: | `BEXPR_case_arg of int * tbexpr_t 265: | `BEXPR_case_index of tbexpr_t 266: | `BEXPR_expr of string * btypecode_t 267: | `BEXPR_range_check of tbexpr_t * tbexpr_t * tbexpr_t 268: | `BEXPR_coerce of tbexpr_t * btypecode_t 269: ] 270: 271: and tbexpr_t = bexpr_t * btypecode_t 272: 273: and glr_symbol_t = [`Term of int | `Nonterm of int list] 274: and bglr_entry_t = string option * glr_symbol_t 275: and bproduction_t = bglr_entry_t list 276: 277: and bparameter_t = {pkind:param_kind_t; pid:string; pindex:int; ptyp:btypecode_t} 278: and breqs_t = (bid_t * btypecode_t list) list 279: and bvs_t = (string * int) list 280: and bparams_t = bparameter_t list * tbexpr_t option 281: and bclass_member_t = [ 282: | `BMemberVal of id_t * btypecode_t 283: | `BMemberVar of id_t * btypecode_t 284: | `BMemberFun of id_t * bvs_t * btypecode_t 285: | `BMemberProc of id_t * bvs_t * btypecode_t 286: | `BMemberCtor of id_t * btypecode_t 287: ] 288: 289: and btype_qual_t = [ 290: | base_type_qual_t 291: | `Bound_needs_shape of btypecode_t 292: ] 293: 294: and bbdcl_t = 295: [ 296: | `BBDCL_function of property_t list * bvs_t * bparams_t * btypecode_t * bexe_t list 297: | `BBDCL_procedure of property_t list * bvs_t * bparams_t * bexe_t list 298: | `BBDCL_val of bvs_t * btypecode_t 299: | `BBDCL_var of bvs_t * btypecode_t 300: | `BBDCL_ref of bvs_t * btypecode_t 301: | `BBDCL_tmp of bvs_t * btypecode_t 302: | `BBDCL_glr of property_t list * bvs_t * btypecode_t * (bproduction_t * bexe_t list) 303: | `BBDCL_regmatch of property_t list * bvs_t * bparams_t * btypecode_t * regular_args_t 304: | `BBDCL_reglex of property_t list * bvs_t * bparams_t * int * btypecode_t * regular_args_t 305: 306: (* binding structures [prolog] *) 307: | `BBDCL_newtype of bvs_t * btypecode_t 308: | `BBDCL_abs of bvs_t * btype_qual_t list * c_t * breqs_t 309: | `BBDCL_const of bvs_t * btypecode_t * c_t * breqs_t 310: | `BBDCL_fun of property_t list * bvs_t * btypecode_t list * btypecode_t * c_t * breqs_t * prec_t 311: | `BBDCL_callback of property_t list * bvs_t * btypecode_t list * btypecode_t list * int * btypecode_t * breqs_t * prec_t 312: | `BBDCL_proc of property_t list * bvs_t * btypecode_t list * c_t * breqs_t 313: | `BBDCL_insert of bvs_t * c_t * ikind_t * breqs_t 314: 315: | `BBDCL_union of bvs_t * (id_t * int * btypecode_t) list 316: | `BBDCL_struct of bvs_t * (id_t * btypecode_t) list 317: | `BBDCL_cstruct of bvs_t * (id_t * btypecode_t) list 318: | `BBDCL_cclass of bvs_t * bclass_member_t list 319: | `BBDCL_class of property_t list * bvs_t 320: | `BBDCL_typeclass of property_t list * bvs_t 321: | `BBDCL_instance of property_t list * 322: bvs_t * 323: btypecode_t (* constraint *) * 324: bid_t * 325: btypecode_t list 326: | `BBDCL_nonconst_ctor of bvs_t * int * btypecode_t * int * btypecode_t * 327: bvs_t * btypecode_t (* existentials and constraint for GADTs *) 328: ] 329: 330: and baxiom_method_t = [`BPredicate of tbexpr_t | `BEquation of tbexpr_t * tbexpr_t] 331: and reduction_t = id_t * bvs_t * bparameter_t list * tbexpr_t * tbexpr_t 332: and axiom_t = id_t * range_srcref * int option * axiom_kind_t * bvs_t * bparams_t * baxiom_method_t 333: 334: and typevarmap_t = (int,btypecode_t) Hashtbl.t 335: 336: type env_t = (bid_t * id_t * name_map_t * name_map_t list) list 337: 338: type symbol_definition_t = 339: [ 340: | `SYMDEF_newtype of typecode_t 341: | `SYMDEF_abs of type_qual_t list * c_t * named_req_expr_t 342: | `SYMDEF_regdef of regexp_t 343: | `SYMDEF_regmatch of params_t * (regexp_t * expr_t) list 344: | `SYMDEF_reglex of params_t * int * (regexp_t * expr_t) list 345: | `SYMDEF_glr of typecode_t * (reduced_production_t * sexe_t list) 346: 347: | `SYMDEF_parameter of param_kind_t * typecode_t 348: | `SYMDEF_typevar of typecode_t (* usually type TYPE *) 349: 350: | `SYMDEF_axiom of params_t * axiom_method_t 351: | `SYMDEF_lemma of params_t * axiom_method_t 352: | `SYMDEF_reduce of parameter_t list * expr_t * expr_t 353: | `SYMDEF_function of params_t * typecode_t * property_t list * sexe_t list 354: 355: | `SYMDEF_match_check of pattern_t * (string *int) 356: | `SYMDEF_module 357: | `SYMDEF_class 358: 359: | `SYMDEF_const_ctor of int * typecode_t * int * ivs_list_t 360: | `SYMDEF_nonconst_ctor of int * typecode_t * int * ivs_list_t * typecode_t 361: 362: | `SYMDEF_const of typecode_t * c_t * named_req_expr_t 363: | `SYMDEF_var of typecode_t 364: | `SYMDEF_val of typecode_t 365: | `SYMDEF_ref of typecode_t 366: | `SYMDEF_lazy of typecode_t * expr_t 367: | `SYMDEF_fun of property_t list * typecode_t list * typecode_t * c_t * named_req_expr_t * prec_t 368: | `SYMDEF_callback of property_t list * typecode_t list * typecode_t * named_req_expr_t 369: | `SYMDEF_insert of c_t * ikind_t * named_req_expr_t 370: | `SYMDEF_union of (id_t * int * vs_list_t * typecode_t) list 371: | `SYMDEF_struct of (id_t * typecode_t) list 372: | `SYMDEF_cstruct of (id_t * typecode_t) list 373: | `SYMDEF_cclass of class_member_t list 374: | `SYMDEF_typeclass 375: | `SYMDEF_type_alias of typecode_t 376: | `SYMDEF_inherit of qualified_name_t 377: | `SYMDEF_inherit_fun of qualified_name_t 378: | `SYMDEF_instance of qualified_name_t 379: ] 380: 381: type symbol_data_t = { 382: id:string; 383: sr:range_srcref; 384: parent:int option; 385: vs:ivs_list_t; 386: pubmap:name_map_t; 387: privmap:name_map_t; 388: dirs:dir_t list; 389: symdef:symbol_definition_t; 390: } 391: 392: type symbol_table_t = (int, symbol_data_t) Hashtbl.t 393: 394: type symbol_data3_t = string * int option * range_srcref * bbdcl_t 395: type fully_bound_symbol_table_t = (int, symbol_data3_t) Hashtbl.t 396: 397: type type_registry_t = (btypecode_t,int) Hashtbl.t 398: