Skip to content

Commit

Permalink
Add new Occur_check implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
FardaleM committed Oct 2, 2024
1 parent 3d1a187 commit 10ce46d
Show file tree
Hide file tree
Showing 6 changed files with 73 additions and 2 deletions.
1 change: 1 addition & 0 deletions lib/common/Subst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ type t = Type.t Variable.Map.t

let empty = Variable.Map.empty
let add = Variable.Map.add
let remove = Variable.Map.remove

let rec apply (env : Type.Env.t) t =
let substitute ty = apply env t ty in
Expand Down
1 change: 1 addition & 0 deletions lib/common/Subst.mli
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ type t = Type.t Variable.Map.t

val empty : t
val add : Variable.t -> Type.t -> t -> t
val remove : Variable.t -> t -> t

val apply : Type.Env.t -> t -> Type.t -> Type.t
val simplify : Type.Env.t -> Variable.Set.t -> t -> t
Expand Down
1 change: 1 addition & 0 deletions lib/unification/Env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ let tyenv t = t.tyenv
let gen flags e : Variable.t = Variable.Gen.gen flags e.tyenv.var_gen

let add e v ty = e.vars <- Subst.add v ty e.vars
let remove e v = e.vars <- Subst.remove v e.vars

let init_partial e v =
e.partials <- Variable.Map.update v
Expand Down
1 change: 1 addition & 0 deletions lib/unification/Env.mli
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ val representative : t -> Variable.t -> representative
val push_tuple : t -> ACTerm.t -> ACTerm.t -> unit
val push_arrow : t -> ArrowTerm.t -> ArrowTerm.t -> unit
val add : t -> Variable.t -> Type.t -> unit
val remove : t -> Variable.t -> unit
val init_partial : t -> Variable.t -> unit
val extend_partial : ?by:int -> t -> Variable.t -> Type.t -> unit

Expand Down
29 changes: 29 additions & 0 deletions lib/unification/Occur_check.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
open CCOption.Infix

type state = Done | Seen | Fresh

exception Cycle of Variable.t list

let find_cycle graph =
let states = Variable.HMap.create 10 in
Variable.Map.iter (fun v _ -> Variable.HMap.add states v Fresh) graph;
let rec dfs v =
match Variable.HMap.get_or ~default:Fresh states v with
| Fresh ->
Variable.HMap.add states v Seen;
let res =
let t = Variable.Map.get_or ~default:Type.dummy v graph in
Iter.find_map dfs (Type.iter_vars t)
in
Variable.HMap.add states v Done;
let+ u, path = res in
if Variable.equal u v then raise (Cycle (u :: path)) else (u, v :: path)
| Seen -> Some (v, [v])
| Done -> None
in
try
Variable.Map.iter (fun v _ -> assert (CCOption.is_none (dfs v))) graph;
None
with Cycle l -> Some l

let occur_check env = find_cycle (Env.vars env)
42 changes: 40 additions & 2 deletions lib/unification/Syntactic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ include Infix
(** Checking for cycles *)

(* TO OPTIM/MEASURE *)
let occur_check env : return =
let _occur_check env : return =
Trace.with_span ~__FUNCTION__ ~__LINE__ ~__FILE__ __FUNCTION__ (fun _sp ->
debug (fun m -> m "@[<v>Occur check in@,%a@]" Env.pp env);
let nb_predecessors = Variable.HMap.create 17 in
Expand Down Expand Up @@ -104,9 +104,47 @@ let occur_check env : return =
in
loop 0 vars_without_predecessors)

let rec occur_check env : return =
match Occur_check.occur_check env with
| None -> Done
| Some l ->
Logs.debug (fun m -> m "Occur check in: %a" Env.pp env);
Logs.debug (fun m -> m "Cycle: %a" (CCList.pp Variable.pp) l);
let rec collapse stack = function
| u::v::tl -> (
match Env.representative env u with
| Env.V _ -> failwith "Impossible"
| Env.E (_, t) ->
match t with
| Type.Var _ | FrozenVar _ | Other _ -> failwith "Impossible"
| Constr _ | Arrow _ -> None
| Tuple l ->
let stack =
Type.NSet.fold
(fun t stack ->
match t with
| Type.Var v' when Variable.equal v v' -> stack
| t ->
Stack.push stack t
(Type.tuple (Env.tyenv env) Type.NSet.empty)(*unit*))
l stack
in
collapse stack tl
)
| _ -> Some stack
in
match collapse Stack.empty l with
| None -> FailedOccurCheck env
| Some stack ->
let v = List.hd l in
List.iter (fun u -> Env.add env u (Type.var (Env.tyenv env) v)) (List.tl l);
Env.remove env v;
let* () = process_stack env stack in
occur_check env

(** Main process *)

let rec process_stack env (stack : Stack.t) : return =
and process_stack env (stack : Stack.t) : return =
Trace.with_span ~__FUNCTION__ ~__LINE__ ~__FILE__ __FUNCTION__ (fun _sp ->
debug (fun m -> m "Process_stack");
Timeout.check ();
Expand Down

0 comments on commit 10ce46d

Please sign in to comment.