Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Simplify type variables #1263

Closed
wants to merge 4 commits into from
Closed

Simplify type variables #1263

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
73949e9
Create a proper type for type substitution
Halbaroth Oct 25, 2024
3aeec5d
Use type variables of Dolmen directly
Halbaroth Oct 25, 2024
b3f0e79
better API + documentation
Halbaroth Oct 25, 2024
91c013c
Linter
Halbaroth Oct 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions src/lib/frontend/translate.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -523,8 +523,8 @@ and handle_ty_app ?(update = false) ty_c l =
variable. *)
let rec apply_ty_substs tysubsts ty =
match ty with
| Ty.Tvar { v; _ } ->
Ty.M.find v tysubsts
| Ty.Tvar tv ->
Ty.Subst.eval tysubsts tv

| Text (tyl, hs) ->
Ty.Text (List.map (apply_ty_substs tysubsts) tyl, hs)
Expand Down Expand Up @@ -561,9 +561,9 @@ and handle_ty_app ?(update = false) ty_c l =
List.fold_left2 (
fun acc tv ty ->
match tv with
| Ty.Tvar { v; _ } -> Ty.M.add v ty acc
| Ty.Tvar tv -> Ty.Subst.update tv ty acc
| _ -> assert false
) Ty.M.empty args tyl
) Ty.Subst.id args tyl
in
apply_ty_substs tysubsts ty

Expand Down Expand Up @@ -1687,7 +1687,7 @@ let make_form name_base f loc ~decl_kind =
in
assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
let ff = E.purify_form ff in
if Ty.Svty.is_empty (E.free_type_vars ff) then ff
if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
else
E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind

Expand Down Expand Up @@ -1943,7 +1943,7 @@ let make dloc_file acc stmt =
assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
let ff = E.purify_form ff in
let e =
if Ty.Svty.is_empty (E.free_type_vars ff) then ff
if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
else
E.mk_forall name_base loc
Var.Map.empty [] ff ~toplevel:true ~decl_kind
Expand All @@ -1964,7 +1964,7 @@ let make dloc_file acc stmt =
assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
let ff = E.purify_form ff in
let e =
if Ty.Svty.is_empty (E.free_type_vars ff) then ff
if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
else
E.mk_forall name_base loc
Var.Map.empty [] ff ~toplevel:true ~decl_kind
Expand Down
14 changes: 7 additions & 7 deletions src/lib/reasoners/matching.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
if Options.get_debug_matching() >= 3 then
let print fmt Matching_types.{ sbs; sty; _ } =
Format.fprintf fmt ">>> sbs= %a | sty= %a@ "
(SubstE.pp E.print) sbs Ty.print_subst sty
(SubstE.pp E.print) sbs Ty.Subst.pp sty
in
print_dbg
~module_name:"Matching" ~function_name:"match_pats_modulo"
Expand All @@ -124,7 +124,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
print_dbg
~module_name:"Matching" ~function_name:"match_one_pat"
"match_pat: %a with subst: sbs= %a | sty= %a"
E.print pat0 (SubstE.pp E.print) sbs Ty.print_subst sty
E.print pat0 (SubstE.pp E.print) sbs Ty.Subst.pp sty


let match_one_pat_against Matching_types.{ sbs; sty; _ } pat0 t =
Expand All @@ -136,14 +136,14 @@ module Make (X : Arg) : S with type theory = X.t = struct
E.print pat0
E.print t
(SubstE.pp E.print) sbs
Ty.print_subst sty
Ty.Subst.pp sty

let match_term Matching_types.{ sbs; sty; _ } t pat =
if Options.get_debug_matching() >= 3 then
print_dbg
~module_name:"Matching" ~function_name:"match_term"
"I match %a against %a with subst: sbs=%a | sty= %a"
E.print pat E.print t (SubstE.pp E.print) sbs Ty.print_subst sty
E.print pat E.print t (SubstE.pp E.print) sbs Ty.Subst.pp sty

let match_list Matching_types.{ sbs; sty; _ } pats xs =
if Options.get_debug_matching() >= 3 then
Expand All @@ -153,7 +153,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
E.print_list pats
E.print_list xs
(SubstE.pp E.print) sbs
Ty.print_subst sty
Ty.Subst.pp sty

let match_class_of t cl =
if Options.get_debug_matching() >= 3 then
Expand All @@ -177,7 +177,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
(fun gsbt ->
print_dbg ~header:false
">>> sbs = %a and sbty = %a@ "
(SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty
(SubstE.pp E.print) gsbt.sbs Ty.Subst.pp gsbt.sty
)res

end
Expand Down Expand Up @@ -492,7 +492,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
else
let egs =
{ sbs = SubstE.empty;
sty = Ty.esubst;
sty = Ty.Subst.id;
gen = 0;
goal = false;
s_term_orig = [];
Expand Down
Loading
Loading