1 files changed, 105 insertions, 54 deletions

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d9ee73b8..9fcbb8c6 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -28,8 +28,9 @@ let isubst_union s1 s2 =
   |  _,  _ -> None) s1 s2
 
 let subst_src_typ substs t =
-  let rec s_snexp (Nexp_aux (ne,l) as nexp) =
+  let rec s_snexp substs (Nexp_aux (ne,l) as nexp) =
     let re ne = Nexp_aux (ne,l) in
+    let s_snexp = s_snexp substs in
     match ne with
     | Nexp_var (Kid_aux (_,l) as kid) ->
        (try KSubst.find kid substs
@@ -42,22 +43,25 @@ let subst_src_typ substs t =
     | Nexp_exp ne -> re (Nexp_exp (s_snexp ne))
     | Nexp_neg ne -> re (Nexp_neg (s_snexp ne))
   in
-  let rec s_styp ((Typ_aux (t,l)) as ty) =
+  let rec s_styp substs ((Typ_aux (t,l)) as ty) =
     let re t = Typ_aux (t,l) in
     match t with
     | Typ_wild
     | Typ_id _
     | Typ_var _
       -> ty
-    | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp t1, s_styp t2,e))
-    | Typ_tup ts -> re (Typ_tup (List.map s_styp ts))
-    | Typ_app (id,tas) -> re (Typ_app (id,List.map s_starg tas))
-  and s_starg (Typ_arg_aux (ta,l) as targ) =
+    | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp substs t1, s_styp substs t2,e))
+    | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
+    | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
+    | Typ_exist (kids,nc,t) ->
+       let substs = List.fold_left (fun sub v -> KSubst.remove v sub) substs kids in
+       re (Typ_exist (kids,nc,s_styp substs t))
+  and s_starg substs (Typ_arg_aux (ta,l) as targ) =
     match ta with
-    | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (s_snexp ne),l)
-    | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp t),l)
+    | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (s_snexp substs ne),l)
+    | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp substs t),l)
     | Typ_arg_order _ -> targ
-  in s_styp t
+  in s_styp substs t
 
 let make_vector_lit sz i =
   let f j = if (i lsr (sz-j-1)) mod 2 = 0 then '0' else '1' in
@@ -128,6 +132,42 @@ let rec cross = function
      let t' = cross t in
      List.concat (List.map (fun y -> List.map (fun l' -> (x,y)::l') t') l)
 
+let rec cross' = function
+  | [] -> [[]]
+  | (h::t) ->
+     let t' = cross' t in
+     List.concat (List.map (fun x -> List.map (List.cons x) t') h)
+
+let kidset_bigunion = function
+  | [] -> KidSet.empty
+  | h::t -> List.fold_left KidSet.union h t
+
+(* TODO: deal with non-set constraints, intersections, etc somehow *)
+let extract_set_nc var (NC_aux (_,l) as nc) =
+  let rec aux (NC_aux (nc,l)) =
+    let re nc = NC_aux (nc,l) in
+    match nc with
+    | NC_nat_set_bounded (id,is) when Kid.compare id var = 0 -> Some (is,re NC_true)
+    | NC_and (nc1,nc2) ->
+       (match aux nc1, aux nc2 with
+       | None, None -> None
+       | None, Some (is,nc2') -> Some (is, re (NC_and (nc1,nc2')))
+       | Some (is,nc1'), None -> Some (is, re (NC_and (nc1',nc2)))
+       | Some _, Some _ ->
+          raise (Reporting_basic.err_general l ("Multiple set constraints for " ^ string_of_kid var)))
+    | _ -> None
+  in match aux nc with
+  | Some is -> is
+  | None ->
+     raise (Reporting_basic.err_general l ("No set constraint for " ^ string_of_kid var))
+
+
+(* TODO: maybe fold this into subst_src_typ? *)
+let inst_src_type insts ty =
+  let insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) insts in
+  let subst = ksubst_from_list insts in
+  subst_src_typ subst ty
+
 (* Given a type for a constructor, work out which refinements we ought to produce *)
 (* TODO collision avoidance *)
 let split_src_type id ty (TypQ_aux (q,ql)) =
