diff options
| -rw-r--r-- | doc/Makefile | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 8 |
2 files changed, 10 insertions, 4 deletions
diff --git a/doc/Makefile b/doc/Makefile index ae542571..b3802b34 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -52,10 +52,12 @@ ifeq ($(shell which sail),) $(error Cannot find sail executable, make sure it is in PATH) endif +RISCV=../../sail-riscv + .PHONY: clean -code_riscv.tex: ../riscv/prelude.sail ../riscv/riscv_duopod.sail - sail -o code_riscv -latex ../riscv/prelude.sail ../riscv/riscv_duopod.sail +code_riscv.tex: ${RISCV}/prelude.sail ${RISCV}/riscv_duopod.sail + sail -o code_riscv -latex ${RISCV}/prelude.sail ${RISCV}/riscv_duopod.sail cp code_riscv/commands.tex code_riscv.tex code_myreplicatebits.tex: examples/my_replicate_bits.sail diff --git a/src/type_check.ml b/src/type_check.ml index ee80296f..b3c691fb 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4272,14 +4272,18 @@ let check_val_spec env (VS_aux (vs, (l, _))) = typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); let env = Env.add_extern id ext_opt env in let env = if is_cast then Env.add_cast id env else env in + let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in + (* !opt_expand_valspec controls whether the actual valspec in + the AST is expanded, the val_spec type stored in the + environment is always expanded and uses typq' and typ' *) let typq, typ = if !opt_expand_valspec then - expand_bind_synonyms ts_l env (typq, typ) + (typq', typ') else (typq, typ) in let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in - (vs, id, typq, typ, env) + (vs, id, typq', typ', env) in let eff = match typ with |