summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair2018-12-08 01:06:28 +0000
committerAlasdair2018-12-08 02:48:04 +0000
commitd8f0854ca9d80d3af8d6a4aaec778643eda9421c (patch)
treed7d64ccbc3e972ceae549080f62c0c036452c6a6
parent2c25110ad2f5e636239ba65a2154aae79ffa253c (diff)
Compiling again
Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of uvar as the result of unify. Plus A_ could either stand for argument, or Any/A type which is quite appropriate in most use cases. Restore instantiation info in infer_funapp'. Ideally we would save this instead of recomputing it ever time we need it. However I checked and there are over 300 places in the code that would need to be changed to add an extra argument to E_app. Still some issues causing specialisation to fail however. Improve the error message when we swap how we infer/check an l-expression, as this could previously cause the actual cause of a type-checking failure to be effectively hidden.
Diffstat
-rw-r--r--language/sail.ott111
-rw-r--r--src/ast_util.ml122
-rw-r--r--src/ast_util.mli3
-rw-r--r--src/c_backend.ml22
-rw-r--r--src/constraint.ml6
-rw-r--r--src/initial_check.ml12
-rw-r--r--src/monomorphise.ml150
-rw-r--r--src/ocaml_backend.ml38
-rw-r--r--src/pretty_print_common.ml16
-rw-r--r--src/pretty_print_coq.ml101
-rw-r--r--src/pretty_print_lem.ml64
-rw-r--r--src/pretty_print_sail.ml10
-rw-r--r--src/return_analysis.ml2
-rw-r--r--src/rewrites.ml50
-rw-r--r--src/spec_analysis.ml10
-rw-r--r--src/specialize.ml79
-rw-r--r--src/specialize.mli4
-rw-r--r--src/state.ml32
-rw-r--r--src/type_check.ml308
-rw-r--r--src/type_check.mli9
-rw-r--r--src/type_error.ml24
-rw-r--r--test/typecheck/pass/exist_synonym/v1.expect3
-rw-r--r--test/typecheck/pass/exist_synonym/v2.expect3
-rw-r--r--test/typecheck/pass/global_type_var/v1.expect20
-rw-r--r--test/typecheck/pass/global_type_var/v2.expect20
25 files changed, 606 insertions, 613 deletions
diff --git a/language/sail.ott b/language/sail.ott
index b35e64d3..585a2939 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -209,8 +209,8 @@ base_effect :: 'BE_' ::=
| wmem :: :: wmem {{ com write memory }}
| wmea :: :: eamem {{ com signal effective address for writing memory }}
| exmem :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }}
- | wmv :: :: wmv {{ com write memory, sending only value }}
- | wmvt :: :: wmvt {{ com write memory, sending only value and tag }}
+ | wmv :: :: wmv {{ com write memory, sending only value }}
+ | wmvt :: :: wmvt {{ com write memory, sending only value and tag }}
| barr :: :: barr {{ com memory barrier }}
| depend :: :: depend {{ com dynamic footprint }}
| undef :: :: undef {{ com undefined-instruction exception }}
@@ -221,57 +221,24 @@ base_effect :: 'BE_' ::=
effect :: 'Effect_' ::=
{{ aux _ l }}
- | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }}
- | pure :: M :: pure {{ com sugar for empty effect set }}
+ | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }}
+ | pure :: M :: pure {{ com sugar for empty effect set }}
{{ lem (Effect_set []) }}
typ :: 'Typ_' ::=
{{ com type expressions, of kind Type }}
{{ aux _ l }}
- | :: :: internal_unknown
- | id :: :: id
- {{ com defined type }}
- | kid :: :: var
- {{ com type variable }}
- | ( typ1 , ... , typn ) -> typ2 effectkw effect :: :: fn
- {{ com Function (first-order only in user code) }}
- | typ1 <-> typ2 :: :: bidir
- {{ com Mapping }}
-% TODO: build first-order restriction into AST or just into type rules? neither - see note
-% TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax.
- | ( typ1 , .... , typn ) :: :: tup
- {{ com Tuple }}
- | exist kid1 , .. , kidn , n_constraint . typ :: :: exist
-% TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker
- | id < typ_arg1 , .. , typ_argn > :: :: app
- {{ com type constructor application }}
- | ( typ ) :: S :: paren {{ ichlo [[typ]] }}
-% | range < nexp1, nexp2> :: :: range {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1 }}
- | [| nexp |] :: S :: range1 {{ichlo range <[[nexp]], 0> }} {{ com sugar for \texttt{range<0, nexp>} }}
- | [| nexp : nexp' |] :: S :: range2 {{ichlo range <[[nexp]],[[nexp']]> }} {{ com sugar for \texttt{range< nexp, nexp'>} }}
-% | atom < nexp > :: :: atom {{ com equivalent to range<nexp,nexp> }}
- | [: nexp :] :: S :: atom1 {{ichlo atom <[[nexp]]> }} {{ com sugar for \texttt{atom<nexp>}=\texttt{range<nexp,nexp>} }}
-% use .. not - to avoid ambiguity with nexp -
-% total maps and vectors indexed by finite subranges of nat
-% | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
-% probably some sugar for vector types, using [ ] similarly to enums:
-% (but with .. not : in the former, to avoid confusion...)
- | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }}
-{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$ \texttt{|]} }}
- | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }}
-{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }}
- | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }}
- | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }}
-% | register [ id ] :: S :: register {{ ichlo (Typ_app Id "lteq_atom_atom") }}
-% ...so bit [ nexp ] etc is just an instance of that
-% | List < typ > :: :: list {{ com list of [[typ]] }}
-% | Set < typ > :: :: set {{ com finite set of [[typ]] }}
-% | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }}
-% "reg t" is basically the ML "t ref"
-% not sure how first-class it should be, though
-% use "reg word32" etc for the types of vanilla registers
-
-typ_arg :: 'Typ_arg_' ::=
+ | :: :: internal_unknown
+ | id :: :: id {{ com defined type }}
+ | kid :: :: var {{ com type variable }}
+ | ( typ1 , ... , typn ) -> typ2 effectkw effect :: :: fn {{ com Function (first-order only) }}
+ | typ1 <-> typ2 :: :: bidir {{ com Mapping }}
+ | ( typ1 , .... , typn ) :: :: tup {{ com Tuple }}
+ | { kid1 ... kidn , n_constraint . typ } :: :: exist
+ | id ( typ_arg1 , ... , typ_argn ) :: :: app {{ com type constructor application }}
+ | ( typ ) :: S :: paren {{ ichlo [[typ]] }}
+
+typ_arg :: 'A_' ::=
{{ com type constructor arguments of all kinds }}
{{ aux _ l }}
| nexp :: :: nexp
@@ -282,21 +249,18 @@ typ_arg :: 'Typ_arg_' ::=
n_constraint :: 'NC_' ::=
{{ com constraint over kind Int }}
{{ aux _ l }}
- | nexp = nexp' :: :: equal
+ | nexp == nexp' :: :: equal
| nexp >= nexp' :: :: bounded_ge
| nexp '<=' nexp' :: :: bounded_le
| nexp != nexp' :: :: not_equal
| kid 'IN' { num1 , ... , numn } :: :: set
- | n_constraint \/ n_constraint' :: :: or
- | n_constraint /\ n_constraint' :: :: and
+ | n_constraint & n_constraint' :: :: or
+ | n_constraint | n_constraint' :: :: and
| id ( typ_arg0 , ... , typ_argn ) :: :: app
| kid :: :: var
| true :: :: true
| false :: :: false
-% Note only id on the left and constants on the right in a
-% finite-set-bound, as we don't think we need anything more
-
kinded_id :: 'KOpt_' ::=
{{ com optionally kind-annotated identifier }}
{{ aux _ l }}
@@ -386,8 +350,8 @@ type_def_aux :: 'TD_' ::=
kind_def :: 'KD_' ::=
{{ com Definition body for elements of kind }}
{{ aux _ annot }} {{ auxparam 'a }}
- | Def kind id name_scm_opt = nexp :: :: nabbrev
- {{ com $[[Nat]]$-expression abbreviation }}
+ | Def kind id name_scm_opt = nexp :: :: nabbrev
+ {{ com Int-expression abbreviation }}
type_union :: 'Tu_' ::=
{{ com type union constructors }}
@@ -638,13 +602,9 @@ exp :: 'E_' ::=
| if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
| loop exp1 exp2 :: :: loop
- | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }}
- | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }}
+ | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }}
+ | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }}
| foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }}
- | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }}
- | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }}
- | foreach ( id from exp1 downto exp2 by exp3 ) exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }}
- | foreach ( id from exp1 downto exp2 ) exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }}
% vectors
| [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }}
@@ -740,29 +700,26 @@ exp :: 'E_' ::=
lexp :: 'LEXP_' ::= {{ com lvalue expression }}
{{ aux _ annot }} {{ auxparam 'a }}
- | id :: :: id {{ com identifier }}
- | deref exp :: :: deref
- | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }}
- | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }}
-{{ com sugared form of above for explicit tuple $[[exp]]$ }}
- | ( typ ) id :: :: cast
-{{ com cast }}
- | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }}
- | lexp1 @ ... @ lexpn :: :: vector_concat {{ com vector concatenation L-exp }}
- | lexp [ exp ] :: :: vector {{ com vector element }}
- | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }}
- | lexp . id :: :: field {{ com struct field }}
+ | id :: :: id {{ com identifier }}
+ | deref exp :: :: deref
+ | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }}
+ | ( typ ) id :: :: cast
+ | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }}
+ | lexp1 @ ... @ lexpn :: :: vector_concat {{ com vector concatenation L-exp }}
+ | lexp [ exp ] :: :: vector {{ com vector element }}
+ | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }}
+ | lexp . id :: :: field {{ com struct field }}
fexp :: 'FE_' ::=
{{ com field expression }}
{{ aux _ annot }} {{ auxparam 'a }}
- | id = exp :: :: Fexp
+ | id = exp :: :: Fexp
opt_default :: 'Def_val_' ::=
{{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map
{{ aux _ annot }} {{ auxparam 'a }}
- | :: :: empty
- | ; default = exp :: :: dec
+ | :: :: empty
+ | ; default = exp :: :: dec
pexp :: 'Pat_' ::=
{{ com pattern match }}
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 788008d1..f6b8317d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -315,7 +315,7 @@ let rec constraint_disj (NC_aux (nc_aux, l) as nc) =
| _ -> [nc]
let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown)
-let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown)
+let mk_typ_arg arg = A_aux (arg, Parse_ast.Unknown)
let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown)
let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
@@ -330,23 +330,23 @@ let unit_typ = mk_id_typ (mk_id "unit")
let bit_typ = mk_id_typ (mk_id "bit")
let real_typ = mk_id_typ (mk_id "real")
let app_typ id args = mk_typ (Typ_app (id, args))
-let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (Typ_arg_typ typ)]))
+let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (A_typ typ)]))
let atom_typ nexp =
- mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))]))
+ mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp (nexp_simp nexp))]))
let range_typ nexp1 nexp2 =
- mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1));
- mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))]))
+ mk_typ (Typ_app (mk_id "range", [mk_typ_arg (A_nexp (nexp_simp nexp1));
+ mk_typ_arg (A_nexp (nexp_simp nexp2))]))
let bool_typ = mk_id_typ (mk_id "bool")
let string_typ = mk_id_typ (mk_id "string")
-let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
+let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (A_typ typ)]))
let tuple_typ typs = mk_typ (Typ_tup typs)
let function_typ arg_typs ret_typ eff = mk_typ (Typ_fn (arg_typs, ret_typ, eff))
let vector_typ n ord typ =
mk_typ (Typ_app (mk_id "vector",
- [mk_typ_arg (Typ_arg_nexp (nexp_simp n));
- mk_typ_arg (Typ_arg_order ord);
- mk_typ_arg (Typ_arg_typ typ)]))
+ [mk_typ_arg (A_nexp (nexp_simp n));
+ mk_typ_arg (A_order ord);
+ mk_typ_arg (A_typ typ)]))
let exc_typ = mk_id_typ (mk_id "exception")
@@ -374,10 +374,10 @@ let nc_var kid = mk_nc (NC_var kid)
let nc_true = mk_nc NC_true
let nc_false = mk_nc NC_false
-let arg_nexp ?loc:(l=Parse_ast.Unknown) n = Typ_arg_aux (Typ_arg_nexp n, l)
-let arg_order ?loc:(l=Parse_ast.Unknown) ord = Typ_arg_aux (Typ_arg_order ord, l)
-let arg_typ ?loc:(l=Parse_ast.Unknown) typ = Typ_arg_aux (Typ_arg_typ typ, l)
-let arg_bool ?loc:(l=Parse_ast.Unknown) nc = Typ_arg_aux (Typ_arg_bool nc, l)
+let arg_nexp ?loc:(l=Parse_ast.Unknown) n = A_aux (A_nexp n, l)
+let arg_order ?loc:(l=Parse_ast.Unknown) ord = A_aux (A_order ord, l)
+let arg_typ ?loc:(l=Parse_ast.Unknown) typ = A_aux (A_typ typ, l)
+let arg_bool ?loc:(l=Parse_ast.Unknown) nc = A_aux (A_bool nc, l)
let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc]))
@@ -426,6 +426,14 @@ let quant_map_items f = function
| TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l)
| TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l)
+let is_quant_kopt = function
+ | QI_aux (QI_id _, _) -> true
+ | _ -> false
+
+let is_quant_constraint = function
+ | QI_aux (QI_const _, _) -> true
+ | _ -> false
+
let unaux_nexp (Nexp_aux (nexp, _)) = nexp
let unaux_order (Ord_aux (ord, _)) = ord
let unaux_typ (Typ_aux (typ, _)) = typ
@@ -670,12 +678,12 @@ and string_of_typ_aux = function
| Typ_exist (kids, nc, typ) ->
"{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"
and string_of_typ_arg = function
- | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
+ | A_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
and string_of_typ_arg_aux = function
- | Typ_arg_nexp n -> string_of_nexp n
- | Typ_arg_typ typ -> string_of_typ typ
- | Typ_arg_order o -> string_of_order o
- | Typ_arg_bool nc -> string_of_n_constraint nc
+ | A_nexp n -> string_of_nexp n
+ | A_typ typ -> string_of_typ typ
+ | A_order o -> string_of_order o
+ | A_bool nc -> string_of_n_constraint nc
and string_of_n_constraint = function
| NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
| NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
@@ -993,13 +1001,13 @@ module Typ = struct
| Typ_bidir _, _ -> -1 | _, Typ_bidir _ -> 1
| Typ_tup _, _ -> -1 | _, Typ_tup _ -> 1
| Typ_exist _, _ -> -1 | _, Typ_exist _ -> 1
- and arg_compare (Typ_arg_aux (ta1,_)) (Typ_arg_aux (ta2,_)) =
+ and arg_compare (A_aux (ta1,_)) (A_aux (ta2,_)) =
match ta1, ta2 with
- | Typ_arg_nexp n1, Typ_arg_nexp n2 -> Nexp.compare n1 n2
- | Typ_arg_typ t1, Typ_arg_typ t2 -> compare t1 t2
- | Typ_arg_order o1, Typ_arg_order o2 -> order_compare o1 o2
- | Typ_arg_nexp _, _ -> -1 | _, Typ_arg_nexp _ -> 1
- | Typ_arg_typ _, _ -> -1 | _, Typ_arg_typ _ -> 1
+ | A_nexp n1, A_nexp n2 -> Nexp.compare n1 n2
+ | A_typ t1, A_typ t2 -> compare t1 t2
+ | A_order o1, A_order o2 -> order_compare o1 o2
+ | A_nexp _, _ -> -1 | _, A_nexp _ -> 1
+ | A_typ _, _ -> -1 | _, A_typ _ -> 1
end
module TypMap = Map.Make(Typ)
@@ -1055,21 +1063,21 @@ let is_ref_typ (Typ_aux (typ_aux, _)) = match typ_aux with
let rec is_vector_typ = function
| Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_]), _) -> true
- | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) ->
+ | Typ_aux (Typ_app (Id_aux (Id "register",_), [A_aux (A_typ rtyp,_)]), _) ->
is_vector_typ rtyp
| _ -> false
let typ_app_args_of = function
| Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
- (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
+ (c, List.map (fun (A_aux (a,_)) -> a) targs, l)
| Typ_aux (_, l) as typ ->
raise (Reporting.err_typ l
("typ_app_args_of called on non-app type " ^ string_of_typ typ))
let rec vector_typ_args_of typ = match typ_app_args_of typ with
- | ("vector", [Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], l) ->
+ | ("vector", [A_nexp len; A_order ord; A_typ etyp], l) ->
(nexp_simp len, ord, etyp)
- | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
+ | ("register", [A_typ rtyp], _) -> vector_typ_args_of rtyp
| (_, _, l) ->
raise (Reporting.err_typ l
("vector_typ_args_of called on non-vector type " ^ string_of_typ typ))
@@ -1162,12 +1170,12 @@ and tyvars_of_typ (Typ_aux (t,_)) =
| Typ_exist (kids, nc, t) ->
let s = KidSet.union (tyvars_of_typ t) (tyvars_of_constraint nc) in
List.fold_left (fun s k -> KidSet.remove k s) s kids
-and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) =
+and tyvars_of_typ_arg (A_aux (ta,_)) =
match ta with
- | Typ_arg_nexp nexp -> tyvars_of_nexp nexp
- | Typ_arg_typ typ -> tyvars_of_typ typ
- | Typ_arg_order _ -> KidSet.empty
- | Typ_arg_bool nc -> tyvars_of_constraint nc
+ | A_nexp nexp -> tyvars_of_nexp nexp
+ | A_typ typ -> tyvars_of_typ typ
+ | A_order _ -> KidSet.empty
+ | A_bool nc -> tyvars_of_constraint nc
let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with
| QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
@@ -1184,7 +1192,7 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
| Typ_app (_,[size;_;_]) when mwords && is_bitvector_typ typ ->
wrap (E_app (mk_id "undefined_bitvector",
undefined_of_typ_args mwords l annot size)) typ
- | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp i, _)]) when string_of_id atom = "atom" ->
+ | Typ_app (atom, [A_aux (A_nexp i, _)]) when string_of_id atom = "atom" ->
wrap (E_sizeof i) typ
| Typ_app (id, args) ->
wrap (E_app (prepend_id "undefined_" id,
@@ -1199,11 +1207,11 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
case when re-writing those functions. *)
wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ
| Typ_internal_unknown | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *)
-and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) =
match typ_arg_aux with
- | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
- | Typ_arg_typ typ -> [undefined_of_typ mwords l annot typ]
- | Typ_arg_order _ -> []
+ | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
+ | A_typ typ -> [undefined_of_typ mwords l annot typ]
+ | A_order _ -> []
let destruct_pexp (Pat_aux (pexp,ann)) =
match pexp with
@@ -1426,13 +1434,13 @@ let rec locate_typ f (Typ_aux (typ_aux, l)) =
in
Typ_aux (typ_aux, f l)
-and locate_typ_arg f (Typ_arg_aux (typ_arg_aux, l)) =
+and locate_typ_arg f (A_aux (typ_arg_aux, l)) =
let typ_arg_aux = match typ_arg_aux with
- | Typ_arg_nexp nexp -> Typ_arg_nexp (locate_nexp f nexp)
- | Typ_arg_typ typ -> Typ_arg_typ (locate_typ f typ)
- | Typ_arg_order ord -> Typ_arg_order (locate_order f ord)
+ | A_nexp nexp -> A_nexp (locate_nexp f nexp)
+ | A_typ typ -> A_typ (locate_typ f typ)
+ | A_order ord -> A_order (locate_order f ord)
in
- Typ_arg_aux (typ_arg_aux, f l)
+ A_aux (typ_arg_aux, f l)
let rec locate_typ_pat f (TP_aux (tp_aux, l)) =
let tp_aux = match tp_aux with
@@ -1552,7 +1560,7 @@ let unique l =
let order_subst_aux sv subst = function
| Ord_var kid ->
begin match subst with
- | Typ_arg_aux (Typ_arg_order ord, _) when Kid.compare kid sv = 0 ->
+ | A_aux (A_order ord, _) when Kid.compare kid sv = 0 ->
unaux_order ord
| _ -> Ord_var kid
end
@@ -1565,7 +1573,7 @@ let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv s
and nexp_subst_aux sv subst = function
| Nexp_var kid ->
begin match subst with
- | Typ_arg_aux (Typ_arg_nexp n, _) when Kid.compare kid sv = 0 -> unaux_nexp n
+ | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> unaux_nexp n
| _ -> Nexp_var kid
end
| Nexp_id id -> Nexp_id id
@@ -1590,7 +1598,7 @@ and constraint_subst_aux l sv subst = function
| NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
| NC_set (kid, ints) as set_nc ->
begin match subst with
- | Typ_arg_aux (Typ_arg_nexp n, _) when Kid.compare kid sv = 0 ->
+ | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 ->
nexp_set_to_or l n ints
| _ -> set_nc
end
@@ -1599,7 +1607,7 @@ and constraint_subst_aux l sv subst = function
| NC_app (id, args) -> NC_app (id, List.map (typ_arg_subst sv subst) args)
| NC_var kid ->
begin match subst with
- | Typ_arg_aux (Typ_arg_bool nc, _) when Kid.compare kid sv = 0 ->
+ | A_aux (A_bool nc, _) when Kid.compare kid sv = 0 ->
unaux_constraint nc
| _ -> NC_var kid
end
@@ -1612,7 +1620,7 @@ and typ_subst_aux sv subst = function
| Typ_id v -> Typ_id v
| Typ_var kid ->
begin match subst with
- | Typ_arg_aux (Typ_arg_typ typ, _) when Kid.compare kid sv = 0 ->
+ | A_aux (A_typ typ, _) when Kid.compare kid sv = 0 ->
unaux_typ typ
| _ -> Typ_var kid
end
@@ -1623,19 +1631,19 @@ and typ_subst_aux sv subst = function
| Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ)
| Typ_exist (kids, nc, typ) -> Typ_exist (kids, constraint_subst sv subst nc, typ_subst sv subst typ)
-and typ_arg_subst sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_arg_subst_aux sv subst arg, l)
+and typ_arg_subst sv subst (A_aux (arg, l)) = A_aux (typ_arg_subst_aux sv subst arg, l)
and typ_arg_subst_aux sv subst = function
- | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp)
- | Typ_arg_typ typ -> Typ_arg_typ (typ_subst sv subst typ)
- | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord)
- | Typ_arg_bool nc -> Typ_arg_bool (constraint_subst sv subst nc)
+ | A_nexp nexp -> A_nexp (nexp_subst sv subst nexp)
+ | A_typ typ -> A_typ (typ_subst sv subst typ)
+ | A_order ord -> A_order (order_subst sv subst ord)
+ | A_bool nc -> A_bool (constraint_subst sv subst nc)
let subst_kid subst sv v x =
x
- |> subst sv (mk_typ_arg (Typ_arg_bool (nc_var v)))
- |> subst sv (mk_typ_arg (Typ_arg_nexp (nvar v)))
- |> subst sv (mk_typ_arg (Typ_arg_order (Ord_aux (Ord_var v, Parse_ast.Unknown))))
- |> subst sv (mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var v))))
+ |> subst sv (mk_typ_arg (A_bool (nc_var v)))
+ |> subst sv (mk_typ_arg (A_nexp (nvar v)))
+ |> subst sv (mk_typ_arg (A_order (Ord_aux (Ord_var v, Parse_ast.Unknown))))
+ |> subst sv (mk_typ_arg (A_typ (mk_typ (Typ_var v))))
let quant_item_subst_kid_aux sv subst = function
| QI_id (KOpt_aux (KOpt_none kid, l)) as qid ->
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 73ab4a01..fe36dfb6 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -184,6 +184,9 @@ val quant_kopts : typquant -> kinded_id list
val quant_split : typquant -> kinded_id list * n_constraint list
val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
+val is_quant_kopt : quant_item -> bool
+val is_quant_constraint : quant_item -> bool
+
(* Functions to map over the annotations in sub-expressions *)
val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
diff --git a/src/c_backend.ml b/src/c_backend.ml
index fa21f96d..535a0b67 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -155,16 +155,16 @@ let rec ctyp_of_typ ctx typ =
| _ -> CT_int
end
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "list" ->
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
CT_list (ctyp_of_typ ctx typ)
(* When converting a sail bitvector type into C, we have three options in order of efficiency:
- If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits.
- If the length is less than 64, then use a small bits type, sbits.
- If the length may be larger than 64, use a large bits type lbits. *)
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _);
- Typ_arg_aux (Typ_arg_order ord, _);
- Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id vtyp_id, _)), _)])
+ | Typ_app (id, [A_aux (A_nexp n, _);
+ A_aux (A_order ord, _);
+ A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)])
when string_of_id id = "vector" && string_of_id vtyp_id = "bit" ->
let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
begin match nexp_simp n with
@@ -173,14 +173,14 @@ let rec ctyp_of_typ ctx typ =
| _ -> CT_lbits direction
end
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _);
- Typ_arg_aux (Typ_arg_order ord, _);
- Typ_arg_aux (Typ_arg_typ typ, _)])
+ | Typ_app (id, [A_aux (A_nexp n, _);
+ A_aux (A_order ord, _);
+ A_aux (A_typ typ, _)])
when string_of_id id = "vector" ->
let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
CT_vector (direction, ctyp_of_typ ctx typ)
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "register" ->
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
CT_ref (ctyp_of_typ ctx typ)
| Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> Bindings.bindings)
@@ -822,7 +822,7 @@ let rec compile_aval l ctx = function
[iclear (CT_lbits true) gs]
(* If we have a bitvector value, that isn't a literal then we need to set bits individually. *)
- | AV_vector (avals, Typ_aux (Typ_app (id, [_; Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id bit_id, _)), _)]), _))
+ | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _))
when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 ->
let len = List.length avals in
let direction = match ord with
@@ -849,7 +849,7 @@ let rec compile_aval l ctx = function
[]
(* Compiling a vector literal that isn't a bitvector *)
- | AV_vector (avals, Typ_aux (Typ_app (id, [_; Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ typ, _)]), _))
+ | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ typ, _)]), _))
when string_of_id id = "vector" ->
let len = List.length avals in
let direction = match ord with
@@ -878,7 +878,7 @@ let rec compile_aval l ctx = function
| AV_list (avals, Typ_aux (typ, _)) ->
let ctyp = match typ with
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ
| _ -> c_error "Invalid list type"
in
let gs = gensym () in
diff --git a/src/constraint.ml b/src/constraint.ml
index 460e8c76..f512eb8a 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -109,10 +109,10 @@ let rec smt_constraint (NC_aux (aux, l) : n_constraint) : sexpr =
| NC_false -> Atom "false"
| NC_var v -> smt_var v
-and smt_typ_arg (Typ_arg_aux (aux, l) : typ_arg) : sexpr =
+and smt_typ_arg (A_aux (aux, l) : typ_arg) : sexpr =
match aux with
- | Typ_arg_nexp nexp -> smt_nexp nexp
- | Typ_arg_bool nc -> smt_constraint nc
+ | A_nexp nexp -> smt_nexp nexp
+ | A_bool nc -> smt_constraint nc
| _ ->
raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function")
diff --git a/src/initial_check.ml b/src/initial_check.ml
index e84f655c..0f1af63d 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -166,10 +166,10 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
Typ_aux (aux, l)
and to_ast_typ_arg ctx (ATyp_aux (_, l) as atyp) = function
- | K_type -> Typ_arg_aux (Typ_arg_typ (to_ast_typ ctx atyp), l)
- | K_int -> Typ_arg_aux (Typ_arg_nexp (to_ast_nexp ctx atyp), l)
- | K_order -> Typ_arg_aux (Typ_arg_order (to_ast_order ctx atyp), l)
- | K_bool -> Typ_arg_aux (Typ_arg_bool (to_ast_constraint ctx atyp), l)
+ | K_type -> A_aux (A_typ (to_ast_typ ctx atyp), l)
+ | K_int -> A_aux (A_nexp (to_ast_nexp ctx atyp), l)
+ | K_order -> A_aux (A_order (to_ast_order ctx atyp), l)
+ | K_bool -> A_aux (A_bool (to_ast_constraint ctx atyp), l)
and to_ast_nexp ctx (P.ATyp_aux (aux, l)) =
let aux = match aux with
@@ -801,8 +801,8 @@ let quant_item_typ = function
| QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))]
| _ -> []
let quant_item_arg = function
- | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt)))]
- | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))]
+ | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
+ | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))]
| _ -> []
let undefined_typschm id typq =
let qis = quant_items typq in
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 41a27be7..74ef8376 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -143,11 +143,11 @@ let subst_src_typ substs t =
let substs = List.fold_left (fun sub v -> KBindings.remove v sub) substs kids in
re (Typ_exist (kids,nc,s_styp substs t))
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
- and s_starg substs (Typ_arg_aux (ta,l) as targ) =
+ and s_starg substs (A_aux (ta,l) as targ) =
match ta with
- | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (subst_nexp substs ne),l)
- | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp substs t),l)
- | Typ_arg_order _ -> targ
+ | A_nexp ne -> A_aux (A_nexp (subst_nexp substs ne),l)
+ | A_typ t -> A_aux (A_typ (s_styp substs t),l)
+ | A_order _ -> targ
in s_styp substs t
let make_vector_lit sz i =
@@ -339,14 +339,14 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
| _ -> insts', Typ_aux (Typ_exist (kids', nc, t'), l)
end
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) =
+and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) =
match ta with
- | Typ_arg_nexp _
- | Typ_arg_order _
+ | A_nexp _
+ | A_order _
-> insts, tyarg
- | Typ_arg_typ typ ->
+ | A_typ typ ->
let insts', typ' = inst_src_type insts typ in
- insts', Typ_arg_aux (Typ_arg_typ typ',l)
+ insts', A_aux (A_typ typ',l)
let rec contains_exist (Typ_aux (ty,l)) =
match ty with
@@ -359,12 +359,12 @@ let rec contains_exist (Typ_aux (ty,l)) =
| Typ_app (_,args) -> List.exists contains_exist_arg args
| Typ_exist _ -> true
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and contains_exist_arg (Typ_arg_aux (arg,_)) =
+and contains_exist_arg (A_aux (arg,_)) =
match arg with
- | Typ_arg_nexp _
- | Typ_arg_order _
+ | A_nexp _
+ | A_order _
-> false
- | Typ_arg_typ typ -> contains_exist typ
+ | A_typ typ -> contains_exist typ
let rec size_nvars_nexp (Nexp_aux (ne,_)) =
match ne with
@@ -402,8 +402,8 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
List.concat insts, Typ_aux (Typ_tup tys,l)) (cross' tys) in
(kidset_bigunion vars, insttys)
| Typ_app (Id_aux (Id "vector",_),
- [Typ_arg_aux (Typ_arg_nexp sz,_);
- _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
+ [A_aux (A_nexp sz,_);
+ _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
(KidSet.of_list (size_nvars_nexp sz), [[],typ])
| Typ_app (_, tas) ->
(KidSet.empty,[[],typ]) (* We only support sizes for bitvectors mentioned explicitly, not any buried
@@ -525,7 +525,7 @@ let refine_constructor refinements l env id args =
match Type_check.destruct_exist env constr_ty with
| None -> None
| Some (kids,nc,constr_ty) ->
- let (bindings,_,_) = Type_check.unify l env constr_ty arg_ty in
+ let bindings = Type_check.unify l env (tyvars_of_typ constr_ty) constr_ty arg_ty in
let find_kid kid = try Some (KBindings.find kid bindings) with Not_found -> None in
let bindings = List.map find_kid kids in
let matches_refinement (mapping,_,_) =
@@ -533,7 +533,7 @@ let refine_constructor refinements l env id args =
(fun v (_,w) ->
match v,w with
| _,None -> true
- | Some (U_nexp (Nexp_aux (Nexp_constant n, _))),Some m -> Big_int.equal n m
+ | Some (A_aux (A_nexp (Nexp_aux (Nexp_constant n, _)), _)),Some m -> Big_int.equal n m
| _,_ -> false) bindings mapping
in
match List.find matches_refinement irefinements with
@@ -699,25 +699,25 @@ let fabricate_nexp_exist env l typ kids nc typ' =
match kids,nc,Env.expand_synonyms env typ' with
| ([kid],NC_aux (NC_set (kid',i::_),_),
Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 ->
Nexp_aux (Nexp_constant i,Unknown)
| ([kid],NC_aux (NC_true,_),
Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
when Kid.compare kid kid'' = 0 ->
nint 32
| ([kid],NC_aux (NC_set (kid',i::_),_),
Typ_aux (Typ_app (Id_aux (Id "range",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_);
- Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+ A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 &&
Kid.compare kid kid''' = 0 ->
Nexp_aux (Nexp_constant i,Unknown)
| ([kid],NC_aux (NC_true,_),
Typ_aux (Typ_app (Id_aux (Id "range",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_);
- Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+ A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
when Kid.compare kid kid'' = 0 &&
Kid.compare kid kid''' = 0 ->
nint 32
@@ -734,7 +734,7 @@ let fabricate_nexp l tannot =
let atom_typ_kid kid = function
| Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_) ->
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_) ->
Kid.compare kid kid' = 0
| _ -> false
@@ -850,7 +850,7 @@ let try_app (l,ann) (id,args) =
E_aux (E_lit L_aux (L_num i,_), _);
E_aux (E_lit L_aux (L_num len,_), _)] ->
(match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with
- | Typ_aux (Typ_app (_,[_;Typ_arg_aux (Typ_arg_order ord,_);_]),_) ->
+ | Typ_aux (Typ_app (_,[_;A_aux (A_order ord,_);_]),_) ->
(match slice_lit lit i len ord with
| Some lit' -> Some (E_aux (E_lit lit',(l,ann)))
| None -> None)
@@ -1698,7 +1698,7 @@ let split_defs all_errors splits defs =
[L_zero; L_one]
| _ -> cannot ("don't know about type " ^ string_of_id id))
- | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
+ | Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp len,_);_;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
(match len with
| Nexp_aux (Nexp_constant sz,_) ->
let lits = make_vectors (Big_int.to_int sz) in
@@ -1709,7 +1709,7 @@ let split_defs all_errors splits defs =
cannot ("length not constant, " ^ string_of_nexp len)
)
(* set constrained numbers *)
- | Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (value,_) as nexp),_)]) ->
+ | Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp (Nexp_aux (value,_) as nexp),_)]) ->
begin
let mk_lit kid i =
let lit = L_aux (L_num i,new_l) in
@@ -1844,7 +1844,7 @@ let split_defs all_errors splits defs =
let kid_subst = match orig_typ with
| Typ_aux
(Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp
+ [A_aux (A_nexp
(Nexp_aux (Nexp_var var,_)),_)]),_) ->
[var,nconstant j]
| _ -> []
@@ -2188,18 +2188,18 @@ let rec sizes_of_typ (Typ_aux (t,l)) =
| Typ_exist (kids,_,typ) ->
List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids
| Typ_app (Id_aux (Id "vector",_),
- [Typ_arg_aux (Typ_arg_nexp size,_);
- _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
+ [A_aux (A_nexp size,_);
+ _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) ->
KidSet.of_list (size_nvars_nexp size)
| Typ_app (_,tas) ->
kidset_bigunion (List.map sizes_of_typarg tas)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and sizes_of_typarg (Typ_arg_aux (ta,_)) =
+and sizes_of_typarg (A_aux (ta,_)) =
match ta with
- Typ_arg_nexp _
- | Typ_arg_order _
+ A_nexp _
+ | A_order _
-> KidSet.empty
- | Typ_arg_typ typ -> sizes_of_typ typ
+ | A_typ typ -> sizes_of_typ typ
let sizes_of_annot (l, tannot) =
match destruct_tannot tannot with
@@ -2262,17 +2262,17 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
let mk_exp nexp l l' =
let nexp = replace_size nexp in
E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
- [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)),
+ [A_aux (A_nexp nexp,l')]),Generated Unknown)),
E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,empty_tannot))),
(Generated l,empty_tannot))
in
match typ with
| Typ_aux (Typ_app (Id_aux (Id "range",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp nexp',_)]),_)
+ [A_aux (A_nexp nexp,l');A_aux (A_nexp nexp',_)]),_)
when nexp_identical nexp nexp' ->
mk_exp nexp l l'
| Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,l')]),_) ->
+ [A_aux (A_nexp nexp,l')]),_) ->
mk_exp nexp l l'
| _ -> raise (Reporting.err_unreachable l __POS__
"atom stopped being an atom?")
@@ -2281,13 +2281,13 @@ let replace_type env typ =
let Typ_aux (t,l) = Env.expand_synonyms env typ in
match t with
| Typ_app (Id_aux (Id "range",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp _,_)]) ->
+ [A_aux (A_nexp nexp,l');A_aux (A_nexp _,_)]) ->
Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
- [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l)
+ [A_aux (A_nexp nexp,l')]),Generated l)
| Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,l')]) ->
+ [A_aux (A_nexp nexp,l')]) ->
Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
- [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l)
+ [A_aux (A_nexp nexp,l')]),Generated l)
| _ -> raise (Reporting.err_unreachable l __POS__
"atom stopped being an atom?")
@@ -2308,12 +2308,12 @@ let rewrite_size_parameters env (Defs defs) =
let nmap =
match Env.base_typ_of env typ with
Typ_aux (Typ_app(Id_aux (Id "range",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,_);
- Typ_arg_aux (Typ_arg_nexp nexp',_)]),_)
+ [A_aux (A_nexp nexp,_);
+ A_aux (A_nexp nexp',_)]),_)
when Nexp.compare nexp nexp' = 0 && not (NexpMap.mem nexp nmap) ->
NexpMap.add nexp i nmap
| Typ_aux (Typ_app(Id_aux (Id "atom", _),
- [Typ_arg_aux (Typ_arg_nexp nexp,_)]), _)
+ [A_aux (A_nexp nexp,_)]), _)
when not (NexpMap.mem nexp nmap) ->
NexpMap.add nexp i nmap
| _ -> nmap
@@ -2331,7 +2331,7 @@ in *)
match destruct_tannot tannot with
| Some (env,typ,_) ->
begin match Env.base_typ_of env typ with
- | Typ_aux (Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp size,_);_;_]),_)
+ | Typ_aux (Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp size,_);_;_]),_)
when not (is_nexp_constant size) ->
begin
match NexpMap.find size nexp_map with
@@ -2845,14 +2845,16 @@ let rec deps_of_nc kid_deps (NC_aux (nc,l)) =
let deps_of_typ l kid_deps arg_deps typ =
deps_of_tyvars l kid_deps arg_deps (tyvars_of_typ typ)
-let deps_of_uvar l fn_id env arg_deps = function
- | U_nexp (Nexp_aux (Nexp_var kid,_))
+let deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) =
+ match aux with
+ | A_nexp (Nexp_aux (Nexp_var kid,_))
when List.exists (fun k -> Kid.compare kid k == 0) env.top_kids ->
Parents (CallerKidSet.singleton (fn_id,kid))
- | U_nexp nexp -> InFun (deps_of_nexp l env.kid_deps arg_deps nexp)
- | U_order _ -> InFun dempty
- | U_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ)
-
+ | A_nexp nexp -> InFun (deps_of_nexp l env.kid_deps arg_deps nexp)
+ | A_order _ -> InFun dempty
+ | A_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ)
+ | A_bool nc -> InFun (deps_of_nc env.kid_deps nc)
+
let mk_subrange_pattern vannot vstart vend =
let (len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in
match ord with
@@ -2937,8 +2939,8 @@ let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
| kid -> Nexp_aux (Nexp_var kid,Generated l)
| exception Not_found -> nexp
-let simplify_size_uvar env typ_env = function
- | U_nexp nexp -> U_nexp (simplify_size_nexp env typ_env nexp)
+let simplify_size_typ_arg env typ_env = function
+ | A_aux (A_nexp nexp, l) -> A_aux (A_nexp (simplify_size_nexp env typ_env nexp), l)
| x -> x
(* Takes an environment of dependencies on vars, type vars, and flow control,
@@ -3030,10 +3032,10 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
| _ -> Unknown (l, "Effects from function application")
in
let kid_inst = instantiation_of exp in
- let kid_inst = KBindings.map (simplify_size_uvar env typ_env) kid_inst in
+ let kid_inst = KBindings.map (simplify_size_typ_arg env typ_env) kid_inst in
(* Change kids in instantiation to the canonical ones from the type signature *)
let kid_inst = KBindings.fold (fun kid -> KBindings.add (orig_kid kid)) kid_inst KBindings.empty in
- let kid_deps = KBindings.map (deps_of_uvar l fn_id env deps) kid_inst in
+ let kid_deps = KBindings.map (deps_of_typ_arg l fn_id env deps) kid_inst in
let rdep,r' =
if Id.compare fn_id id == 0 then
let bad = Unknown (l,"Recursive call of " ^ string_of_id id) in
@@ -3265,7 +3267,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
let env = env_of_annot annot in
let Typ_aux (typ,_) = Env.base_typ_of env (typ_of_annot annot) in
match typ with
- | Typ_app (Id_aux (Id "atom",_),[Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)]) ->
+ | Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]) ->
equal_kids env kid
| _ -> KidSet.empty
in
@@ -3287,7 +3289,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
in
let eqn_instantiations = Type_check.instantiate_simple_equations qs in
let eqn_kid_deps = KBindings.map (function
- | U_nexp nexp -> Some (nexp_frees nexp)
+ | A_aux (A_nexp nexp, _) -> Some (nexp_frees nexp)
| _ -> None) eqn_instantiations
in
let arg i pat =
@@ -3944,15 +3946,15 @@ let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ =
P_aux (P_typ (src_typ, P_aux (P_tup ps,(Generated src_l, src_ann))),(Generated src_l, src_ann)),
E_aux (E_tuple es,(Generated tar_l, tar_ann))
| Typ_app (Id_aux (Id "vector",_),
- [Typ_arg_aux (Typ_arg_nexp size,_); _;
- Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]),
+ [A_aux (A_nexp size,_); _;
+ A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]),
Typ_app (Id_aux (Id "vector",_) as t_id,
- [Typ_arg_aux (Typ_arg_nexp size',l_size'); t_ord;
- Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_) as t_bit]) -> begin
+ [A_aux (A_nexp size',l_size'); t_ord;
+ A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_) as t_bit]) -> begin
match simplify_size_nexp env quant_kids size, simplify_size_nexp env quant_kids size' with
| Some size, Some size' when Nexp.compare size size' <> 0 ->
let var = fresh () in
- let tar_typ' = Typ_aux (Typ_app (t_id, [Typ_arg_aux (Typ_arg_nexp size',l_size');t_ord;t_bit]),
+ let tar_typ' = Typ_aux (Typ_app (t_id, [A_aux (A_nexp size',l_size');t_ord;t_bit]),
tar_l) in
let () = at_least_one := Some tar_typ' in
P_aux (P_id var,(Generated src_l,src_ann)),
@@ -4052,7 +4054,7 @@ let add_bitvector_casts (Defs defs) =
let matched_typ = Env.base_typ_of env (typ_of_annot ann') in
match e',matched_typ with
| E_sizeof (Nexp_aux (Nexp_var kid,_)), _
- | _, Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_) ->
+ | _, Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_) ->
let map_case pexp =
let pat,guard,body,ann = destruct_pexp pexp in
let body = match pat, guard with
@@ -4176,16 +4178,16 @@ let replace_nexp_in_typ env typ orig new_nexp =
let fs, targs = List.split (List.map aux_targ targs) in
List.exists (fun x -> x) fs, Typ_aux (Typ_app (id, targs),l)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
- and aux_targ (Typ_arg_aux (ta,l) as typ_arg) =
+ and aux_targ (A_aux (ta,l) as typ_arg) =
match ta with
- | Typ_arg_nexp nexp ->
+ | A_nexp nexp ->
if prove env (nc_eq nexp orig)
- then true, Typ_arg_aux (Typ_arg_nexp new_nexp,l)
+ then true, A_aux (A_nexp new_nexp,l)
else false, typ_arg
- | Typ_arg_typ typ ->
+ | A_typ typ ->
let f, typ = aux typ in
- f, Typ_arg_aux (Typ_arg_typ typ,l)
- | Typ_arg_order _ -> false, typ_arg
+ f, A_aux (A_typ typ,l)
+ | A_order _ -> false, typ_arg
in aux typ
let fresh_nexp_kid nexp =
@@ -4277,13 +4279,13 @@ let rewrite_toplevel_nexps (Defs defs) =
Typ_aux (Typ_exist (kids,(* TODO? *) nc, aux typ'),l)
| Typ_app (id,targs) -> Typ_aux (Typ_app (id,List.map aux_targ targs),l)
| _ -> typ_full
- and aux_targ (Typ_arg_aux (ta,l) as ta_full) =
+ and aux_targ (A_aux (ta,l) as ta_full) =
match ta with
- | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (aux typ),l)
- | Typ_arg_order _ -> ta_full
- | Typ_arg_nexp nexp ->
+ | A_typ typ -> A_aux (A_typ (aux typ),l)
+ | A_order _ -> ta_full
+ | A_nexp nexp ->
match find_nexp env nexp_map nexp with
- | (kid,_) -> Typ_arg_aux (Typ_arg_nexp (nvar kid),l)
+ | (kid,_) -> A_aux (A_nexp (nvar kid),l)
| exception Not_found -> ta_full
in aux typ
in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index a3d47814..cfd79290 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -103,10 +103,10 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg =
| Typ_id id when string_of_id id = "exception" -> string "Printexc.to_string" ^^ space ^^ arg
| Typ_id id -> ocaml_string_of id ^^ space ^^ arg
| Typ_app (id, []) -> ocaml_string_of id ^^ space ^^ arg
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id eid, _)), _)])
+ | Typ_app (id, [A_aux (A_typ (Typ_aux (Typ_id eid, _)), _)])
when string_of_id id = "list" && string_of_id eid = "bit" ->
string "string_of_bits" ^^ space ^^ arg
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "list" ->
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
let farg = gensym () in
separate space [string "string_of_list \", \""; parens (separate space [string "fun"; farg; string "->"; ocaml_string_typ typ farg]); arg]
| Typ_app (_, _) -> string "\"APP\""
@@ -147,9 +147,9 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) =
| Typ_var kid -> zencode_kid kid
| Typ_exist _ -> assert false
| Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
-and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+and ocaml_typ_arg ctx (A_aux (typ_arg_aux, _) as typ_arg) =
match typ_arg_aux with
- | Typ_arg_typ typ -> ocaml_typ ctx typ
+ | A_typ typ -> ocaml_typ ctx typ
| _ -> failwith ("OCaml: unexpected type argument " ^ string_of_typ_arg typ_arg)
let ocaml_typquant typq =
@@ -602,7 +602,7 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
^//^ (bar ^^ space ^^ ocaml_enum ctx ids))
^^ ocaml_def_end
^^ ocaml_string_of_enum ctx id ids
- | TD_abbrev (id, typq, Typ_arg_aux (Typ_arg_typ typ, _)) ->
+ | TD_abbrev (id, typq, A_aux (A_typ typ, _)) ->
separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; ocaml_typ ctx typ]
^^ ocaml_def_end
^^ ocaml_string_of_abbrev ctx id typq typ
@@ -698,15 +698,15 @@ let ocaml_pp_generators ctx defs orig_types required =
string_of_typ full_typ))
| Typ_app (id,args) ->
List.fold_left add_req_from_typarg (add_req_from_id required id) args
- and add_req_from_typarg required (Typ_arg_aux (arg,_)) =
+ and add_req_from_typarg required (A_aux (arg,_)) =
match arg with
- | Typ_arg_typ typ -> add_req_from_typ required typ
- | Typ_arg_nexp _
- | Typ_arg_order _
+ | A_typ typ -> add_req_from_typ required typ
+ | A_nexp _
+ | A_order _
-> required
and add_req_from_td required (TD_aux (td,(l,_))) =
match td with
- | TD_abbrev (_, _, Typ_arg_aux (Typ_arg_typ typ, _)) ->
+ | TD_abbrev (_, _, A_aux (A_typ typ, _)) ->
add_req_from_typ required typ
| TD_record (_, _, _, fields, _) ->
List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields
@@ -723,7 +723,7 @@ let ocaml_pp_generators ctx defs orig_types required =
match Bindings.find id typemap with
| TD_aux (td,_) ->
(match td with
- | TD_abbrev (_,tqs,Typ_arg_aux (Typ_arg_typ _, _)) -> tqs
+ | TD_abbrev (_,tqs,A_aux (A_typ _, _)) -> tqs
| TD_record (_,_,tqs,_,_) -> tqs
| TD_variant (_,_,tqs,_,_) -> tqs
| TD_enum _ -> TypQ_aux (TypQ_no_forall,Unknown)
@@ -743,10 +743,10 @@ let ocaml_pp_generators ctx defs orig_types required =
let name = "gen_" ^ type_name id in
let make_tyarg kindedid =
if is_nat_kopt kindedid
- then mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kindedid)))
+ then mk_typ_arg (A_nexp (nvar (kopt_kid kindedid)))
else if is_order_kopt kindedid
- then mk_typ_arg (Typ_arg_order (mk_ord (Ord_var (kopt_kid kindedid))))
- else mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kindedid))))
+ then mk_typ_arg (A_order (mk_ord (Ord_var (kopt_kid kindedid))))
+ else mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kindedid))))
in
let targs = List.map make_tyarg tquants in
let gen_tyvars_pp, out_typ = match gen_tyvars with
@@ -778,20 +778,20 @@ let ocaml_pp_generators ctx defs orig_types required =
| _ -> space ^^ separate space args_pp
in
string ("g.gen_" ^ typ_str) ^^ args_pp
- and typearg (Typ_arg_aux (arg,_)) =
+ and typearg (A_aux (arg,_)) =
match arg with
- | Typ_arg_nexp (Nexp_aux (nexp,l) as full_nexp) ->
+ | A_nexp (Nexp_aux (nexp,l) as full_nexp) ->
(match nexp with
| Nexp_constant c -> string (Big_int.to_string c) (* TODO: overflow *)
| Nexp_var v -> mk_arg v
| _ -> raise (Reporting.err_todo l
("Unsupported nexp for generators: " ^ string_of_nexp full_nexp)))
- | Typ_arg_order (Ord_aux (ord,_)) ->
+ | A_order (Ord_aux (ord,_)) ->
(match ord with
| Ord_var v -> mk_arg v
| Ord_inc -> string "true"
| Ord_dec -> string "false")
- | Typ_arg_typ typ -> parens (string "fun g -> " ^^ gen_type typ)
+ | A_typ typ -> parens (string "fun g -> " ^^ gen_type typ)
in
let make_subgen (Typ_aux (typ,l) as full_typ) =
let typ_str, args_pp =
@@ -845,7 +845,7 @@ let ocaml_pp_generators ctx defs orig_types required =
let tqs, body, constructors, builders =
let TD_aux (td,(l,_)) = Bindings.find id typemap in
match td with
- | TD_abbrev (_,tqs,Typ_arg_aux (Typ_arg_typ typ, _)) ->
+ | TD_abbrev (_,tqs,A_aux (A_typ typ, _)) ->
tqs, gen_type typ, None, None
| TD_variant (_,_,tqs,variants,_) ->
tqs,
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 1fb35158..0f1dee90 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -140,10 +140,10 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
| _ -> app_typ ty
and app_typ ((Typ_aux (t, _)) as ty) = match t with
| Typ_app(Id_aux (Id "range", _), [
- Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
- Typ_arg_aux(Typ_arg_nexp m, _);]) ->
+ A_aux(A_nexp (Nexp_aux(Nexp_constant n, _)), _);
+ A_aux(A_nexp m, _);]) ->
(squarebars (if Big_int.equal n Big_int.zero then nexp m else doc_op colon (doc_int n) (nexp m)))
- | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+ | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
(squarecolons (nexp n))
| Typ_app(id,args) ->
(* trailing space to avoid >> token in case of nested app types *)
@@ -158,13 +158,13 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
group (parens (typ ty))
| Typ_internal_unknown -> string "UNKNOWN"
- and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
+ and doc_typ_arg (A_aux(t,_)) = match t with
(* Be careful here because typ_arg is implemented as nexp in the
* parser - in practice falling through app_typ after all the proper nexp
- * cases; so Typ_arg_typ has the same precedence as a Typ_app *)
- | Typ_arg_typ t -> app_typ t
- | Typ_arg_nexp n -> nexp n
- | Typ_arg_order o -> doc_ord o
+ * cases; so A_typ has the same precedence as a Typ_app *)
+ | A_typ t -> app_typ t
+ | A_nexp n -> nexp n
+ | A_order o -> doc_ord o
(* same trick to handle precedence of nexp *)
and nexp ne = sum_typ ne
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 50a97fa8..025156cc 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -268,7 +268,7 @@ let rec coq_nvars_of_typ (Typ_aux (t,l)) =
| Typ_tup ts ->
List.fold_left (fun s t -> KidSet.union s (trec t))
KidSet.empty ts
- | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+ | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) ->
trec etyp
| Typ_app(Id_aux (Id "implicit", _),_)
(* TODO: update when complex atom types are sorted out *)
@@ -280,11 +280,11 @@ let rec coq_nvars_of_typ (Typ_aux (t,l)) =
| Typ_exist (kids,_,t) -> trec t
| Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types"
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and coq_nvars_of_typ_arg (Typ_arg_aux (ta,_)) =
+and coq_nvars_of_typ_arg (A_aux (ta,_)) =
match ta with
- | Typ_arg_nexp nexp -> tyvars_of_nexp (orig_nexp nexp)
- | Typ_arg_typ typ -> coq_nvars_of_typ typ
- | Typ_arg_order _ -> KidSet.empty
+ | A_nexp nexp -> tyvars_of_nexp (orig_nexp nexp)
+ | A_typ typ -> coq_nvars_of_typ typ
+ | A_order _ -> KidSet.empty
(* Follows Coq precedence levels *)
let rec doc_nc_prop ctx nc =
@@ -353,8 +353,8 @@ let doc_nc_exp ctx nc =
let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
match typ with
- | Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_);
- Typ_arg_aux(Typ_arg_nexp high,_)]) ->
+ | Typ_app(Id_aux (Id "range", _), [A_aux(A_nexp low,_);
+ A_aux(A_nexp high,_)]) ->
(* TODO: avoid name clashes *)
let kid = mk_kid "rangevar" in
let var = nvar kid in
@@ -411,16 +411,16 @@ let doc_typ, doc_atomic_typ =
| _ -> app_typ atyp_needed ty
and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_app(Id_aux (Id "vector", _), [
- Typ_arg_aux (Typ_arg_nexp m, _);
- Typ_arg_aux (Typ_arg_order ord, _);
- Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
+ A_aux (A_nexp m, _);
+ A_aux (A_order ord, _);
+ A_aux (A_typ elem_typ, _)]) ->
(* TODO: remove duplication with exists, below *)
let tpp = match elem_typ with
| Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> (* TODO: coq-compatible simplification *)
string "mword " ^^ doc_nexp ctx m
| _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in
if atyp_needed then parens tpp else tpp
- | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+ | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) ->
let tpp = string "register_ref regstate register_value " ^^ typ etyp in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "range", _), _)
@@ -430,7 +430,7 @@ let doc_typ, doc_atomic_typ =
| None -> raise (Reporting.err_unreachable l __POS__ "Bad range type"))
| Typ_app(Id_aux (Id "implicit", _),_) ->
(string "Z")
- | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+ | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
(string "Z")
| Typ_app(id,args) ->
let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in
@@ -457,7 +457,7 @@ let doc_typ, doc_atomic_typ =
in
match ty' with
| Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,_)]),_) ->
+ [A_aux (A_nexp nexp,_)]),_) ->
begin match nexp, kids with
| (Nexp_aux (Nexp_var kid,_)), [kid'] when Kid.compare kid kid' == 0 ->
braces (separate space [doc_var ctx kid; colon; string "Z";
@@ -469,9 +469,9 @@ let doc_typ, doc_atomic_typ =
ampersand; doc_arithfact ctx ~exists:kids nc])
end
| Typ_aux (Typ_app (Id_aux (Id "vector",_),
- [Typ_arg_aux (Typ_arg_nexp m, _);
- Typ_arg_aux (Typ_arg_order ord, _);
- Typ_arg_aux (Typ_arg_typ elem_typ, _)]),_) ->
+ [A_aux (A_nexp m, _);
+ A_aux (A_order ord, _);
+ A_aux (A_typ elem_typ, _)]),_) ->
(* TODO: proper handling of m, complex elem type, dedup with above *)
let var = mk_kid "_vec" in (* TODO collision avoid *)
let kid_set = KidSet.of_list kids in
@@ -515,10 +515,10 @@ let doc_typ, doc_atomic_typ =
end*)
| Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types"
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
- and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
- | Typ_arg_typ t -> app_typ true t
- | Typ_arg_nexp n -> doc_nexp ctx n
- | Typ_arg_order o -> empty
+ and doc_typ_arg (A_aux(t,_)) = match t with
+ | A_typ t -> app_typ true t
+ | A_nexp n -> doc_nexp ctx n
+ | A_order o -> empty
in typ', atomic_typ
in (fun ctx -> (fst (fns ctx))), (fun ctx -> (snd (fns ctx)))
@@ -530,10 +530,10 @@ let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) =
(* TODO: should we resurrect this?
let replace_typ_size ctxt env (Typ_aux (t,a)) =
match t with
- | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) ->
+ | Typ_app (Id_aux (Id "vector",_) as id, [A_aux (A_nexp size,_);ord;typ']) ->
begin
let mk_typ nexp =
- Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
+ Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
in
match Type_check.solve env size with
| Some n -> mk_typ (nconstant n)
@@ -645,10 +645,10 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
| Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (typeclass_nexps t2) (List.map typeclass_nexps t1)
| Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
| Typ_app (Id_aux (Id "vector",_),
- [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
- _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
+ [A_aux (A_nexp size_nexp,_);
+ _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
| Typ_app (Id_aux (Id "itself",_),
- [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) ->
+ [A_aux (A_nexp size_nexp,_)]) ->
let size_nexp = nexp_simp size_nexp in
if is_nexp_constant size_nexp then NexpSet.empty else
NexpSet.singleton (orig_nexp size_nexp)
@@ -693,8 +693,7 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
let arg_typs =
match Env.expand_synonyms env ctor_typ with
| Typ_aux (Typ_fn (arg_typs, ret_typ, _), _) ->
- (* The FIXME comes from the typechecker code, not sure what it's about... *)
- let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
+ let unifiers = unify l env (tyvars_of_typ ret_typ) ret_typ typ in
List.map (subst_unifiers unifiers) arg_typs
| _ -> assert false
in
@@ -742,14 +741,14 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
| _ -> parens (separate_map comma_sp (doc_pat ctxt false exists_as_pairs) (List.combine pats typs)))
| P_list pats ->
let el_typ = match typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_)
+ | Typ_aux (Typ_app (f, [A_aux (A_typ el_typ,_)]),_)
when Id.compare f (mk_id "list") = 0 -> el_typ
| _ -> raise (Reporting.err_unreachable l __POS__ "list pattern not a list")
in
brackets (separate_map semi (fun p -> doc_pat ctxt false true (p, el_typ)) pats)
| P_cons (p,p') ->
let el_typ = match typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_)
+ | Typ_aux (Typ_app (f, [A_aux (A_typ el_typ,_)]),_)
when Id.compare f (mk_id "list") = 0 -> el_typ
| _ -> raise (Reporting.err_unreachable l __POS__ "list pattern not a list")
in
@@ -776,7 +775,7 @@ let find_e_ids exp =
let typ_id_of (Typ_aux (typ, l)) = match typ with
| Typ_id id -> id
- | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
+ | Typ_app (register, [A_aux (A_typ (Typ_aux (Typ_id id, _)), _)])
when string_of_id register = "register" -> id
| Typ_app (id, _) -> id
| _ -> raise (Reporting.err_unreachable l __POS__ "failed to get type id")
@@ -861,16 +860,16 @@ let is_no_Z_proof_fn env id =
let replace_atom_return_type ret_typ =
(* TODO: more complex uses of atom *)
match ret_typ with
- | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) ->
+ | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),l) ->
let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l)
| _ -> false, ret_typ
let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) =
match argty, fnty with
- | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),
- Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_);
- Typ_arg_aux(Typ_arg_nexp high,_)]) ->
+ | Typ_app(Id_aux (Id "atom", _), [A_aux (A_nexp nexp,_)]),
+ Typ_app(Id_aux (Id "range", _), [A_aux(A_nexp low,_);
+ A_aux(A_nexp high,_)]) ->
Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high))
| _ -> false
@@ -932,8 +931,8 @@ let doc_exp, doc_let =
(* Avoid using helper functions which simplify the nexps *)
is_bitvector_typ in_typ && is_bitvector_typ out_typ &&
match in_typ, out_typ with
- | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_),
- Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) ->
+ | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
+ Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
not (similar_nexps ctxt (env_of exp) n1 n2)
| _ -> false
in
@@ -1185,8 +1184,8 @@ let doc_exp, doc_let =
(* Avoid using helper functions which simplify the nexps *)
is_bitvector_typ typ_of_arg' && is_bitvector_typ typ_from_fn' &&
match typ_of_arg', typ_from_fn' with
- | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_),
- Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) ->
+ | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
+ Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
not (similar_nexps ctxt env n1 n2)
| _ -> false
in
@@ -1235,8 +1234,8 @@ let doc_exp, doc_let =
(* Avoid using helper functions which simplify the nexps *)
is_bitvector_typ in_typ && is_bitvector_typ out_typ &&
match in_typ, out_typ with
- | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_),
- Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) ->
+ | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
+ Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
not (similar_nexps ctxt env n1 n2)
| _ -> false
in pack,unpack,autocast
@@ -1333,8 +1332,8 @@ let doc_exp, doc_let =
(* Avoid using helper functions which simplify the nexps *)
is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
match outer_typ', cast_typ' with
- | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_),
- Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) ->
+ | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
+ Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
not (similar_nexps ctxt env n1 n2)
| _ -> false
in
@@ -1656,9 +1655,9 @@ let types_used_with_generic_eq defs =
List.fold_left add_typ_arg (IdSet.add id idset) args
| Typ_tup ts -> List.fold_left add_typ idset ts
| _ -> idset
- and add_typ_arg idset (Typ_arg_aux (ta,_)) =
+ and add_typ_arg idset (A_aux (ta,_)) =
match ta with
- | Typ_arg_typ typ -> add_typ idset typ
+ | A_typ typ -> add_typ idset typ
| _ -> idset
in
let alg =
@@ -1711,7 +1710,7 @@ let rec doc_range (BF_aux(r,_)) = match r with
| BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with
- | TD_abbrev(id,typq,Typ_arg_aux (Typ_arg_typ typ, _)) ->
+ | TD_abbrev(id,typq,A_aux (A_typ typ, _)) ->
let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in
doc_op coloneq
(separate space [string "Definition"; doc_id_type id;
@@ -1729,7 +1728,7 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with
let quant_item = function
| QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l)
| QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) ->
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, l)), l)]
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid, l)), l)]
| _ -> [] in
let targs = List.concat (List.map quant_item qs) in
mk_typ (Typ_app (id, targs))
@@ -1879,7 +1878,7 @@ let rec atom_constraint ctxt (pat, typ) =
match pat, typ with
| P_aux (P_id id, _),
Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp nexp,_)]),_) ->
+ [A_aux (A_nexp nexp,_)]),_) ->
(match nexp with
(* When the kid is mapped to the id, we don't need a constraint *)
| Nexp_aux (Nexp_var kid,_)
@@ -2039,12 +2038,12 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
match destruct_exist env full_typ with
| Some ([kid], NC_aux (NC_true,_),
Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
when Kid.compare kid kid' == 0 ->
parens (separate space [doc_id id; colon; string "Z"])
| Some ([kid], nc,
Typ_aux (Typ_app (Id_aux (Id "atom",_),
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
when Kid.compare kid kid' == 0 ->
(used_a_pattern := true;
squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]))
@@ -2169,8 +2168,8 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in
let reftyp =
mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
- [mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname)));
- mk_typ_arg (Typ_arg_typ ftyp)])) in
+ [mk_typ_arg (A_typ (mk_id_typ (mk_id tname)));
+ mk_typ_arg (A_typ ftyp)])) in
let rfannot = doc_tannot empty_ctxt Env.empty false reftyp in
doc_op equals
(concat [string "let "; parens (concat [string tname; underscore; doc_id fid; rfannot])])
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index e5613961..1764ab92 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -224,14 +224,14 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) =
List.fold_left (fun s t -> NexpSet.union s (trec t))
NexpSet.empty ts
| Typ_app(Id_aux (Id "vector", _), [
- Typ_arg_aux (Typ_arg_nexp m, _);
- Typ_arg_aux (Typ_arg_order ord, _);
- Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
+ A_aux (A_nexp m, _);
+ A_aux (A_order ord, _);
+ A_aux (A_typ elem_typ, _)]) ->
let m = nexp_simp m in
if !opt_mwords && is_bit_typ elem_typ && not (is_nexp_constant m) then
NexpSet.singleton (orig_nexp m)
else trec elem_typ
- | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+ | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) ->
trec etyp
| Typ_app(Id_aux (Id "range", _),_)
| Typ_app(Id_aux (Id "implicit", _),_)
@@ -242,11 +242,11 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) =
| Typ_exist (kids,_,t) -> trec t
| Typ_bidir _ -> raise (Reporting.err_unreachable l __POS__ "Lem doesn't support bidir types")
| Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
-and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) =
+and lem_nexps_of_typ_arg (A_aux (ta,_)) =
match ta with
- | Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
- | Typ_arg_typ typ -> lem_nexps_of_typ typ
- | Typ_arg_order _ -> NexpSet.empty
+ | A_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
+ | A_typ typ -> lem_nexps_of_typ typ
+ | A_order _ -> NexpSet.empty
let lem_tyvars_of_typ typ =
NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp))
@@ -274,9 +274,9 @@ let doc_typ_lem, doc_atomic_typ_lem =
| _ -> app_typ atyp_needed ty
and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with
| Typ_app(Id_aux (Id "vector", _), [
- Typ_arg_aux (Typ_arg_nexp m, _);
- Typ_arg_aux (Typ_arg_order ord, _);
- Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
+ A_aux (A_nexp m, _);
+ A_aux (A_order ord, _);
+ A_aux (A_typ elem_typ, _)]) ->
let tpp = match elem_typ with
| Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when !opt_mwords ->
string "mword " ^^ doc_nexp_lem (nexp_simp m)
@@ -287,14 +287,14 @@ let doc_typ_lem, doc_atomic_typ_lem =
"cannot pretty-print bitvector type with non-constant length")) *)
| _ -> string "list" ^^ space ^^ typ elem_typ in
if atyp_needed then parens tpp else tpp
- | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+ | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) ->
let tpp = string "register_ref regstate register_value " ^^ typ etyp in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "range", _),_) ->
(string "integer")
| Typ_app(Id_aux (Id "implicit", _),_) ->
(string "integer")
- | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+ | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
(string "integer")
| Typ_app(id,args) ->
let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args) in
@@ -325,10 +325,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
end
| Typ_bidir _ -> unreachable l __POS__ "Lem doesn't support bidir types"
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
- and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
- | Typ_arg_typ t -> app_typ true t
- | Typ_arg_nexp n -> doc_nexp_lem (nexp_simp n)
- | Typ_arg_order o -> empty
+ and doc_typ_arg_lem (A_aux(t,_)) = match t with
+ | A_typ t -> app_typ true t
+ | A_nexp n -> doc_nexp_lem (nexp_simp n)
+ | A_order o -> empty
in typ', atomic_typ
(* Check for variables in types that would be pretty-printed. *)
@@ -338,10 +338,10 @@ let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) =
let replace_typ_size ctxt env (Typ_aux (t,a)) =
match t with
- | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) ->
+ | Typ_app (Id_aux (Id "vector",_) as id, [A_aux (A_nexp size,_);ord;typ']) ->
begin
let mk_typ nexp =
- Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
+ Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
in
match Type_check.solve env size with
| Some n -> mk_typ (nconstant n)
@@ -443,16 +443,16 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
| Typ_fn (ts,t,_) -> List.fold_left NexpSet.union (typeclass_nexps t) (List.map typeclass_nexps ts)
| Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
| Typ_app (Id_aux (Id "vector",_),
- [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
- _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
+ [A_aux (A_nexp size_nexp,_);
+ _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)])
| Typ_app (Id_aux (Id "itself",_),
- [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) ->
+ [A_aux (A_nexp size_nexp,_)]) ->
let size_nexp = nexp_simp size_nexp in
if is_nexp_constant size_nexp then NexpSet.empty else
NexpSet.singleton (orig_nexp size_nexp)
| Typ_app (id, args) ->
let add_arg_nexps nexps = function
- | Typ_arg_aux (Typ_arg_typ typ, _) ->
+ | A_aux (A_typ typ, _) ->
NexpSet.union nexps (typeclass_nexps typ)
| _ -> nexps
in
@@ -533,8 +533,8 @@ let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in
typ_needs_printed t && KidSet.is_empty visible_kids
| _ -> false
-and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with
- | Typ_arg_typ t -> typ_needs_printed t
+and typ_needs_printed_arg (A_aux (targ, _)) = match targ with
+ | A_typ t -> typ_needs_printed t
| _ -> false
let contains_early_return exp =
@@ -553,7 +553,7 @@ let find_e_ids exp =
let typ_id_of (Typ_aux (typ, l)) = match typ with
| Typ_id id -> id
- | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
+ | Typ_app (register, [A_aux (A_typ (Typ_aux (Typ_id id, _)), _)])
when string_of_id register = "register" -> id
| Typ_app (id, _) -> id
| _ -> raise (Reporting.err_unreachable l __POS__ "failed to get type id")
@@ -1006,7 +1006,7 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
| BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
- | TD_abbrev(id,typq,Typ_arg_aux (Typ_arg_typ typ, _)) ->
+ | TD_abbrev(id,typq,A_aux (A_typ typ, _)) ->
let typschm = TypSchm_aux (TypSchm_ts (typq, typ), l) in
doc_op equals
(separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
@@ -1022,7 +1022,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
let quant_item = function
| QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l)
| QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) ->
- [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, l)), l)]
+ [A_aux (A_nexp (Nexp_aux (Nexp_var kid, l)), l)]
| _ -> [] in
let targs = List.concat (List.map quant_item qs) in
mk_typ (Typ_app (id, targs))
@@ -1031,8 +1031,8 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
(* let doc_field (ftyp, fid) =
let reftyp =
mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
- [mk_typ_arg (Typ_arg_typ rectyp);
- mk_typ_arg (Typ_arg_typ ftyp)])) in
+ [mk_typ_arg (A_typ rectyp);
+ mk_typ_arg (A_typ ftyp)])) in
let rfannot = doc_tannot_lem empty_ctxt env false reftyp in
let get, set =
string "rec_val" ^^ dot ^^ fname fid,
@@ -1389,8 +1389,8 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in
let reftyp =
mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
- [mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname)));
- mk_typ_arg (Typ_arg_typ ftyp)])) in
+ [mk_typ_arg (A_typ (mk_id_typ (mk_id tname)));
+ mk_typ_arg (A_typ ftyp)])) in
let rfannot = doc_tannot_lem empty_ctxt Env.empty false reftyp in
doc_op equals
(concat [string "let "; parens (concat [string tname; underscore; doc_id_lem fid; rfannot])])
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7fb67a06..bae1b893 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -165,7 +165,7 @@ let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
(* Resugar set types like {|1, 2, 3|} *)
| Typ_exist ([kid1],
NC_aux (NC_set (kid2, ints), _),
- Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
+ Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
| Typ_exist (kids, nc, typ) ->
@@ -181,11 +181,11 @@ let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
| Typ_bidir (typ1, typ2) ->
separate space [doc_typ typ1; string "<->"; doc_typ typ2]
| Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
-and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
+and doc_typ_arg (A_aux (ta_aux, _)) =
match ta_aux with
- | Typ_arg_typ typ -> doc_typ typ
- | Typ_arg_nexp nexp -> doc_nexp nexp
- | Typ_arg_order o -> doc_ord o
+ | A_typ typ -> doc_typ typ
+ | A_nexp nexp -> doc_nexp nexp
+ | A_order o -> doc_ord o
and doc_arg_typs = function
| [typ] -> doc_typ typ
| typs -> parens (separate_map (comma ^^ space) doc_typ typs)
diff --git a/src/return_analysis.ml b/src/return_analysis.ml
index 06565b01..256f97cf 100644
--- a/src/return_analysis.ml
+++ b/src/return_analysis.ml
@@ -110,7 +110,7 @@ let existentialize_annot funcl_annot annot =
let funcl_env = env_of_annot funcl_annot in
let env = env_of_annot annot in
match Env.expand_synonyms env (typ_of_annot annot) with
- | (Typ_aux (Typ_app (ty_id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _) as typ)
+ | (Typ_aux (Typ_app (ty_id, [A_aux (A_nexp nexp, _)]), _) as typ)
when Id.compare ty_id (mk_id "atom") = 0 ->
let tyvars = Env.get_typ_vars funcl_env |> KBindings.bindings in
let toplevel_kids =
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 82228206..d5601d08 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -264,13 +264,13 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
| Typ_app (id, targs) ->
Typ_aux (Typ_app (id, List.map (rewrite_typ_arg env) targs), l)
| _ -> typ_aux
- and rewrite_typ_arg env (Typ_arg_aux (targ, l) as targ_aux) = match targ with
- | Typ_arg_nexp nexp ->
- Typ_arg_aux (Typ_arg_nexp (rewrite_nexp_ids env nexp), l)
- | Typ_arg_typ typ ->
- Typ_arg_aux (Typ_arg_typ (rewrite_typ env typ), l)
- | Typ_arg_order ord ->
- Typ_arg_aux (Typ_arg_order ord, l)
+ and rewrite_typ_arg env (A_aux (targ, l) as targ_aux) = match targ with
+ | A_nexp nexp ->
+ A_aux (A_nexp (rewrite_nexp_ids env nexp), l)
+ | A_typ typ ->
+ A_aux (A_typ (rewrite_typ env typ), l)
+ | A_order ord ->
+ A_aux (A_order ord, l)
in
let rewrite_annot (l, tannot) =
@@ -409,7 +409,7 @@ let rewrite_sizeof (Defs defs) =
| P_id id | P_as (_, id) ->
let (Typ_aux (typ,_) as typ_aux) = typ_of_annot annot in
(match typ with
- | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp nexp, _)])
+ | Typ_app (atom, [A_aux (A_nexp nexp, _)])
when string_of_id atom = "atom" ->
[nexp, E_id id]
| Typ_app (vector, _) when string_of_id vector = "vector" ->
@@ -470,7 +470,7 @@ let rewrite_sizeof (Defs defs) =
assert (not (Str.string_match ex_regex (string_of_kid kid) 0));
let uvar = try Some (KBindings.find (orig_kid kid) inst) with Not_found -> None in
match uvar with
- | Some (U_nexp nexp) ->
+ | Some (A_aux (A_nexp nexp, _)) ->
let sizeof = E_aux (E_sizeof nexp, (l, mk_tannot env (atom_typ nexp) no_effect)) in
(try rewrite_trivial_sizeof_exp sizeof with
| Type_error (l, err) ->
@@ -2302,8 +2302,8 @@ let rewrite_type_union_typs rw_typ (Tu_aux (Tu_ty_id (typ, id), annot)) =
let rewrite_type_def_typs rw_typ rw_typquant (TD_aux (td, annot)) =
match td with
- | TD_abbrev (id, typq, Typ_arg_aux (Typ_arg_typ typ, l)) ->
- TD_aux (TD_abbrev (id, rw_typquant typq, Typ_arg_aux (Typ_arg_typ (rw_typ typ), l)), annot)
+ | TD_abbrev (id, typq, A_aux (A_typ typ, l)) ->
+ TD_aux (TD_abbrev (id, rw_typquant typq, A_aux (A_typ (rw_typ typ), l)), annot)
| TD_record (id, nso, typq, typ_ids, flag) ->
TD_aux (TD_record (id, nso, rw_typquant typq, List.map (fun (typ, id) -> (rw_typ typ, id)) typ_ids, flag), annot)
| TD_variant (id, nso, typq, tus, flag) ->
@@ -2355,8 +2355,8 @@ let rewrite_undefined_if_gen always_bitvector defs =
let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
and simple_typ_aux = function
| Typ_id id -> Typ_id id
- | Typ_app (id, [_; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
- Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)])
+ | Typ_app (id, [_; _; A_aux (A_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
+ Typ_app (mk_id "list", [A_aux (A_typ (simple_typ typ), l)])
| Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 ->
Typ_id (mk_id "int")
| Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
@@ -2366,9 +2366,9 @@ and simple_typ_aux = function
| Typ_tup typs -> Typ_tup (List.map simple_typ typs)
| Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
| typ_aux -> typ_aux
-and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
+and simple_typ_arg (A_aux (typ_arg_aux, l)) =
match typ_arg_aux with
- | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
+ | A_typ typ -> [A_aux (A_typ (simple_typ typ), l)]
| _ -> []
(* This pass aims to remove all the Num quantifiers from the specification. *)
@@ -3010,7 +3010,7 @@ let rec binding_typs_of_pat (P_aux (p_aux, p_annot) as pat) =
let construct_toplevel_string_append_call env f_id bindings binding_typs guard expr =
(* s# if match f#(s#) { Some (bindings) => guard, _ => false) } => let Some(bindings) = f#(s#) in expr *)
let s_id = fresh_stringappend_id () in
- let option_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (match binding_typs with
+ let option_typ = app_typ (mk_id "option") [A_aux (A_typ (match binding_typs with
| [] -> unit_typ
| [typ] -> typ
| typs -> tuple_typ typs
@@ -3042,7 +3042,7 @@ let construct_toplevel_string_append_func env f_id pat =
else
bindings
in
- let option_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (match binding_typs with
+ let option_typ = app_typ (mk_id "option") [A_aux (A_typ (match binding_typs with
| [] -> unit_typ
| [typ] -> typ
| typs -> tuple_typ typs
@@ -3102,7 +3102,7 @@ let construct_toplevel_string_append_func env f_id pat =
in
let mapping_inner_typ =
match Env.get_val_spec (mk_id mapping_prefix_func) env with
- | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [Typ_arg_aux (Typ_arg_typ typ, _)]), _), _), _)) -> typ
+ | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [A_aux (A_typ typ, _)]), _), _), _)) -> typ
| _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?"
in
@@ -3119,7 +3119,7 @@ let construct_toplevel_string_append_func env f_id pat =
[annot_exp (E_id s_id) unk env string_typ]))
unk env mapping_inner_typ in
(* construct some pattern -- Some (n#, len#) *)
- let opt_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ mapping_inner_typ, unk)] in
+ let opt_typ = app_typ (mk_id "option") [A_aux (A_typ mapping_inner_typ, unk)] in
let tup_arg_pat = match arg_pats with
| [] -> assert false
| [arg_pat] -> arg_pat
@@ -3278,7 +3278,7 @@ let rec rewrite_defs_pat_string_append =
in
let mapping_inner_typ =
match Env.get_val_spec (mk_id mapping_prefix_func) env with
- | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [Typ_arg_aux (Typ_arg_typ typ, _)]), _), _), _)) -> typ
+ | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [A_aux (A_typ typ, _)]), _), _), _)) -> typ
| _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?"
in
@@ -3295,7 +3295,7 @@ let rec rewrite_defs_pat_string_append =
[annot_exp (E_id s_id) unk env string_typ]))
unk env mapping_inner_typ in
(* construct some pattern -- Some (n#, len#) *)
- let opt_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ mapping_inner_typ, unk)] in
+ let opt_typ = app_typ (mk_id "option") [A_aux (A_typ mapping_inner_typ, unk)] in
let tup_arg_pat = match arg_pats with
| [] -> assert false
| [arg_pat] -> arg_pat
@@ -3926,14 +3926,14 @@ let remove_reference_types exp =
let rec rewrite_t (Typ_aux (t_aux,a)) = (Typ_aux (rewrite_t_aux t_aux,a))
and rewrite_t_aux t_aux = match t_aux with
- | Typ_app (Id_aux (Id "reg",_), [Typ_arg_aux (Typ_arg_typ (Typ_aux (t_aux2, _)), _)]) ->
+ | Typ_app (Id_aux (Id "reg",_), [A_aux (A_typ (Typ_aux (t_aux2, _)), _)]) ->
rewrite_t_aux t_aux2
| Typ_app (name,t_args) -> Typ_app (name,List.map rewrite_t_arg t_args)
| Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map rewrite_t arg_typs, rewrite_t ret_typ, eff)
| Typ_tup ts -> Typ_tup (List.map rewrite_t ts)
| _ -> t_aux
and rewrite_t_arg t_arg = match t_arg with
- | Typ_arg_aux (Typ_arg_typ t, a) -> Typ_arg_aux (Typ_arg_typ (rewrite_t t), a)
+ | A_aux (A_typ t, a) -> A_aux (A_typ (rewrite_t t), a)
| _ -> t_arg in
let rec rewrite_annot (l, tannot) =
@@ -4329,7 +4329,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
let prefix_wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_exp (E_lit (mk_lit L_unit))])))) in
let string_defs =
begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
- let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+ let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
@@ -4339,7 +4339,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
forwards_prefix_spec @ forwards_prefix_fun
else
if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
- let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+ let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 84fa8235..2ab64f1c 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -101,7 +101,7 @@ and free_type_names_maybe_t consider_var = function
| Some t -> free_type_names_t consider_var t
| None -> mt
and free_type_names_t_arg consider_var = function
- | Typ_arg_aux (Typ_arg_typ t, _) -> free_type_names_t consider_var t
+ | A_aux (A_typ t, _) -> free_type_names_t consider_var t
| _ -> mt
and free_type_names_t_args consider_var targs =
nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs)
@@ -129,9 +129,9 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
| Typ_exist (kids,_,t') -> fv_of_typ consider_var (List.fold_left (fun b (Kid_aux (Var v,_)) -> Nameset.add v b) bound kids) used t'
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with
- | Typ_arg_typ t -> fv_of_typ consider_var bound used t
- | Typ_arg_nexp n -> fv_of_nexp consider_var bound used n
+and fv_of_targ consider_var bound used (Ast.A_aux(targ,_)) : Nameset.t = match targ with
+ | A_typ t -> fv_of_typ consider_var bound used t
+ | A_nexp n -> fv_of_nexp consider_var bound used n
| _ -> used
and fv_of_nexp consider_var bound used (Ast.Nexp_aux(n,_)) = match n with
@@ -309,7 +309,7 @@ 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_type_def consider_var (TD_aux(t,_)) = match t with
- | TD_abbrev(id,typq,Typ_arg_aux(Typ_arg_typ typ, l)) ->
+ | 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_record(id,_,typq,tids,_) ->
diff --git a/src/specialize.ml b/src/specialize.ml
index 6e625176..0f5b939c 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -54,8 +54,8 @@ open Rewriter
open Extra_pervasives
let is_typ_ord_uvar = function
- | Type_check.U_typ _ -> true
- | Type_check.U_order _ -> true
+ | A_aux (A_nexp _, _) -> true
+ | A_aux (A_order _, _) -> true
| _ -> false
let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
@@ -71,24 +71,20 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
in
Typ_aux (typ_aux, l)
-and nexp_simp_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
+and nexp_simp_typ_arg (A_aux (typ_arg_aux, l)) =
let typ_arg_aux = match typ_arg_aux with
- | Typ_arg_nexp n -> Typ_arg_nexp (nexp_simp n)
- | Typ_arg_typ typ -> Typ_arg_typ (nexp_simp_typ typ)
- | Typ_arg_order ord -> Typ_arg_order ord
+ | A_nexp n -> A_nexp (nexp_simp n)
+ | A_typ typ -> A_typ (nexp_simp_typ typ)
+ | A_order ord -> A_order ord
+ | A_bool nc -> A_bool (constraint_simp nc)
in
- Typ_arg_aux (typ_arg_aux, l)
-
-let nexp_simp_uvar = function
- | Type_check.U_nexp nexp -> (prerr_endline ("Simp nexp " ^ string_of_nexp nexp); Type_check.U_nexp (nexp_simp nexp))
- | Type_check.U_typ typ -> Type_check.U_typ (nexp_simp_typ typ)
- | uvar -> uvar
+ A_aux (typ_arg_aux, l)
(* We have to be careful about whether the typechecker has renamed anything returned by instantiation_of.
This part of the typechecker API is a bit ugly. *)
let fix_instantiation instantiation =
- let instantiation = KBindings.bindings (KBindings.filter (fun _ uvar -> is_typ_ord_uvar uvar) instantiation) in
- let instantiation = List.map (fun (kid, uvar) -> Type_check.orig_kid kid, nexp_simp_uvar uvar) instantiation in
+ let instantiation = KBindings.bindings (KBindings.filter (fun _ arg -> is_typ_ord_uvar arg) instantiation) in
+ let instantiation = List.map (fun (kid, arg) -> Type_check.orig_kid kid, nexp_simp_typ_arg arg) instantiation in
List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty instantiation
let rec polymorphic_functions is_kopt (Defs defs) =
@@ -146,11 +142,12 @@ let string_of_instantiation instantiation =
"exist " ^ Util.string_of_list " " kid_name kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ
| Typ_internal_unknown -> "UNKNOWN"
and string_of_typ_arg = function
- | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
+ | A_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
and string_of_typ_arg_aux = function
- | Typ_arg_nexp n -> string_of_nexp n
- | Typ_arg_typ typ -> string_of_typ typ
- | Typ_arg_order o -> string_of_order o
+ | A_nexp n -> string_of_nexp n
+ | A_typ typ -> string_of_typ typ
+ | A_order o -> string_of_order o
+ | A_bool nc -> string_of_n_constraint nc
and string_of_n_constraint = function
| NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
| NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
@@ -166,13 +163,7 @@ let string_of_instantiation instantiation =
| NC_aux (NC_false, _) -> "false"
in
- let string_of_uvar = function
- | U_nexp n -> string_of_nexp n
- | U_order o -> string_of_order o
- | U_typ typ -> string_of_typ typ
- in
-
- let string_of_binding (kid, uvar) = string_of_kid kid ^ " => " ^ string_of_uvar uvar in
+ let string_of_binding (kid, arg) = string_of_kid kid ^ " => " ^ string_of_typ_arg arg in
Util.zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation))
let id_of_instantiation id instantiation =
@@ -182,7 +173,7 @@ let id_of_instantiation id instantiation =
let rec variant_generic_typ id (Defs defs) =
match defs with
| DEF_type (TD_aux (TD_variant (id', _, typq, _, _), _)) :: _ when Id.compare id id' = 0 ->
- mk_typ (Typ_app (id', List.map (fun kopt -> mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt))))) (quant_kopts typq)))
+ mk_typ (Typ_app (id', List.map (fun kopt -> mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))) (quant_kopts typq)))
| _ :: defs -> variant_generic_typ id (Defs defs)
| [] -> failwith ("No variant with id " ^ string_of_id id)
@@ -207,9 +198,10 @@ let rec instantiations_of id ast =
begin match Type_check.typ_of_annot annot with
| Typ_aux (Typ_app (variant_id, _), _) as typ ->
let open Type_check in
- let instantiation, _, _ = unify (fst annot) (env_of_annot annot)
- (variant_generic_typ variant_id ast)
- typ
+ let instantiation = unify (fst annot) (env_of_annot annot)
+ (tyvars_of_typ (variant_generic_typ variant_id ast))
+ (variant_generic_typ variant_id ast)
+ typ
in
instantiations := fix_instantiation instantiation :: !instantiations;
pat
@@ -262,11 +254,11 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
| Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
+and typ_arg_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
match typ_arg_aux with
- | Typ_arg_nexp n -> KidSet.empty
- | Typ_arg_typ typ -> typ_frees ~exs:exs typ
- | Typ_arg_order ord -> KidSet.empty
+ | A_nexp n -> KidSet.empty
+ | A_typ typ -> typ_frees ~exs:exs typ
+ | A_order ord -> KidSet.empty
let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
match typ_aux with
@@ -279,20 +271,11 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
List.fold_left KidSet.union (typ_int_frees ~exs:exs ret_typ) (List.map (typ_int_frees ~exs:exs) arg_typs)
| Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and typ_arg_int_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
+and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
match typ_arg_aux with
- | Typ_arg_nexp n -> KidSet.diff (tyvars_of_nexp n) exs
- | Typ_arg_typ typ -> KidSet.empty
- | Typ_arg_order ord -> KidSet.empty
-
-let uvar_int_frees = function
- | Type_check.U_nexp n -> tyvars_of_nexp n
- | Type_check.U_typ typ -> typ_int_frees typ
- | _ -> KidSet.empty
-
-let uvar_typ_frees = function
- | Type_check.U_typ typ -> typ_frees typ
- | _ -> KidSet.empty
+ | A_nexp n -> KidSet.diff (tyvars_of_nexp n) exs
+ | A_typ typ -> typ_int_frees ~exs:exs typ
+ | A_order ord -> KidSet.empty
let specialize_id_valspec instantiations id ast =
match split_defs (is_valspec id) ast with
@@ -313,8 +296,8 @@ let specialize_id_valspec instantiations id ast =
(* Collect any new type variables introduced by the instantiation *)
let collect_kids kidsets = KidSet.elements (List.fold_left KidSet.union KidSet.empty kidsets) in
- let typ_frees = KBindings.bindings instantiation |> List.map snd |> List.map uvar_typ_frees |> collect_kids in
- let int_frees = KBindings.bindings instantiation |> List.map snd |> List.map uvar_int_frees |> collect_kids in
+ let typ_frees = KBindings.bindings instantiation |> List.map snd |> List.map typ_arg_frees |> collect_kids in
+ let int_frees = KBindings.bindings instantiation |> List.map snd |> List.map typ_arg_int_frees |> collect_kids in
(* Remove type variables from the type quantifier. *)
let kopts, constraints = quant_split typq in
diff --git a/src/specialize.mli b/src/specialize.mli
index 87533e9b..f2c94a48 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -68,6 +68,6 @@ val polymorphic_functions : (kinded_id -> bool) -> 'a defs -> IdSet.t
which case specialize returns the AST unmodified. *)
val specialize : tannot defs -> Env.t -> tannot defs * Env.t
-val instantiations_of : id -> tannot defs -> uvar KBindings.t list
+val instantiations_of : id -> tannot defs -> typ_arg KBindings.t list
-val string_of_instantiation : uvar KBindings.t -> string
+val string_of_instantiation : typ_arg KBindings.t -> string
diff --git a/src/state.ml b/src/state.ml
index 00f81bf4..4fc2e1e8 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -102,12 +102,12 @@ let generate_initial_regstate defs =
if string_of_id id = "unit" then "()" else
Bindings.find id vals []
| Typ_app (id, _) when string_of_id id = "list" -> "[||]"
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" ->
+ | Typ_app (id, [A_aux (A_nexp nexp, _)]) when string_of_id id = "atom" ->
string_of_nexp nexp
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" ->
+ | Typ_app (id, [A_aux (A_nexp nexp, _); _]) when string_of_id id = "range" ->
string_of_nexp nexp
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ;
- Typ_arg_aux (Typ_arg_typ etyp, _)])
+ | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ;
+ A_aux (A_typ etyp, _)])
when string_of_id id = "vector" ->
(* Output a list of initial values of the vector elements, or a
literal binary zero value if this is a bitvector and the
@@ -146,7 +146,7 @@ let generate_initial_regstate defs =
string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")"
in
Bindings.add id init_val vals
- | TD_abbrev (id, tq, Typ_arg_aux (Typ_arg_typ typ, _)) ->
+ | TD_abbrev (id, tq, A_aux (A_typ typ, _)) ->
let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in
Bindings.add id init_val vals
| TD_record (id, _, tq, fields, _) ->
@@ -174,12 +174,12 @@ let generate_initial_regstate defs =
let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with
| Typ_id id -> id
| Typ_app (id, args) ->
- let name_arg (Typ_arg_aux (targ, _)) = match targ with
- | Typ_arg_typ targ -> string_of_id (regval_constr_id mwords targ)
- | Typ_arg_nexp nexp when is_nexp_constant (nexp_simp nexp) ->
+ let name_arg (A_aux (targ, _)) = match targ with
+ | A_typ targ -> string_of_id (regval_constr_id mwords targ)
+ | A_nexp nexp when is_nexp_constant (nexp_simp nexp) ->
string_of_nexp (nexp_simp nexp)
- | Typ_arg_order (Ord_aux (Ord_inc, _)) -> "inc"
- | Typ_arg_order (Ord_aux (Ord_dec, _)) -> "dec"
+ | A_order (Ord_aux (Ord_inc, _)) -> "inc"
+ | A_order (Ord_aux (Ord_dec, _)) -> "dec"
| _ ->
raise (Reporting.err_typ l "Unsupported register type")
in
@@ -194,9 +194,9 @@ let register_base_types mwords typs =
match t with
| Typ_app (id, args)
when IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) ->
- let add_typ_arg base_typs (Typ_arg_aux (targ, _)) =
+ let add_typ_arg base_typs (A_aux (targ, _)) =
match targ with
- | Typ_arg_typ typ -> add_base_typs typs typ
+ | A_typ typ -> add_base_typs typs typ
| _ -> typs
in
List.fold_left add_typ_arg typs args
@@ -243,12 +243,12 @@ let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
let etyp_of, of_etyp = regval_convs_lem mwords etyp in
"(fun v -> vector_of_regval " ^ etyp_of ^ " v)",
"(fun v -> regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)"
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+ | Typ_app (id, [A_aux (A_typ etyp, _)])
when string_of_id id = "list" ->
let etyp_of, of_etyp = regval_convs_lem mwords etyp in
"(fun v -> list_of_regval " ^ etyp_of ^ " v)",
"(fun v -> regval_of_list " ^ of_etyp ^ " v)"
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+ | Typ_app (id, [A_aux (A_typ etyp, _)])
when string_of_id id = "option" ->
let etyp_of, of_etyp = regval_convs_lem mwords etyp in
"(fun v -> option_of_regval " ^ etyp_of ^ " v)",
@@ -407,12 +407,12 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
let etyp_of, of_etyp = regval_convs_coq etyp in
"(fun v => vector_of_regval " ^ size ^ " " ^ etyp_of ^ " v)",
"(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)"
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+ | Typ_app (id, [A_aux (A_typ etyp, _)])
when string_of_id id = "list" ->
let etyp_of, of_etyp = regval_convs_coq etyp in
"(fun v => list_of_regval " ^ etyp_of ^ " v)",
"(fun v => regval_of_list " ^ of_etyp ^ " v)"
- | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+ | Typ_app (id, [A_aux (A_typ etyp, _)])
when string_of_id id = "option" ->
let etyp_of, of_etyp = regval_convs_coq etyp in
"(fun v => option_of_regval " ^ etyp_of ^ " v)",
diff --git a/src/type_check.ml b/src/type_check.ml
index 2c10b8ae..42616361 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -96,6 +96,7 @@ type type_error =
| Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
| Err_no_num_ident of id
| Err_other of string
+ | Err_because of type_error * type_error
exception Type_error of l * type_error;;
@@ -125,7 +126,7 @@ let orig_kid (Kid_aux (Var v, l) as kid) =
let is_list (Typ_aux (typ_aux, _)) =
match typ_aux with
- | Typ_app (f, [Typ_arg_aux (Typ_arg_typ typ, _)])
+ | Typ_app (f, [A_aux (A_typ typ, _)])
when string_of_id f = "list" -> Some typ
| _ -> None
@@ -174,12 +175,12 @@ and strip_n_constraint_aux = function
and strip_n_constraint = function
| NC_aux (nc_aux, _) -> NC_aux (strip_n_constraint_aux nc_aux, Parse_ast.Unknown)
and strip_typ_arg = function
- | Typ_arg_aux (typ_arg_aux, _) -> Typ_arg_aux (strip_typ_arg_aux typ_arg_aux, Parse_ast.Unknown)
+ | A_aux (typ_arg_aux, _) -> A_aux (strip_typ_arg_aux typ_arg_aux, Parse_ast.Unknown)
and strip_typ_arg_aux = function
- | Typ_arg_nexp nexp -> Typ_arg_nexp (strip_nexp nexp)
- | Typ_arg_typ typ -> Typ_arg_typ (strip_typ typ)
- | Typ_arg_order ord -> Typ_arg_order (strip_order ord)
- | Typ_arg_bool nc -> Typ_arg_bool (strip_n_constraint nc)
+ | A_nexp nexp -> A_nexp (strip_nexp nexp)
+ | A_typ typ -> A_typ (strip_typ typ)
+ | A_order ord -> A_order (strip_order ord)
+ | A_bool nc -> A_bool (strip_n_constraint nc)
and strip_order = function
| Ord_aux (ord_aux, _) -> Ord_aux (strip_order_aux ord_aux, Parse_ast.Unknown)
and strip_order_aux = function
@@ -466,14 +467,14 @@ end = struct
let kopts, ncs = quant_split typq in
let rec subst_args kopts args =
match kopts, args with
- | kopt :: kopts, (Typ_arg_aux (Typ_arg_nexp _, _) as arg) :: args when is_nat_kopt kopt ->
+ | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_nat_kopt kopt ->
List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args)
- | kopt :: kopts, Typ_arg_aux (Typ_arg_typ arg, _) :: args when is_typ_kopt kopt ->
+ | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
subst_args kopts args
- | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt ->
+ | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
subst_args kopts args
| [], [] -> ncs
- | _, Typ_arg_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
+ | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
| _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
in
let ncs = subst_args kopts args in
@@ -488,7 +489,7 @@ end = struct
| NC_app (id, args) ->
(try
begin match Bindings.find id env.typ_synonyms env args with
- | Typ_arg_aux (Typ_arg_bool nc, _) -> expand_constraint_synonyms env nc
+ | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc
| _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
end
with Not_found -> NC_aux (NC_app (id, List.map (expand_synonyms_arg env) args), l))
@@ -503,7 +504,7 @@ end = struct
| Typ_app (id, args) ->
(try
begin match Bindings.find id env.typ_synonyms env args with
- | Typ_arg_aux (Typ_arg_typ typ, _) -> expand_synonyms env typ
+ | A_aux (A_typ typ, _) -> expand_synonyms env typ
| _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
end
with
@@ -511,7 +512,7 @@ end = struct
| Typ_id id ->
(try
begin match Bindings.find id env.typ_synonyms env [] with
- | Typ_arg_aux (Typ_arg_typ typ, _) -> expand_synonyms env typ
+ | A_aux (A_typ typ, _) -> expand_synonyms env typ
| _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
end
with
@@ -544,11 +545,11 @@ end = struct
let env = { env with constraints = nc :: env.constraints } in
Typ_aux (Typ_exist (kids, nc, expand_synonyms env typ), l)
| Typ_var v -> Typ_aux (Typ_var v, l)
- and expand_synonyms_arg env (Typ_arg_aux (typ_arg, l)) =
+ and expand_synonyms_arg env (A_aux (typ_arg, l)) =
match typ_arg with
- | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (expand_synonyms env typ), l)
- | Typ_arg_bool nc -> Typ_arg_aux (Typ_arg_bool (expand_constraint_synonyms env nc), l)
- | arg -> Typ_arg_aux (arg, l)
+ | A_typ typ -> A_aux (A_typ (expand_synonyms env typ), l)
+ | A_bool nc -> A_aux (A_bool (expand_constraint_synonyms env nc), l)
+ | arg -> A_aux (arg, l)
(** Map over all nexps in a type - excluding those in existential constraints **)
let rec map_nexps f (Typ_aux (typ_aux, l) as typ) =
@@ -560,10 +561,10 @@ end = struct
| Typ_tup typs -> Typ_aux (Typ_tup (List.map (map_nexps f) typs), l)
| Typ_exist (kids, nc, typ) -> Typ_aux (Typ_exist (kids, nc, map_nexps f typ), l)
| Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map (map_nexps_arg f) args), l)
- and map_nexps_arg f (Typ_arg_aux (arg_aux, l) as arg) =
+ and map_nexps_arg f (A_aux (arg_aux, l) as arg) =
match arg_aux with
- | Typ_arg_order _ | Typ_arg_typ _ | Typ_arg_bool _ -> arg
- | Typ_arg_nexp n -> Typ_arg_aux (Typ_arg_nexp (f n), l)
+ | A_order _ | A_typ _ | A_bool _ -> arg
+ | A_nexp n -> A_aux (A_nexp (f n), l)
let canonical env typ =
let typ = expand_synonyms env typ in
@@ -646,12 +647,12 @@ end = struct
wf_typ ~exs:(KidSet.of_list kids) { env with constraints = nc :: env.constraints } typ
| Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed")
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
- and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) =
+ and wf_typ_arg ?exs:(exs=KidSet.empty) env (A_aux (typ_arg_aux, _)) =
match typ_arg_aux with
- | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp
- | Typ_arg_typ typ -> wf_typ ~exs:exs env typ
- | Typ_arg_order ord -> wf_order env ord
- | Typ_arg_bool nc -> wf_constraint ~exs:exs env nc
+ | A_nexp nexp -> wf_nexp ~exs:exs env nexp
+ | A_typ typ -> wf_typ ~exs:exs env typ
+ | A_order ord -> wf_order env ord
+ | A_bool nc -> wf_constraint ~exs:exs env nc
and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
match nexp_aux with
| Nexp_id _ -> ()
@@ -820,10 +821,10 @@ end = struct
in
let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in
begin if strip_typ typ1 = string_typ then
- let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+ let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
add_val_spec prefix_id (typq, forwards_prefix_typ) env
else if strip_typ typ2 = string_typ then
- let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+ let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
add_val_spec prefix_id (typq, backwards_prefix_typ) env
else
env
@@ -882,11 +883,11 @@ end = struct
let rec record_typ_args = function
| [] -> []
| ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt ->
- mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis
+ mk_typ_arg (A_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis
| ((QI_aux (QI_id kopt, _)) :: qis) when is_typ_kopt kopt ->
- mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis
+ mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis
| ((QI_aux (QI_id kopt, _)) :: qis) when is_order_kopt kopt ->
- mk_typ_arg (Typ_arg_order (mk_ord (Ord_var (kopt_kid kopt)))) :: record_typ_args qis
+ mk_typ_arg (A_order (mk_ord (Ord_var (kopt_kid kopt)))) :: record_typ_args qis
| (_ :: qis) -> record_typ_args qis
in
let rectyp = match record_typ_args (quant_items typq) with
@@ -1109,15 +1110,15 @@ end = struct
rewrap (Typ_fn (List.map aux arg_typs, aux ret_typ, eff))
| Typ_tup ts ->
rewrap (Typ_tup (List.map aux ts))
- | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) when string_of_id r = "register" ->
+ | Typ_app (r, [A_aux (A_typ rtyp,_)]) when string_of_id r = "register" ->
aux rtyp
| Typ_app (id, targs) ->
rewrap (Typ_app (id, List.map aux_arg targs))
| t -> rewrap t
- and aux_arg (Typ_arg_aux (targ,a)) =
- let rewrap targ = Typ_arg_aux (targ,a) in
+ and aux_arg (A_aux (targ,a)) =
+ let rewrap targ = A_aux (targ,a) in
match targ with
- | Typ_arg_typ typ -> rewrap (Typ_arg_typ (aux typ))
+ | A_typ typ -> rewrap (A_typ (aux typ))
| targ -> rewrap targ in
aux (expand_synonyms env typ)
@@ -1195,11 +1196,11 @@ let exist_typ constr typ =
let destruct_numeric env typ =
let typ = Env.expand_synonyms env typ in
match destruct_exist env typ, typ with
- | Some (kids, nc, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _)), _ when string_of_id id = "atom" ->
+ | Some (kids, nc, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _)), _ when string_of_id id = "atom" ->
Some (kids, nc, nexp)
- | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _) when string_of_id id = "atom" ->
+ | None, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _) when string_of_id id = "atom" ->
Some ([], nc_true, nexp)
- | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) when string_of_id id = "range" ->
+ | None, Typ_aux (Typ_app (id, [A_aux (A_nexp lo, _); A_aux (A_nexp hi, _)]), _) when string_of_id id = "range" ->
let kid = fresh_existential () in
Some ([kid], nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi), nvar kid)
| None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" ->
@@ -1230,17 +1231,17 @@ let destruct_range env typ =
Util.option_default ([], nc_true, typ) (destruct_exist env typ)
in
match typ_aux with
- | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
+ | Typ_app (f, [A_aux (A_nexp n, _)])
when string_of_id f = "atom" -> Some (kids, constr, n, n)
- | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)])
+ | Typ_app (f, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)])
when string_of_id f = "range" -> Some (kids, constr, n1, n2)
| _ -> None
let destruct_vector env typ =
let destruct_vector' = function
- | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
- Typ_arg_aux (Typ_arg_order o, _);
- Typ_arg_aux (Typ_arg_typ vtyp, _)]
+ | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
+ A_aux (A_order o, _);
+ A_aux (A_typ vtyp, _)]
), _) when string_of_id id = "vector" -> Some (nexp_simp n1, o, vtyp)
| typ -> None
in
@@ -1255,12 +1256,12 @@ let rec is_typ_monomorphic (Typ_aux (typ, l)) =
| Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
| Typ_exist _ | Typ_var _ -> false
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and is_typ_arg_monomorphic (Typ_arg_aux (arg, _)) =
+and is_typ_arg_monomorphic (A_aux (arg, _)) =
match arg with
- | Typ_arg_nexp _ -> true
- | Typ_arg_typ typ -> is_typ_monomorphic typ
- | Typ_arg_order (Ord_aux (Ord_dec, _)) | Typ_arg_order (Ord_aux (Ord_inc, _)) -> true
- | Typ_arg_order (Ord_aux (Ord_var _, _)) -> false
+ | A_nexp _ -> true
+ | A_typ typ -> is_typ_monomorphic typ
+ | A_order (Ord_aux (Ord_dec, _)) | A_order (Ord_aux (Ord_inc, _)) -> true
+ | A_order (Ord_aux (Ord_var _, _)) -> false
(**************************************************************************)
(* 2. Subtyping and constraint solving *)
@@ -1373,11 +1374,11 @@ let rec typ_nexps (Typ_aux (typ_aux, l)) =
List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
| Typ_bidir (typ1, typ2) ->
typ_nexps typ1 @ typ_nexps typ2
-and typ_arg_nexps (Typ_arg_aux (typ_arg_aux, l)) =
+and typ_arg_nexps (A_aux (typ_arg_aux, l)) =
match typ_arg_aux with
- | Typ_arg_nexp n -> [n]
- | Typ_arg_typ typ -> typ_nexps typ
- | Typ_arg_order ord -> []
+ | A_nexp n -> [n]
+ | A_typ typ -> typ_nexps typ
+ | A_order ord -> []
let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
match typ_aux with
@@ -1390,11 +1391,11 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
| Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
| Typ_fn (arg_typs, ret_typ, _) -> List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
| Typ_bidir (typ1, typ2) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
-and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
+and typ_arg_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
match typ_arg_aux with
- | Typ_arg_nexp n -> nexp_frees ~exs:exs n
- | Typ_arg_typ typ -> typ_frees ~exs:exs typ
- | Typ_arg_order ord -> order_frees ord
+ | A_nexp n -> nexp_frees ~exs:exs n
+ | A_typ typ -> typ_frees ~exs:exs typ
+ | A_order ord -> order_frees ord
let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
match nexp1, nexp2 with
@@ -1457,11 +1458,11 @@ let typ_identical env typ1 typ2 =
| Typ_exist (kids1, nc1, typ1), Typ_exist (kids2, nc2, typ2) when List.length kids1 = List.length kids2 ->
List.for_all2 (fun k1 k2 -> Kid.compare k1 k2 = 0) kids1 kids2 && nc_identical nc1 nc2 && typ_identical' typ1 typ2
| _, _ -> false
- and typ_arg_identical (Typ_arg_aux (arg1, _)) (Typ_arg_aux (arg2, _)) =
+ and typ_arg_identical (A_aux (arg1, _)) (A_aux (arg2, _)) =
match arg1, arg2 with
- | Typ_arg_nexp n1, Typ_arg_nexp n2 -> nexp_identical n1 n2
- | Typ_arg_typ typ1, Typ_arg_typ typ2 -> typ_identical' typ1 typ2
- | Typ_arg_order ord1, Typ_arg_order ord2 -> ord_identical ord1 ord2
+ | A_nexp n1, A_nexp n2 -> nexp_identical n1 n2
+ | A_typ typ1, A_typ typ2 -> typ_identical' typ1 typ2
+ | A_order ord1, A_order ord2 -> ord_identical ord1 ord2
| _, _ -> false
in
typ_identical' (Env.expand_synonyms env typ1) (Env.expand_synonyms env typ2)
@@ -1472,7 +1473,7 @@ let unify_error l str = raise (Unification_error (l, str))
let merge_unifiers l kid uvar1 uvar2 =
match uvar1, uvar2 with
- | Some (Typ_arg_aux (Typ_arg_nexp n1, _)), Some (Typ_arg_aux (Typ_arg_nexp n2, _)) ->
+ | Some (A_aux (A_nexp n1, _)), Some (A_aux (A_nexp n2, _)) ->
if nexp_identical n1 n2 then
Some (arg_nexp n1)
else
@@ -1488,16 +1489,22 @@ let merge_uvars l unifiers1 unifiers2 =
let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as typ2) =
match aux1, aux2 with
+ | Typ_internal_unknown, _ | _, Typ_internal_unknown
+ when Env.allow_unknowns env ->
+ KBindings.empty
+
| Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2)
- | Typ_app (range, [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]),
- Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp m, _)])
+ | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]),
+ Typ_app (atom, [A_aux (A_nexp m, _)])
when string_of_id range = "range" && string_of_id atom = "atom" ->
merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m)
| Typ_app (id1, args1), Typ_app (id2, args2) when List.length args1 = List.length args2 && Id.compare id1 id2 = 0 ->
List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2)
+ | Typ_app (id1, []), Typ_id id2 when Id.compare id1 id2 = 0 -> KBindings.empty
+ | Typ_id id1, Typ_app (id2, []) when Id.compare id1 id2 = 0 -> KBindings.empty
| Typ_id id1, Typ_id id2 when Id.compare id1 id2 = 0 -> KBindings.empty
| Typ_tup typs1, Typ_tup typs2 when List.length typs1 = List.length typs2 ->
@@ -1505,11 +1512,11 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as
| _, _ -> unify_error l ("Cound not unify " ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2)
-and unify_typ_arg l env goals (Typ_arg_aux (aux1, _) as typ_arg1) (Typ_arg_aux (aux2, _) as typ_arg2) =
+and unify_typ_arg l env goals (A_aux (aux1, _) as typ_arg1) (A_aux (aux2, _) as typ_arg2) =
match aux1, aux2 with
- | Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l env goals typ1 typ2
- | Typ_arg_nexp nexp1, Typ_arg_nexp nexp2 -> unify_nexp l env goals nexp1 nexp2
- | Typ_arg_order ord1, Typ_arg_order ord2 -> unify_order l goals ord1 ord2
+ | A_typ typ1, A_typ typ2 -> unify_typ l env goals typ1 typ2
+ | A_nexp nexp1, A_nexp nexp2 -> unify_nexp l env goals nexp1 nexp2
+ | A_order ord1, A_order ord2 -> unify_order l goals ord1 ord2
| _, _ -> unify_error l ("Could not unify type arguments " ^ string_of_typ_arg typ_arg1 ^ " and " ^ string_of_typ_arg typ_arg2)
and unify_order l goals (Ord_aux (aux1, _) as ord1) (Ord_aux (aux2, _) as ord2) =
@@ -1589,14 +1596,22 @@ and unify_nexp l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_au
else unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
| _ -> unify_error l ("Cannot unify Int expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
-let unify l env typ1 typ2 goals =
- typ_print (lazy (Util.("Unify " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2));
+let unify l env goals typ1 typ2 =
+ typ_print (lazy (Util.("Unify " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2
+ ^ " for " ^ Util.string_of_list ", " string_of_kid (KidSet.elements goals)));
let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in
- unify_typ l env goals typ1 typ2
+ if not (KidSet.is_empty (KidSet.inter goals (tyvars_of_typ typ2))) then
+ typ_error l ("Occurs check failed: " ^ string_of_typ typ2 ^ " contains "
+ ^ Util.string_of_list ", " string_of_kid (KidSet.elements goals))
+ else
+ unify_typ l env goals typ1 typ2
let subst_unifiers unifiers typ =
List.fold_left (fun typ (v, arg) -> typ_subst v arg typ) typ (KBindings.bindings unifiers)
+let subst_unifiers_typ_arg unifiers typ_arg =
+ List.fold_left (fun typ_arg (v, arg) -> typ_arg_subst v arg typ_arg) typ_arg (KBindings.bindings unifiers)
+
let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) =
match aux with
| QI_id kopt when Kid.compare (kopt_kid kopt) v = 0 ->
@@ -1614,18 +1629,18 @@ let instantiate_quants quants unifier =
let destruct_atom_nexp env typ =
match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
+ | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _)]), _)
when string_of_id f = "atom" -> Some n
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp m, _)]), _)
+ | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _); A_aux (A_nexp m, _)]), _)
when string_of_id f = "range" && nexp_identical n m -> Some n
| _ -> None
let destruct_atom_kid env typ =
match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, _)), _)]), _)
+ | Typ_aux (Typ_app (f, [A_aux (A_nexp (Nexp_aux (Nexp_var kid, _)), _)]), _)
when string_of_id f = "atom" -> Some kid
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid1, _)), _);
- Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _)
+ | Typ_aux (Typ_app (f, [A_aux (A_nexp (Nexp_aux (Nexp_var kid1, _)), _);
+ A_aux (A_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _)
when string_of_id f = "range" && Kid.compare kid1 kid2 = 0 -> Some kid1
| _ -> None
@@ -1657,11 +1672,11 @@ let rec kid_order kids (Typ_aux (aux, l) as typ) =
List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kids) args
| Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and kid_order_arg kids (Typ_arg_aux (aux, l) as arg) =
+and kid_order_arg kids (A_aux (aux, l) as arg) =
match aux with
- | Typ_arg_typ typ -> kid_order kids typ
- | Typ_arg_nexp nexp -> kid_order_nexp kids nexp
- | Typ_arg_order _ -> ([], kids)
+ | A_typ typ -> kid_order kids typ
+ | A_nexp nexp -> kid_order_nexp kids nexp
+ | A_order _ -> ([], kids)
let rec alpha_equivalent env typ1 typ2 =
let counter = ref 0 in
@@ -1686,10 +1701,10 @@ let rec alpha_equivalent env typ1 typ2 =
Typ_app (id, List.map relabel_arg args)
in
Typ_aux (relabelled_aux, l)
- and relabel_arg (Typ_arg_aux (aux, l) as arg) =
+ and relabel_arg (A_aux (aux, l) as arg) =
match aux with
- | Typ_arg_nexp _ | Typ_arg_order _ -> arg
- | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (relabel typ), l)
+ | A_nexp _ | A_order _ -> arg
+ | A_typ typ -> A_aux (A_typ (relabel typ), l)
in
let typ1 = relabel (Env.expand_synonyms env typ1) in
@@ -1707,7 +1722,7 @@ let unwrap_exist env typ =
let unifier_constraint env (v, arg) =
match arg with
- | Typ_arg_aux (Typ_arg_nexp nexp, _) -> Env.add_constraint (nc_eq (nvar v) nexp) env
+ | A_aux (A_nexp nexp, _) -> Env.add_constraint (nc_eq (nvar v) nexp) env
| _ -> env
let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as typ2) =
@@ -1742,7 +1757,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in
if not (kids' = []) then typ_error l "Universally quantified constraint generated" else ();
let unifiers =
- try unify l env typ2 typ1 (KidSet.of_list kids) with
+ try unify l env (tyvars_of_typ typ2) typ2 typ1 with
| Unification_error (_, m) -> typ_error l m
in
let nc = List.fold_left (fun nc (kid, uvar) -> constraint_subst kid uvar nc) nc (KBindings.bindings unifiers) in
@@ -1860,9 +1875,9 @@ in inst_from_eq
let destruct_vec_typ l env typ =
let destruct_vec_typ' l = function
- | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
- Typ_arg_aux (Typ_arg_order o, _);
- Typ_arg_aux (Typ_arg_typ vtyp, _)]
+ | Typ_aux (Typ_app (id, [A_aux (A_nexp n1, _);
+ A_aux (A_order o, _);
+ A_aux (A_typ vtyp, _)]
), _) when string_of_id id = "vector" -> (n1, o, vtyp)
| typ -> typ_error l ("Expected vector type, got " ^ string_of_typ typ)
in
@@ -1927,10 +1942,10 @@ let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with
let destruct_atom (Typ_aux (typ_aux, _)) =
match typ_aux with
- | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp, _)])
+ | Typ_app (f, [A_aux (A_nexp nexp, _)])
when string_of_id f = "atom" ->
Util.option_map (fun c -> (c, nexp)) (big_int_of_nexp nexp)
- | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp nexp1, _); Typ_arg_aux (Typ_arg_nexp nexp2, _)])
+ | Typ_app (f, [A_aux (A_nexp nexp1, _); A_aux (A_nexp nexp2, _)])
when string_of_id f = "range" ->
begin
match big_int_of_nexp nexp1, big_int_of_nexp nexp2 with
@@ -2152,7 +2167,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
in
let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env rectyp_q typ (tyvars_of_typ rectyp_q) with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let checked_exp = crule check_exp env exp field_typ' in
FE_aux (FE_Fexp (field, checked_exp), (l, None))
@@ -2167,7 +2182,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
in
let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env rectyp_q typ (tyvars_of_typ rectyp_q) with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let checked_exp = crule check_exp env exp field_typ' in
FE_aux (FE_Fexp (field, checked_exp), (l, None))
@@ -2411,7 +2426,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
try
let inferred_cast = irule infer_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) in
let ityp, env = bind_existential l (typ_of inferred_cast) env in
- inferred_cast, unify l env typ ityp goals, env
+ inferred_cast, unify l env goals typ ityp, env
with
| Type_error (_, err) -> try_casts casts
| Unification_error (_, err) -> try_casts casts
@@ -2421,7 +2436,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
try
typ_debug (lazy "PERFORMING COERCING UNIFICATION");
let atyp, env = bind_existential l (typ_of annotated_exp) env in
- annotated_exp, unify l env typ atyp goals, env
+ annotated_exp, unify l env goals typ atyp, env
with
| Unification_error (_, m) when Env.allow_casts env ->
let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
@@ -2475,7 +2490,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| P_cons (hd_pat, tl_pat) ->
begin
match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
+ | Typ_aux (Typ_app (f, [A_aux (A_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
let hd_pat, env, hd_guards = bind_pat env hd_pat ltyp in
let tl_pat, env, tl_guards = bind_pat env tl_pat typ in
annot_pat (P_cons (hd_pat, tl_pat)) typ, env, hd_guards @ tl_guards
@@ -2499,7 +2514,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| P_list pats ->
begin
match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
+ | Typ_aux (Typ_app (f, [A_aux (A_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
let rec process_pats env = function
| [] -> [], env, []
| (pat :: pats) ->
@@ -2543,9 +2558,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
begin
try
- let goals = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item quants) in
+ let goals = quant_kopts typq |> List.map kopt_kid |> KidSet.of_list in
typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for pattern " ^ string_of_typ typ));
- let unifiers = unify l env ret_typ typ goals in
+ let unifiers = unify l env goals ret_typ typ in
let arg_typ' = subst_unifiers unifiers arg_typ in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
@@ -2578,7 +2593,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ));
(* FIXME: There's no obvious goals here *)
- let unifiers = unify l env typ2 typ (tyvars_of_typ typ2) in
+ let unifiers = unify l env (tyvars_of_typ typ2) typ2 typ in
let arg_typ' = subst_unifiers unifiers typ1 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
@@ -2596,7 +2611,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
try
typ_debug (lazy "Unifying mapping forwards failed, trying backwards.");
typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ));
- let unifiers = unify l env typ1 typ (tyvars_of_typ typ1) in
+ let unifiers = unify l env (tyvars_of_typ typ1) typ1 typ in
let arg_typ' = subst_unifiers unifiers typ2 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
@@ -2734,13 +2749,13 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
| TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0 ->
List.fold_left2 bind_typ_pat_arg env tpats typs
| _, _ -> typ_error l ("Couldn't bind type " ^ string_of_typ typ ^ " with " ^ string_of_typ_pat typ_pat)
-and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (A_aux (typ_arg_aux, _) as typ_arg) =
match typ_pat_aux, typ_arg_aux with
| TP_wild, _ -> env
- | TP_var kid, Typ_arg_nexp nexp ->
+ | TP_var kid, A_nexp nexp ->
Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid K_int env)
- | _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ
- | _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order"
+ | _, A_typ typ -> bind_typ_pat env typ_pat typ
+ | _, A_order _ -> typ_error l "Cannot bind type pattern against order"
| _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) =
@@ -2787,7 +2802,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
let eff = if is_register then mk_effect [BE_wreg] else no_effect in
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env rectyp_q regtyp (tyvars_of_typ rectyp_q) with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let checked_exp = crule check_exp env exp field_typ' in
annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) field_typ') checked_exp, env
@@ -2817,11 +2832,13 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
annot_assign tlexp inferred_exp, env'
with
- | Type_error (_, _) ->
- let inferred_lexp = infer_lexp env lexp in
- let checked_exp = crule check_exp env exp (lexp_typ_of inferred_lexp) in
- annot_assign inferred_lexp checked_exp, env
-
+ | Type_error (l, err) ->
+ try
+ let inferred_lexp = infer_lexp env lexp in
+ let checked_exp = crule check_exp env exp (lexp_typ_of inferred_lexp) in
+ annot_assign inferred_lexp checked_exp, env
+ with Type_error (l, err') -> typ_raise l (Err_because (err', err))
+
and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ));
let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some ((env, typ, eff),None))) in
@@ -2846,7 +2863,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| LEXP_deref exp ->
let inferred_exp = infer_exp env exp in
begin match typ_of inferred_exp with
- | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" ->
+ | Typ_aux (Typ_app (r, [A_aux (A_typ vtyp, _)]), _) when string_of_id r = "register" ->
subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
| _ ->
typ_error l (string_of_typ typ ^ " must be a register type in " ^ string_of_exp exp ^ ")")
@@ -2899,7 +2916,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
let inferred_v_lexp = infer_lexp env v_lexp in
let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
match v_typ_aux with
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
when Id.compare id (mk_id "vector") = 0 ->
let inferred_exp1 = infer_exp env exp1 in
let inferred_exp2 = infer_exp env exp2 in
@@ -2921,7 +2938,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
let inferred_v_lexp = infer_lexp env v_lexp in
let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
match v_typ_aux with
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
when Id.compare id (mk_id "vector") = 0 ->
let inferred_exp = infer_exp env exp in
let nexp, env = bind_numeric l (typ_of inferred_exp) env in
@@ -2936,7 +2953,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
begin
let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) =
match v_typ_aux with
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord ->
typ_equality l env elem_typ first_elem_typ;
nsum acc len
@@ -2947,7 +2964,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
let v_typs = List.map (fun lexp -> Env.expand_synonyms env (lexp_typ_of lexp)) inferred_v_lexps in
match v_typ_aux with
- | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+ | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)])
when Id.compare id (mk_id "vector") = 0 ->
let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in
annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ)
@@ -2981,7 +2998,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
end
| E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
- | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])))
+ | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp nexp)])))
| E_constraint nc ->
Env.wf_constraint env nc;
annot_exp (E_constraint nc) bool_typ
@@ -3022,7 +3039,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
in
let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env rectyp_q typ (tyvars_of_typ rectyp_q) with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let inferred_exp = crule check_exp env exp field_typ' in
FE_aux (FE_Fexp (field, inferred_exp), (l, None))
@@ -3179,6 +3196,13 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
let universals = Env.get_typ_vars env in
let universal_constraints = Env.get_constraints env in
+ let all_unifiers = ref KBindings.empty in
+ let record_unifiers unifiers =
+ let previous_unifiers = !all_unifiers in
+ let updated_unifiers = KBindings.map (subst_unifiers_typ_arg unifiers) previous_unifiers in
+ all_unifiers := merge_uvars l updated_unifiers unifiers;
+ in
+
let quants, typ_args, typ_ret, eff =
match Env.expand_synonyms env f_typ with
| Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) -> ref (quant_items typq), typ_args, ref typ_ret, eff
@@ -3202,9 +3226,11 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
| None -> typ_args
| Some expect when is_exist (Env.expand_synonyms env expect) || is_exist !typ_ret -> typ_args
| Some expect ->
- let goals = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item !quants) in
+ let goals = quant_kopts (mk_typquant !quants) |> List.map kopt_kid |> KidSet.of_list in
try
- let unifiers = unify l env !typ_ret expect goals |> KBindings.bindings in
+ let unifiers = unify l env goals !typ_ret expect in
+ record_unifiers unifiers;
+ let unifiers = KBindings.bindings unifiers in
typ_debug (lazy (Util.("Unifiers " |> magenta |> clear)
^ Util.string_of_list ", " (fun (v, arg) -> string_of_kid v ^ " => " ^ string_of_typ_arg arg) unifiers));
List.iter (fun unifier -> quants := instantiate_quants !quants unifier) unifiers;
@@ -3219,12 +3245,14 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
if KidSet.for_all (is_bound env) (tyvars_of_typ typ) then
crule check_exp env arg typ, remaining_typs, env
else
- let goals = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item !quants) in
+ let goals = quant_kopts (mk_typquant !quants) |> List.map kopt_kid |> KidSet.of_list in
+ typ_debug (lazy ("Quantifiers " ^ Util.string_of_list ", " string_of_quant_item !quants));
let inferred_arg = irule infer_exp env arg in
let inferred_arg, unifiers, env =
try type_coercion_unify env goals inferred_arg typ with
| Unification_error (l, m) -> typ_error l m
in
+ record_unifiers unifiers;
let unifiers = KBindings.bindings unifiers in
typ_debug (lazy (Util.("Unifiers " |> magenta |> clear)
^ Util.string_of_list ", " (fun (v, arg) -> string_of_kid v ^ " => " ^ string_of_typ_arg arg) unifiers));
@@ -3266,7 +3294,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
let exp = annot_exp (E_app (f, xs)) typ_ret eff in
typ_debug (lazy ("RETURNING: " ^ string_of_exp exp));
- exp, KBindings.empty (* FIXME *)
+ exp, !all_unifiers
and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as typ) =
let (Typ_aux (typ_aux, _) as typ), env = bind_existential l typ env in
@@ -3298,7 +3326,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
| MP_cons (hd_mpat, tl_mpat) ->
begin
match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
+ | Typ_aux (Typ_app (f, [A_aux (A_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
let hd_mpat, env, hd_guards = bind_mpat allow_unknown other_env env hd_mpat ltyp in
let tl_mpat, env, tl_guards = bind_mpat allow_unknown other_env env tl_mpat typ in
annot_mpat (MP_cons (hd_mpat, tl_mpat)) typ, env, hd_guards @ tl_guards
@@ -3322,7 +3350,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
| MP_list mpats ->
begin
match Env.expand_synonyms env typ with
- | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
+ | Typ_aux (Typ_app (f, [A_aux (A_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
let rec process_mpats env = function
| [] -> [], env, []
| (pat :: mpats) ->
@@ -3365,7 +3393,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
begin
try
typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
- let unifiers = unify l env ret_typ typ (tyvars_of_typ ret_typ) in
+ let unifiers = unify l env (tyvars_of_typ ret_typ) ret_typ typ in
let arg_typ' = subst_unifiers unifiers arg_typ in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
@@ -3395,7 +3423,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
begin
try
typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
- let unifiers = unify l env typ2 typ (tyvars_of_typ typ2) in
+ let unifiers = unify l env (tyvars_of_typ typ2) typ2 typ in
let arg_typ' = subst_unifiers unifiers typ1 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
@@ -3412,7 +3440,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
try
typ_debug (lazy "Unifying mapping forwards failed, trying backwards.");
typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
- let unifiers = unify l env typ1 typ (tyvars_of_typ typ1) in
+ let unifiers = unify l env (tyvars_of_typ typ1) typ1 typ in
let arg_typ' = subst_unifiers unifiers typ2 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
@@ -4164,14 +4192,14 @@ let check_default env (DT_aux (ds, l)) =
| DT_order (Ord_aux (Ord_var _, _)) -> typ_error l "Cannot have variable default order"
let kinded_id_arg kind_id =
- let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in
+ let typ_arg arg = A_aux (arg, Parse_ast.Unknown) in
match kind_id with
- | KOpt_aux (KOpt_none kid, _) -> typ_arg (Typ_arg_nexp (nvar kid))
- | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
+ | KOpt_aux (KOpt_none kid, _) -> typ_arg (A_nexp (nvar kid))
+ | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> typ_arg (A_nexp (nvar kid))
| KOpt_aux (KOpt_kind (K_aux (K_order, _), kid), _) ->
- typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
+ typ_arg (A_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
| KOpt_aux (KOpt_kind (K_aux (K_type, _), kid), _) ->
- typ_arg (Typ_arg_typ (mk_typ (Typ_var kid)))
+ typ_arg (A_typ (mk_typ (Typ_var kid)))
let fold_union_quant quants (QI_aux (qi, l)) =
match qi with
@@ -4197,21 +4225,21 @@ let mk_synonym typq typ_arg =
let kopts, ncs = quant_split typq in
let rec subst_args kopts args =
match kopts, args with
- | kopt :: kopts, Typ_arg_aux (Typ_arg_nexp arg, _) :: args when is_nat_kopt kopt ->
+ | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_nat_kopt kopt ->
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
- | kopt :: kopts, Typ_arg_aux (Typ_arg_typ arg, _) :: args when is_typ_kopt kopt ->
+ | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs
- | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt ->
+ | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_order arg) typ_arg, ncs
- | kopt :: kopts, Typ_arg_aux (Typ_arg_bool arg, _) :: args when is_order_kopt kopt ->
+ | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_order_kopt kopt ->
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
| [], [] -> typ_arg, ncs
- | _, Typ_arg_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments"
+ | _, A_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments"
| _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments"
in
fun env args ->
@@ -4234,7 +4262,7 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
fun env (TD_aux (tdef, (l, _))) ->
let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
match tdef with
- | TD_abbrev (id, typq, (Typ_arg_aux (Typ_arg_typ _, _) as typ_arg)) ->
+ | TD_abbrev (id, typq, (A_aux (A_typ _, _) as typ_arg)) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
(* For type synonyms for non-Type kinds we omit them from the AST *)
| TD_abbrev (id, typq, typ_arg) ->
@@ -4255,9 +4283,9 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
begin
match typ with
(* The type of a bitfield must be a constant-width bitvector *)
- | Typ_aux (Typ_app (v, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant size, _)), _);
- Typ_arg_aux (Typ_arg_order order, _);
- Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id b, _)), _)]), _)
+ | Typ_aux (Typ_app (v, [A_aux (A_nexp (Nexp_aux (Nexp_constant size, _)), _);
+ A_aux (A_order order, _);
+ A_aux (A_typ (Typ_aux (Typ_id b, _)), _)]), _)
when string_of_id v = "vector" && string_of_id b = "bit" ->
let size = Big_int.to_int size in
let (Defs defs), env = check env (Bitfield.macro id size order ranges) in
@@ -4343,11 +4371,11 @@ let initial_env =
|> Env.add_val_spec (mk_id "size_itself_int")
(TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
Parse_ast.Unknown)],Parse_ast.Unknown),
- function_typ [app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]]
+ function_typ [app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]]
(atom_typ (nvar (mk_kid "n"))) no_effect)
|> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value")
|> Env.add_val_spec (mk_id "make_the_value")
(TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
Parse_ast.Unknown)],Parse_ast.Unknown),
function_typ [atom_typ (nvar (mk_kid "n"))]
- (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) no_effect)
+ (app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]) no_effect)
diff --git a/src/type_check.mli b/src/type_check.mli
index 7dc2da30..52ade6fa 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -80,6 +80,7 @@ type type_error =
| Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
| Err_no_num_ident of id
| Err_other of string
+ | Err_because of type_error * type_error
exception Type_error of l * type_error;;
@@ -359,7 +360,13 @@ val destruct_vector : Env.t -> typ -> (nexp * order * typ) option
val subst_unifiers : typ_arg KBindings.t -> typ -> typ
-val unify : l -> Env.t -> typ -> typ -> typ_arg KBindings.t * kid list * n_constraint option
+(** [unify l env goals typ1 typ2] returns set of typ_arg bindings such
+ that substituting those bindings using every type variable in goals
+ will make typ1 and typ2 equal. Will throw a Unification_error if
+ typ1 and typ2 cannot unification (although unification in Sail is
+ not complete). Will throw a type error if any goals appear in in
+ typ2 (occurs check). *)
+val unify : l -> Env.t -> KidSet.t -> typ -> typ -> typ_arg KBindings.t
val alpha_equivalent : Env.t -> typ -> typ -> bool
diff --git a/src/type_error.ml b/src/type_error.ml
index 0fa238ed..9144e993 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -133,7 +133,7 @@ let rec analyze_unresolved_quant2 locals ncs = function
(* If we have a really anonymous type-variable, try to find a
regular variable that corresponds to it. *)
let is_linked v = function
- | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
+ | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 ->
[(v, nid id, typ)]
| (id, (mut, typ)) ->
@@ -178,7 +178,7 @@ let rec analyze_unresolved_quant locals ncs = function
(* If we have a really anonymous type-variable, try to find a
regular variable that corresponds to it. *)
let is_linked v = function
- | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
+ | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 ->
[(v, nid id, typ)]
| (id, (mut, typ)) ->
@@ -206,18 +206,20 @@ let rec pp_type_error = function
in
coercion ^^ hardline
^^ (string "Coercion failed because:" ^//^ pp_type_error trigger)
- ^^ hardline
- ^^ (string "Possible reasons:" ^//^ separate_map hardline pp_type_error reasons)
+ ^^ if not (reasons = []) then
+ hardline
+ ^^ (string "Possible reasons:" ^//^ separate_map hardline pp_type_error reasons)
+ else
+ empty
| Err_no_overloading (id, errs) ->
string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_type_error err) errs)
| Err_subtype (typ1, typ2, constrs, locs) ->
- enclose (string (Util.termcode 1)) (string (Util.termcode 21))
- (separate space [ string (string_of_typ typ1);
- string "is not a subtype of";
- string (string_of_typ typ2) ])
+ (separate space [ string (string_of_typ typ1);
+ string "is not a subtype of";
+ string (string_of_typ typ2) ])
^/^ string "in context"
^/^ bullet pp_n_constraint constrs
^/^ string "where"
@@ -232,6 +234,12 @@ let rec pp_type_error = function
^^ twice hardline
^^ group (separate_map hardline (analyze_unresolved_quant locals ncs) quants)
+ (* We only got err, because of previous error, err' *)
+ | Err_because (err, err') ->
+ pp_type_error err
+ ^^ hardline ^^ string "This error occured because of a previous error:"
+ ^//^ pp_type_error err'
+
| Err_other str -> string str
let rec string_of_type_error err =
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 583c4485..fb1b2619 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -3,5 +3,4 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char
let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4
-Failed because
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
+Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index baddbcb0..5bde04ba 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -3,5 +3,4 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char
let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4
-Failed because
-Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
+Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index f190de92..7e3b517c 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -3,22 +3,22 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
let _ = test(32)
Tried performing type coercion from int(32) to int('size) on 32
-Failed because
-int(32) is not a subtype of int('size)
-in context
-* 'size = 'ex8#
-* ('ex8# = 32 | 'ex8# = 64)
-* ('ex7# = 32 | 'ex7# = 64)
-where
-* 'ex7# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
+Coercion failed because:
+ int(32) is not a subtype of int('size)
+ in context
+ * 'size = 'ex8#
+ * ('ex8# = 32 | 'ex8# = 64)
+ * ('ex7# = 32 | 'ex7# = 64)
+ where
+ * 'ex7# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
let (size as 'size) : {|32, 64|} = 32
-* 'ex8# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
+ * 'ex8# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
let (size as 'size) : {|32, 64|} = 32
-* 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
+ * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
let (size as 'size) : {|32, 64|} = 32
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index ddfac3e4..dc1281d2 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -3,22 +3,22 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
let _ = test(64)
Tried performing type coercion from int(64) to int('size) on 64
-Failed because
-int(64) is not a subtype of int('size)
-in context
-* 'size = 'ex8#
-* ('ex8# = 32 | 'ex8# = 64)
-* ('ex7# = 32 | 'ex7# = 64)
-where
-* 'ex7# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
+Coercion failed because:
+ int(64) is not a subtype of int('size)
+ in context
+ * 'size = 'ex8#
+ * ('ex8# = 32 | 'ex8# = 64)
+ * ('ex7# = 32 | 'ex7# = 64)
+ where
+ * 'ex7# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
let (size as 'size) : {|32, 64|} = 32
-* 'ex8# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
+ * 'ex8# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
let (size as 'size) : {|32, 64|} = 32
-* 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
+ * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
let (size as 'size) : {|32, 64|} = 32
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 03:57:11 +0000