type-assert, subtypematch.

src/compiler/flx_bind/flx_bind_bexe.ml

@@ -262,9 +262,17 @@ print_endline ("Bind_exe, return type " ^ Flx_print.sbt bsym_table state.ret_typ
     let result = try Some (bind_exe' state bsym_table (sr, x)) with _ -> None
     in begin match result with
     | None -> []
-    | Some _ -> clierrx "[flx_bind/flx_bind_bexe.ml:295: E15] " sr ("type_error expected, statement compiled! " ^ string_of_exe 0 exe);
+    | Some _ -> clierrx "[flx_bind/flx_bind_bexe.ml:265: E15] " sr ("type_error expected, statement compiled! " ^ string_of_exe 0 exe);
     end
 
+  | EXE_type_assert x ->
+    let result = try Some (bind_exe' state bsym_table (sr, x)) with _ -> None
+    in begin match result with
+    | Some _ -> []
+    | None -> clierrx "[flx_bind/flx_bind_bexe.ml:272: E15a] " sr ("type-assert failed to compile! " ^ string_of_exe 0 exe);
+    end
+
+
   | EXE_label s ->
       state.reachable <- true;
       let maybe_index = lookup_label_in_env state.lookup_state bsym_table state.env sr s in

src/compiler/flx_bind/flx_bind_expression.ml

@@ -151,6 +151,7 @@ let rec bind_expression'
   | EXPR_vsprintf _
   | EXPR_interpolate _
   | EXPR_type_match _
+  | EXPR_subtype_match _
   | EXPR_noexpand _
   | EXPR_letin _
   | EXPR_typeof _

src/compiler/flx_bind/flx_bind_type.ml

@@ -291,6 +291,11 @@ print_endline ("Calling Flx_beta.adjust, possibly incorrectly, type = " ^ sbt bs
     let t = bt t in
     bind_type_match bsym_table state.counter bt btp params sr t ps ubt 
 
+  | TYP_subtype_match (t,ps) as ubt ->
+    let t = bt t in
+    bind_subtype_match bsym_table state.counter bt btp params sr t ps ubt 
+
+
   | TYP_dual t -> Flx_btype_dual.dual (bt t)
 
   | TYP_ellipsis ->

src/compiler/flx_bind/flx_guess_meta_type.ml

@@ -94,6 +94,7 @@ let rec guess_metatype sr t : kind =
 
   | TYP_apply _
 
+  | TYP_subtype_match _
   | TYP_type_match _
   | TYP_patany _
     -> print_endline ("Woops, dunno meta type of " ^ string_of_typecode t); kind_type

src/compiler/flx_bind/flx_metatype.ml

@@ -174,6 +174,7 @@ print_endline ("Metatyping term " ^ st term);
   | BTYP_union _
   | BTYP_polyrecord (_, _)
   | BTYP_type_match (_, _)
+  | BTYP_subtype_match (_, _)
   | BTYP_tuple_cons (_, _)
   | BTYP_tuple_snoc (_, _)
   | BTYP_unitsum _ -> kind_type

src/compiler/flx_bind/flx_tpat.ml

@@ -170,4 +170,77 @@ let bind_type_match bsym_table counter bt btp params sr t ps ubt =
 
   btyp_type_match (t,pts)
 
+let bind_subtype_match bsym_table counter bt btp params sr t ps ubt =
+  let pts = ref [] in
+  let finished = ref false in
+  List.iter begin fun (p',t') ->
+    let p',explicit_vars,any_vars, as_vars, eqns =
+      type_of_tpattern counter p'
+    in
+    let p' = bt p' in
+    let eqns = List.map (fun (j,t) -> j, bt t) eqns in
+    let varset =
+      let x = List.fold_left
+        (fun s (i,_) -> BidSet.add i s)
+        BidSet.empty explicit_vars
+      in
+      List.fold_left (fun s i -> BidSet.add i s)
+      x any_vars
+    in
+
+    (* HACK! GACK! we have to assume a variable in a pattern is is a TYPE
+     * variable .. type patterns don't include coercion terms at the moment,
+     * so there isn't any way to even specify the metatype In some contexts
+     * the kinding can be infered, for example:
+     *
+     * int * ?x
+     *
+     * clearly x has to be a type .. but a lone type variable would require
+     * the argument typing to be known ... no notation for that yet either
+     * *)
+    let args = List.map (fun (i,s) ->
+    s, btyp_type_var (i,btyp_type 0)) (explicit_vars @ as_vars)
+    in
+    let t' = btp t' (params@args) in
+    let t' = list_subst counter eqns t' in
+    pts := ({pattern=p'; pattern_vars=varset; assignments=eqns},t') :: !pts;
+    let u = maybe_specialisation bsym_table counter [p', t] in
+    match u with
+    | None ->  ()
+        (* CRAP! The below argument is correct BUT ..  our unification
+         * algorithm isn't strong enough ...  so just let this thru and hope
+         * it is reduced later on instantiation
+         *)
+        (* If the initially bound, context free pattern can never unify with
+         * the argument, we have a choice: chuck an error, or just eliminate
+         * the match case -- I'm going to chuck an error for now, because I
+         * don't see why one would ever code such a case, except as a
+         * mistake. *)
+        (*
+        clierrx "[flx_bind/flx_tpat.ml:145: E262] " sr
+          ("[bind_type'] type match argument\n" ^
+          sbt bsym_table t ^
+          "\nwill never unify with pattern\n" ^
+          sbt bsym_table p'
+          )
+        *)
+    | Some mgu ->
+        if !finished then begin
+(*
+          print_endline "[bind_type] Warning: useless match case in typematch ignored:";
+          print_endline (Flx_srcref.short_string_of_src sr);
+          print_endline (string_of_typecode ubt);
+*)
+        end
+        else
+          let mguvars = List.fold_left
+            (fun s (i,_) -> BidSet.add i s)
+            BidSet.empty mgu
+          in
+          if varset = mguvars then finished := true
+  end ps;
+  let pts = List.rev !pts in
+
+  btyp_subtype_match (t,pts)
+
 

src/compiler/flx_core/flx_ast.ml

@@ -111,6 +111,7 @@ and typecode_t =
   | TYP_type_tuple of typecode_t list          (** meta type product *)
 
   | TYP_type_match of typecode_t * (typecode_t * typecode_t) list
+  | TYP_subtype_match of typecode_t * (typecode_t * typecode_t) list
   | TYP_type_extension of Flx_srcref.t * typecode_t list * typecode_t
   | TYP_tuple_cons of Flx_srcref.t * typecode_t * typecode_t
   | TYP_tuple_snoc of Flx_srcref.t * typecode_t * typecode_t
@@ -242,6 +243,7 @@ and expr_t =
   | EXPR_expr of Flx_srcref.t * Flx_code_spec.t * typecode_t * expr_t
 
   | EXPR_type_match of Flx_srcref.t * (typecode_t * (typecode_t * typecode_t) list)
+  | EXPR_subtype_match of Flx_srcref.t * (typecode_t * (typecode_t * typecode_t) list)
   | EXPR_typecase_match of Flx_srcref.t * (typecode_t * (typecode_t * expr_t) list)
 
   | EXPR_extension of Flx_srcref.t * expr_t list * expr_t
@@ -421,6 +423,7 @@ and connection_t =
 and statement_t =
   | STMT_circuit of Flx_srcref.t * connection_t list
   | STMT_type_error of Flx_srcref.t * statement_t
+  | STMT_type_assert of Flx_srcref.t * statement_t
   | STMT_cgoto of Flx_srcref.t * expr_t
   | STMT_ifcgoto of Flx_srcref.t * expr_t * expr_t
   | STMT_try of Flx_srcref.t 
@@ -676,6 +679,7 @@ and statement_t =
 type exe_t =
   | EXE_circuit of connection_t list
   | EXE_type_error of exe_t
+  | EXE_type_assert of exe_t
   | EXE_code of CS.t * expr_t (* for inline C++ code *)
   | EXE_noreturn_code of CS.t * expr_t  (* for inline C++ code *)
   | EXE_comment of string (* for documenting generated code *)
@@ -777,6 +781,7 @@ let src_of_typecode = function
   | TYP_typefun _
   | TYP_type_tuple _
   | TYP_type_match _
+  | TYP_subtype_match _
   -> Flx_srcref.dummy_sr
 
 let src_of_expr (e : expr_t) = match e with
@@ -849,6 +854,7 @@ let src_of_expr (e : expr_t) = match e with
   | EXPR_as_var (s,_)
   | EXPR_match (s, _)
   | EXPR_type_match (s, _)
+  | EXPR_subtype_match (s, _)
   | EXPR_typecase_match (s, _)
   | EXPR_cond (s,_)
   | EXPR_expr (s,_,_,_)
@@ -873,6 +879,7 @@ let src_of_stmt (e : statement_t) = match e with
   | STMT_virtual_type (s,_)
   | STMT_circuit (s,_)
   | STMT_type_error (s,_)
+  | STMT_type_assert (s,_)
   | STMT_try s
   | STMT_endtry s
   | STMT_catch (s,_,_)

src/compiler/flx_core/flx_beta.ml

@@ -590,6 +590,7 @@ print_endline ("Calculated isrec= " ^ if isrec then "true" else "false");
     end
 
   | BTYP_type_match (tt,pts) ->
+  begin
 (*
     print_endline ("Typematch [before reduction] " ^ sbt bsym_table t ^ "=" ^ Flx_btype.st t);
 *)
@@ -621,7 +622,9 @@ print_endline ("Calculated isrec= " ^ if isrec then "true" else "false");
     let pts = List.rev !new_matches in
     match pts with
     | [] ->
+      (*
       print_endline ("[beta-reduce] typematch failure " ^ sbt bsym_table t);
+      *)
       t 
 
     | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
@@ -638,3 +641,59 @@ print_endline ("Calculated isrec= " ^ if isrec then "true" else "false");
         adjust bsym_table t'
       with Not_found -> btyp_type_match (tt,pts)
 
+  end
+  | BTYP_subtype_match (tt,pts) ->
+  begin
+(*
+    print_endline ("Typematch [before reduction] " ^ sbt bsym_table t ^ "=" ^ Flx_btype.st t);
+*)
+    let tt = br tt in
+    let new_matches = ref [] in
+    List.iter (fun ({pattern=p; pattern_vars=dvars; assignments=eqns}, t') ->
+      (*
+      print_endline (spc ^"Tring to unify argument with " ^
+        sbt bsym_table p');
+      *)
+      let p =  br p in
+      let x =
+        {
+          pattern=p;
+          assignments=List.map (fun (j,t) -> j, br t) eqns;
+          pattern_vars=dvars;
+        }, t'
+      in
+      match maybe_specialisation bsym_table counter [p,tt] with
+      | Some _ -> new_matches := x :: !new_matches
+      | None ->
+        (*
+        print_endline (spc ^"Discarding pattern " ^ sbt bsym_table p');
+        *)
+        ()
+    )
+    pts
+    ;
+    let pts = List.rev !new_matches in
+    match pts with
+    | [] ->
+      (*
+      print_endline ("[beta-reduce] typematch failure " ^ sbt bsym_table t);
+      *)
+      t 
+
+    | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
+      let maybe_mgu = maybe_specialisation_with_dvars bsym_table counter [p', tt] dvars in
+      begin match maybe_mgu with
+      | Some mgu ->
+        (*
+        print_endline "Typematch success";
+        *)
+        let t' = list_subst counter (mgu @ eqns) t' in
+        let t' = br t' in
+        (*
+        print_endline ("type match reduction result=" ^ sbt bsym_table t');
+        *)
+        adjust bsym_table t'
+      | None -> btyp_subtype_match (tt,pts)
+      end
+  end
+

src/compiler/flx_core/flx_btype.ml

@@ -68,6 +68,7 @@ and t =
   *)
   | BTYP_type_map of t * t
   | BTYP_type_match of t * (btpattern_t * t) list
+  | BTYP_subtype_match of t * (btpattern_t * t) list
 
   | BTYP_tuple_cons of t * t 
   | BTYP_tuple_snoc of t * t 
@@ -167,6 +168,15 @@ and str_of_btype typ =
     let cases = String.concat "\n  | " (List.map (fun (p,t) -> sp p ^ " => " ^ s t) pats) in
     "BTYP_type_match("^s v^",(\n" ^cases ^ "\n))\n"
 
+  | BTYP_subtype_match (v,pats) -> 
+    let sa (i,t) = string_of_int i ^ " <- " ^ s t in
+    let sas a = catmap ", " sa a in
+    let sbs pvs = BidSet.fold (fun i acc -> (if acc="" then "" else acc ^ "," ) ^ string_of_int i) pvs "" in
+    let sp {pattern=pat; pattern_vars=pvs; assignments=a; }  = "forall " ^ sbs pvs ^ ". " ^ s pat ^ " with " ^ sas a in
+    let cases = String.concat "\n  | " (List.map (fun (p,t) -> sp p ^ " => " ^ s t) pats) in
+    "BTYP_subtype_match("^s v^",(\n" ^cases ^ "\n))\n"
+
+
   | BTYP_type_map (f,t) -> "BTYP_type_map(" ^ s f ^"," ^s t^")"
 
   | BTYP_tuple_cons (h,t) -> "BTYP_tuple_cons (" ^ s h ^"**" ^ s t^")"
@@ -230,6 +240,7 @@ let complete_type t =
     | BTYP_rev t -> uf t
     | BTYP_uniq t -> uf t
 
+    | BTYP_subtype_match (a,tts)
     | BTYP_type_match (a,tts) ->
         uf a;
         List.iter (fun (p,x) -> uf x) tts
@@ -488,6 +499,10 @@ let btyp_type_map (f,a) =
 let btyp_type_match (t, ps) =
   BTYP_type_match (t, ps)
 
+let btyp_subtype_match (t, ps) =
+  BTYP_subtype_match (t, ps)
+
+
 (** Construct a BTYP_type_set type. *)
 let btyp_type_set ts =
   BTYP_type_set ts
@@ -640,6 +655,8 @@ let flat_iter
        * bid. *)
   | BTYP_type_apply (a,b) -> f_btype a; f_btype b
   | BTYP_type_map (a,b) -> f_btype a; f_btype b
+
+  | BTYP_subtype_match (t,ps)
   | BTYP_type_match (t,ps) ->
       f_btype t;
       List.iter begin fun (tp, t) ->
@@ -732,6 +749,20 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) = function
         end ps
       in
       btyp_type_match (f_btype t, ps)
+
+  | BTYP_subtype_match (t,ps) ->
+      let ps =
+        List.map begin fun (tp, t) ->
+          { tp with
+            pattern = f_btype tp.pattern;
+            assignments = List.map
+              (fun (i, t) -> f_bid i, f_btype t)
+              tp.assignments },
+          f_btype t
+        end ps
+      in
+      btyp_subtype_match (f_btype t, ps)
+
   | BTYP_type_set ts ->
       let g acc elt =
         (* SHOULD USE UNIFICATIION! *)
@@ -915,7 +946,14 @@ and unfold msg t =
          * they mean *)
         let tts = List.map (fun (p,x) -> p,uf x) tts in
         btyp_type_match (a,tts)
-
+
+     | BTYP_subtype_match (a,tts) ->
+        let a = uf a in
+        (* don't unfold recursions in patterns yet because we don't know what
+         * they mean *)
+        let tts = List.map (fun (p,x) -> p,uf x) tts in
+        btyp_subtype_match (a,tts)
+
     | _ -> t'
   in aux 0 t
 

src/compiler/flx_core/flx_btype.mli

@@ -46,6 +46,7 @@ and t = private
   | BTYP_type_apply of t * t
   | BTYP_type_map of t * t
   | BTYP_type_match of t * (btpattern_t * t) list
+  | BTYP_subtype_match of t * (btpattern_t * t) list
   | BTYP_tuple_cons of t * t
   | BTYP_tuple_snoc of t * t
   | BTYP_type_set of t list
@@ -127,6 +128,7 @@ val btyp_type_var : bid_t * kind -> t
 val btyp_type_apply : t * t -> t
 val btyp_type_map : t * t -> t
 val btyp_type_match : t * (btpattern_t * t) list -> t
+val btyp_subtype_match : t * (btpattern_t * t) list -> t
 val btyp_type_set : t list -> t
 val btyp_type_set_union : t list -> t
 val btyp_type_set_intersection : t list -> t

src/compiler/flx_core/flx_btype_rec.ml

@@ -83,6 +83,7 @@ let fix i t =
     | BTYP_type_function _
     | BTYP_type_tuple _
     | BTYP_type_match _
+    | BTYP_subtype_match _
     | BTYP_type_set_union _ -> t
     | BTYP_type_set_intersection _ -> t
   in

src/compiler/flx_core/flx_fold.ml

@@ -66,6 +66,7 @@ let fold (bsym_table: Flx_bsym_table.t) counter t =
     | BTYP_type_function _
     | BTYP_type_tuple _
     | BTYP_type_match _ -> () (* assume fixpoint can't span these boundaries *)
+    | BTYP_subtype_match _ -> () (* assume fixpoint can't span these boundaries *)
       (* failwith ("[fold] unexpected metatype " ^ sbt sym_table t') *)
   in
     try aux [] 0 t; t