diff options
| author | Alasdair Armstrong | 2019-01-21 19:02:46 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-01-21 19:02:55 +0000 |
| commit | 2c81fff611c458fe04b2de2045247bdc77f8f80a (patch) | |
| tree | d2d47805a63c86e2947fd00f1816e8e30c5b8748 /src | |
| parent | 07cf22289b1b4bb2300d4670573a7faee7211a04 (diff) | |
Update manual snapshot and add basic sail -latex documentation
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index b3c691fb..1b6efa46 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1243,7 +1243,7 @@ let prove_z3 env (NC_aux (_, l) as nc) = | Constraint.Sat -> typ_debug (lazy "sat"); false | Constraint.Unknown -> typ_debug (lazy "unknown"); false -let solve env (Nexp_aux (_, l) as nexp) = +let solve env (Nexp_aux (_, l) as nexp) = typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_nexp nexp ^ " = ?")); match nexp with @@ -1255,6 +1255,8 @@ let solve env (Nexp_aux (_, l) as nexp) = let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in Constraint.solve_z3 l vars constr (mk_kid "solve#") + + let prove env nc = typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); let (NC_aux (nc_aux, _) as nc) = Env.expand_constraint_synonyms env nc in |