diff options
| author | Alasdair Armstrong | 2018-11-30 19:33:50 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-11-30 19:35:29 +0000 |
| commit | 666062ce4d97fe48307d1feb5bb4eb32087b177a (patch) | |
| tree | eaf5eda1617912c7c11da6556ba8534250f1773f /src/spec_analysis.ml | |
| parent | 0363a325ca6c498e086519c4ecaf1f51dbff7f64 (diff) | |
Remove constraint synonyms
They weren't needed for ASL parser like I thought they would be, and
they increase the complexity of dealing with constraints throughout
Sail, so just remove them.
Also fix some compiler warnings
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index c858754e..fa68c6f2 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -282,6 +282,10 @@ and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) = (fun e (b,u,s) -> fv_of_exp consider_var b u s e) args (bound,used,set) in bound,Nameset.add (string_of_id id) used,set + | LEXP_vector_concat(args) -> + List.fold_right + (fun e (b,u,s) -> + fv_of_lexp consider_var b u s e) args (bound,used,set) | LEXP_field(lexp,_) -> fv_of_lexp consider_var bound used set lexp | LEXP_vector(lexp,exp) -> let bound_l,used,set = fv_of_lexp consider_var bound used set lexp in @@ -486,8 +490,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function List.fold_left Nameset.union Nameset.empty (List.map snd fvs) | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef | DEF_reg_dec rdec -> fv_of_rd consider_var rdec - | DEF_constraint (id, _, _) -> - raise (Reporting.err_unreachable (id_loc id) __POS__ "Constraint should be re-written") + | DEF_pragma _ -> mt,mt let group_defs consider_scatter_as_one (Ast.Defs defs) = List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs |