diff options
| author | Alasdair Armstrong | 2018-12-12 17:37:13 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-12 17:47:55 +0000 |
| commit | 56fb5bf999d7cc900d6535da4168e220862d3d9c (patch) | |
| tree | 4dd0c0a3926c1cc10c39e94f00e7473acc1af0d1 /src/spec_analysis.ml | |
| parent | 54914eff75322309ad6505905c24806f3c7396f3 (diff) | |
Add a test case for various simple boolean properties
test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.
// de Morgan
_prove(constraint(not('p | 'q) <--> not('p) & not('q)));
_prove(constraint(not('p & 'q) <--> not('p) | not('q)));
introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.
Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.
Also ensure that this test case works correctly in Lem
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 0f8db0ff..940fbfe5 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -310,10 +310,13 @@ let typ_variants consider_var bound tunions = let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with | KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp +let fv_of_abbrev consider_var bound used typq typ_arg = + let ts_bound = if consider_var then typq_bindings typq else mt in + ts_bound, fv_of_targ consider_var (Nameset.union bound ts_bound) used typ_arg + let fv_of_type_def consider_var (TD_aux(t,_)) = match t with - | TD_abbrev(id,typq,A_aux(A_typ typ, l)) -> - let typschm = TypSchm_aux (TypSchm_ts (typq,typ), l) in - init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm) + | TD_abbrev(id,typq,typ_arg) -> + init_env (string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg) | TD_record(id,_,typq,tids,_) -> let binds = init_env (string_of_id id) in let bounds = if consider_var then typq_bindings typq else mt in |