Fixed pretty printer for existentials

Also fixed substitution functions so as to not substitute captured kind identifiers

4 files changed, 35 insertions, 22 deletions

diff --git a/src/parser.mly b/src/parser.mly
index fa2cb0c7..f2d986b1 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -437,7 +437,7 @@ nexp_typ4:
     { tloc (ATyp_id $2) }
   | tyvar
     { tloc (ATyp_var $1) }
-  | Lparen tup_typ Rparen
+  | Lparen exist_typ Rparen
     { $2 }
 
 tup_typ_list:
@@ -453,10 +453,10 @@ tup_typ:
      { tloc (ATyp_tup $2) }
 
 exist_typ:
-  | tup_typ
-    { $1 }
   | Exist tyvars Comma nexp_constraint Dot tup_typ
     { tloc (ATyp_exist ($2, $4, $6)) }
+  | tup_typ
+    { $1 }
 
 typ:
   | exist_typ
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index a627328d..9c870b05 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -111,7 +111,7 @@ let doc_ord (Ord_aux(o,_)) = match o with
   | Ord_inc -> string "inc"
   | Ord_dec -> string "dec"
 
-let doc_typ, doc_atomic_typ, doc_nexp =
+let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   (* following the structure of parser for precedence *)
   let rec typ ty = fn_typ ty
   and fn_typ ((Typ_aux (t, _)) as ty) = match t with
@@ -119,6 +119,8 @@ let doc_typ, doc_atomic_typ, doc_nexp =
       separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct]
   | _ -> tup_typ ty
   and tup_typ ((Typ_aux (t, _)) as ty) = match t with
+  | Typ_exist (kids, nc, ty) ->
+     separate space [string "exist"; separate_map space doc_var kids ^^ comma; nexp_constraint nc ^^ dot; typ ty]
   | Typ_tup typs -> parens (separate_map comma_sp app_typ typs)
   | _ -> app_typ ty
   and app_typ ((Typ_aux (t, _)) as ty) = match t with
@@ -214,8 +216,21 @@ let doc_typ, doc_atomic_typ, doc_nexp =
     | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
       group (parens (nexp ne))
 
-  (* expose doc_typ, doc_atomic_typ and doc_nexp *)
-  in typ, atomic_typ, nexp
+  and nexp_constraint (NC_aux(nc,_)) = match nc with
+    | NC_fixed(n1,n2) -> doc_op equals (nexp n1) (nexp n2)
+    | NC_not_equal (n1, n2) -> doc_op (string "!=") (nexp n1) (nexp n2)
+    | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (nexp n1) (nexp n2)
+    | NC_bounded_le(n1,n2) -> doc_op (string "<=") (nexp n1) (nexp n2)
+    | NC_nat_set_bounded(v,bounds) ->
+       doc_op (string "IN") (doc_var v)
+              (braces (separate_map comma_sp doc_int bounds))
+    | NC_or (nc1, nc2) ->
+       parens (separate space [nexp_constraint nc1; string "|"; nexp_constraint nc2])
+    | NC_and (nc1, nc2) ->
+       separate space [nexp_constraint nc1; string "&"; nexp_constraint nc2]
+
+  (* expose doc_typ, doc_atomic_typ, doc_nexp and doc_nexp_constraint *)
+  in typ, atomic_typ, nexp, nexp_constraint
 
 let pp_format_id (Id_aux(i,_)) =
   match i with
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 668e791c..e3aeaa40 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -58,19 +58,6 @@ let doc_bkind (BK_aux(k,_)) =
 let doc_kind (K_aux(K_kind(klst),_)) =
   separate_map (spaces arrow) doc_bkind klst
 
-let rec doc_nexp_constraint (NC_aux(nc,_)) = match nc with
-  | NC_fixed(n1,n2) -> doc_op equals (doc_nexp n1) (doc_nexp n2)
-  | NC_not_equal (n1, n2) -> doc_op (string "!=") (doc_nexp n1) (doc_nexp n2)
-  | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (doc_nexp n1) (doc_nexp n2)
-  | NC_bounded_le(n1,n2) -> doc_op (string "<=") (doc_nexp n1) (doc_nexp n2)
-  | NC_nat_set_bounded(v,bounds) ->
-      doc_op (string "IN") (doc_var v)
-             (braces (separate_map comma_sp doc_int bounds))
-  | NC_or (nc1, nc2) ->
-     parens (separate space [doc_nexp_constraint nc1; string "|"; doc_nexp_constraint nc2])
-  | NC_and (nc1, nc2) ->
-     separate space [doc_nexp_constraint nc1; string "&"; doc_nexp_constraint nc2]
-
 let doc_qi (QI_aux(qi,_)) = match qi with
   | QI_const n_const -> doc_nexp_constraint n_const
   | QI_id(KOpt_aux(ki,_)) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 87a9a31c..d23b7041 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -249,7 +249,8 @@ and typ_subst_nexp_aux sv subst = function
   | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
-  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ) (* FIXME *)
+  | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_nexp sv subst typ)
 and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l)
 and typ_subst_arg_nexp_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp)
@@ -265,6 +266,7 @@ and typ_subst_typ_aux sv subst = function
   | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_typ sv subst typ)
 and typ_subst_arg_typ sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_typ_aux sv subst arg, l)
 and typ_subst_arg_typ_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
@@ -287,6 +289,7 @@ and typ_subst_order_aux sv subst = function
   | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2, effs)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_order sv subst typ)
 and typ_subst_arg_order sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_order_aux sv subst arg, l)
 and typ_subst_arg_order_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
@@ -302,7 +305,8 @@ and typ_subst_kid_aux sv subst = function
   | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2, effs)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args)
-  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ) (* FIXME *)
+  | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
+  | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_kid sv subst typ)
 and typ_subst_arg_kid sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_kid_aux sv subst arg, l)
 and typ_subst_arg_kid_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp)
@@ -2367,7 +2371,8 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
          else typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
                            ^ " not resolved during application of " ^ string_of_id f)
        end
-    | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args)) when KidSet.is_empty (typ_frees typ) ->
+    | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args))
+         when List.for_all (fun kid -> is_bound kid env) (KidSet.elements (typ_frees typ)) ->
        begin
          let carg = crule check_exp env arg typ in
          let (iargs, ret_typ', env) = instantiate env quants (utyps, typs) ret_typ (uargs, args) in
@@ -2454,6 +2459,12 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
   typ_debug ("Existentials: " ^ string_of_list ", " string_of_kid existentials);
   typ_debug ("Existential constraints: " ^ string_of_list ", " string_of_n_constraint ex_constraints);
 
+  let nc_true = nc_eq (nconstant 0) (nconstant 0) in
+  let typ_ret =
+    if existentials = []
+    then typ_ret
+    else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, typ_ret))
+  in
   let exp = annot_exp (E_app (f, xs_reordered)) typ_ret eff in
 
   match ret_ctx_typ with