diff options
Diffstat (limited to 'src/spec_analysis.ml')
| -rw-r--r-- | src/spec_analysis.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 180b96b2..9453e999 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -386,17 +386,17 @@ let rec find_scattered_of name = function | [] -> [] | DEF_scattered (SD_aux(sda,_) as sd):: defs -> (match sda with - | SD_scattered_function(_,_,_,id) - | SD_scattered_funcl(FCL_aux(FCL_Funcl(id,_),_)) - | SD_scattered_unioncl(id,_) -> + | SD_function(_,_,_,id) + | SD_funcl(FCL_aux(FCL_Funcl(id,_),_)) + | SD_unioncl(id,_) -> if name = string_of_id id then [sd] else [] | _ -> [])@ (find_scattered_of name defs) | _::defs -> find_scattered_of name defs -let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd,_)) = match sd with - | SD_scattered_function(_,tannot_opt,_,id) -> +let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd,(l, _))) = match sd with + | SD_function(_,tannot_opt,_,id) -> let b,ns = (match tannot_opt with | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) -> let bindings = if consider_var then typq_bindings typq else mt in @@ -404,7 +404,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd | Typ_annot_opt_aux(Typ_annot_opt_none, _) -> mt, mt) in init_env (string_of_id id),ns - | SD_scattered_funcl (FCL_aux(FCL_Funcl(id,pexp),_)) -> + | SD_funcl (FCL_aux(FCL_Funcl(id,pexp),_)) -> begin match pexp with | Pat_aux(Pat_exp (pat,exp),_) -> @@ -423,7 +423,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd | _ -> mt in scattered_binds, exp_ns end - | SD_scattered_variant (id,_,_) -> + | SD_variant (id,_,_) -> let name = string_of_id id in let uses = if consider_scatter_as_one @@ -435,12 +435,12 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd Nameset.remove name pieces_uses else mt in init_env name, uses - | SD_scattered_unioncl(id, type_union) -> + | SD_unioncl(id, type_union) -> let typ_name = string_of_id id in let b = init_env typ_name in let (b,r) = typ_variants consider_var b [type_union] in (Nameset.remove typ_name b, Nameset.add typ_name r) - | SD_scattered_end id -> + | SD_end id -> let name = string_of_id id in let uses = if consider_scatter_as_one (*Note: if this is a function ending, the dec is included *) @@ -450,6 +450,7 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd (List.map (fv_of_scattered consider_var false []) scattered_defs) (init_env name) else init_env name in init_env (name ^ "/end"), uses + | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to find free variables for scattered mapping clause") let fv_of_rd consider_var (DEC_aux (d, annot)) = (* When we get the free variables of a register, we have to ensure |
