summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml332
-rw-r--r--src/initial_check.mli7
-rw-r--r--src/parser.mly52
-rw-r--r--src/process_file.ml12
-rw-r--r--src/process_file.mli4
-rw-r--r--src/sail.ml2
-rw-r--r--src/sail_lib.ml2
-rw-r--r--src/type_check.ml7
-rw-r--r--src/type_internal.ml1
-rw-r--r--src/type_internal.mli1
10 files changed, 249 insertions, 171 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 3c1ab601..46a90742 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -4,7 +4,8 @@ open Ast
type kind = Type_internal.kind
type typ = Type_internal.t
-type envs = Nameset.t * kind Envmap.t * tannot Envmap.t
+(*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *)
+type envs = Nameset.t * kind Envmap.t * order
type 'a envs_out = 'a * envs
let id_to_string (Id_aux(id,l)) =
@@ -78,7 +79,7 @@ let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),
| K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) }
| _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None
-let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
+let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) : Ast.typ =
match t with
| Parse_ast.ATyp_aux(t,l) ->
Typ_aux( (match t with
@@ -100,10 +101,48 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
| K_infer -> k.k <- K_Typ; Typ_var v
| _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
| None -> typ_error l "Encountered an unbound variable" None (Some v) None)
- | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env arg),
- (to_ast_typ k_env ret),
+ | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env def_ord arg),
+ (to_ast_typ k_env def_ord ret),
(to_ast_effects k_env efct))
- | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env) typs)
+ | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs)
+ | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_tb",il), [ b; r; ord ; ti]) ->
+ let make_r bot top =
+ match bot,top with
+ | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) ->
+ Parse_ast.ATyp_aux(Parse_ast.ATyp_constant ((t-b)+1),l)
+ | bot,(Parse_ast.ATyp_aux(_,l) as top) ->
+ Parse_ast.ATyp_aux((Parse_ast.ATyp_sum
+ ((Parse_ast.ATyp_aux
+ (Parse_ast.ATyp_sum (top,
+ Parse_ast.ATyp_aux(Parse_ast.ATyp_constant 1,Parse_ast.Unknown)),
+ Parse_ast.Unknown)),
+ (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in
+ let base = to_ast_nexp k_env b in
+ let rise = match def_ord with
+ | Ord_aux(Ord_inc,dl) -> to_ast_nexp k_env (make_r b r)
+ | Ord_aux(Ord_dec,dl) -> to_ast_nexp k_env (make_r r b)
+ | _ -> raise (Reporting_basic.err_unreachable l "Default order not inc or dec") in
+ Typ_app(Id_aux(Id "vector",il),
+ [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown);
+ Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown);
+ Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown);
+ Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);])
+ | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) ->
+ let make_sub_one t =
+ match t with
+ | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (t-1),l)
+ | t -> (Parse_ast.ATyp_aux
+ (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (-1),Parse_ast.Unknown)),
+ Parse_ast.Unknown)) in
+ let (base,rise) = match def_ord with
+ | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r)
+ | Ord_aux(Ord_dec,dl) -> (to_ast_nexp k_env (make_sub_one r)), (to_ast_nexp k_env r)
+ | _ -> raise (Reporting_basic.err_unreachable l "Default order not inc or dec") in
+ Typ_app(Id_aux(Id "vector",il),
+ [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown);
+ Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown);
+ Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown);
+ Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);])
| Parse_ast.ATyp_app(pid,typs) ->
let id = to_ast_id pid in
let k = Envmap.apply k_env (id_to_string id) in
@@ -111,7 +150,7 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
| Some({k = K_Lam(args,t)}) ->
if ((List.length args) = (List.length typs))
then
- Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env k a)) args typs))
+ Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env def_ord k a)) args typs))
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)
@@ -150,23 +189,24 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
times_loop typs false
| _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None)
-and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order =
+and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order =
match o with
| Parse_ast.ATyp_aux(t,l) ->
- Ord_aux( (match t with
- | Parse_ast.ATyp_var(v) ->
- let v = to_ast_var v in
- let mk = Envmap.apply k_env (var_to_string v) in
- (match mk with
- | Some(k) -> (match k.k with
- | K_Ord -> Ord_var v
- | K_infer -> k.k <- K_Ord; Ord_var v
- | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k))
- | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
- | Parse_ast.ATyp_inc -> Ord_inc
- | Parse_ast.ATyp_dec -> Ord_dec
- | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None None
- ), l)
+ (match t with
+ | Parse_ast.ATyp_var(v) ->
+ let v = to_ast_var v in
+ let mk = Envmap.apply k_env (var_to_string v) in
+ (match mk with
+ | Some(k) -> (match k.k with
+ | K_Ord -> Ord_aux(Ord_var v, l)
+ | K_infer -> k.k <- K_Ord; Ord_aux(Ord_var v,l)
+ | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k))
+ | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
+ | Parse_ast.ATyp_inc -> Ord_aux(Ord_inc,l)
+ | Parse_ast.ATyp_dec -> Ord_aux(Ord_dec,l)
+ | Parse_ast.ATyp_default_ord -> def_ord
+ | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None None
+ )
and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
match e with
@@ -198,13 +238,13 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
| _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
), l)
-and to_ast_typ_arg (k_env : kind Envmap.t) (kind : kind) (arg : Parse_ast.atyp) : Ast.typ_arg =
+and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg : Parse_ast.atyp) : Ast.typ_arg =
let l = (match arg with Parse_ast.ATyp_aux(_,l) -> l) in
Typ_arg_aux (
(match kind.k with
- | K_Typ -> Typ_arg_typ (to_ast_typ k_env arg)
+ | K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg)
| K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg)
- | K_Ord -> Typ_arg_order (to_ast_order k_env arg)
+ | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg)
| K_Efct -> Typ_arg_effect (to_ast_effects k_env arg)
| _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")),
l)
@@ -278,12 +318,12 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant
let lst,k_env,local_env = to_ast_q_items k_env Nameset.empty Envmap.empty qlist in
TypQ_aux(TypQ_tq(lst),l), k_env, local_env)
-let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm * kind Envmap.t * kind Envmap.t =
+let to_ast_typschm (k_env:kind Envmap.t) (def_ord:order) (tschm:Parse_ast.typschm) :Ast.typschm * kind Envmap.t * 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,local_env = to_ast_typquant k_env tquant in
- let typ = to_ast_typ k_env t in
+ let typ = to_ast_typ k_env def_ord t in
TypSchm_aux(TypSchm_ts(tq,typ),l),k_env,local_env)
let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit =
@@ -301,123 +341,132 @@ let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit =
| Parse_ast.L_string(s) -> L_string(s))
,l)
-let rec to_ast_pat (k_env : kind Envmap.t) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : tannot pat =
+let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : tannot pat =
P_aux(
(match pat with
| Parse_ast.P_lit(lit) -> P_lit(to_ast_lit lit)
| Parse_ast.P_wild -> P_wild
- | Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env pat,to_ast_id id)
- | Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env typ,to_ast_pat k_env pat)
+ | Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id)
+ | Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat)
| Parse_ast.P_id(id) -> P_id(to_ast_id id)
| Parse_ast.P_app(id,pats) ->
if pats = []
then P_id (to_ast_id id)
- else P_app(to_ast_id id, List.map (to_ast_pat k_env) pats)
- | Parse_ast.P_record(fpats,_) -> P_record(List.map
- (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) -> FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env fp),(l,NoTyp)))
- fpats, false)
- | Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env) pats)
- | Parse_ast.P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_ast_pat k_env pat) ipats)
- | Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env) pats)
- | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env) pats)
- | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env) pats)
+ else P_app(to_ast_id id, List.map (to_ast_pat k_env def_ord) pats)
+ | Parse_ast.P_record(fpats,_) ->
+ P_record(List.map
+ (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) ->
+ FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,NoTyp)))
+ fpats, false)
+ | Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env def_ord) pats)
+ | Parse_ast.P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_ast_pat k_env def_ord pat) ipats)
+ | Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env def_ord) pats)
+ | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats)
+ | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats)
), (l,NoTyp))
-let rec to_ast_letbind (k_env : kind Envmap.t) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : tannot letbind =
+let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (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)
+ let typsch, k_env, _ = to_ast_typschm k_env def_ord typschm in
+ LB_val_explicit(typsch,to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
| Parse_ast.LB_val_implicit(pat,exp) ->
- LB_val_implicit(to_ast_pat k_env pat, to_ast_exp k_env exp)
+ LB_val_implicit(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
), (l,NoTyp))
-and 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) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot exp =
E_aux(
(match exp with
| Parse_ast.E_block(exps) ->
- (match to_ast_fexps false k_env exps with
+ (match to_ast_fexps false k_env def_ord exps with
| Some(fexps) -> E_record(fexps)
- | None -> E_block(List.map (to_ast_exp k_env) exps))
- | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env) exps)
+ | None -> E_block(List.map (to_ast_exp k_env def_ord) exps))
+ | Parse_ast.E_nondet(exps) -> E_nondet(List.map (to_ast_exp k_env def_ord) 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_cast(typ,exp) -> E_cast(to_ast_typ k_env def_ord typ, to_ast_exp k_env def_ord exp)
| Parse_ast.E_app(f,args) ->
- (match List.map (to_ast_exp k_env) args with
+ (match List.map (to_ast_exp k_env def_ord) args with
| [] -> E_app(to_ast_id f, [])
| [E_aux(E_tuple(exps),_)] -> E_app(to_ast_id f, exps)
| exps -> E_app(to_ast_id f, exps))
- | 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_app_infix(left,op,right) ->
+ E_app_infix(to_ast_exp k_env def_ord left, to_ast_id op, to_ast_exp k_env def_ord right)
+ | Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env def_ord) exps)
+ | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3)
| Parse_ast.E_for(id,e1,e2,e3,atyp,e4) ->
- E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3,to_ast_order k_env atyp, to_ast_exp k_env e4)
+ E_for(to_ast_id id,to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2,
+ to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4)
| Parse_ast.E_vector(exps) ->
- (match to_ast_iexps false k_env exps with
+ (match to_ast_iexps false k_env def_ord exps with
| Some([]) -> E_vector([])
| Some(iexps) -> E_vector_indexed(iexps,
Def_val_aux(Def_val_empty,(l,NoTyp)))
- | None -> E_vector(List.map (to_ast_exp k_env) exps))
+ | None -> E_vector(List.map (to_ast_exp k_env def_ord) exps))
| Parse_ast.E_vector_indexed(iexps,Parse_ast.Def_val_aux(default,dl)) ->
- (match to_ast_iexps true k_env iexps with
+ (match to_ast_iexps true k_env def_ord iexps with
| Some(iexps) -> E_vector_indexed (iexps,
Def_val_aux((match default with
| Parse_ast.Def_val_empty -> Def_val_empty
- | Parse_ast.Def_val_dec e -> Def_val_dec (to_ast_exp k_env e)),(dl,NoTyp)))
+ | Parse_ast.Def_val_dec e -> Def_val_dec (to_ast_exp k_env def_ord e)),(dl,NoTyp)))
| _ -> raise (Reporting_basic.err_unreachable l "to_ast_iexps didn't throw error"))
- | 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_vector_append(e1,e2) -> E_vector_append(to_ast_exp k_env e1,to_ast_exp k_env e2)
- | 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_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
+ | Parse_ast.E_vector_subrange(vex,exp1,exp2) ->
+ E_vector_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
+ | Parse_ast.E_vector_update(vex,exp1,exp2) ->
+ E_vector_update(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
+ | Parse_ast.E_vector_update_subrange(vex,e1,e2,e3) ->
+ E_vector_update_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord e1,
+ to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3)
+ | Parse_ast.E_vector_append(e1,e2) -> E_vector_append(to_ast_exp k_env def_ord e1,to_ast_exp k_env def_ord e2)
+ | Parse_ast.E_list(exps) -> E_list(List.map (to_ast_exp k_env def_ord) exps)
+ | Parse_ast.E_cons(e1,e2) -> E_cons(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord 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)
+ (match to_ast_fexps true k_env def_ord fexps with
+ | Some(fexps) -> E_record_update(to_ast_exp k_env def_ord 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)
- | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env exp)
+ | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id)
+ | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
+ | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp)
+ | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp)
+ | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp)
), (l,NoTyp))
-and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp =
+and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp =
LEXP_aux(
(match exp with
| Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
| Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) ->
(match f with
| Parse_ast.Id(id) ->
- (match List.map (to_ast_exp k_env) args with
+ (match List.map (to_ast_exp k_env def_ord) args with
| [] -> LEXP_memory(to_ast_id f',[])
| [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps)
| args -> LEXP_memory(to_ast_id f', args))
| _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
| Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
- LEXP_cast(to_ast_typ k_env typ, to_ast_id id)
- | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp)
- | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
- | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id)
+ LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id)
+ | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
+ | Parse_ast.E_vector_subrange(vexp,exp1,exp2) ->
+ LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
+ | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id)
| _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
, (l,NoTyp))
-and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp =
+and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (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,NoTyp))
+ | Parse_ast.Pat_exp(pat,exp) -> Pat_aux(Pat_exp(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,NoTyp))
-and to_ast_fexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_ast.exp list) : tannot fexps option =
+and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : tannot fexps option =
match exps with
| [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,NoTyp)))
- | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env fexp in
+ | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env def_ord fexp in
(match maybe_fexp,maybe_error with
| Some(fexp),None ->
- (match (to_ast_fexps fail_on_error k_env exps) with
+ (match (to_ast_fexps fail_on_error k_env def_ord exps) with
| Some(FES_aux(FES_Fexps(fexps,_),l)) -> Some(FES_aux(FES_Fexps(fexp::fexps,false),l))
| _ -> None)
| None,Some(l,msg) ->
@@ -426,12 +475,12 @@ and to_ast_fexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_as
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 =
+and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (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,NoTyp))),None
+ Some(FE_aux(FE_Fexp(to_ast_id id, to_ast_exp k_env def_ord r), (l,NoTyp))),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) ->
@@ -441,12 +490,12 @@ and to_ast_record_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_as
| _ ->
None,Some(l, "Expected a field assignment to be identifier = expression")
-and to_ast_iexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_ast.exp list) : (int * tannot exp) list option =
+and to_ast_iexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps:Parse_ast.exp list):(int * tannot exp) list option =
match exps with
| [] -> Some([])
- | iexp::exps -> (match to_iexp_try k_env iexp with
+ | iexp::exps -> (match to_iexp_try k_env def_ord iexp with
| Some(iexp),None ->
- (match to_ast_iexps fail_on_error k_env exps with
+ (match to_ast_iexps fail_on_error k_env def_ord exps with
| Some(iexps) -> Some(iexp::iexps)
| _ -> None)
| None,Some(l,msg) ->
@@ -454,19 +503,19 @@ and to_ast_iexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_as
then typ_error l msg None None None
else None
| _ -> None)
-and to_iexp_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l): Parse_ast.exp): ((int * tannot exp) option * (l*string) option) =
+and to_iexp_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l): Parse_ast.exp): ((int * tannot exp) 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_lit(Parse_ast.L_aux (Parse_ast.L_num i,ll)),cl), Parse_ast.Id_aux(Parse_ast.Id("="),leq) ->
- Some(i,to_ast_exp k_env r),None
+ Some(i,to_ast_exp k_env def_ord r),None
| Parse_ast.E_aux(_,li), Parse_ast.Id_aux (Parse_ast.Id("="),leq) ->
None,(Some(li,"Expected a constant number to begin this indexed vector assignemnt"))
| Parse_ast.E_aux(_,cl), Parse_ast.Id_aux(_,leq) ->
None,(Some(leq,"Expected an indexed vector assignment constant = expression")))
| _ -> None,(Some(l,"Expected an indexed vector assignment: constant = expression"))
-let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_spec) envs_out =
+let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : (tannot default_spec) envs_out =
match default with
| Parse_ast.DT_aux(df,l) ->
(match df with
@@ -474,25 +523,34 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe
let k,k_typ = to_ast_base_kind bk in
let v = to_ast_var v in
let key = var_to_string v in
- DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),t_env)
+ DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),default_order)
| Parse_ast.DT_typ(typschm,id) ->
- let tps,_,_ = to_ast_typschm k_env typschm in
- DT_aux(DT_typ(tps,to_ast_id id),l),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
- )
-
-let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec) envs_out =
+ let tps,_,_ = to_ast_typschm k_env default_order typschm in
+ DT_aux(DT_typ(tps,to_ast_id id),l),(names,k_env,default_order)
+ | Parse_ast.DT_order(bk,o) ->
+ let k,k_typ = to_ast_base_kind bk in
+ (match (k,o) with
+ | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) ->
+ let default_order = Ord_aux(Ord_inc,lo) in
+ DT_aux(DT_order default_order,l),(names,k_env,default_order)
+ | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) ->
+ let default_order = Ord_aux(Ord_dec,lo) in
+ DT_aux(DT_order default_order,l),(names,k_env,default_order)
+ | _ -> typ_error l "Inc and Dec must have kind Order" None None None))
+
+let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (tannot val_spec) envs_out =
match val_ with
| Parse_ast.VS_aux(vs,l) ->
(match vs with
| Parse_ast.VS_val_spec(ts,id) ->
- let typsch,_,_ = to_ast_typschm k_env ts in
- VS_aux(VS_val_spec(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,t_env)
+ let typsch,_,_ = to_ast_typschm k_env default_order ts in
+ VS_aux(VS_val_spec(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,default_order)
| Parse_ast.VS_extern_spec(ts,id,s) ->
- let typsch,_,_ = to_ast_typschm k_env ts in
- VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,NoTyp)),(names,k_env,t_env)
+ let typsch,_,_ = to_ast_typschm k_env default_order ts in
+ VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,NoTyp)),(names,k_env,default_order)
| Parse_ast.VS_extern_no_rename(ts,id) ->
- let typsch,_,_ = to_ast_typschm k_env ts in
- VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *)
+ let typsch,_,_ = to_ast_typschm k_env default_order ts in
+ VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,default_order))
let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) =
@@ -510,19 +568,19 @@ let rec to_ast_range (Parse_ast.BF_aux(r,l)) = (* TODO add check that ranges are
| Parse_ast.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)),
l)
-let to_ast_type_union k_env (Parse_ast.Tu_aux(tu,l)) =
+let to_ast_type_union k_env default_order (Parse_ast.Tu_aux(tu,l)) =
match tu with
- | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l))
+ | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env default_order atyp),(to_ast_id id)),l))
| Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l))
-let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_def) envs_out =
+let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_def) envs_out =
match td with
| Parse_ast.TD_aux(td,l) ->
(match td with
| 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,k_env,_ = to_ast_typschm k_env typschm in
+ let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in
let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,NoTyp)) in
let typ = (match typschm with
| TypSchm_aux(TypSchm_ts(tq,typ), _) ->
@@ -530,27 +588,27 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
| [] -> {k = K_Typ}
| typs -> {k= K_Lam(typs,{k=K_Typ})}
end) in
- td_abrv,(names,Envmap.insert k_env (key,typ),t_env)
+ td_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
| Parse_ast.TD_record(id,name_scm_opt,typq,fields,_) ->
let id = to_ast_id id in
let key = id_to_string id in
let typq,k_env,_ = to_ast_typquant k_env typq in
- let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *)
+ let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *)
let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
let typ = (match (typquant_to_quantkinds k_env typq) with
| [ ] -> {k = K_Typ}
| typs -> {k = K_Lam(typs,{k=K_Typ})}) in
- td_rec, (names,Envmap.insert k_env (key,typ), t_env)
+ td_rec, (names,Envmap.insert k_env (key,typ), def_ord)
| Parse_ast.TD_variant(id,name_scm_opt,typq,arms,_) ->
let id = to_ast_id id in
let key = id_to_string id in
let typq,k_env,_ = to_ast_typquant k_env typq in
- let arms = List.map (to_ast_type_union k_env) arms in (* Add check that all arms have unique names *)
+ let arms = List.map (to_ast_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
let typ = (match (typquant_to_quantkinds k_env typq) with
| [ ] -> {k = K_Typ}
| typs -> {k = K_Lam(typs,{k=K_Typ})}) in
- td_var, (names,Envmap.insert k_env (key,typ), t_env)
+ td_var, (names,Envmap.insert k_env (key,typ), def_ord)
| Parse_ast.TD_enum(id,name_scm_opt,enums,_) ->
let id = to_ast_id id in
let key = id_to_string id in
@@ -558,14 +616,14 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let keys = List.map id_to_string enums in
let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
- td_enum, (names,k_env,t_env)
+ td_enum, (names,k_env,def_ord)
| Parse_ast.TD_register(id,t1,t2,ranges) ->
let id = to_ast_id id in
let key = id_to_string id in
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
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,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),t_env))
+ TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
Rec_aux((match r with
@@ -573,27 +631,28 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
| Parse_ast.Rec_rec -> Rec_rec
),l)
-let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot_opt * kind Envmap.t * kind Envmap.t=
+let to_ast_tannot_opt (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.Typ_annot_opt_aux(tp,l)):tannot_opt * kind Envmap.t * 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,k_local = to_ast_typquant k_env tq in
- Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),l),k_env,k_local
+ Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env def_ord typ),l),k_env,k_local
let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : effect_opt =
match e with
| Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
| Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),l)
-let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
+let to_ast_funcl (names,k_env,def_ord) (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)
+ | Parse_ast.FCL_Funcl(id,pat,exp) ->
+ FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),l)
-let to_ast_fundef (names,k_env,t_env) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out =
+let to_ast_fundef (names,k_env,def_ord) (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,NoTyp)), (names,k_env,t_env)
+ let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord 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, def_ord)) funcls), (l,NoTyp)), (names,k_env,def_ord)
type def_progress =
No_def
@@ -610,34 +669,35 @@ let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : par
| Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
| _,_ -> def_in_progress id defs)
-let to_ast_alias_spec k_env (Parse_ast.E_aux(e,le)) =
+let to_ast_alias_spec k_env def_ord (Parse_ast.E_aux(e,le)) =
AL_aux(
(match e with
| Parse_ast.E_field(Parse_ast.E_aux(Parse_ast.E_id id,li), field) ->
AL_subreg(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_id field)
| Parse_ast.E_vector_access(Parse_ast.E_aux(Parse_ast.E_id id,li),range) ->
- AL_bit(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env range)
+ AL_bit(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env def_ord range)
| Parse_ast.E_vector_subrange(Parse_ast.E_aux(Parse_ast.E_id id,li),base,stop) ->
- AL_slice(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env base,to_ast_exp k_env stop)
+ AL_slice(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env def_ord base,to_ast_exp k_env def_ord stop)
| Parse_ast.E_vector_append(Parse_ast.E_aux(Parse_ast.E_id first,lf),
Parse_ast.E_aux(Parse_ast.E_id second,ls)) ->
AL_concat(RI_aux(RI_id (to_ast_id first),(lf,NoTyp)),
RI_aux(RI_id (to_ast_id second),(ls,NoTyp)))
+ | _ -> raise (Reporting_basic.err_unreachable le "Found an expression not supported by parser in to_ast_alias_spec")
), (le,NoTyp))
-let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(regdec,l)) =
+let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
DEC_aux(
(match regdec with
| Parse_ast.DEC_reg(typ,id) ->
- DEC_reg(to_ast_typ k_env typ,to_ast_id id)
+ DEC_reg(to_ast_typ k_env def_ord typ,to_ast_id id)
| Parse_ast.DEC_alias(id,e) ->
- DEC_alias(to_ast_id id,to_ast_alias_spec k_env e)
+ DEC_alias(to_ast_id id,to_ast_alias_spec k_env def_ord e)
| Parse_ast.DEC_typ_alias(typ,id,e) ->
- DEC_typ_alias(to_ast_typ k_env typ,to_ast_id id,to_ast_alias_spec k_env e)
+ DEC_typ_alias(to_ast_typ k_env def_ord typ,to_ast_id id,to_ast_alias_spec k_env def_ord e)
),(l,NoTyp))
-let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (id * partial_def) list =
- let envs = (names,k_env,t_env) in
+let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list =
+ let envs = (names,k_env,def_ord) in
match def with
| Parse_ast.DEF_type(t_def) ->
let td,envs = to_ast_typedef envs t_def in
@@ -646,7 +706,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
let fd,envs = to_ast_fundef envs f_def in
((Finished(DEF_fundef(fd))),envs),partial_defs
| Parse_ast.DEF_val(lbind) ->
- let lb = to_ast_letbind k_env lbind in
+ let lb = to_ast_letbind k_env def_ord lbind in
((Finished(DEF_val(lb))),envs),partial_defs
| Parse_ast.DEF_spec(val_spec) ->
let vs,envs = to_ast_spec envs val_spec in
@@ -661,7 +721,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
(match sd with
| Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
let rec_opt = to_ast_rec rec_opt in
- let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
+ let tannot,k_env',k_local = to_ast_tannot_opt k_env def_ord tannot_opt in
let effects_opt = to_ast_effects_opt k_env' effects_opt in
let id = to_ast_id id in
(match (def_in_progress id partial_defs) with
@@ -677,7 +737,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
| Some(d,k) ->
(match !d with
| DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false ->
- let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in
+ let funcl = to_ast_funcl (names,Envmap.union k k_env,def_ord) funcl in
d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),false;
(No_def,envs),partial_defs
| _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
@@ -688,7 +748,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
let typq, k_env',_ = to_ast_typquant k_env typquant in
(match (def_in_progress id partial_defs) with
| None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,NoTyp)))),false) in
- (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
+ (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),def_ord)),(id,(partial_def,k_env'))::partial_defs
| Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
| Parse_ast.SD_scattered_unioncl(id,tu) ->
let id = to_ast_id id in
@@ -697,7 +757,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
| Some(d,k) ->
(match !d with
| DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false ->
- d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),false;
+ d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k def_ord tu],false),tl)),false;
(No_def,envs),partial_defs
| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
@@ -732,12 +792,12 @@ let rec to_ast_defs_helper envs partial_defs = function
then (fst !d) :: defs, envs, partial_defs
else typ_error l "Scattered type definition never ended" (Some id) None None))
-let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : tannot Envmap.t) (Parse_ast.Defs(defs)) =
- let defs,(_,k_env,_),partial_defs = to_ast_defs_helper (default_names,kind_env,typ_env) [] defs in
+let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : order) (Parse_ast.Defs(defs)) =
+ let defs,(_,k_env,def_ord),partial_defs = to_ast_defs_helper (default_names,kind_env,def_ord) [] defs in
List.iter
(fun (id,(d,k)) ->
(match !d with
| (d,false) -> typ_error Parse_ast.Unknown "Scattered definition never ended" (Some id) None None
| (_, true) -> ()))
partial_defs;
- (Defs defs),k_env
+ (Defs defs),k_env,def_ord
diff --git a/src/initial_check.mli b/src/initial_check.mli
index feed37b8..14108e08 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -4,8 +4,9 @@ open Type_internal
type kind = Type_internal.kind
type typ = Type_internal.t
-type envs = Nameset.t * kind Envmap.t * tannot Envmap.t
+(*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *)
+type envs = Nameset.t * kind Envmap.t * Ast.order
type 'a envs_out = 'a * envs
-val to_ast : Nameset.t -> kind Envmap.t -> tannot Envmap.t -> Parse_ast.defs -> tannot defs * kind Envmap.t
-val to_ast_exp : kind Envmap.t -> Parse_ast.exp -> Type_internal.tannot Ast.exp
+val to_ast : Nameset.t -> kind Envmap.t -> Ast.order -> Parse_ast.defs -> tannot defs * kind Envmap.t * Ast.order
+val to_ast_exp : kind Envmap.t -> Ast.order -> Parse_ast.exp -> Type_internal.tannot Ast.exp
diff --git a/src/parser.mly b/src/parser.mly
index b36085a5..e805b4b5 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -105,18 +105,25 @@ let make_r bot top =
ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)),
(ATyp_aux ((ATyp_neg bot),Unknown)))), l)
-let make_vector_sugar_bounded is_inc typ typ1 typ2 =
- let rise,ord =
- if is_inc
- then make_r typ1 typ2,ATyp_inc
- else make_r typ2 typ1,ATyp_dec in
- ATyp_app(Id_aux(Id("vector"),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ])
-let make_vector_sugar typ typ1 =
- let sub_one = match typ1 with
- | ATyp_aux(ATyp_constant t,l) -> ATyp_aux(ATyp_constant (t-1),l)
- | ATyp_aux(_, l) -> ATyp_aux (ATyp_sum (typ1,
- ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l) in
- make_vector_sugar_bounded true typ (ATyp_aux(ATyp_constant(0),Unknown)) sub_one
+let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 =
+ let (rise,ord,name) =
+ if order_set
+ then if is_inc
+ then (make_r typ1 typ2,ATyp_inc,name)
+ else (make_r typ2 typ1,ATyp_dec,name)
+ else if name = "vector"
+ then (typ2, ATyp_default_ord,"vector_sugar_tb") (* rise not calculated, but top and bottom came from specification *)
+ else (typ2, ATyp_default_ord,"vector_sugar_r") (* rise and base not calculated, rise only from specification *) in
+ ATyp_app(Id_aux(Id(name),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ])
+let make_vector_sugar order_set is_inc typ typ1 =
+ let zero = (ATyp_aux(ATyp_constant 0,Unknown)) in
+ let (typ1,typ2) = match (order_set,is_inc,typ1) with
+ | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (t-1),l)
+ | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1,
+ ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l)
+ | (true,false,_) -> typ1,zero
+ | (false,_,_) -> zero,typ1 in
+ make_vector_sugar_bounded order_set is_inc "vector_sugar_r" typ typ1 typ2
%}
@@ -336,21 +343,21 @@ vec_typ:
| atomic_typ
{ $1 }
| tid Lsquare nexp_typ Rsquare
- { tloc (make_vector_sugar (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
+ { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
| tid Lsquare nexp_typ Colon nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+ { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
| tid Lsquare nexp_typ LtColon nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+ { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
| tid Lsquare nexp_typ ColonGt nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+ { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
| tyvar Lsquare nexp_typ Rsquare
- { tloc (make_vector_sugar (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) }
+ { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) }
| tyvar Lsquare nexp_typ Colon nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
+ { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
| tyvar Lsquare nexp_typ LtColon nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
+ { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
| tyvar Lsquare nexp_typ ColonGt nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded false (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
+ { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
app_typs:
| nexp_typ
@@ -1116,10 +1123,13 @@ type_def:
| Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
{ tdloc (TD_register($2, $7, $9, $12)) }
-
default_typ:
| Default atomic_kind tyvar
{ defloc (DT_kind($2,$3)) }
+ | Default atomic_kind Inc
+ { defloc (DT_order($2, tloc (ATyp_inc))) }
+ | Default atomic_kind Dec
+ { defloc (DT_order($2, tloc (ATyp_dec))) }
| Default typquant typ id
{ defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) }
| Default typ id
diff --git a/src/process_file.ml b/src/process_file.ml
index 98dd4db9..40325ba5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -86,14 +86,18 @@ let parse_file (f : string) : Parse_ast.defs =
| Lexer.LexError(s,p) ->
raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
-let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t)=
- Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs
+(*Should add a flag to say whether we want to consider Oinc or Odec the default order *)
+let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
+ Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
-let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) : Type_internal.tannot Ast.defs =
+let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs =
let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
Type_internal.namesch = Envmap.empty; Type_internal.enum_env = Envmap.empty;
- Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty} in
+ Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty;
+ Type_internal.default_o =
+ {Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc
+ | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec)};} in
Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env)) defs
let open_output_with_check file_name =
diff --git a/src/process_file.mli b/src/process_file.mli
index 49fe8254..29c6cb55 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -45,8 +45,8 @@
(**************************************************************************)
val parse_file : string -> Parse_ast.defs
-val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t
-val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Type_internal.tannot Ast.defs
+val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
+val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs
type out_type =
| Lem_ast_out
diff --git a/src/sail.ml b/src/sail.ml
index a3a52c1b..7359789b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -396,7 +396,7 @@ let main() =
then Printf.printf "L2 pre alpha \n"
else let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in
let asts = (List.map (fun (f,past) -> (f,convert_ast past)) parsed) in
- let chkedasts = (List.map (fun (f,(ast,kenv)) -> (f,check_ast ast kenv)) asts) in
+ let chkedasts = (List.map (fun (f,(ast,kenv,ord)) -> (f,check_ast ast kenv ord)) asts) in
begin
(if !(opt_print_verbose)
then ((Pretty_print.pp_defs stdout) (snd (List.hd chkedasts)))
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 66db451a..d1a5b891 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -12,7 +12,7 @@ let parse_exps s =
let lexbuf = Lexing.from_string s in
try
let pre_exps = Parser.nonempty_exp_list Lexer.token lexbuf in
- List.map (Initial_check.to_ast_exp Type_internal.initial_kind_env) pre_exps
+ List.map (Initial_check.to_ast_exp Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown))) pre_exps
with
| Parsing.Parse_error ->
let pos = Lexing.lexeme_start_p lexbuf in
diff --git a/src/type_check.ml b/src/type_check.ml
index 40a5f04c..fde2df33 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -224,9 +224,9 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let t',cs' = type_consistent (Patt l) d_env t expect_t in
(P_aux((P_record(pats',false)),(l,Base(([],t'),Emp_local,constraints@cs',pure_e))),env,constraints@cs',t'))
| P_vector pats ->
- let item_t = match expect_actual.t with
- | Tapp("vector",[b;r;o;TA_typ i]) -> i
- | Tuvar _ -> new_t ()
+ let (item_t, base, rise, ord) = match expect_actual.t with
+ | Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o)
+ | Tuvar _ -> (new_t (),new_n (),new_n(), d_env.default_o)
| _ -> typ_error l ("Expected a vector by pattern form, but a " ^ t_to_string expect_actual ^ " by type") in
let (pats',ts,t_envs,constraints) =
List.fold_right
@@ -1385,6 +1385,7 @@ let check_default envs (DT_aux(ds,l)) =
let (Env(d_env,t_env)) = envs in
match ds with
| DT_kind _ -> ((DT_aux(ds,l)),envs)
+ | DT_order ord -> (DT_aux(ds,l), Env({d_env with default_o = (aorder_to_ord ord)},t_env))
| DT_typ(typs,id) ->
let tannot = typschm_to_tannot envs typs Default in
(DT_aux(ds,l),
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 9834552e..27205c2e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -111,6 +111,7 @@ type def_envs = {
enum_env : (string list) emap;
rec_env : rec_env list;
alias_env : alias_kind emap;
+ default_o : order;
}
type exp = tannot Ast.exp
diff --git a/src/type_internal.mli b/src/type_internal.mli
index fb4f1948..f7e2d73f 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -109,6 +109,7 @@ type def_envs = {
enum_env : (string list) emap;
rec_env : rec_env list;
alias_env : alias_kind emap;
+ default_o : order;
}
type exp = tannot Ast.exp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:38:09 +0000