From 666062ce4d97fe48307d1feb5bb4eb32087b177a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 30 Nov 2018 19:33:50 +0000
Subject: 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
---
 src/spec_analysis.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'src/spec_analysis.ml')

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
-- 
cgit v1.2.3