diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 27 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 9 |
3 files changed, 33 insertions, 5 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 2849b466..d9ee73b8 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -558,6 +558,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 @@ -675,8 +695,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 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 diff --git a/src/type_check.ml b/src/type_check.ml index 2cfdb899..8a7983ce 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1845,7 +1845,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 @@ -2311,11 +2314,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 |