From 9650491762d389fe84aa96a63efc535bdbd9c5de Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 14 Aug 2017 15:04:12 +0100 Subject: Don't reverse lexp tuple during type checking --- src/type_check.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index e69a40e8..dbaeb98f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2303,11 +2303,11 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = let (Typ_aux (typ_aux, _)) = typ in match typ_aux with | Typ_tup typs -> - let bind_tuple_lexp (tlexps, env) lexp typ = + let bind_tuple_lexp lexp typ (tlexps, env) = let tlexp, env = bind_lexp env lexp typ in tlexp :: tlexps, env in let tlexps, env = - try List.fold_left2 bind_tuple_lexp ([], env) lexps typs with + try List.fold_right2 bind_tuple_lexp lexps typs ([], env) with | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length" in annot_lexp (LEXP_tup tlexps) typ, env -- cgit v1.2.3 From 42a0675290b5fbf61cab24c1d87ce2d85da639cd Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 14 Aug 2017 15:04:38 +0100 Subject: Keep all asserts in the program during type checking --- src/type_check.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index dbaeb98f..a2481f3f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1852,7 +1852,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ begin try let nc = assert_constraint const_expr in - check_block l (Env.add_constraint nc env) exps typ + let cexp = annot_exp (E_constraint nc) bool_typ in + let checked_msg = crule check_exp env assert_msg string_typ in + let texp = annot_exp (E_assert (cexp, checked_msg)) unit_typ in + texp :: check_block l (Env.add_constraint nc env) exps typ with | Not_a_constraint -> check_block l env exps typ end -- cgit v1.2.3 From 404eef7b9a446f8b1da2024cbf722911958d9f52 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 14 Aug 2017 17:28:19 +0100 Subject: Some overloaded equality support in monomorphisation --- src/monomorphise.ml | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 27b5237e..a9ddd1a7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -559,6 +559,26 @@ let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = | L_undef, _ | _, L_undef -> None | _ -> Some (l1 = l2) +(* TODO: we should really specify which functions are equality in the prelude, + rather than fixing them here. *) +let eq_fns = [Id "eq_int"; Id "eq_vec"; Id "eq_string"; Id "eq_real"] +let neq_fns = [Id "neq_anything"] + +let try_app (l,ann) (Id_aux (id,_),args) = + let is_eq = List.mem id eq_fns in + let is_neq = (not is_eq) && List.mem id neq_fns in + if is_eq || is_neq then + let new_l = Generated l in + match args with + | [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] -> + let lit b = if b then L_true else L_false in + let lit b = lit (if is_eq then b else not b) in + (match lit_eq l1 l2 with + | None -> None + | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann)))) + | _ -> None + else None + let try_app_infix (l,ann) (E_aux (e1,ann1)) (Id_aux (id,_)) (E_aux (e2,ann2)) = let i = match id with Id x -> x | DeIid x -> x in @@ -676,8 +696,11 @@ let split_defs splits defs = | E_cast (t,e') -> re (E_cast (t, const_prop_exp substs e')) | E_app (id,es) -> let es' = List.map (const_prop_exp substs) es in - (match const_prop_try_fn (id,es') with - | None -> re (E_app (id,es')) + (match try_app (l,annot) (id,es') with + | None -> + (match const_prop_try_fn (id,es') with + | None -> re (E_app (id,es')) + | Some r -> r) | Some r -> r) | E_app_infix (e1,id,e2) -> let e1',e2' = const_prop_exp substs e1,const_prop_exp substs e2 in -- cgit v1.2.3 From 637ed6dcd3831fb831ab30f7ed1dc00226a8fa7c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 14 Aug 2017 17:28:41 +0100 Subject: Existentials in free type var functions --- src/spec_analysis.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 1475da7a..5281ef27 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -211,6 +211,7 @@ let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with | Typ_tup ts -> free_type_names_ts consider_var ts | Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs) | Typ_wild -> mt + | Typ_exist (kids,_,t') -> List.fold_left (fun s kid -> Nameset.remove (string_of_kid kid) s) (free_type_names_t consider_var t') kids and free_type_names_ts consider_var ts = nameset_bigunion (List.map (free_type_names_t consider_var) ts) and free_type_names_maybe_t consider_var = function | Some t -> free_type_names_t consider_var t @@ -239,6 +240,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used | Typ_app(id,targs) -> List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) + | Typ_exist (kids,_,t') -> fv_of_typ consider_var (List.fold_left (fun b (Kid_aux (Var v,_)) -> Nameset.add v b) bound kids) used t' and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with | Typ_arg_typ t -> fv_of_typ consider_var bound used t -- cgit v1.2.3