diff options
| -rw-r--r-- | language/l2.lem | 3 | ||||
| -rw-r--r-- | language/l2.ml | 3 | ||||
| -rw-r--r-- | language/l2.ott | 3 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 | ||||
| -rw-r--r-- | language/l2_typ.ott | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 18 | ||||
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 5 | ||||
| -rw-r--r-- | src/parser.mly | 30 | ||||
| -rw-r--r-- | src/pretty_print.ml | 7 | ||||
| -rw-r--r-- | src/rewriter.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 51 | ||||
| -rw-r--r-- | src/type_internal.ml | 203 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
14 files changed, 218 insertions, 111 deletions
diff --git a/language/l2.lem b/language/l2.lem index d9b410cd..eb598113 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -50,8 +50,9 @@ type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) + | Nexp_neg of nexp (* For internal use *) and nexp = | Nexp_aux of nexp_aux * l diff --git a/language/l2.ml b/language/l2.ml index dc96020d..d4423c54 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -45,8 +45,9 @@ nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) + | Nexp_neg of nexp (* For internal use *) and nexp = Nexp_aux of nexp_aux * l diff --git a/language/l2.ott b/language/l2.ott index 77b2483b..59de79cd 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -166,8 +166,9 @@ nexp :: 'Nexp_' ::= | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} | nexp1 + nexp2 :: :: sum {{ com sum }} + | nexp1 - nexp2 :: :: minus {{ com subtraction, error for nexp1 to be smaller than nexp2 }} | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: :: neg {{ com For internal use. Not M as a dataconstructor is required }} + | neg nexp :: :: neg {{ com For internal use }} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 5aaf8086..ed594d3b 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -84,6 +84,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_constant of int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) + | ATyp_minus of atyp * atyp (* subtraction *) | ATyp_exp of atyp (* exponential *) | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) | ATyp_inc (* increasing (little-endian) *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 74522150..7126b9e0 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -168,6 +168,7 @@ atyp :: 'ATyp_' ::= | num :: :: constant {{ com constant }} | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} + | atyp1 - atyp2 :: :: minus {{ com subtraction }} | 2** atyp :: :: exp {{ com exponential }} | neg atyp :: :: neg {{ com Internal (but not M as I want a datatype constructor) negative nexp }} | ( atyp ) :: S :: paren {{ icho [[atyp]] }} diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 12baa059..3ffc5b2b 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -85,6 +85,7 @@ ne :: 'Ne_' ::= | infinity :: :: inf | ne1 * ne2 :: :: mult | ne1 + ... + nen :: :: add + | ne1 - ne2 :: :: minus | 2 ** ne :: :: exp | ( - ne ) :: :: unary | zero :: S :: zero diff --git a/src/initial_check.ml b/src/initial_check.ml index 9b285032..8c613f36 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -180,16 +180,14 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = Nexp_aux(Nexp_sum(n1,n2),l) | Parse_ast.ATyp_exp(t1) -> Nexp_aux(Nexp_exp(to_ast_nexp k_env t1),l) | Parse_ast.ATyp_neg(t1) -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l) - | Parse_ast.ATyp_tup(typs) -> - let rec times_loop (typs : Parse_ast.atyp list) (one_ok : bool) : nexp = - (match typs,one_ok with - | [],_ | [_],false -> raise (Reporting_basic.err_unreachable l "to_ast_nexp has ATyp_tup with empty list or list with one element") - | [t],true -> to_ast_nexp k_env t - | (t1::typs),_ -> let n1 = to_ast_nexp k_env t1 in - let n2 = times_loop typs true in - (Nexp_aux((Nexp_times(n1,n2)),l))) (*TODO This needs just a portion of the l, think about adding a way to split*) - in - times_loop typs false + | Parse_ast.ATyp_times(t1,t2) -> + let n1 = to_ast_nexp k_env t1 in + let n2 = to_ast_nexp k_env t2 in + Nexp_aux(Nexp_times(n1,n2),l) + | Parse_ast.ATyp_minus(t1,t2) -> + let n1 = to_ast_nexp k_env t1 in + let n2 = to_ast_nexp k_env t2 in + Nexp_aux(Nexp_minus(n1,n2),l) | _ -> 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) (def_ord : order) (o: Parse_ast.atyp) : Ast.order = diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 2724ba9c..1ea6df3e 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -141,12 +141,13 @@ let doc_typ, doc_atomic_typ, doc_nexp = and nexp ne = sum_typ ne and sum_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_sum(n1,n2) -> doc_op plus (sum_typ n1) (star_typ n2) + | Nexp_minus(n1,n2) -> doc_op minus (sum_typ n1) (star_typ n2) | _ -> star_typ ne and star_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_times(n1,n2) -> doc_op star (star_typ n1) (exp_typ n2) | _ -> exp_typ ne and exp_typ ((Nexp_aux(n,_)) as ne) = match n with - | Nexp_exp n1 -> doc_unop (string "2**") (neg_typ n1) + | Nexp_exp n1 -> doc_unop (string "2**") (atomic_nexp_typ n1) | _ -> neg_typ ne and neg_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_neg n1 -> @@ -158,7 +159,7 @@ let doc_typ, doc_atomic_typ, doc_nexp = and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_constant i -> doc_int i - | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ -> + | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _ -> group (parens (nexp ne)) (* expose doc_typ, doc_atomic_typ and doc_nexp *) diff --git a/src/parser.mly b/src/parser.mly index b6b7ecf3..2ae64887 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -393,29 +393,18 @@ app_num_typ: | Num { tloc (ATyp_constant $1) } -/* XXX this part of the parser makes absolutely no sense to me */ -star_typ_list: - | app_num_typ - { [$1] } - | app_num_typ Star star_typ_list - { $1::$3 } - star_typ: - | star_typ_list - { match $1 with - | [] -> assert false - | [t] -> t - (* XXX why is ATyp_tup star-separated here, but comma-separated - below? *) - | ts -> tloc (ATyp_tup(ts)) } + | app_num_typ + { $1 } + | app_num_typ Star nexp_typ + { tloc (ATyp_times ($1, $3)) } exp_typ: | star_typ { $1 } - | TwoStarStar nexp_typ + | TwoStarStar atomic_typ { tloc (ATyp_exp($2)) } -/* XXX this is wrong - for instance, 2** 3 + 5 is parsed as 2** (3+5) */ nexp_typ: | exp_typ { $1 } @@ -427,6 +416,15 @@ nexp_typ: { tloc (ATyp_sum((tlocl (ATyp_constant $1) 1 1),$3)) } | Lparen Num Plus nexp_typ Rparen { tloc (ATyp_sum((tlocl (ATyp_constant $2) 2 2),$4)) } + | atomic_typ Minus nexp_typ + { tloc (ATyp_minus($1,$3)) } + | Lparen atomic_typ Minus nexp_typ Rparen + { tloc (ATyp_minus($2,$4)) } + | Num Minus nexp_typ + { tloc (ATyp_minus((tlocl (ATyp_constant $1) 1 1),$3)) } + | Lparen Num Minus nexp_typ Rparen + { tloc (ATyp_minus((tlocl (ATyp_constant $2) 2 2),$4)) } + tup_typ_list: | app_typ Comma app_typ diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 8665d42d..9d9ed8a0 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -123,6 +123,7 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) = | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_int i) ^ ")" | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" + | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")" | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^ @@ -255,6 +256,7 @@ and pp_format_n n = | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")" | Npos_inf -> "Ne_inf" | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])" + | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")" | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")" @@ -704,12 +706,13 @@ let doc_typ, doc_atomic_typ, doc_nexp = and nexp ne = sum_typ ne and sum_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_sum(n1,n2) -> doc_op plus (sum_typ n1) (star_typ n2) + | Nexp_minus(n1,n2) -> doc_op minus (sum_typ n1) (star_typ n2) | _ -> star_typ ne and star_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_times(n1,n2) -> doc_op star (star_typ n1) (exp_typ n2) | _ -> exp_typ ne and exp_typ ((Nexp_aux(n,_)) as ne) = match n with - | Nexp_exp n1 -> doc_unop (string "2**") (neg_typ n1) + | Nexp_exp n1 -> doc_unop (string "2**") (atomic_nexp_typ n1) | _ -> neg_typ ne and neg_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_neg n1 -> @@ -721,7 +724,7 @@ let doc_typ, doc_atomic_typ, doc_nexp = and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_constant i -> doc_int i - | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ -> + | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) (* expose doc_typ, doc_atomic_typ and doc_nexp *) diff --git a/src/rewriter.ml b/src/rewriter.ml index afcba19b..9335ea5d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -21,6 +21,8 @@ let rec rewrite_nexp_to_exp program_vars l nexp = (l, (tag_annot typ (External (Some "add"))))) | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2), (l, tag_annot typ (External (Some "multiply")))) + | Nsub (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "-",l)),rewrite n2), + (l, tag_annot typ (External (Some "minus")))) | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))), (Id_aux (Id "**",l)), rewrite n), (l, tag_annot typ (External (Some "power")))) diff --git a/src/type_check.ml b/src/type_check.ml index 7ed4f19f..9723fd09 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -118,6 +118,7 @@ and anexp_to_nexp ((Nexp_aux(n,l)) : Ast.nexp) : nexp = | Nexp_constant i -> {nexp=Nconst (big_int_of_int i)} | Nexp_times(n1,n2) -> {nexp=Nmult(anexp_to_nexp n1,anexp_to_nexp n2)} | Nexp_sum(n1,n2) -> {nexp=Nadd(anexp_to_nexp n1,anexp_to_nexp n2)} + | Nexp_minus(n1,n2) -> {nexp=Nsub(anexp_to_nexp n1,anexp_to_nexp n2)} | Nexp_exp n -> {nexp=N2n(anexp_to_nexp n,None)} | Nexp_neg n -> {nexp=Nneg(anexp_to_nexp n)} and aeffect_to_effect ((Effect_aux(e,l)) : Ast.effect) : effect = @@ -188,9 +189,9 @@ let into_register d_env (t : tannot) : tannot = let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * bounds_env * t) = let (Env(d_env,t_env,b_env,tp_env)) = envs in - (*let _ = Printf.printf "checking pattern with expected type %s\n" (t_to_string expect_t) in*) + (*let _ = Printf.eprintf "checking pattern with expected type %s\n" (t_to_string expect_t) in*) let expect_t,cs = get_abbrev d_env expect_t in - (*let _ = Printf.printf "check pattern expect_t after abbrev %s\n" (t_to_string expect_t) in*) + (*let _ = Printf.eprintf "check pattern expect_t after abbrev %s\n" (t_to_string expect_t) in*) let expect_actual = match expect_t.t with | Tabbrev(_,t) -> t | _ -> expect_t in match p with | P_lit (L_aux(lit,l')) -> @@ -267,7 +268,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) | _ -> default) | P_app(id,pats) -> let i = id_to_string id in - (*let _ = Printf.printf "checking constructor pattern %s\n" i in*) + let _ = Printf.eprintf "checking constructor pattern %s\n" i in (match Envmap.apply t_env i with | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined") | Some(Base((params,t),Constructor,constraints,eft,bounds)) -> @@ -577,8 +578,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let cast_t = typ_subst tp_env cast_t in let ct = {t = Toptions(cast_t,None)} in let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param ct e in + let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" (t_to_string cast_t) (constraints_to_string cs) in let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false u e' cast_t in + let _ = Printf.eprintf "Type checking cast: after first coerce t' %s is and constraints are %s\n" (t_to_string t') (constraints_to_string cs2) in let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false cast_t e' expect_t in + let _ = Printf.eprintf "Type checking cast: after second coerce t' %s is and constraints are %s\n" (t_to_string t') (constraints_to_string cs3) in (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef)) | E_app(id,parms) -> let i = id_to_string id in @@ -605,7 +609,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let check_result ret imp tag cs ef parms = match (imp,imp_param) with | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) -> - (*let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in*) + let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in let internal_exp = let implicit = {t= Tapp("implicit",[TA_nexp n])} in let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in @@ -613,8 +617,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): type_coerce (Expr l) d_env Guarantee false false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) -> - (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in - let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in*) + let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in + let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in let internal_exp = let implicit_user = {t = Tapp("implicit",[TA_nexp ne])} in let implicit = {t= Tapp("implicit",[TA_nexp n])} in @@ -635,16 +639,16 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Some(Base(tp,Default,_,_,_)) -> typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use") | Some(Base((params,t),tag,cs,ef,bounds)) -> - (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*) + let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in let t,cs,ef,_ = subst params t cs ef in (match t.t with | Tfn(arg,ret,imp,ef') -> - (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in - let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in*) + let _ = Printf.eprintf "Checking funcation call of %s\n" i in + let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in let parms,arg_t,cs_p,ef_p = check_parms arg parms in - (*let _ = Printf.eprintf "Checked parms of %s\n" i in*) + let _ = Printf.eprintf "Checked parms of %s\n" i in let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' parms in - (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*) + let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in (e',ret_t,t_env,cs@cs_p@cs_r, bounds,union_effects ef' (union_effects ef_p ef_r)) | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) | Some(Overload(Base((params,t),tag,cs,ef,_),overload_return,variants)) -> @@ -1717,25 +1721,28 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, ^ id_to_string id ^ " differs from other definitions of " ^ id') | None -> Some(id_to_string id)) funcls None in let in_env = Envmap.apply t_env id in + let typ_params = match in_env with + | Some(Base( (params,u),Spec,constraints,eft,_)) -> params + | _ -> [] in let ret_t,param_t,tannot,t_param_env = match tannotopt with | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') -> let (ids,_,constraints) = typq_to_params envs typq in let t = typ_to_t false false typ in - let t,constraints,_,t_param_env = subst ids t constraints pure_e in + let t,constraints,_,t_param_env = subst (if ids=[] then typ_params else ids) t constraints pure_e in let p_t = new_t () in let ef = new_e () in t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef,nob),t_param_env in let check t_env tp_env imp_param = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> -(* let _ = Printf.eprintf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) + let _ = Printf.eprintf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in let t', _ = type_consistent (Patt l) d_env Require false param_t t' in let exp',_,_,cs_e,_,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in -(* let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in - let _ = Printf.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) in*) + let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in + let _ = Printf.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) in let cs = [CondCons(Fun l,cs_p,cs_e)] in (FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef,nob)))),(cs,ef))) funcls) in let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = @@ -1747,11 +1754,11 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, in match (in_env,tannot) with | Some(Base( (params,u),Spec,constraints,eft,_)), Base( (p',t),_,c',eft',_) -> - (*let _ = Printf.eprintf "Function %s is in env\n" id in*) + let _ = Printf.eprintf "Function %s is in env\n" id in let u,constraints,eft,t_param_env_spec = subst params u constraints eft in let t_param_cs = type_param_consistent l t_param_env_spec t_param_env in let _,cs_decs = type_consistent (Specc l) d_env Require false t u in - (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in*) + let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in let imp_param = match u.t with | Tfn(_,_,IP_user n,_) -> Some n | _ -> None in @@ -1760,14 +1767,14 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in let cs' = resolve_constraints (cs@cs_decs@constraints@c'@t_param_cs) in - (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in*) + let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in let tannot = check_tannot l tannot imp_param cs' ef in - (*let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*) + let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in let funcls = match imp_param with | Some {nexp = Nvar i} -> List.map (update_pattern i) funcls | _ -> funcls in - (*let _ = Printf.eprintf "done funcheck case 1\n" in*) + let _ = Printf.eprintf "done funcheck case 1\n" in (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,Envmap.insert t_env (id,tannot),b_env,tp_env) | _ , _-> @@ -1775,9 +1782,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let funcls,cs_ef = check t_env t_param_env None in let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in let cs' = resolve_constraints cs in - (*let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" id (constraints_to_string cs') in*) + let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" id (constraints_to_string cs') in let tannot = check_tannot l tannot None cs' ef in - (*let _ = Printf.eprintf "done funcheck case2\n" in*) + let _ = Printf.eprintf "done funcheck case2\n" in (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)),b_env,tp_env) diff --git a/src/type_internal.ml b/src/type_internal.ml index 989460a8..0e309d82 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -44,13 +44,14 @@ and nexp_aux = | Npos_inf | Nneg_inf | Nadd of nexp * nexp + | Nsub of nexp * nexp | Nmult of nexp * nexp | N2n of nexp * big_int option | Npow of nexp * int (* nexp raised to the int *) | Nneg of nexp (* Unary minus for representing new vector sizes after vector slicing *) | Ninexact (*Result of +inf + -inf which is neither less than nor greater than other numbers really *) | Nuvar of n_uvar -and n_uvar = { nindex : int; mutable nsubst : nexp option; mutable nin : bool; } +and n_uvar = { nindex : int; mutable nsubst : nexp option; mutable nin : bool; mutable leave_var : bool} and effect = { mutable effect : effect_aux } and effect_aux = | Evar of string @@ -158,7 +159,11 @@ let rec t_to_string t = match t.t with | Tid i -> i | Tvar i -> i - | Tfn(t1,t2,_,e) -> (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e + | Tfn(t1,t2,imp,e) -> + let implicit = match imp with + | IP_none -> "" + | IP_length n | IP_start n | IP_user n -> " with implicit parameter " ^ n_to_string n ^ " " in + (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e ^ implicit | Ttup(tups) -> "(" ^ string_of_list ", " t_to_string tups ^ ")" | Tapp(i,args) -> i ^ "<" ^ string_of_list ", " targ_to_string args ^ ">" | Tabbrev(ti,ta) -> (t_to_string ti) ^ " : " ^ (t_to_string ta) @@ -178,6 +183,7 @@ and n_to_string n = | Npos_inf -> "infinity" | Nneg_inf -> "-infinity" | Nadd(n1,n2) -> "("^ (n_to_string n1) ^ " + " ^ (n_to_string n2) ^")" + | Nsub(n1,n2) -> "("^ (n_to_string n1) ^ " - " ^ (n_to_string n2) ^ ")" | Nmult(n1,n2) -> "(" ^ (n_to_string n1) ^ " * " ^ (n_to_string n2) ^ ")" | N2n(n,None) -> "2**" ^ (n_to_string n) | N2n(n,Some i) -> "2**" ^ (n_to_string n) ^ "(*" ^ (string_of_big_int i) ^ "*)" @@ -338,6 +344,10 @@ let rec compare_nexps n1 n2 = | a -> a) | Nadd _ , _ -> -1 | _ , Nadd _ -> 1 + | Nsub(n1,n12),Nsub(n2,n22) -> + (match compare_nexps n1 n2 with + | 0 -> compare_nexps n12 n22 + | a -> a) | Npow(n1,_),Npow(n2,_)-> compare_nexps n1 n2 | Npow _ , _ -> -1 | _ , Npow _ -> 1 @@ -363,7 +373,7 @@ let rec contains_const n = | Nvar _ | Nuvar _ | Npow _ | N2n _ | Npos_inf | Nneg_inf -> false | Nconst _ -> true | Nneg n -> contains_const n - | Nmult(n1,n2) | Nadd(n1,n2) -> (contains_const n1) || (contains_const n2) + | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (contains_const n1) || (contains_const n2) let rec get_var n = match n.nexp with @@ -376,7 +386,7 @@ let rec get_all_nvar n = match n.nexp with | Nvar v -> [v] | Nneg n | N2n(n,_) | Npow(n,_) -> get_all_nvar n - | Nmult(n1,n2) | Nadd(n1,n2) -> (get_all_nvar n1)@(get_all_nvar n2) + | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (get_all_nvar n1)@(get_all_nvar n2) | _ -> [] let get_factor n = @@ -408,13 +418,14 @@ let increment_factor n i = let negate n = {nexp = Nmult ({nexp = Nconst (big_int_of_int (-1))},n)} let rec normalize_nexp n = - (* let _ = Printf.printf "Working on normalizing %s\n" (n_to_string n) in *) + (*let _ = Printf.eprintf "Working on normalizing %s\n" (n_to_string n) in *) match n.nexp with | Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf -> n | Nneg n -> let n',to_recur,add_neg = (match n.nexp with | Nconst i -> {nexp = Nconst (mult_int_big_int (-1) i)},false,false | Nadd(n1,n2) -> {nexp = Nadd(negate n1,negate n2)},true,false + | Nsub(n1,n2) -> {nexp = Nsub(n2,n1) },false,false | Nneg n -> normalize_nexp n,false,false | _ -> n,true,true) in if to_recur @@ -501,8 +512,33 @@ let rec normalize_nexp n = | -1 -> { nexp = Nadd(n21', normalize_nexp { nexp = Nadd(n1',n22')})} | 1 -> { nexp = Nadd(n1',n2') } | _ -> let _ = Printf.eprintf "pattern didn't match unexpextedly here %s %s\n" (n_to_string n1') (n_to_string n2') in assert false) - | _ -> let _ = Printf.eprintf "pattern didn't match here with no vars %s %s\n" (n_to_string n1') (n_to_string n2') in assert false) + | _ -> {nexp = Nadd (n1', n2')}) ) + | Nsub(n1,n2) -> + let n1',n2' = normalize_nexp n1, normalize_nexp n2 in + (*let _ = Printf.eprintf "Normalizing subtraction of %s - %s \n" (n_to_string n1') (n_to_string n2') in*) + (match n1'.nexp,n2'.nexp with + | Nneg_inf, Npos_inf | Npos_inf, Nneg_inf -> {nexp = Ninexact } + | Npos_inf, _ | _,Nneg_inf -> { nexp = Npos_inf } + | Nneg_inf, _ | _,Npos_inf -> { nexp = Nneg_inf } + | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some i2) | N2n(_,Some i1), Nconst i2 -> + let _ = Printf.eprintf "constant subtraction of %s - %s gives %s" (Big_int.string_of_big_int i1) (Big_int.string_of_big_int i2) (Big_int.string_of_big_int (sub_big_int i1 i2)) in + {nexp = Nconst (sub_big_int i1 i2)} + | Nadd(n11,n12), Nconst _ -> {nexp = Nadd(n11,normalize_nexp {nexp = Nsub(n12,n2')})} + | Nconst _, Nadd(n21,n22) -> {nexp = Nadd(n21,normalize_nexp {nexp = Nsub(n22,n1')})} + | Nconst i, _ -> if (eq_big_int i zero) then negate n2' else {nexp = Nsub(n1',n2')} + | _, Nconst i -> if (eq_big_int i zero) then n1' else {nexp = Nsub(n1',n2')} + | Nvar _, Nuvar _ | Nvar _, N2n _ | Nuvar _, Npow _ -> {nexp = Nsub (n2',n1')} + | N2n(_,Some i1),N2n(_,Some i2) -> {nexp = Nconst (sub_big_int i1 i2)} + | N2n(n1,_), N2n(n2,_) -> + (match compare_nexps n1 n2 with + | 0 -> n_zero + | _ -> { nexp = Nsub (n1',n2')}) + | Npow(n1,i1), Npow (n2,i2) -> + (match compare_nexps n1 n2, compare i1 i2 with + | 0,0 -> n_zero + | _ -> {nexp = Nsub (n1',n2')}) + | _ -> {nexp = Nsub(n1',n2')}) | Nmult(n1,n2) -> let n1',n2' = normalize_nexp n1, normalize_nexp n2 in (match n1'.nexp,n2'.nexp with @@ -617,9 +653,12 @@ let new_t _ = let new_n _ = let i = !n_count in n_count := i + 1; - let n = { nexp = Nuvar { nindex = i; nsubst = None ; nin = false}} in + let n = { nexp = Nuvar { nindex = i; nsubst = None ; nin = false ; leave_var = false}} in nuvars := n::!nuvars; n +let leave_nuvar n = match n.nexp with + | Nuvar u -> u.leave_var <- true; n + | _ -> n let new_o _ = let i = !o_count in o_count := i + 1; @@ -752,23 +791,34 @@ let rec occurs_in_pending_subst n_box n : bool = | _ -> occurs_in_nexp n_box n and occurs_in_nexp n_box nuvar : bool = - (*let _ = Printf.eprintf "occurs_in_nexp given n_box %s nuvar %s eq? %b\n" (n_to_string n_box) (n_to_string nuvar) (n_box.nexp == nuvar.nexp) in*) + let _ = Printf.eprintf "occurs_in_nexp given n_box %s nuvar %s eq? %b\n" (n_to_string n_box) (n_to_string nuvar) (n_box.nexp == nuvar.nexp) in if n_box.nexp == nuvar.nexp then true else match n_box.nexp with | Nuvar _ -> occurs_in_pending_subst n_box nuvar - | Nadd (nb1,nb2) | Nmult (nb1,nb2) -> occurs_in_nexp nb1 nuvar || occurs_in_nexp nb2 nuvar + | Nadd (nb1,nb2) | Nsub(nb1,nb2)| Nmult (nb1,nb2) -> occurs_in_nexp nb1 nuvar || occurs_in_nexp nb2 nuvar | Nneg nb | N2n(nb,None) | Npow(nb,_) -> occurs_in_nexp nb nuvar | _ -> false let rec reduce_n_unifications n = - match n.nexp with + let _ = Printf.eprintf "reduce_n_unifications %s\n" (n_to_string n) in + (match n.nexp with | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> () | N2n(n1,_) | Npow(n1,_) | Nneg n1 -> reduce_n_unifications n1 - | Nadd(n1,n2) | Nmult(n1,n2) -> reduce_n_unifications n1; reduce_n_unifications n2 + | Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> reduce_n_unifications n1; reduce_n_unifications n2 | Nuvar nu -> (match nu.nsubst with | None -> () - | Some(nexp) -> reduce_n_unifications(nexp); n.nexp <- nexp.nexp) + | Some(nexp) -> + reduce_n_unifications(nexp); if nu.leave_var then ignore(leave_nuvar(nexp)) else (); n.nexp <- nexp.nexp)); + let _ = Printf.eprintf "n reduced to %s\n" (n_to_string n) in () + +let rec leave_nu_as_var n = + match n.nexp with + | Nuvar nu -> + (match nu.nsubst with + | None -> nu.leave_var + | Some(nexp) -> nu.leave_var || leave_nu_as_var nexp) + | _ -> false let equate_n (n_box : nexp) (n : nexp) : bool = (*let _ = Printf.eprintf "equate_n given n_box %s and n %s\n" (n_to_string n_box) (n_to_string n) in*) @@ -819,16 +869,16 @@ let equate_e (e_box : effect) (e : effect) : unit = | _ -> e_box.effect <- e.effect) -let rec fresh_var i mkr bindings = - let v = "'v" ^ (string_of_int i) in +let fresh_var prefix i mkr bindings = + let v = "'" ^ prefix ^ (string_of_int i) in match Envmap.apply bindings v with - | Some _ -> fresh_var (i+1) mkr bindings - | None -> mkr v + | Some _ -> mkr v false + | None -> mkr v true let rec fresh_tvar bindings t = match t.t with | Tuvar { index = i;subst = None } -> - fresh_var i (fun v -> equate_t t {t=Tvar v};Some (v,{k=K_Typ})) bindings + fresh_var "tv" i (fun v add -> equate_t t {t=Tvar v}; if add then Some (v,{k=K_Typ}) else None) bindings | Tuvar { index = i; subst = Some ({t = Tuvar _} as t') } -> let kv = fresh_tvar bindings t' in equate_t t t'; @@ -838,10 +888,10 @@ let rec fresh_tvar bindings t = None | _ -> None let rec fresh_nvar bindings n = - (*let _ = Printf.printf "fresh_nvar for %s\n" (n_to_string n) in*) + let _ = Printf.eprintf "fresh_nvar for %s\n" (n_to_string n) in match n.nexp with | Nuvar { nindex = i;nsubst = None } -> - fresh_var i (fun v -> n.nexp <- (Nvar v); Some(v,{k=K_Nat})) bindings + fresh_var "nv" i (fun v add -> n.nexp <- (Nvar v); (Printf.eprintf "fresh nvar set %i to %s : %s\n" i v (n_to_string n)); if add then Some(v,{k=K_Nat}) else None) bindings | Nuvar { nindex = i; nsubst = Some({nexp=Nuvar _} as n')} -> let kv = fresh_nvar bindings n' in n.nexp <- n'.nexp; @@ -853,7 +903,7 @@ let rec fresh_nvar bindings n = let rec fresh_ovar bindings o = match o.order with | Ouvar { oindex = i;osubst = None } -> - fresh_var i (fun v -> equate_o o {order = (Ovar v)}; Some(v,{k=K_Nat})) bindings + fresh_var "ov" i (fun v add -> equate_o o {order = (Ovar v)}; if add then Some(v,{k=K_Nat}) else None) bindings | Ouvar { oindex = i; osubst = Some({order=Ouvar _} as o')} -> let kv = fresh_ovar bindings o' in equate_o o o'; @@ -865,7 +915,7 @@ let rec fresh_ovar bindings o = let rec fresh_evar bindings e = match e.effect with | Euvar { eindex = i;esubst = None } -> - fresh_var i (fun v -> equate_e e {effect = (Evar v)}; Some(v,{k=K_Nat})) bindings + fresh_var "ev" i (fun v add -> equate_e e {effect = (Evar v)}; if add then Some(v,{k=K_Nat}) else None) bindings | Euvar { eindex = i; esubst = Some({effect=Euvar _} as e')} -> let kv = fresh_evar bindings e' in equate_e e e'; @@ -946,7 +996,7 @@ let mk_pure_imp arg ret var = {t = Tfn (arg,ret,IP_length {nexp = Nvar var},pure let mk_nv v = {nexp = Nvar v} let mk_add n1 n2 = {nexp = Nadd (n1,n2) } -let mk_sub n1 n2 = {nexp = Nadd (n1, {nexp = Nneg n2})} +let mk_sub n1 n2 = {nexp = Nsub (n1, n2)} let mk_mult n1 n2 = {nexp = Nmult(n1,n2) } let mk_range n1 n2 = {t=Tapp("range",[TA_nexp n1;TA_nexp n2])} @@ -1322,7 +1372,7 @@ let initial_typ_env = ])); ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m")) - (mk_range (mk_nv "m") n_zero))), + (mk_range (mk_nv "m") (mk_nv "m")))), External (Some "length"),[],pure_e,nob)); (* incorrect types for typechecking processed sail code; do we care? *) ("mask",Base(((mk_typ_params ["a"])@(mk_nat_params["n";"m";"o";"p"])@(mk_ord_params["ord"]), @@ -1545,9 +1595,9 @@ let rec typ_subst s_env t = and ip_subst s_env ip = match ip with | IP_none -> ip - | IP_length n -> IP_length (n_subst s_env n) - | IP_start n -> IP_start (n_subst s_env n) - | IP_user n -> IP_user (n_subst s_env n) + | IP_length n -> IP_length (leave_nuvar (n_subst s_env n)) + | IP_start n -> IP_start (leave_nuvar (n_subst s_env n)) + | IP_user n -> IP_user (leave_nuvar (n_subst s_env n)) and ta_subst s_env ta = match ta with | TA_typ t -> TA_typ (typ_subst s_env t) @@ -1556,15 +1606,17 @@ and ta_subst s_env ta = | TA_ord o -> TA_ord (o_subst s_env o) and n_subst s_env n = match n.nexp with - | Nvar i -> (match Envmap.apply s_env i with - | Some(TA_nexp n1) -> n1 - | _ -> { nexp = Nvar i }) + | Nvar i -> + (match Envmap.apply s_env i with + | Some(TA_nexp n1) -> n1 + | _ -> { nexp = Nvar i }) | Nuvar _ -> new_n() | Nconst _ | Npos_inf | Nneg_inf -> n | N2n(n1,i) -> { nexp = N2n (n_subst s_env n1,i) } | Npow(n1,i) -> { nexp = Npow (n_subst s_env n1,i) } | Nneg n1 -> { nexp = Nneg (n_subst s_env n1) } | Nadd(n1,n2) -> { nexp = Nadd(n_subst s_env n1,n_subst s_env n2) } + | Nsub(n1,n2) -> {nexp = Nsub(n_subst s_env n1,n_subst s_env n2) } | Nmult(n1,n2) -> { nexp = Nmult(n_subst s_env n1,n_subst s_env n2) } and o_subst s_env o = match o.order with @@ -1640,7 +1692,7 @@ let rec t_remove_unifications s_env t = (match fresh_tvar s_env t with | Some ks -> Envmap.insert s_env ks | None -> s_env) - | _ -> resolve_tsubst t; s_env) + | _ -> ignore(resolve_tsubst t); s_env) | Tfn(t1,t2,_,e) -> e_remove_unifications (t_remove_unifications (t_remove_unifications s_env t1) t2) e | Ttup(ts) -> List.fold_right (fun t s_env -> t_remove_unifications s_env t) ts s_env | Tapp(i,args) -> List.fold_right (fun t s_env -> ta_remove_unifications s_env t) args s_env @@ -1653,7 +1705,7 @@ and ta_remove_unifications s_env ta = | TA_eft e -> (e_remove_unifications s_env e) | TA_ord o -> (o_remove_unifications s_env o) and n_remove_unifications s_env n = - (*let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in*) + let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in match n.nexp with | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env | Nuvar nu -> @@ -1662,13 +1714,13 @@ and n_remove_unifications s_env n = | _ -> resolve_nsubst n; n in (match n'.nexp with | Nuvar _ -> - (*let _ = Printf.eprintf "nuvar is before turning into var %s\n" (n_to_string n') in*) + let _ = Printf.eprintf "nuvar is before turning into var %s\n" (n_to_string n') in (match fresh_nvar s_env n with | Some ks -> Envmap.insert s_env ks | None -> s_env) | _ -> s_env) | N2n(n1,_) | Npow(n1,_) | Nneg n1 -> (n_remove_unifications s_env n1) - | Nadd(n1,n2) | Nmult(n1,n2) -> (n_remove_unifications (n_remove_unifications s_env n1) n2) + | Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> (n_remove_unifications (n_remove_unifications s_env n1) n2) and o_remove_unifications s_env o = match o.order with | Ouvar _ -> (match fresh_ovar s_env o with @@ -1721,6 +1773,7 @@ and n_to_nexp n = | Nneg_inf -> Nexp_constant min_int (* see above *) | Nmult(n1,n2) -> Nexp_times(n_to_nexp n1,n_to_nexp n2) | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2) + | Nsub(n1,n2) -> Nexp_minus(n_to_nexp n1,n_to_nexp n2) | N2n(n,_) -> Nexp_exp (n_to_nexp n) | Npow(n,1) -> let Nexp_aux(n',_) = n_to_nexp n in n' | Npow(n,i) -> Nexp_times(n_to_nexp n,n_to_nexp{nexp = Npow(n,i-1)}) @@ -2137,13 +2190,13 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2 (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in + let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] (*This constraint failing should be a warning, but truncation is ok*)*) in let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in + let cs = [] (* See above [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) @@ -2156,13 +2209,13 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2 (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> - let cs = [LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in + let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> - let cs = [LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in + let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) @@ -2302,7 +2355,7 @@ let rec contains_var nu n = match n.nexp with | Nvar _ | Nuvar _ -> nexp_eq_check nu n | Nconst _ | Npos_inf | Nneg_inf -> false - | Nadd(n1,n2) | Nmult(n1,n2) -> contains_var nu n1 || contains_var nu n2 + | Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> contains_var nu n1 || contains_var nu n2 | Nneg n | N2n(n,_) | Npow(n,_) -> contains_var nu n let rec contains_in_vars in_env n = @@ -2319,6 +2372,7 @@ let rec subst_nuvars nu nc n = | Nuvar _ -> if nexp_eq_check nu n then nc else n | Nmult(n1,n2) -> {nexp=Nmult(subst_nuvars nu nc n1,subst_nuvars nu nc n2)} | Nadd(n1,n2) -> {nexp=Nadd(subst_nuvars nu nc n1,subst_nuvars nu nc n2)} + | Nsub(n1,n2) -> {nexp=Nsub(subst_nuvars nu nc n1,subst_nuvars nu nc n2)} | Nneg n -> {nexp= Nneg (subst_nuvars nu nc n)} | N2n(n,i) -> {nexp = N2n((subst_nuvars nu nc n),i)} | Npow(n,i) -> {nexp = Npow((subst_nuvars nu nc n),i)} @@ -2327,7 +2381,7 @@ let rec get_nuvars n = match n.nexp with | Nconst _ | Nvar _ | Npos_inf | Nneg_inf -> [] | Nuvar _ -> [n] - | Nmult(n1,n2) | Nadd(n1,n2) -> (get_nuvars n1)@(get_nuvars n2) + | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (get_nuvars n1)@(get_nuvars n2) | Nneg n | N2n(n,_) | Npow(n,_) -> get_nuvars n let freshen n = @@ -2337,13 +2391,43 @@ let freshen n = (n,env_map) +let rec equate_nuvars in_env cs = + let _ = Printf.eprintf "equate_nuvars\n" in + let equate = equate_nuvars in_env in + match cs with + | [] -> [] + | (Eq(co,n1,n2) as c)::cs -> + (match (n1.nexp,n2.nexp) with + | Nuvar u1, Nuvar u2 -> + let _ = Printf.eprintf "setting two nuvars, %s and %s in equate\n" (n_to_string n1) (n_to_string n2) in + let occurs = (occurs_in_nexp n1 n2) || (occurs_in_nexp n2 n1) in + if not(occurs) + then begin ignore(resolve_nsubst n1); ignore(resolve_nsubst n2); + if (equate_n n1 n2) then equate cs else c::equate cs end + else c::equate cs + | _ -> c::equate cs) + | CondCons(co,pats,exps):: cs -> + let pats' = equate pats in + let exps' = equate exps in + (match pats',exps' with + | [],[] -> equate cs + | _ -> CondCons(co,pats',exps')::(equate cs)) + | BranchCons(co,branches)::cs -> + let b' = equate branches in + if [] = b' + then equate cs + else BranchCons(co,b')::(equate cs) + | x::cs -> x::(equate cs) + + let rec simple_constraint_check in_env cs = let check = simple_constraint_check in_env in -(* let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in *) + let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in match cs with | [] -> [] | Eq(co,n1,n2)::cs -> let eq_to_zero ok_to_set n1 n2 = + let _ = Printf.eprintf "eq_to_zero called with n1 %s and n2%s\n" (n_to_string n1) (n_to_string n2) in let new_n = normalize_nexp (mk_sub n1 n2) in (match new_n.nexp with | Nconst i -> @@ -2361,16 +2445,16 @@ let rec simple_constraint_check in_env cs = | _ -> Some(Eq(co,n1,n2))) | _ -> Some(Eq(co,n1,n2))) in let check_eq ok_to_set n1 n2 = - (*let _ = Printf.eprintf "eq check, about to normalize_nexp of %s, %s arising from %s \n" (n_to_string n1) (n_to_string n2) (co_to_string co) in *) + let _ = Printf.eprintf "eq check, about to normalize_nexp of %s, %s arising from %s \n" (n_to_string n1) (n_to_string n2) (co_to_string co) in let n1',n2' = normalize_nexp n1,normalize_nexp n2 in - (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *) + let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in (match n1'.nexp,n2'.nexp with | Ninexact,nok | nok,Ninexact -> eq_error (get_c_loc co) ("Type constraint arising from here requires " ^ n_to_string {nexp = nok} ^ " to be equal to +inf + -inf") | Npos_inf,Npos_inf | Nneg_inf, Nneg_inf -> None | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst(i2) -> if eq_big_int i1 i2 then None else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string n1 ^ " to equal " ^ n_to_string n2 ) | Nuvar u1, Nuvar u2 -> - (*let _ = Printf.eprintf "setting two nuvars, %s and %s, it is ok_to_set %b\n" (n_to_string n1) (n_to_string n2) ok_to_set in*) + let _ = Printf.eprintf "setting two nuvars, %s and %s, it is ok_to_set %b\n" (n_to_string n1) (n_to_string n2) ok_to_set in let occurs = (occurs_in_nexp n1' n2') || (occurs_in_nexp n2' n1') in if ok_to_set && not(occurs) then begin ignore(resolve_nsubst n1'); ignore(resolve_nsubst n2'); @@ -2378,15 +2462,21 @@ let rec simple_constraint_check in_env cs = else if occurs then eq_to_zero ok_to_set n1' n2' else Some(Eq(co,n1',n2')) | _, Nuvar u -> + let _ = Printf.eprintf "setting right nuvar\n" in let occurs = occurs_in_nexp n1' n2' in - if not(u.nin) && ok_to_set && not(occurs) + let leave = leave_nu_as_var n2' in + let _ = Printf.eprintf "occurs? %b, leave? %b n1' %s in n2' %s\n" occurs leave (n_to_string n1') (n_to_string n2') in + if not(u.nin) && ok_to_set && not(occurs) && not(leave) then if (equate_n n2' n1') then None else (Some (Eq(co,n1',n2'))) else if occurs then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end else Some (Eq(co,n1',n2')) | Nuvar u, _ -> + let _ = Printf.eprintf "setting left nuvar\n" in let occurs = occurs_in_nexp n2' n1' in - if not(u.nin) && ok_to_set && not(occurs) + let leave = leave_nu_as_var n1' in + let _ = Printf.eprintf "occurs? %b, leave? %b n2' %s in n1' %s\n" occurs leave (n_to_string n2') (n_to_string n1') in + if not(u.nin) && ok_to_set && not(occurs) && not(leave) then if equate_n n1' n2' then None else (Some (Eq(co,n1',n2'))) else if occurs then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end @@ -2404,9 +2494,9 @@ let rec simple_constraint_check in_env cs = | Some(c) -> c::(check cs)) | _ -> (Eq(co,n1,n2)::(check cs))) | GtEq(co,enforce,n1,n2)::cs -> - (*let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in let n1',n2' = normalize_nexp n1,normalize_nexp n2 in - (*let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*) + let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in (match n1'.nexp,n2'.nexp with | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst i2 -> if ge_big_int i1 i2 @@ -2427,9 +2517,9 @@ let rec simple_constraint_check in_env cs = ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) | _ -> GtEq(co,enforce,n1',n2')::(check cs))) | LtEq(co,enforce,n1,n2)::cs -> - (*let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in let n1',n2' = normalize_nexp n1,normalize_nexp n2 in - (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *) + let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in (match n1'.nexp,n2'.nexp with | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst i2 -> if le_big_int i1 i2 @@ -2473,13 +2563,14 @@ let resolve_constraints cs = if not !do_resolve_constraints then cs else - let rec fix len cs = + let rec fix checker len cs = (*let _ = Printf.eprintf "Calling simple constraint check, fix check point is %i\n" len in *) - let cs' = simple_constraint_check (in_constraint_env cs) cs in + let cs' = checker (in_constraint_env cs) cs in let len' = constraint_size cs' in - if len > len' then fix len' cs' + if len > len' then fix checker len' cs' else cs' in - let complex_constraints = fix (constraint_size cs) cs in + let nuvar_equated = fix equate_nuvars (constraint_size cs) cs in + let complex_constraints = fix simple_constraint_check (constraint_size nuvar_equated) nuvar_equated in (*let _ = Printf.eprintf "Resolved as many constraints as possible, leaving %i\n" (constraint_size complex_constraints) in*) complex_constraints @@ -2490,11 +2581,11 @@ let check_tannot l annot imp_param constraints efs = ignore(effects_eq (Specc l) efs e); let s_env = (t_remove_unifications (Envmap.from_list params) t) in let params = Envmap.to_list s_env in - (*let _ = Printf.eprintf "parameters going to save are " in + let _ = Printf.eprintf "parameters going to save are " in let _ = List.iter (fun (s,_) -> Printf.eprintf "%s " s) params in - let _ = Printf.eprintf "\n" in*) + let _ = Printf.eprintf "\n" in ignore (remove_internal_unifications s_env); - (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *) + let _ = Printf.eprintf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in let t' = match (t.t,imp_param) with | Tfn(p,r,_,e),Some x -> {t = Tfn(p,r,IP_user x,e) } | _ -> t in diff --git a/src/type_internal.mli b/src/type_internal.mli index f087f7f4..5d732406 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -48,6 +48,7 @@ and nexp_aux = | Npos_inf (* Used to define nat and int types, does not arise from source otherwise *) | Nneg_inf (* Used to define int type, does not arise from source otherwise *) | Nadd of nexp * nexp + | Nsub of nexp * nexp | Nmult of nexp * nexp | N2n of nexp * big_int option (* Optionally contains the 2^n result for const n, for different constraint equations *) | Npow of nexp * int (* Does not appear in source *) |