diff options
| -rw-r--r-- | src/type_check.ml | 10 | ||||
| -rw-r--r-- | src/type_internal.ml | 10 | ||||
| -rw-r--r-- | src/type_internal.mli | 2 |
3 files changed, 11 insertions, 11 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 0d86d365..be944d31 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -127,10 +127,10 @@ let rec quants_to_consts (Env (d_env,t_env)) qis : (t_params * nexp_range list) | KOpt_kind(kind,Kid_aux((Var i),l'')) -> ((i,kind_to_k kind)::ids,cs)) | QI_const(NC_aux(nconst,l')) -> (match nconst with - | NC_fixed(n1,n2) -> (ids,Eq(Spec l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_bounded_ge(n1,n2) -> (ids,GtEq(Spec l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_bounded_le(n1,n2) -> (ids,LtEq(Spec l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,In(Spec l',i,bounds)::cs))) + | NC_fixed(n1,n2) -> (ids,Eq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_bounded_ge(n1,n2) -> (ids,GtEq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_bounded_le(n1,n2) -> (ids,LtEq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,In(Specc l',i,bounds)::cs))) let typq_to_params envs (TypQ_aux(tq,l)) = @@ -1252,7 +1252,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),_,c',eft') -> (*let _ = Printf.printf "Function %s is in env\n" id in*) let u,constraints,eft = subst params u constraints eft in - let t',cs = type_consistent (Spec l) d_env t u in + let t',cs = type_consistent (Specc l) d_env t u in let t_env = if is_rec then t_env else Envmap.remove t_env id in let funcls,cs_ef = check t_env in let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in diff --git a/src/type_internal.ml b/src/type_internal.ml index 5dd6f34d..0a499260 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -71,7 +71,7 @@ type constraint_origin = | Patt of Parse_ast.l | Expr of Parse_ast.l | Abre of Parse_ast.l - | Spec of Parse_ast.l + | Specc of Parse_ast.l (* Constraints for nexps, plus the location which added the constraint *) type nexp_range = @@ -104,7 +104,7 @@ let get_index n = | _ -> assert false let get_c_loc = function - | Patt l | Expr l | Abre l | Spec l -> l + | Patt l | Expr l | Abre l | Specc l -> l let rec string_of_list sep string_of = function | [] -> "" @@ -527,8 +527,8 @@ let initial_typ_env = mk_range (Nvar "o") (Nvar "p")])}, (mk_range (Nadd ({nexp=(Nvar "n")},{ nexp = Nneg({nexp=Nvar "o"})})) (Nadd({nexp=Nvar "m"},{nexp =Nneg {nexp=Nvar "p"}}))), pure_e)}),External (Some "minus"), - [GtEq(Spec(Parse_ast.Int("-",None)),{nexp=Nvar "n"},{nexp=Nvar "o"}); - GtEq(Spec(Parse_ast.Int("-",None)),{nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nvar "o"})],pure_e)); + [GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nvar "n"},{nexp=Nvar "o"}); + GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nvar "o"})],pure_e)); ("mod",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e)); ("quot",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "quot"),[],pure_e)); (*Type incomplete*) @@ -1083,7 +1083,7 @@ let resolve_constraints cs = let check_tannot l annot constraints efs = match annot with | Some((params,t),tag,cs,e) -> - ignore(effects_eq (Spec l) efs e); + ignore(effects_eq (Specc l) efs e); let params = Envmap.to_list (t_remove_unifications (Envmap.from_list params) t) in (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *) Some((params,t),tag,cs,e) diff --git a/src/type_internal.mli b/src/type_internal.mli index f85117a9..07b0e746 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -66,7 +66,7 @@ type constraint_origin = | Patt of Parse_ast.l | Expr of Parse_ast.l | Abre of Parse_ast.l - | Spec of Parse_ast.l + | Specc of Parse_ast.l (* Constraints for nexps, plus the location which added the constraint *) type nexp_range = |