diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 186 |
1 files changed, 107 insertions, 79 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 704c290c..3ae9180b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -252,13 +252,13 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant let lst,k_env = to_ast_q_items k_env Nameset.empty qlist in TypQ_aux(TypQ_tq(lst),l), k_env) -let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm = +let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm * kind Envmap.t = match tschm with | Parse_ast.TypSchm_aux(ts,l) -> (match ts with | Parse_ast.TypSchm_ts(tquant,t) -> let tq,k_env = to_ast_typquant k_env tquant in let typ = to_ast_typ k_env t in - TypSchm_aux(TypSchm_ts(tq,typ),l)) + TypSchm_aux(TypSchm_ts(tq,typ),l),k_env) let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit = L_aux( @@ -293,75 +293,48 @@ let rec to_ast_pat (k_env : kind Envmap.t) (Parse_ast.P_aux(pat,l) : Parse_ast.p | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env) pats) ), (l,None)) -(* - -type -exp_aux = (* Expression *) - E_block of (exp) list (* block (parsing conflict with structs?) *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of atyp * exp (* cast *) - | E_app of exp * (exp) list (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of (exp) list (* tuple *) - | E_if of exp * exp * exp (* conditional *) - | E_vector of (exp) list (* vector (indexed from 0) *) - | E_vector_indexed of ((int * exp)) list (* vector (indexed consecutively) *) - | E_vector_access of exp * exp (* vector access *) - | E_vector_subrange of exp * exp * exp (* subvector extraction *) - | E_vector_update of exp * exp * exp (* vector functional update *) - | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) - | E_list of (exp) list (* list *) - | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) (*Not generated by parser, must be disambiguated from types *) - | E_record_update of exp * fexps (* functional update of struct *) - | E_field of exp * id (* field projection from struct *) - | E_case of exp * (pexp) list (* pattern matching *) - | E_let of letbind * exp (* let expression *) - | E_assign of exp * exp (* imperative assignment *) (*left side not disambiguated to lexp by parser*) - -__ ast __ - -and 'a exp_aux = (* Expression *) - E_block of ('a exp) list (* block (parsing conflict with structs?) *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * 'a exp (* cast *) - | E_app of 'a exp * ('a exp) list (* function application *) - | E_app_infix of 'a exp * id * 'a exp (* infix function application *) - | E_tuple of ('a exp) list (* tuple *) - | E_if of 'a exp * 'a exp * 'a exp (* conditional *) - | E_vector of ('a exp) list (* vector (indexed from 0) *) - | E_vector_indexed of ((int * 'a exp)) list (* vector (indexed consecutively) *) - | E_vector_access of 'a exp * 'a exp (* vector access *) - | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *) - | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *) - | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *) - | E_list of ('a exp) list (* list *) - | E_cons of 'a exp * 'a exp (* cons *) - | E_record of 'a fexps (* struct *) - | E_record_update of 'a exp * 'a fexps (* functional update of struct *) - | E_field of 'a exp * id (* field projection from struct *) - | E_case of 'a exp * ('a pexp) list (* pattern matching *) - | E_let of 'a letbind * 'a exp (* let expression *) - | E_assign of 'a lexp * 'a exp (* imperative assignment *) -*) +let rec to_ast_letbind (k_env : kind Envmap.t) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : tannot letbind = + LB_aux( + (match lb with + | Parse_ast.LB_val_explicit(typschm,pat,exp) -> + let typsch, k_env = to_ast_typschm k_env typschm in + LB_val_explicit(typsch,to_ast_pat k_env pat, to_ast_exp k_env exp) + | Parse_ast.LB_val_implicit(pat,exp) -> + LB_val_implicit(to_ast_pat k_env pat, to_ast_exp k_env exp) + ), (l,None)) -let rec to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot exp = +and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot exp = E_aux( (match exp with - | Parse_ast.E_block(exps) -> assert false + | Parse_ast.E_block(exps) -> + (match to_ast_fexps false k_env exps with + | Some(fexps) -> E_record(fexps) + | None -> E_block(List.map (to_ast_exp k_env) exps)) | Parse_ast.E_id(id) -> E_id(to_ast_id id) | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit) | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env typ, to_ast_exp k_env exp) - | Parse_ast.E_app(f,args) -> assert false - | Parse_ast.E_app_infix(left,op,right) -> assert false + | Parse_ast.E_app(f,args) -> E_app(to_ast_exp k_env f, List.map (to_ast_exp k_env) args) + | Parse_ast.E_app_infix(left,op,right) -> E_app_infix(to_ast_exp k_env left, to_ast_id op, to_ast_exp k_env right) | Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env) exps) | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3) | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env) exps) | Parse_ast.E_vector_indexed(iexps) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps) | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env vexp, to_ast_exp k_env exp) + | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2) + | Parse_ast.E_vector_update(vex,exp1,exp2) -> E_vector_update(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2) + | Parse_ast.E_vector_update_subrange(vex,e1,e2,e3) -> E_vector_update_subrange(to_ast_exp k_env vex, to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3) + | Parse_ast.E_list(exps) -> E_list(List.map (to_ast_exp k_env) exps) + | Parse_ast.E_cons(e1,e2) -> E_cons(to_ast_exp k_env e1, to_ast_exp k_env e2) + | Parse_ast.E_record _ -> raise (Reporting_basic.err_unreachable l "parser generated an E_record") + | Parse_ast.E_record_update(exp,fexps) -> + (match to_ast_fexps true k_env fexps with + | Some(fexps) -> E_record_update(to_ast_exp k_env exp, fexps) + | _ -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none")) + | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env exp, to_ast_id id) + | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env exp, List.map (to_ast_case k_env) pexps) + | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env leb, to_ast_exp k_env exp) + | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env lexp, to_ast_exp k_env exp) ), (l,None)) and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp = @@ -373,6 +346,40 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id) | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None) , (l,None)) + +and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp = + match pex with + | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env pat, to_ast_exp k_env exp),(l,None)) + +and to_ast_fexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_ast.exp list) : tannot fexps option = + match exps with + | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,None))) + | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env fexp in + (match maybe_fexp,maybe_error with + | Some(fexp),None -> + (match (to_ast_fexps fail_on_error k_env exps) with + | Some(FES_aux(FES_Fexps(fexps,_),l)) -> Some(FES_aux(FES_Fexps(fexp::fexps,false),l)) + | _ -> None) + | None,Some(l,msg) -> + if fail_on_error + then typ_error l msg None None + else None + | _ -> None) + +and to_ast_record_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot fexp option * (l * string) option = + match exp with + | Parse_ast.E_app_infix(left,op,r) -> + (match left, op with + | Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> + Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env r), (l,None))),None + | Parse_ast.E_aux(_,li) , Parse_ast.Id_aux(Parse_ast.Id("="),leq) -> + None,Some(li,"Expected an identifier to begin this field assignment") + | Parse_ast.E_aux(Parse_ast.E_id(id),li), Parse_ast.Id_aux(_,leq) -> + None,Some(leq,"Expected a field assignment to be identifier = expression") + | Parse_ast.E_aux(_,li),Parse_ast.Id_aux(_,leq) -> + None,Some(l,"Expected a field assignment to be identifier = expression")) + | _ -> + None,Some(l, "Expected a field assignment to be identifier = expression") let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_typing_spec) envs_out = match default with @@ -384,7 +391,7 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe let key = id_to_string id in DT_aux(DT_kind(k,id),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env) | Parse_ast.DT_typ(typschm,id) -> - let tps = to_ast_typschm k_env typschm in + let tps,_ = to_ast_typschm k_env typschm in DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *) ) @@ -393,7 +400,8 @@ let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec | Parse_ast.VS_aux(vs,l) -> (match vs with | Parse_ast.VS_val_spec(ts,id) -> - VS_aux(VS_val_spec(to_ast_typschm k_env ts,to_ast_id id),(l,None)),(names,k_env,t_env)) (*Do names and t_env need updating this pass? *) + let typsch,_ = to_ast_typschm k_env ts in + VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env)) (*Do names and t_env need updating this pass? *) let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = Name_sect_aux( @@ -417,7 +425,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de | Parse_ast.TD_abbrev(id,name_scm_opt,typschm) -> let id = to_ast_id id in let key = id_to_string id in - let typschm = to_ast_typschm k_env typschm in + let typschm,_ = to_ast_typschm k_env typschm in let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,None)) in let typ = (match typschm with | TypSchm_aux(TypSchm_ts(tq,typ), _) -> @@ -462,24 +470,41 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in TD_aux(TD_register(id,n1,n2,ranges),(l,None)), (names,k_env,t_env)) -(* +let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = + Rec_aux((match r with + | Parse_ast.Rec_nonrec -> Rec_nonrec + | Parse_ast.Rec_rec -> Rec_rec + ),l) -type -type_def = - TD_aux of type_def_aux * l +let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot tannot_opt * kind Envmap.t = + match tp with + | Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none") + | Parse_ast.Typ_annot_opt_some(tq,typ) -> + let typq,k_env = to_ast_typquant k_env tq in + Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env -type -type_def_aux = (* Type definition body *) - TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) +let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effects_opt_aux(e,l)) : tannot effects_opt = + match e with + | Parse_ast.Effects_opt_pure -> Effects_opt_aux(Effects_opt_pure,(l,None)) + | Parse_ast.Effects_opt_effects(typ) -> Effects_opt_aux(Effects_opt_effects(to_ast_effects k_env typ),(l,None)) + +let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) = + match fcl with + | Parse_ast.FCL_Funcl(id,pat,exp) -> FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env pat, to_ast_exp k_env exp),(l,None)) + +let to_ast_fundef (names,k_env,t_env) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = + match fd with + | Parse_ast.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> + let tannot_opt, k_env = to_ast_tannot_opt k_env tannot_opt in + FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, t_env)) funcls), (l,None)), (names,k_env,t_env) + +(* -*) +type +fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list -(* type def_aux = (* Top-level definition *) @@ -504,8 +529,12 @@ let to_ast_def (names, k_env, t_env) partial_defs def : ((tannot def) option) en | Parse_ast.DEF_type(t_def) -> let td,envs = to_ast_typedef envs t_def in ((Some(DEF_aux(DEF_type(td),(l,None)))),envs),partial_defs - | Parse_ast.DEF_fundef(f_def) -> assert false - | Parse_ast.DEF_val(lbind) -> assert false + | Parse_ast.DEF_fundef(f_def) -> + let fd,envs = to_ast_fundef envs f_def in + ((Some(DEF_aux(DEF_fundef(fd),(l,None)))),envs),partial_defs + | Parse_ast.DEF_val(lbind) -> + let lb = to_ast_letbind k_env lbind in + ((Some(DEF_aux(DEF_val(lb),(l,None)))),envs),partial_defs | Parse_ast.DEF_spec(val_spec) -> let vs,envs = to_ast_spec envs val_spec in ((Some(DEF_aux(DEF_spec(vs),(l,None)))),envs),partial_defs @@ -530,5 +559,4 @@ let rec to_ast_defs_helper envs partial_defs = function let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : t Envmap.t) (Parse_ast.Defs(defs)) = let defs,_,partial_defs = to_ast_defs_helper (default_names,kind_env,typ_env) [] defs in - (* (Defs defs) *) (*TODO there will be type defs in partial defs that need to replace "placeholders" in the def list *) - (Defs [ ] ) (* Until not all forms return assert false *) + (Defs defs) (*TODO there will be type defs in partial defs that need to replace "placeholders" in the def list *) |