@@ -146,65 +186,55 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
     | Nexp_neg n
       -> size_nvars_nexp n
   in
-  let rec size_nvars_ty (Typ_aux (ty,l)) =
+  let rec size_nvars_ty (Typ_aux (ty,l) as typ) =
     match ty with
     | Typ_wild
     | Typ_id _
     | Typ_var _
-      -> []
+      -> (KidSet.empty,[[],typ])
     | Typ_fn _ ->
        raise (Reporting_basic.err_general l ("Function type in constructor " ^ i))
-    | Typ_tup ts -> List.concat (List.map size_nvars_ty ts)
+    | Typ_tup ts ->
+       let (vars,tys) = List.split (List.map size_nvars_ty ts) in
+       let insttys = List.map (fun x -> let (insts,tys) = List.split x in
+                                        List.concat insts, Typ_aux (Typ_tup tys,l)) (cross' tys) in
+       (kidset_bigunion vars, insttys)
     | Typ_app (Id_aux (Id "vector",_),
                [_;Typ_arg_aux (Typ_arg_nexp sz,_);
                 _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
-       size_nvars_nexp sz
+       (KidSet.of_list (size_nvars_nexp sz), [[],typ])
     | Typ_app (_, tas) ->
-       []  (* We only support sizes for bitvectors mentioned explicitly, not any buried
-              inside another type *)
+       (KidSet.empty,[[],typ])  (* We only support sizes for bitvectors mentioned explicitly, not any buried
+                      inside another type *)
+    | Typ_exist (kids, nc, t) ->
+       let (vars,tys) = size_nvars_ty t in
+       let bound = KidSet.of_list kids in
+       let still_bound = KidSet.diff bound vars in
+       let mono = KidSet.inter bound vars in
+       let free = KidSet.diff vars bound in
+       let (insts,nc') = KidSet.fold (fun k (insts,nc) -> let (is,nc') = extract_set_nc k nc in (List.map (fun i -> (k,i)) is)::insts,nc') mono ([],nc) in
+       let insts = cross' insts in
+       let tys = List.concat (List.map (fun (inst0,ty) ->
+         List.map (fun inst -> (inst@inst0,inst_src_type inst ty)) insts) tys) in
+       let tys = List.map (fun (inst,ty) -> inst,Typ_aux (Typ_exist (KidSet.elements still_bound, nc', ty),l)) tys in
+       (free,tys)
   in
-  let nvars = List.sort_uniq Kid.compare (size_nvars_ty ty) in
-  match nvars with
+  (* TODO: reject universally quantification or monomorphise it *)
+  let (_,variants) = size_nvars_ty ty in
+  match variants with
   | [] -> None
   | sample::__ ->
-     (* Only check for constraints if we found a size to constrain *)
-     let qs =
-       match q with
-       | TypQ_no_forall -> 
-          raise (Reporting_basic.err_general ql
-                   ("No set constraint for variable " ^ string_of_kid sample ^ " in constructor " ^ i))
-       | TypQ_tq qs -> qs
-     in
-     let find_set (Kid_aux (Var nvar,_) as kid) =
-       match list_extract (function
-       | QI_aux (QI_const (NC_aux (NC_nat_set_bounded (Kid_aux (Var nvar',_),vals),_)),_)
-         -> if nvar = nvar' then Some vals else None
-       | _ -> None) qs with
-       | None ->
-          raise (Reporting_basic.err_general ql
-                   ("No set constraint for variable " ^ nvar ^ " in constructor " ^ i))
-       | Some vals -> (kid,vals)
-     in
-     let nvar_sets = List.map find_set nvars in
-     let total_variants = List.fold_left ( * ) 1 (List.map (fun (_,l) -> List.length l) nvar_sets) in
-     let () = if total_variants > size_set_limit then
+     let () = if List.length variants > size_set_limit then
          raise (Reporting_basic.err_general ql
-                  (string_of_int total_variants ^ "variants for constructor " ^ i ^
+                  (string_of_int (List.length variants) ^ "variants for constructor " ^ i ^
                      "bigger than limit " ^ string_of_int size_set_limit)) else ()
      in
-     let variants = cross nvar_sets in
      let wrap = match id with
        | Id_aux (Id i,l) -> (fun f -> Id_aux (Id (f i),Generated l))
        | Id_aux (DeIid i,l) -> (fun f -> Id_aux (DeIid (f i),l))
      in
      let name l i = String.concat "_" (i::(List.map (fun (v,i) -> string_of_kid v ^ string_of_int i) l)) in
-     Some (List.map (fun l -> (l, wrap (name l))) variants)
-
-(* TODO: maybe fold this into subst_src_typ? *)
-let inst_src_type insts ty =
-  let insts = List.map (fun (v,i) -> (v,Nexp_aux (Nexp_constant i,Generated Unknown))) insts in
-  let subst = ksubst_from_list insts in
-  subst_src_typ subst ty
+     Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants)
 
 let reduce_nexp subst ne =
   let rec eval (Nexp_aux (ne,_) as nexp) =
@@ -394,6 +424,7 @@ let bindings_from_pat p =
     | P_typ (_,p) -> aux_pat p
     | P_id id ->
        if pat_id_is_variable env id then [id] else []
+    | P_var kid -> [id_of_kid kid]
     | P_vector ps
     | P_vector_concat ps
     | P_app (_,ps)
@@ -408,7 +439,7 @@ let bindings_from_pat p =
 
 let remove_bound env pat =
   let bound = bindings_from_pat pat in
-  List.fold_left (fun sub v -> ISubst.remove v env) env bound
+  List.fold_left (fun sub v -> ISubst.remove v sub) env bound
 
 (* Remove explicit existential types from the AST, so that the sizes of
    bitvectors will be filled in throughout.
@@ -461,6 +492,8 @@ let rec deexist_exp (E_aux (e,(l,(annot : Type_check.tannot))) as exp) =
   | E_let (lb,e1) -> re (E_let (deexist_letbind lb, deexist_exp e1))
   | E_assign (le,e1) -> re (E_assign (deexist_lexp le, deexist_exp e1))
   | E_exit e1 -> re (E_exit (deexist_exp e1))
+  | E_throw e1 -> re (E_throw (deexist_exp e1))
+  | E_try (e1,cases) -> re (E_try (deexist_exp e1, List.map deexist_pexp cases))
   | E_return e1 -> re (E_return (deexist_exp e1))
   | E_assert (e1,e2) -> re (E_assert (deexist_exp e1,deexist_exp e2))
 and deexist_pexp (Pat_aux (pe,(l,annot))) =
@@ -548,6 +581,13 @@ let can_match (E_aux (e,(l,annot)) as exp0) cases =
      in findpat_generic checkpat "bit" cases
   | _ -> None
 
+(* Remove top-level casts from an expression.  Useful when we need to look at
+   subexpressions to reduce something, but could break type-checking if we used
+   it everywhere. *)
+let rec drop_casts = function
+  | E_aux (E_cast (_,e),_) -> drop_casts e
+  | exp -> exp
+
 
 (* Similarly, simple conditionals *)
 let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) =
@@ -566,8 +606,8 @@ let neq_fns = [Id "neq_anything"]
 let try_app (l,ann) (Id_aux (id,_),args) =
   let is_eq = List.mem id eq_fns in
   let is_neq = (not is_eq) && List.mem id neq_fns in
+  let new_l = Generated l in
   if is_eq || is_neq then
-    let new_l = Generated l in
     match args with
     | [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] ->
        let lit b = if b then L_true else L_false in
@@ -576,6 +616,11 @@ let try_app (l,ann) (Id_aux (id,_),args) =
        | None -> None
        | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann))))
     | _ -> None
+  else if id = Id "cast_bit_bool" then
+    match args with
+    | [E_aux (E_lit L_aux (L_zero,_),_)] -> Some (E_aux (E_lit (L_aux (L_false,new_l)),(l,ann)))
+    | [E_aux (E_lit L_aux (L_one ,_),_)] -> Some (E_aux (E_lit (L_aux (L_true ,new_l)),(l,ann)))
+    | _ -> None
   else None
 
 
@@ -591,7 +636,6 @@ let try_app_infix (l,ann) (E_aux (e1,ann1)) (Id_aux (id,_)) (E_aux (e2,ann2)) =
      | None -> None)
   | _ -> None
 
-
 (* We may need to split up a pattern match if (1) we've been told to case split
    on a variable by the user, or (2) we monomorphised a constructor that's used
    in the pattern. *)
@@ -610,7 +654,7 @@ let split_defs splits defs =
          | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)])
          | Some variants ->
             ([(id,variants)],
-             List.map (fun (insts, id') -> Tu_aux (Tu_ty_id (inst_src_type insts ty,id'),Generated l)) variants))
+             List.map (fun (insts, id', ty) -> Tu_aux (Tu_ty_id (ty,id'),Generated l)) variants))
     in
     let sc_type_def ((TD_aux (tda,annot)) as td) =
       match tda with
