diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lexer.mll | 4 | ||||
| -rw-r--r-- | src/parser.mly | 14 | ||||
| -rw-r--r-- | src/pretty_print.ml | 111 | ||||
| -rw-r--r-- | src/pretty_print.mli | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 1 |
5 files changed, 122 insertions, 10 deletions
diff --git a/src/lexer.mll b/src/lexer.mll index 0024b2b8..1aa5d18d 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -60,6 +60,7 @@ let kw_table = [ ("and", (fun _ -> And)); ("as", (fun _ -> As)); + ("bits", (fun _ -> Bits)); ("by", (fun _ -> By)); ("case", (fun _ -> Case)); ("clause", (fun _ -> Clause)); @@ -68,7 +69,7 @@ let kw_table = ("effect", (fun _ -> Effect)); ("Effects", (fun _ -> Effects)); ("end", (fun _ -> End)); - ("enum", (fun _ -> Enum)); + ("enumerate", (fun _ -> Enumerate)); ("else", (fun _ -> Else)); ("false", (fun _ -> False)); ("forall", (fun _ -> Forall)); @@ -81,6 +82,7 @@ let kw_table = ("member", (fun x -> Member)); ("Nat", (fun x -> Nat)); ("Order", (fun x -> Order)); + ("pure", (fun x -> Pure)); ("rec", (fun x -> Rec)); ("register", (fun x -> Register)); ("scattered", (fun x -> Scattered)); diff --git a/src/parser.mly b/src/parser.mly index 60969ebd..1d4b7a0e 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -120,7 +120,7 @@ let star = "*" /*Terminals with no content*/ -%token And As Bits By Case Clause Const Default Dec Effect Effects End Enum Else False +%token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else False %token Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register %token Scattered Struct Switch Then True Type TYPE Typedef Union With Val @@ -924,6 +924,14 @@ index_range_atomic: | Lparen index_range Rparen { $2 } +enum_body: + | id + { [$1] } + | id Semi + { [$1] } + | id Semi enum_body + { $1::$3 } + index_range: | index_range_atomic { $1 } @@ -968,6 +976,10 @@ type_def: { tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) } | Typedef id Eq Const Union Lcurly c_def_body Rcurly { tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) } + | Typedef id Eq Enumerate Lcurly enum_body Rcurly + { tdloc (TD_enum($2, mk_namesectn (), $6,false)) } + | Typedef id name_sect Eq Enumerate Lcurly enum_body Rcurly + { tdloc (TD_enum($2,$3,$7,false)) } | Typedef id Eq Register Bits Lsquare typ Colon typ Rsquare Lcurly r_def_body Rcurly { tdloc (TD_register($2, $7, $9, $12)) } diff --git a/src/pretty_print.ml b/src/pretty_print.ml index da7d978f..322415c1 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -62,10 +62,10 @@ let rec pp_format_typ (Typ_aux(t,_)) = match t with | Typ_var(id) -> pp_format_id id | Typ_wild -> "_" - | Typ_fn(arg,ret,efct) -> (parens is_atomic_typ arg (pp_format_typ arg)) ^ " -> " ^ + | Typ_fn(arg,ret,efct) -> "(" ^ (parens is_atomic_typ arg (pp_format_typ arg)) ^ " -> " ^ (parens is_atomic_typ ret (pp_format_typ ret)) ^ " " ^ - (pp_format_effects efct) - | Typ_tup(typs) -> "(" ^ (list_format ", " pp_format_typ typs) ^ ")" + (pp_format_effects efct) ^ ")" + | Typ_tup(typs) -> "(" ^ (list_format " * " pp_format_typ typs) ^ ")" | Typ_app(id,args) -> "(" ^ (pp_format_id id) ^ " " ^ (list_format " " pp_format_typ_arg args) ^ ")" and pp_format_nexp (Nexp_aux(n,_)) = match n with @@ -201,21 +201,120 @@ and pp_exp ppf (E_aux(e,_)) = | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")" | E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e + | E_for(id,exp1,exp2,exp3,exp4) -> + fprintf ppf "@[<0> %a %a %a %a %a %a %a %a@ @[<1> %a @] @]" + kwd "foreach " pp_id id kwd " from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 pp_exp exp4 + | E_vector(exps) -> fprintf ppf "@[<0> %a %a %a @]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]" + | E_vector_indexed(iexps) -> + let iformat ppf (i,e) = fprintf ppf "@[<1>%i %a %a %a@]" i kwd " = " pp_exp e kwd "," in + let lformat ppf (i,e) = fprintf ppf "@[<1>%i %a %a @]" i kwd " = " pp_exp e in + fprintf ppf "@[<0> %a %a %a @]" kwd "[" (list_pp iformat lformat) iexps kwd "]" + | E_vector_access(v,e) -> fprintf ppf "@[<0>%a %a %a %a@]" pp_exp v kwd "[" pp_exp e kwd "]" + | E_vector_subrange(v,e1,e2) -> fprintf ppf "@[<0> %a %a %a %a %a %a@]" pp_exp v kwd "[" pp_exp e1 kwd " : " pp_exp e1 kwd "]" + | E_vector_update(v,e1,e2) -> + fprintf ppf "@[<0> %a %a %a %a %a %a %a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd " = " pp_exp e2 kwd "]" + | E_vector_update_subrange(v,e1,e2,e3) -> + fprintf ppf "@[<0>%a%a %a %a %a %a %a %a %a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd ":" pp_exp e2 kwd " = " pp_exp e3 kwd "]" + | E_list(exps) -> fprintf ppf "@[<0> %a %a %a@]" kwd "[|" (list_pp pp_comma_exp pp_exp) exps kwd "|]" + | E_cons(e1,e2) -> fprintf ppf "@[<0> %a %a %a@]" pp_exp e1 kwd ":" pp_exp e2 + | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> fprintf ppf "@[<0> %a %a %a@]" kwd "{" (list_pp pp_semi_fexp pp_fexp) fexps kwd "}" + | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) -> + fprintf ppf "@[<0> %a %a %a %a %a @]" kwd "{" pp_exp exp kwd " with " (list_pp pp_semi_fexp pp_fexp) fexps kwd "}" + | E_field(fexp,id) -> fprintf ppf "@[<0> %a%a%a@]" pp_exp fexp kwd "." pp_id id + | E_case(exp,pexps) -> fprintf ppf "@[<0> %a %a %a %a %a@]" kwd "switch " pp_exp exp kwd "{" (list_pp pp_case pp_case) pexps kwd "}" + | E_let(leb,exp) -> fprintf ppf "@[<0> %a@ %a@ %a @]" pp_let leb kwd "in" pp_exp exp + | E_assign(lexp,exp) -> fprintf ppf "@[<0> %a %a %a@]" pp_lexp lexp kwd " := " pp_exp exp and pp_semi_exp ppf e = fprintf ppf "@[<1>%a %a@]" pp_exp e kwd ";" and pp_comma_exp ppf e = fprintf ppf "@[<1>%a %a@]" pp_exp e kwd "," +and pp_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>%a %a %a@]" pp_id id kwd " = " pp_exp exp +and pp_semi_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_fexp fexp kwd ";" + +and pp_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = fprintf ppf "@[<1>%a %a@ @[<1> %a @] @]" pp_pat pat kwd "-> " pp_exp exp + +and pp_lexp ppf (LEXP_aux(lexp,_)) = + match lexp with + | LEXP_id(id) -> pp_id ppf id + | LEXP_vector(v,exp) -> fprintf ppf "@[%a %a %a %a@]" pp_lexp v kwd "[" pp_exp exp kwd "]" + | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a %a %a %a %a %a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]" + | LEXP_field(v,id) -> fprintf ppf "@[%a%a%a@]" pp_lexp v kwd "." pp_id id + let pp_default ppf (DT_aux(df,_)) = match df with | DT_kind(bk,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_id id | DT_typ(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_typscm ts pp_id id -let pp_def ppf (DEF_aux(d,_)) = +let pp_spec ppf (VS_aux(VS_val_spec(ts,id),_)) = + fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id + +let pp_namescm ppf (Name_sect_aux(ns,_)) = + match ns with + | Name_sect_none -> fprintf ppf "" + | Name_sect_some(s) -> fprintf ppf "[%a \"%s\"]" kwd "name =" s + +let rec pp_range ppf (BF_aux(r,_)) = + match r with + | BF_single(i) -> fprintf ppf "%i" i + | BF_range(i1,i2) -> fprintf ppf "%i .. %i" i1 i2 + | BF_concat(ir1,ir2) -> fprintf ppf "%a %a %a" pp_range ir1 kwd ", " pp_range ir2 + +let pp_typdef ppf (TD_aux(td,_)) = + match td with + | TD_abbrev(id,namescm,typschm) -> + fprintf ppf "@[<0>%a %a %a %a %a@]@\n" kwd "typedef" pp_id id pp_namescm namescm kwd "=" pp_typscm typschm + | TD_record(id,nm,typq,fs,_) -> + let f_pp ppf (typ,id) = + fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in + fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n" + kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "struct" pp_typquant typq kwd "{" (list_pp f_pp f_pp) fs kwd "}" + | TD_variant(id,nm,typq,ar,_) -> + let a_pp ppf (typ,id) = + fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in + fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n" + kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "union" pp_typquant typq kwd "{" (list_pp a_pp a_pp) ar kwd "}" + | TD_enum(id,ns,enums,_) -> + let pp_id_semi ppf id = fprintf ppf "%a%a " pp_id id kwd ";" in + fprintf ppf "@[<0>%a %a %a %a %a %a%a %a@]@\n" + kwd "typedef" pp_id id pp_namescm ns kwd "=" kwd "enumerate" kwd "{" (list_pp pp_id_semi pp_id) enums kwd "}" + | TD_register(id,n1,n2,rs) -> + let pp_rid ppf (r,id) = fprintf ppf "%a %a %a%a " pp_range r kwd ":" pp_id id kwd ";" in + let pp_rids = (list_pp pp_rid pp_rid) in + fprintf ppf "@[<0>%a %a %a %a %a %a %a %a %a %a %a %a%a@]@\n" + kwd "typedef" pp_id id kwd "=" kwd "register" kwd "bits" kwd "[" pp_nexp n1 kwd ":" pp_nexp n2 kwd "]" kwd "{" pp_rids rs kwd "}" + +let pp_rec ppf (Rec_aux(r,_)) = + match r with + | Rec_nonrec -> fprintf ppf "" + | Rec_rec -> fprintf ppf "rec " + +let pp_tannot_opt ppf (Typ_annot_opt_aux(t,_)) = + match t with + | Typ_annot_opt_some(tq,typ) -> fprintf ppf "%a %a " pp_typquant tq pp_typ typ + +let pp_effects_opt ppf (Effects_opt_aux(e,_)) = + match e with + | Effects_opt_pure -> fprintf ppf "" + | Effects_opt_effects e -> pp_effects ppf e + +let pp_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = + fprintf ppf "@[<0>%a %a %a @[<1>%a@] @]@\n" pp_id id pp_pat pat kwd "=" pp_exp exp + +let pp_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) = + let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd "and" pp_funcl funcl in + fprintf ppf "@[<0>%a %a%a%a%a@ @[<1>%a@] @]@\n" + kwd "function" pp_rec r pp_tannot_opt typa pp_effects_opt efa pp_funcl (List.hd fcls) (list_pp pp_funcls pp_funcls) (List.tl fcls) + +let pp_def ppf (DEF_aux(d,(l,_))) = match d with | DEF_default(df) -> pp_default ppf df - -let pp_format_ast defs = "" + | DEF_spec(v_spec) -> pp_spec ppf v_spec + | DEF_type(t_def) -> pp_typdef ppf t_def + | DEF_fundef(f_def) -> pp_fundef ppf f_def + | DEF_val(lbind) -> pp_let ppf lbind + | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "register" pp_typ typ pp_id id + | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs") let pp_defs ppf (Defs(defs)) = fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 30f15181..ebe9301a 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -2,6 +2,4 @@ open Ast open Type_internal open Format -val pp_format_ast : tannot defs -> string - val pp_defs : Format.formatter -> tannot defs -> unit diff --git a/src/type_internal.ml b/src/type_internal.ml index c3258da1..1ad4d40c 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -68,6 +68,7 @@ let initial_kind_env = Envmap.from_list [ ("bool", {k = K_Typ}); ("nat", {k = K_Typ}); + ("unit", {k = K_Typ}); ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}; {k=K_Ord} ], {k = K_Typ}) }); ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ) |