diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.ml | 10 | ||||
| -rw-r--r-- | src/initial_check.ml | 7 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/parse_ast.ml | 5 | ||||
| -rw-r--r-- | src/parser.mly | 24 | ||||
| -rw-r--r-- | src/pretty_print_common.ml | 21 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 15 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 2 | ||||
| -rw-r--r-- | src/test/pattern.sail | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 397 | ||||
| -rw-r--r-- | src/type_check.mli | 13 | ||||
| -rw-r--r-- | src/util.ml | 4 | ||||
| -rw-r--r-- | src/util.mli | 2 |
14 files changed, 371 insertions, 135 deletions
@@ -229,6 +229,7 @@ typ_aux = (* Type expressions, of kind $_$ *) | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) | Typ_tup of (typ) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) + | Typ_exist of kid list * n_constraint * typ and typ = Typ_aux of typ_aux * l diff --git a/src/ast_util.ml b/src/ast_util.ml index 6a97f6bf..955164a3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -212,6 +212,8 @@ and string_of_typ_aux = function | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">" | Typ_fn (typ_arg, typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + | Typ_exist (kids, nc, typ) -> + "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ and string_of_typ_arg = function | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function @@ -219,8 +221,7 @@ and string_of_typ_arg_aux = function | Typ_arg_typ typ -> string_of_typ typ | Typ_arg_order o -> string_of_order o | Typ_arg_effect eff -> string_of_effect eff - -let rec string_of_n_constraint = function +and string_of_n_constraint = function | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 @@ -311,6 +312,9 @@ and string_of_pat (P_aux (pat, l)) = | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2 | P_list pats -> "[||" ^ string_of_list "," string_of_pat pats ^ "||]" + | P_vector_concat pats -> string_of_list " : " string_of_pat pats + | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]" + | P_as (pat, id) -> string_of_pat pat ^ " as " ^ string_of_id id | _ -> "PAT" and string_of_lexp (LEXP_aux (lexp, _)) = match lexp with @@ -318,6 +322,8 @@ and string_of_lexp (LEXP_aux (lexp, _)) = | LEXP_cast (typ, v) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_id v | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")" | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]" + | LEXP_vector_range (lexp, exp1, exp2) -> + string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]" | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")" | _ -> "LEXP" diff --git a/src/initial_check.ml b/src/initial_check.ml index 4d6db996..b831e288 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -207,6 +207,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None) + | Parse_ast.ATyp_exist (kids, nc, atyp) -> + let kids = List.map to_ast_var kids in + let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in + let exist_typ = to_ast_typ k_env def_ord atyp in + Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None ), l) @@ -300,7 +305,7 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")), l) -let rec to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = +and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = match c with | Parse_ast.NC_aux(nc,l) -> NC_aux( (match nc with diff --git a/src/lexer.mll b/src/lexer.mll index 45d8b3c2..228ca38f 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -79,6 +79,7 @@ let kw_table = ("cast", (fun _ -> Cast)); ("false", (fun _ -> False)); ("forall", (fun _ -> Forall)); + ("exist", (fun _ -> Exist)); ("foreach", (fun _ -> Foreach)); ("function", (fun x -> Function_)); ("overload", (fun _ -> Overload)); diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 526dffa8..c2e550f4 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -144,18 +144,19 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) + | ATyp_exist of kid list * n_constraint * atyp and atyp = ATyp_aux of atyp_aux * l -type +and kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) -type +and n_constraint_aux = (* constraint over kind $_$ *) NC_fixed of atyp * atyp | NC_bounded_ge of atyp * atyp diff --git a/src/parser.mly b/src/parser.mly index 62a2c9f4..f2d986b1 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -129,7 +129,7 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with no content*/ %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End -%token Enumerate Else Exit Extern False Forall Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast +%token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef %token Undefined Union With When Val Constraint %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape @@ -286,6 +286,12 @@ tyvar: | TyVar { (Kid_aux((Var($1)),loc ())) } +tyvars: + | tyvar + { [$1] } + | tyvar tyvars + { $1 :: $2 } + atomic_kind: | TYPE { bkloc BK_type } @@ -431,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: @@ -446,10 +452,16 @@ tup_typ: | Lparen tup_typ_list Rparen { tloc (ATyp_tup $2) } -typ: +exist_typ: + | Exist tyvars Comma nexp_constraint Dot tup_typ + { tloc (ATyp_exist ($2, $4, $6)) } | tup_typ { $1 } - | tup_typ MinusGt tup_typ Effect effect_typ + +typ: + | exist_typ + { $1 } + | tup_typ MinusGt exist_typ Effect effect_typ { tloc (ATyp_fn($1,$3,$5)) } lit: @@ -483,7 +495,7 @@ atomic_pat: { ploc P_wild } | Lparen pat As id Rparen { ploc (P_as($2,$4)) } - | Lparen tup_typ Rparen atomic_pat + | Lparen exist_typ Rparen atomic_pat { ploc (P_typ($2,$4)) } | id { ploc (P_app($1,[])) } @@ -569,7 +581,7 @@ atomic_exp: { eloc (E_lit($1)) } | Lparen exp Rparen { $2 } - | Lparen tup_typ Rparen atomic_exp + | Lparen exist_typ Rparen atomic_exp { eloc (E_cast($2,$4)) } | Lparen comma_exps Rparen { eloc (E_tuple($2)) } 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..aff3a976 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,_)) -> @@ -295,7 +282,7 @@ let doc_exp, doc_let = let cases = separate_map (break 1) doc_case pexps in surround 2 1 opening cases rbrace | E_sizeof n -> - separate space [string "sizeof"; doc_nexp n] + parens (separate space [string "sizeof"; doc_nexp n]) | E_constraint nc -> string "constraint" ^^ parens (doc_nexp_constraint nc) | E_exit e -> diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index fdd56ecc..1475da7a 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -238,7 +238,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used | Typ_app(id,targs) -> - List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) + List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with | Typ_arg_typ t -> fv_of_typ consider_var bound used t diff --git a/src/test/pattern.sail b/src/test/pattern.sail index cabe7dad..97e5a0ef 100644 --- a/src/test/pattern.sail +++ b/src/test/pattern.sail @@ -4,9 +4,9 @@ register nat x register nat y typedef wordsize = forall Nat 'n, 'n IN {8,16,32}. [|'n|] -let forall Nat 'n. (wordsize<'n>) word = 8 +(* let forall Nat 'n. (wordsize<'n>) word = 8 *) -function nat main _ = { +function nat main () = { (* works - x and y are set to 42 *) n := 1; diff --git a/src/type_check.ml b/src/type_check.ml index 90e1ad8c..4b00957f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -50,6 +50,11 @@ let opt_tc_debug = ref 0 let opt_no_effects = ref false let depth = ref 0 +let rec take n xs = match n, xs with + | 0, _ -> [] + | n, [] -> [] + | n, (x :: xs) -> x :: take (n - 1) xs + let rec indent n = match n with | 0 -> "" | n -> "| " ^ indent (n - 1) @@ -91,22 +96,52 @@ let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown) let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown) +let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l) +and nexp_simp_aux = function + | Nexp_sum (n1, n2) -> + begin + let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in + let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in + match n1_simp, n2_simp with + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2) + | _, Nexp_neg n2 -> Nexp_minus (n1, n2) + | _, _ -> Nexp_sum (n1, n2) + end + | Nexp_times (n1, n2) -> + begin + let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in + let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in + match n1_simp, n2_simp with + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2) + | _, _ -> Nexp_times (n1, n2) + end + | Nexp_minus (n1, n2) -> + begin + let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in + let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in + typ_debug ("SIMP: " ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2); + match n1_simp, n2_simp with + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2) + | _, _ -> Nexp_minus (n1, n2) + end + | nexp -> nexp + let int_typ = mk_id_typ (mk_id "int") let nat_typ = mk_id_typ (mk_id "nat") let unit_typ = mk_id_typ (mk_id "unit") let bit_typ = mk_id_typ (mk_id "bit") let real_typ = mk_id_typ (mk_id "real") let app_typ id args = mk_typ (Typ_app (id, args)) -let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])) -let range_typ nexp1 nexp2 = mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp nexp1); mk_typ_arg (Typ_arg_nexp nexp2)])) +let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) +let range_typ nexp1 nexp2 = mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1)); mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))])) let bool_typ = mk_id_typ (mk_id "bool") let string_typ = mk_id_typ (mk_id "string") let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)])) let vector_typ n m ord typ = mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp n); - mk_typ_arg (Typ_arg_nexp m); + [mk_typ_arg (Typ_arg_nexp (nexp_simp n)); + mk_typ_arg (Typ_arg_nexp (nexp_simp m)); mk_typ_arg (Typ_arg_order ord); mk_typ_arg (Typ_arg_typ typ)])) @@ -255,6 +290,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) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv subst 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) @@ -270,6 +307,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 @@ -292,6 +330,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 @@ -307,6 +346,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) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv (Nexp_var subst) 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) @@ -321,36 +362,6 @@ let quant_item_subst_kid_aux sv subst = function if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid | QI_const nc -> QI_const (nc_subst_nexp sv (Nexp_var subst) nc) -let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l) -and nexp_simp_aux = function - | Nexp_sum (n1, n2) -> - begin - let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in - let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in - match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2) - | _, Nexp_neg n2 -> Nexp_minus (n1, n2) - | _, _ -> Nexp_sum (n1, n2) - end - | Nexp_times (n1, n2) -> - begin - let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in - let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in - match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2) - | _, _ -> Nexp_times (n1, n2) - end - | Nexp_minus (n1, n2) -> - begin - let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in - let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in - typ_debug ("SIMP: " ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2); - match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2) - | _, _ -> Nexp_minus (n1, n2) - end - | nexp -> nexp - let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l) let typquant_subst_kid_aux sv subst = function @@ -525,26 +536,30 @@ end = struct type error if the type is badly formed. FIXME: Add arity to type constructors, although arity checking for the builtin types does seem to be done by the initial ast check. *) - let rec wf_typ env (Typ_aux (typ_aux, l)) = + let rec wf_typ ?exs:(exs=KidSet.empty) env (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_wild -> () | Typ_id id when bound_typ_id env id -> () | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) | Typ_var kid when KBindings.mem kid env.typ_vars -> () | Typ_var kid -> typ_error l ("Unbound kind identifier " ^ string_of_kid kid) - | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ env typ_arg; wf_typ env typ_ret - | Typ_tup typs -> List.iter (wf_typ env) typs - | Typ_app (id, args) when bound_typ_id env id -> List.iter (wf_typ_arg env) args + | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ ~exs:exs env typ_arg; wf_typ ~exs:exs env typ_ret + | Typ_tup typs -> List.iter (wf_typ ~exs:exs env) typs + | Typ_app (id, args) when bound_typ_id env id -> List.iter (wf_typ_arg ~exs:exs env) args | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id) - and wf_typ_arg env (Typ_arg_aux (typ_arg_aux, _)) = + | Typ_exist ([], _, _) -> typ_error l ("Existential must have some type variables") + | Typ_exist (kids, nc, typ) when KidSet.is_empty exs -> wf_typ ~exs:(KidSet.of_list kids) env typ + | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed") + and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) = match typ_arg_aux with - | Typ_arg_nexp nexp -> wf_nexp env nexp - | Typ_arg_typ typ -> wf_typ env typ + | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp + | Typ_arg_typ typ -> wf_typ ~exs:exs env typ | Typ_arg_order ord -> wf_order env ord | Typ_arg_effect _ -> () (* Check: is this ever used? *) - and wf_nexp env (Nexp_aux (nexp_aux, l)) = + and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) = match nexp_aux with | Nexp_id _ -> typ_error l "Unimplemented: Nexp_id" + | Nexp_var kid when KidSet.mem kid exs -> () | Nexp_var kid -> begin match get_typ_var kid env with @@ -554,11 +569,11 @@ end = struct ^ string_of_base_kind_aux kind ^ " but should have kind Nat") end | Nexp_constant _ -> () - | Nexp_times (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2 - | Nexp_sum (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2 - | Nexp_minus (nexp1, nexp2) -> wf_nexp env nexp1; wf_nexp env nexp2 - | Nexp_exp nexp -> wf_nexp env nexp (* MAYBE: Could put restrictions on what is allowed here *) - | Nexp_neg nexp -> wf_nexp env nexp + | Nexp_times (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 + | Nexp_sum (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 + | Nexp_minus (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 + | Nexp_exp nexp -> wf_nexp ~exs:exs env nexp (* MAYBE: Could put restrictions on what is allowed here *) + | Nexp_neg nexp -> wf_nexp ~exs:exs env nexp and wf_order env (Ord_aux (ord_aux, l)) = match ord_aux with | Ord_var kid -> @@ -898,6 +913,40 @@ let initial_env = Env.empty |> Env.add_typ_synonym (mk_id "atom") (fun args -> mk_typ (Typ_app (mk_id "range", args @ args))) +let ex_counter = ref 0 + +let fresh_existential () = + let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter), Parse_ast.Unknown) in + incr ex_counter; fresh + +let destructure_exist env typ = + match Env.expand_synonyms env typ with + | Typ_aux (Typ_exist (kids, nc, typ), _) -> + let fresh_kids = List.map (fun kid -> (kid, fresh_existential ())) kids in + let nc = List.fold_left (fun nc (kid, fresh) -> nc_subst_nexp kid (Nexp_var fresh) nc) nc fresh_kids in + let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst_nexp kid (Nexp_var fresh) typ) typ fresh_kids in + Some (List.map snd fresh_kids, nc, typ) + | _ -> None + +let is_exist = function + | Typ_aux (Typ_exist (_, _, _), _) -> true + | _ -> false + +let exist_typ constr typ = + let fresh_kid = fresh_existential () in + mk_typ (Typ_exist ([fresh_kid], constr fresh_kid, typ fresh_kid)) + +let destruct_vector_typ env typ = + let destruct_vector_typ' = function + | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); + Typ_arg_aux (Typ_arg_nexp n2, _); + Typ_arg_aux (Typ_arg_order o, _); + Typ_arg_aux (Typ_arg_typ vtyp, _)] + ), _) when string_of_id id = "vector" -> Some (n1, n2, o, vtyp) + | typ -> None + in + destruct_vector_typ' (Env.expand_synonyms env typ) + (**************************************************************************) (* 3. Subtyping and constraint solving *) (**************************************************************************) @@ -921,6 +970,7 @@ type tnf = | Tnf_tup of tnf list | Tnf_index_sort of index_sort | Tnf_app of id * tnf_arg list + | Tnf_exist of kid list * n_constraint * tnf and tnf_arg = | Tnf_arg_nexp of nexp | Tnf_arg_typ of tnf @@ -936,6 +986,8 @@ let rec string_of_tnf = function | Tnf_index_sort IS_int -> "INT" | Tnf_index_sort (IS_prop (kid, props)) -> "{" ^ string_of_kid kid ^ " | " ^ string_of_list " & " (fun (n1, n2) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2) props ^ "}" + | Tnf_exist (kids, nc, tnf) -> + "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_tnf tnf and string_of_tnf_arg = function | Tnf_arg_nexp n -> string_of_nexp n | Tnf_arg_typ tnf -> string_of_tnf tnf @@ -966,6 +1018,7 @@ let rec normalize_typ env (Typ_aux (typ, l)) = try normalize_typ env (Env.get_typ_synonym id env args) with | Not_found -> Tnf_app (id, List.map (normalize_typ_arg env) args) end + | Typ_exist (kids, nc, typ) -> Tnf_exist (kids, nc, normalize_typ env typ) | Typ_fn _ -> typ_error l ("Cannot normalize function type " ^ string_of_typ (Typ_aux (typ, l))) and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) = match typ_arg with @@ -1114,6 +1167,10 @@ let rec subtyp_tnf env tnf1 tnf2 = | Constraint.Unknown [] -> typ_debug "sat"; false | Constraint.Unknown _ -> typ_debug "unknown"; false end + | Tnf_exist (kids, nc, tnf1), _ -> + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in + let env = Env.add_constraint nc env in + subtyp_tnf env tnf1 tnf2 | _, _ -> false and tnf_args_eq env arg1 arg2 = @@ -1123,39 +1180,54 @@ and tnf_args_eq env arg1 arg2 = | Tnf_arg_typ tnf1, Tnf_arg_typ tnf2 -> subtyp_tnf env tnf1 tnf2 && subtyp_tnf env tnf2 tnf1 | _, _ -> assert false -let subtyp l env typ1 typ2 = - if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2) - then () - else typ_error l (string_of_typ typ1 - ^ " is not a subtype of " ^ string_of_typ typ2 - ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)) - -let typ_equality l env typ1 typ2 = - subtyp l env typ1 typ2; subtyp l env typ2 typ1 - (**************************************************************************) (* 4. Unification *) (**************************************************************************) +let rec nexp_frees ?exs:(exs=KidSet.empty) (Nexp_aux (nexp, l)) = + match nexp with + | Nexp_id _ -> KidSet.empty + | Nexp_var kid -> KidSet.singleton kid + | Nexp_constant _ -> KidSet.empty + | Nexp_times (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) + | Nexp_sum (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) + | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) + | Nexp_exp n -> nexp_frees ~exs:exs n + | Nexp_neg n -> nexp_frees ~exs:exs n + let order_frees (Ord_aux (ord_aux, l)) = match ord_aux with | Ord_var kid -> KidSet.singleton kid | _ -> KidSet.empty -let rec typ_frees (Typ_aux (typ_aux, l)) = +let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_wild -> KidSet.empty | Typ_id v -> KidSet.empty + | Typ_var kid when KidSet.mem kid exs -> KidSet.empty | Typ_var kid -> KidSet.singleton kid - | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map typ_frees typs) - | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map typ_arg_frees args) -and typ_arg_frees (Typ_arg_aux (typ_arg_aux, l)) = + | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs) + | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args) + | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ +and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) = match typ_arg_aux with - | Typ_arg_nexp n -> nexp_frees n - | Typ_arg_typ typ -> typ_frees typ + | Typ_arg_nexp n -> nexp_frees ~exs:exs n + | Typ_arg_typ typ -> typ_frees ~exs:exs typ | Typ_arg_order ord -> order_frees ord | Typ_arg_effect _ -> assert false +let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) = + match nexp1, nexp2 with + | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0 + | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 = 0 + | Nexp_constant c1, Nexp_constant c2 -> c1 = c2 + | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b + | Nexp_exp n1, Nexp_exp n2 -> nexp_identical n1 n2 + | Nexp_neg n1, Nexp_neg n2 -> nexp_identical n1 n2 + | _, _ -> false + let ord_identical (Ord_aux (ord1, _)) (Ord_aux (ord2, _)) = match ord1, ord2 with | Ord_var kid1, Ord_var kid2 -> Kid.compare kid1 kid2 = 0 @@ -1292,7 +1364,7 @@ let merge_unifiers l kid uvar1 uvar2 = | Some u1, None -> Some u1 | None, None -> None -let unify l env typ1 typ2 = +let rec unify l env typ1 typ2 = typ_print ("Unify " ^ string_of_typ typ1 ^ " with " ^ string_of_typ typ2); let goals = KidSet.inter (KidSet.diff (typ_frees typ1) (typ_frees typ2)) (typ_frees typ1) in let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) = @@ -1355,8 +1427,15 @@ let unify l env typ1 typ2 = | Typ_arg_effect _, Typ_arg_effect _ -> assert false | _, _ -> unify_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2) in - let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in - unify_typ l typ1 typ2 + match destructure_exist env typ2 with + | Some (kids, nc, typ2) -> + let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in + let unifiers = unify_typ l typ1 typ2 in + typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); + unifiers, kids, Some nc + | None -> + let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in + unify_typ l typ1 typ2, [], None let merge_uvars l unifiers1 unifiers2 = try KBindings.merge (merge_unifiers l) unifiers1 unifiers2 @@ -1364,6 +1443,52 @@ let merge_uvars l unifiers1 unifiers2 = | Unification_error (_, m) -> typ_error l ("Could not merge unification variables: " ^ m) (**************************************************************************) +(* 4.5. Subtyping with existentials *) +(**************************************************************************) + +let nc_subst_uvar kid uvar nc = + match uvar with + | U_nexp nexp -> nc_subst_nexp kid (unaux_nexp nexp) nc + | _ -> nc + +let uv_nexp_constraint env (kid, uvar) = + match uvar with + | U_nexp nexp -> Env.add_constraint (nc_eq (nvar kid) nexp) env + | _ -> env + +let subtyp l env typ1 typ2 = + match destructure_exist env typ2 with + | Some (kids, nc, typ2) -> + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in + let unifiers, existential_kids, existential_nc = + try unify l env typ2 typ1 with + | Unification_error (_, m) -> typ_error l m + in + let nc = List.fold_left (fun nc (kid, uvar) -> nc_subst_uvar kid uvar nc) nc (KBindings.bindings unifiers) in + let env = match existential_kids, existential_nc with + | [], None -> env + | _, Some enc -> + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env existential_kids in + let env = List.fold_left uv_nexp_constraint env (KBindings.bindings unifiers) in + Env.add_constraint enc env + in + if prove env nc then () + else typ_error l ("Could not show " ^ string_of_typ typ1 ^ " is a subset of existential " ^ string_of_typ typ2) + | None -> + if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2) + then () + else typ_error l (string_of_typ typ1 + ^ " is not a subtype of " ^ string_of_typ typ2 + ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)) + +let typ_equality l env typ1 typ2 = + subtyp l env typ1 typ2; subtyp l env typ2 typ1 + +let subtype_check env typ1 typ2 = + try subtyp Parse_ast.Unknown env typ1 typ2; true with + | Type_error _ -> false + +(**************************************************************************) (* 5. Type checking expressions *) (**************************************************************************) @@ -1717,6 +1842,12 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ end in try_overload (Env.get_overloads f env) + | E_return exp, _ -> + let checked_exp = match Env.get_ret_typ env with + | Some ret_typ -> crule check_exp env exp ret_typ + | None -> typ_error l "Cannot use return outside a function" + in + annot_exp (E_return checked_exp) typ | E_app (f, xs), _ -> let inferred_exp = infer_funapp l env f xs (Some typ) in type_coercion env inferred_exp typ @@ -1899,7 +2030,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) begin try typ_debug ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for pattern " ^ string_of_typ typ); - let unifiers = unify l env ret_typ typ in + let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); let arg_typ' = subst_unifiers unifiers arg_typ in let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in @@ -1943,13 +2074,13 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = annot_pat (P_lit lit) (infer_lit env lit), env | P_vector (pat :: pats) -> let fold_pats (pats, env) pat = - let inferred_pat, env = infer_pat env pat in - pats @ [inferred_pat], env + let typed_pat, env = bind_pat env pat bit_typ in + pats @ [typed_pat], env in - let ((inferred_pat :: inferred_pats) as pats), env = + let ((typed_pat :: typed_pats) as pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in let len = nexp_simp (nconstant (List.length pats)) in - let etyp = pat_typ_of inferred_pat in + let etyp = pat_typ_of typed_pat in List.map (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; annot_pat (P_vector pats) (lvector_typ env len etyp), env | P_vector_concat (pat :: pats) -> @@ -1966,6 +2097,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let len = nexp_simp (List.fold_left fold_len len inferred_pats) in annot_pat (P_vector_concat (inferred_pat :: inferred_pats)) (lvector_typ env len vtyp), env + | P_as (pat, id) -> + let (typed_pat, env) = infer_pat env pat in + annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), env | _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat) and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) = @@ -2023,7 +2157,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) vec_typ) checked_exp, env | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in - let unifiers = try unify l env rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in + let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in let field_typ' = subst_unifiers unifiers field_typ in let checked_exp = crule check_exp env exp field_typ' in annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) field_typ') checked_exp, env @@ -2164,12 +2298,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)]))) | E_constraint nc -> annot_exp (E_constraint nc) bool_typ - | E_return exp -> - begin - match Env.get_ret_typ env with - | Some typ -> annot_exp (E_return (crule check_exp env exp typ)) (mk_typ (Typ_id (mk_id "unit"))) - | None -> typ_error l "Return found in non-function environment" - end | E_field (exp, field) -> begin let inferred_exp = irule infer_exp env exp in @@ -2239,6 +2367,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = match is_range (typ_of inferred_f), is_range (typ_of inferred_t) with | None, _ -> typ_error l ("Type of " ^ string_of_exp f ^ " in foreach must be a range") | _, None -> typ_error l ("Type of " ^ string_of_exp t ^ " in foreach must be a range") + (* | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) -> + let loop_vtyp = exist_typ (fun e -> nc_and (nc_lteq l1 (nvar e)) (nc_lteq (nvar e) u2)) (fun e -> atom_typ (nvar e)) in + let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in + annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ *) | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) -> let checked_body = crule check_exp (Env.add_local v (Immutable, range_typ l1 u2) env) body unit_typ in annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ @@ -2289,6 +2421,15 @@ and instantiation_of (E_aux (exp_aux, (l, _)) as exp) = and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let annot_exp exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in let all_unifiers = ref KBindings.empty in + let ex_goal = ref None in + let prove_goal env = match !ex_goal with + | Some goal when prove env goal -> () + | Some goal -> typ_error l ("Could not prove existential goal: " ^ string_of_n_constraint goal) + | None -> () + in + let universals = Env.get_typ_vars env in + let universal_constraints = Env.get_constraints env in + let is_bound kid env = KBindings.mem kid (Env.get_typ_vars env) in let rec number n = function | [] -> [] | (x :: xs) -> (n, x) :: number (n + 1) xs @@ -2297,7 +2438,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = | QI_aux (QI_id _, _) -> false | QI_aux (QI_const nc, _) -> prove env nc in - let rec instantiate quants typs ret_typ args = + let rec instantiate env quants typs ret_typ args = match typs, args with | (utyps, []), (uargs, []) -> begin @@ -2305,15 +2446,16 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = if List.for_all solve_quant quants then let iuargs = List.map2 (fun utyp (n, uarg) -> (n, crule check_exp env uarg utyp)) utyps uargs in - (iuargs, ret_typ) + (iuargs, ret_typ, env) 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') = instantiate quants (utyps, typs) ret_typ (uargs, args) in - ((n, carg) :: iargs, ret_typ') + let (iargs, ret_typ', env) = instantiate env quants (utyps, typs) ret_typ (uargs, args) in + ((n, carg) :: iargs, ret_typ', env) end | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args)) -> begin @@ -2321,56 +2463,92 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let iarg = irule infer_exp env arg in typ_debug ("INFER: " ^ string_of_exp arg ^ " type " ^ string_of_typ (typ_of iarg) ^ " NF " ^ string_of_tnf (normalize_typ env (typ_of iarg))); try - let iarg, unifiers = type_coercion_unify env iarg typ in + let iarg, (unifiers, ex_kids, ex_nc) (* FIXME *) = type_coercion_unify env iarg typ in typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); + typ_debug ("EX KIDS: " ^ string_of_list ", " string_of_kid ex_kids); + let env = match ex_kids, ex_nc with + | [], None -> env + | _, Some enc -> + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env ex_kids in + Env.add_constraint enc env + in all_unifiers := merge_uvars l !all_unifiers unifiers; let utyps' = List.map (subst_unifiers unifiers) utyps in let typs' = List.map (subst_unifiers unifiers) typs in let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in let ret_typ' = subst_unifiers unifiers ret_typ in - let (iargs, ret_typ'') = instantiate quants' (utyps', typs') ret_typ' (uargs, args) in - ((n, iarg) :: iargs, ret_typ'') + let (iargs, ret_typ'', env) = instantiate env quants' (utyps', typs') ret_typ' (uargs, args) in + ((n, iarg) :: iargs, ret_typ'', env) with | Unification_error (l, str) -> typ_debug ("Unification error: " ^ str); - instantiate quants (typ :: utyps, typs) ret_typ ((n, arg) :: uargs, args) + instantiate env quants (typ :: utyps, typs) ret_typ ((n, arg) :: uargs, args) end | (_, []), _ -> typ_error l ("Function " ^ string_of_id f ^ " applied to too many arguments") | _, (_, []) -> typ_error l ("Function " ^ string_of_id f ^ " not applied to enough arguments") in - let instantiate_ret quants typs ret_typ = + let instantiate_ret env quants typs ret_typ = match ret_ctx_typ with - | None -> (quants, typs, ret_typ) + | None -> (quants, typs, ret_typ, env) + | Some rct when is_exist (Env.expand_synonyms env rct) -> (quants, typs, ret_typ, env) | Some rct -> begin typ_debug ("RCT is " ^ string_of_typ rct); typ_debug ("INSTANTIATE RETURN:" ^ string_of_typ ret_typ); - let unifiers = try unify l env ret_typ rct with Unification_error _ -> typ_debug "UERROR"; KBindings.empty in + let unifiers, ex_kids, ex_nc = + try unify l env ret_typ rct with + | Unification_error _ -> typ_debug "UERROR"; KBindings.empty, [], None + in typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); + if ex_kids = [] then () else (typ_debug ("EX GOAL: " ^ string_of_option string_of_n_constraint ex_nc); ex_goal := ex_nc); all_unifiers := merge_uvars l !all_unifiers unifiers; + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env ex_kids in let typs' = List.map (subst_unifiers unifiers) typs in let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in - let ret_typ' = subst_unifiers unifiers ret_typ in - (quants', typs', ret_typ') + let ret_typ' = + match ex_nc with + | None -> subst_unifiers unifiers ret_typ + | Some nc -> mk_typ (Typ_exist (ex_kids, nc, subst_unifiers unifiers ret_typ)) + in + (quants', typs', ret_typ', env) end in - let exp = + let (quants, typ_args, typ_ret, env), eff = match Env.expand_synonyms env f_typ with | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) -> - let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) typ_args typ_ret in - let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in - let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in - annot_exp (E_app (f, xs_reordered)) typ_ret eff + instantiate_ret env (quant_items typq) typ_args typ_ret, eff | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) -> - let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) [typ_arg] typ_ret in - let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in - let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in - annot_exp (E_app (f, xs_reordered)) typ_ret eff + instantiate_ret env (quant_items typq) [typ_arg] typ_ret, eff | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type") in + let (xs_instantiated, typ_ret, env) = instantiate env quants ([], typ_args) typ_ret ([], number 0 xs) in + let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in + + prove_goal env; + + let ty_vars = List.map fst (KBindings.bindings (Env.get_typ_vars env)) in + let existentials = List.filter (fun kid -> not (KBindings.mem kid universals)) ty_vars in + let num_new_ncs = List.length (Env.get_constraints env) - List.length universal_constraints in + let ex_constraints = take num_new_ncs (Env.get_constraints env) in + + 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 KidSet.is_empty (KidSet.inter (typ_frees typ_ret) (KidSet.of_list 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 + typ_debug ("RETURNING: " ^ string_of_typ (typ_of exp)); match ret_ctx_typ with - | None -> exp, !all_unifiers - | Some rct -> type_coercion env exp rct, !all_unifiers + | None -> + exp, !all_unifiers + | Some rct -> + let exp = type_coercion env exp rct in + typ_debug ("RETURNING AFTER COERCION " ^ string_of_typ (typ_of exp)); + exp, !all_unifiers (**************************************************************************) (* 6. Effect system *) @@ -2645,7 +2823,18 @@ let check_tannotopt typq ret_typ = function else typ_error l (string_of_bind (typq, ret_typ) ^ " and " ^ string_of_bind (annot_typq, annot_ret_typ) ^ " do not match between function and val spec") let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux) = - let id = id_of_fundef fd_aux in + let id = + match (List.fold_right + (fun (FCL_aux (FCL_Funcl (id, _, _), _)) id' -> + match id' with + | Some id' -> if string_of_id id' = string_of_id id then Some id' + else typ_error l ("Function declaration expects all definitions to have the same name, " + ^ string_of_id id ^ " differs from other definitions of " ^ string_of_id id') + | None -> Some id) funcls None) + with + | Some id -> id + | None -> typ_error l "funcl list is empty" + in typ_print ("\nChecking function " ^ string_of_id id); let have_val_spec, (quant, (Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) as typ)), env = try true, Env.get_val_spec id env, env with diff --git a/src/type_check.mli b/src/type_check.mli index a2b8a10c..ce66aba3 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -85,6 +85,8 @@ module Env : sig val get_typ_vars : t -> base_kind_aux KBindings.t + val add_typ_var : kid -> base_kind_aux -> t -> t + val is_record : id -> t -> bool val get_accessor : id -> id -> t -> typquant * typ @@ -151,6 +153,8 @@ val npow2 : nexp -> nexp val nvar : kid -> nexp val nid : id -> nexp +val nc_gteq : nexp -> nexp -> n_constraint + (* Sail builtin types. *) val int_typ : typ val nat_typ : typ @@ -163,6 +167,7 @@ val string_typ : typ val real_typ : typ val vector_typ : nexp -> nexp -> order -> typ -> typ val list_typ : typ -> typ +val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ val inc_ord : order val dec_ord : order @@ -187,6 +192,10 @@ val strip_pat : 'a pat -> unit pat re-checked. *) val check_exp : Env.t -> unit exp -> typ -> tannot exp +val infer_exp : Env.t -> unit exp -> tannot exp + +val subtype_check : Env.t -> typ -> typ -> bool + (* Partial functions: The expressions and patterns passed to these functions must be guaranteed to have tannots of the form Some (env, typ) for these to work. *) @@ -204,6 +213,10 @@ val pat_typ_of : tannot pat -> typ val effect_of : tannot exp -> effect val effect_of_annot : tannot -> effect +val destructure_atom_nexp : typ -> nexp + +val destruct_vector_typ : Env.t -> typ -> (nexp * nexp * order * typ) option + type uvar = | U_nexp of nexp | U_order of order diff --git a/src/util.ml b/src/util.ml index d2d4eea7..75732376 100644 --- a/src/util.ml +++ b/src/util.ml @@ -343,3 +343,7 @@ let rec string_of_list sep string_of = function | [] -> "" | [x] -> string_of x | x::ls -> (string_of x) ^ sep ^ (string_of_list sep string_of ls) + +let string_of_option string_of = function + | None -> "" + | Some x -> string_of x diff --git a/src/util.mli b/src/util.mli index cfd6a19e..aa442ada 100644 --- a/src/util.mli +++ b/src/util.mli @@ -205,4 +205,6 @@ module ExtraSet : functor (S : Set.S) -> (*Formatting functions*) val string_of_list : string -> ('a -> string) -> 'a list -> string +val string_of_option : ('a -> string) -> 'a option -> string + val split_on_char : char -> string -> string list |