@@ -710,7 +754,7 @@ let split_defs splits defs =
     | E_if (e1,e2,e3) ->
        let e1' = const_prop_exp substs e1 in
        let e2',e3' = const_prop_exp substs e2, const_prop_exp substs e3 in
-       (match e1' with
+       (match drop_casts e1' with
        | E_aux (E_lit (L_aux ((L_true|L_false) as lit ,_)),_) ->
           let e' = match lit with L_true -> e2' | _ -> e3' in
           (match e' with E_aux (_,(_,annot')) ->
@@ -745,6 +789,10 @@ let split_defs splits defs =
        re (E_let (lb', const_prop_exp substs' e))
     | E_assign (le,e) -> re (E_assign (const_prop_lexp substs le, const_prop_exp substs e))
     | E_exit e -> re (E_exit (const_prop_exp substs e))
+    | E_throw e -> re (E_throw (const_prop_exp substs e))
+    | E_try (e,cases) ->
+       let e' = const_prop_exp substs e in
+       re (E_case (e', List.map (const_prop_pexp substs) cases))
     | E_return e -> re (E_return (const_prop_exp substs e))
     | E_assert (e1,e2) -> re (E_assert (const_prop_exp substs e1,const_prop_exp substs e2))
     | E_internal_cast (ann,e) -> re (E_internal_cast (ann,const_prop_exp substs e))
@@ -836,7 +884,7 @@ let split_defs splits defs =
       (* Substitute what we've learned about nvars into the term *)
       let nsubsts = isubst_from_list !nexp_substs in
       let () = nexp_substs := [] in
-      nexp_subst_exp nsubsts refinements exp'
+      (*nexp_subst_exp nsubsts refinements*) exp'
   in
     
   (* Split a variable pattern into every possible value *)
@@ -933,6 +981,7 @@ let split_defs splits defs =
         match p with
         | P_lit _
         | P_wild
+        | P_var _
           -> None
         | P_as (p',id) when id_matches id ->
            raise (Reporting_basic.err_general l
@@ -988,7 +1037,7 @@ let split_defs splits defs =
                                 ("Constructor " ^ string_of_id id ^ " is not a construtor!"))
               in
               let varmap = build_nexp_subst l constr_out_typ tannot in
-              let map_inst (insts,id') =
+              let map_inst (insts,id',_) =
                 let insts = List.map (fun (v,i) ->
                   ((match List.assoc (string_of_kid v) varmap with
                   | Nexp_aux (Nexp_var s, _) -> s
@@ -1055,6 +1104,8 @@ let split_defs splits defs =
       | E_let (lb,e) -> re (E_let (map_letbind lb, map_exp e))
       | E_assign (le,e) -> re (E_assign (map_lexp le, map_exp e))
       | E_exit e -> re (E_exit (map_exp e))
+      | E_throw e -> re (E_throw e)
+      | E_try (e,cases) -> re (E_try (map_exp e, List.concat (List.map map_pexp cases)))
       | E_return e -> re (E_return (map_exp e))
       | E_assert (e1,e2) -> re (E_assert (map_exp e1,map_exp e2))
       | E_internal_cast (ann,e) -> re (E_internal_cast (ann,map_exp e))