diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.mli | 4 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 22 | ||||
| -rw-r--r-- | src/process_file.ml | 7 | ||||
| -rw-r--r-- | src/process_file.mli | 4 | ||||
| -rw-r--r-- | src/sail.ml | 10 | ||||
| -rw-r--r-- | src/type_check_new.ml | 68 | ||||
| -rw-r--r-- | src/type_check_new.mli | 1 |
7 files changed, 90 insertions, 26 deletions
diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 9a002454..67475616 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -44,9 +44,9 @@ open Ast open Type_internal (* Prints the defs following source syntax *) -val pp_defs : out_channel -> tannot defs -> unit +val pp_defs : out_channel -> 'a defs -> unit val pp_exp : Buffer.t -> exp -> unit -val pat_to_string : tannot pat -> string +val pat_to_string : 'a pat -> string (* Prints on formatter the defs as Lem Ast nodes *) val pp_lem_defs : Format.formatter -> tannot defs -> unit diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 22cb707b..9c33c841 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -40,7 +40,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Type_internal +(* open Type_internal *) open Ast open PPrint open Pretty_print_common @@ -238,6 +238,7 @@ let doc_exp, doc_let = | E_id id -> doc_id id | E_lit lit -> doc_lit lit | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e)) + (* | E_internal_cast((_,NoTyp),e) -> atomic_exp e | E_internal_cast((_,Base((_,t),_,_,_,_,bindings)), (E_aux(_,(_,eannot)) as e)) -> (match t.t,eannot with @@ -247,6 +248,7 @@ let doc_exp, doc_let = | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_,_,_) when nexp_eq n1 n2 -> atomic_exp e | _ -> prefix 2 1 (parens (doc_typ (t_to_typ t))) (group (atomic_exp e))) + *) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -325,6 +327,7 @@ let doc_exp, doc_let = (* doc_op (doc_id op) (exp l) (exp r) *) | E_comment s -> comment (string s) | E_comment_struc e -> comment (exp e) + (* | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*) (match t.t with | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) @@ -342,7 +345,7 @@ let doc_exp, doc_let = | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t))) | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away")) | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false - + *) and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> (match ts with @@ -391,16 +394,18 @@ let doc_exp, doc_let = let doc_default (DT_aux(df,_)) = match df with | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v] | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id] - | DT_order(ord) -> separate space [string "default"; string "order"; doc_ord ord] + | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord] let doc_spec (VS_aux(v,_)) = match v with | VS_val_spec(ts,id) -> - separate space [string "val"; doc_typscm ts; doc_id id] + separate space [string "val"; doc_typscm ts; doc_id id] + | VS_cast_spec (ts, id) -> + separate space [string "val"; string "cast"; doc_typscm ts; doc_id id] | VS_extern_no_rename(ts,id) -> - separate space [string "val"; string "extern"; doc_typscm ts; doc_id id] + separate space [string "val"; string "extern"; doc_typscm ts; doc_id id] | VS_extern_spec(ts,id,s) -> - separate space [string "val"; string "extern"; doc_typscm ts; - doc_op equals (doc_id id) (dquotes (string s))] + separate space [string "val"; string "extern"; doc_typscm ts; + doc_op equals (doc_id id) (dquotes (string s))] let doc_namescm (Name_sect_aux(ns,_)) = match ns with | Name_sect_none -> empty @@ -549,6 +554,9 @@ let rec doc_def def = group (match def with | DEF_val lbind -> doc_let lbind | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef + | DEF_overload (id, ids) -> + let ids_doc = group (separate_map (semi ^^ break 1) doc_id ids) in + string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc | DEF_comm (DC_comm s) -> comment (string s) | DEF_comm (DC_comm_struct d) -> comment (doc_def d) ) ^^ hardline diff --git a/src/process_file.ml b/src/process_file.ml index 63e42219..42d1402b 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -90,6 +90,8 @@ let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tann let opt_new_typecheck = ref false let opt_just_check = ref false +let opt_ddump_tc_ast = ref false +let opt_dno_cast = ref false let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs = let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; @@ -101,7 +103,10 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast. | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec | _ -> Type_internal.Oinc)};} in if !opt_new_typecheck - then let _ = Type_check_new.check Type_check_new.initial_env defs in () + then + let ienv = if !opt_dno_cast then Type_check_new.Env.no_casts Type_check_new.initial_env else Type_check_new.initial_env in + let ast, _ = Type_check_new.check ienv defs in + if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else () else (); if !opt_just_check then exit 0 diff --git a/src/process_file.mli b/src/process_file.mli index 4c703dd2..aa8d3265 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -50,7 +50,9 @@ val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot As val opt_new_typecheck : bool ref val opt_just_check : bool ref - +val opt_ddump_tc_ast : bool ref +val opt_dno_cast : bool ref + type out_type = | Lem_ast_out | Lem_out of string option (* If present, the string is a file to open in the lem backend*) diff --git a/src/sail.ml b/src/sail.ml index 0bdcf4ab..452e6e72 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -88,10 +88,16 @@ let options = Arg.align ([ " (debug) skip constraint resolution in type-checking"); ( "-new_typecheck", Arg.Set opt_new_typecheck, - " use new typechecker with Z3 constraint solving (experimental)"); + " (experimental) use new typechecker with Z3 constraint solving"); ( "-just_check", Arg.Tuple [Arg.Set opt_new_typecheck; Arg.Set opt_just_check], - " terminate immediately after typechecking, implies -new_typecheck"); + " (experimental) terminate immediately after typechecking, implies -new_typecheck"); + ( "-ddump_tc_ast", + Arg.Set opt_ddump_tc_ast, + " (debug) dump the typechecked ast to stdout"); + ( "-dno_cast", + Arg.Set opt_dno_cast, + " (debug) typecheck without any implicit casting"); ( "-v", Arg.Set opt_print_version, " print version"); diff --git a/src/type_check_new.ml b/src/type_check_new.ml index cc232eb8..5f997409 100644 --- a/src/type_check_new.ml +++ b/src/type_check_new.ml @@ -98,6 +98,8 @@ and map_pat_annot_aux f = function | P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats) | P_tup pats -> P_tup (List.map (map_pat_annot f) pats) | P_list pats -> P_list (List.map (map_pat_annot f) pats) + | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats) + | P_vector pats -> P_vector (List.map (map_pat_annot f) pats) | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot map annot in pat" and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot) and map_letbind_annot_aux f = function @@ -262,6 +264,7 @@ let rec string_of_exp (E_aux (exp, _)) = | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]" | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]" | E_vector_subrange (v, n1, n2) -> string_of_exp v ^ "[" ^ string_of_exp n1 ^ " .. " ^ string_of_exp n2 ^ "]" + | E_vector_append (v1, v2) -> string_of_exp v1 ^ " : " ^ string_of_exp v2 | E_if (cond, then_branch, else_branch) -> "if " ^ string_of_exp cond ^ " then " ^ string_of_exp then_branch ^ " else " ^ string_of_exp else_branch | E_field (exp, id) -> string_of_exp exp ^ "." ^ string_of_id id @@ -1084,6 +1087,9 @@ let subtyp l env typ1 typ2 = ^ " 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 rec nexp_frees (Nexp_aux (nexp, l)) = match nexp with | Nexp_id _ -> typ_error l "Unimplemented Nexp_id in nexp_frees" @@ -1254,6 +1260,13 @@ let vector_typ n m ord typ = let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ +let lvector_typ env l typ = + match Env.get_default_order env with + | Ord_aux (Ord_inc, _) as ord -> + vector_typ (nconstant 0) l ord typ + | Ord_aux (Ord_dec, _) as ord -> + vector_typ (nminus l (nconstant 1)) l ord typ + let infer_lit env (L_aux (lit_aux, l) as lit) = match lit_aux with | L_unit -> mk_typ (Typ_id (mk_id "unit")) @@ -1343,6 +1356,10 @@ let typ_of (E_aux (_, (_, tannot))) = match tannot with | Some (_, typ) -> typ | None -> assert false +let pat_typ_of (P_aux (_, (_, tannot))) = match tannot with + | Some (_, typ) -> typ + | None -> assert false + let crule r env exp typ = incr depth; typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ); @@ -1494,6 +1511,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ = and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) = let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in + let switch_typ (P_aux (pat_aux, (l, Some (env, _)))) typ = P_aux (pat_aux, (l, Some (env, typ))) in match pat_aux with | P_id v -> begin @@ -1504,12 +1522,6 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env end | P_wild -> annot_pat P_wild typ, env - | P_typ (typ_annot, pat) -> - begin - subtyp l env typ_annot typ; - let (typed_pat, env) = bind_pat env pat typ_annot in - annot_pat (P_typ (typ_annot, typed_pat)) typ, env - end | P_tup pats -> begin match typ_aux with @@ -1521,16 +1533,46 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) try List.fold_left2 bind_tuple_pat ([], env) pats typs with | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length" in - annot_pat (P_tup tpats) typ, env + annot_pat (P_tup (List.rev tpats)) typ, env | _ -> typ_error l "Cannot bind tuple pattern against non tuple type" end - | P_lit lit -> + | _ -> + let (inferred_pat, env) = infer_pat env pat in + subtyp l env (pat_typ_of inferred_pat) typ; + switch_typ inferred_pat typ, env + +and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = + let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in + match pat_aux with + | P_id v -> begin - let lit_typ = infer_lit env lit in - subtyp l env lit_typ typ; (* CHECK: is the the correct way round? *) - annot_pat (P_lit lit) typ, env + match Env.lookup_id v env with + | Local (Immutable, _) | Unbound -> + typ_error l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation") + | Local (Mutable, _) | Register _ -> + typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat) + | Enum enum -> annot_pat (P_id v) enum, env end - | _ -> typ_error l ("Unhandled pat " ^ string_of_pat pat) + | P_typ (typ_annot, pat) -> + let (typed_pat, env) = bind_pat env pat typ_annot in + annot_pat (P_typ (typ_annot, typed_pat)) typ_annot, env + | P_lit lit -> + annot_pat (P_lit lit) (infer_lit env lit), env + | P_vector_concat (pat :: pats) -> + let fold_pats (pats, env) pat = + let inferred_pat, env = infer_pat env pat in + pats @ [inferred_pat], env + in + let (inferred_pat :: inferred_pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in + let (_, len, _, vtyp) = destructure_vec_typ l (pat_typ_of inferred_pat) in + let fold_len len pat = + let (_, len', _, vtyp') = destructure_vec_typ l (pat_typ_of pat) in + typ_equality l env vtyp vtyp'; + nsum len len' + 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 + | _ -> 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) = let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, Some (env, mk_typ (Typ_id (mk_id "unit"))))) in @@ -1557,7 +1599,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as | _, _ -> typ_error l "Not implemented this register field type yet..." in let checked_exp = crule check_exp env exp vec_typ in - annot_assign (annot_lexp (LEXP_id v) vec_typ) checked_exp, env + annot_assign (annot_lexp (LEXP_field (annot_lexp (LEXP_id v) regtyp, field)) vec_typ) checked_exp, env | _ -> typ_error l "Field l-expression has invalid type" end | _ -> diff --git a/src/type_check_new.mli b/src/type_check_new.mli index cf0500a5..e8685bb2 100644 --- a/src/type_check_new.mli +++ b/src/type_check_new.mli @@ -67,6 +67,7 @@ module Env : sig val lookup_id : id -> t -> lvar val fresh_kid : t -> kid val expand_synonyms : t -> typ -> typ + val no_casts : t -> t val empty : t end |