Commit 7cd31e1d authored by POTTIER Francois's avatar POTTIER Francois

Introduce the type [ground_sort] and the functions [ground] and [unground].

parent ade16d61
......@@ -44,6 +44,9 @@ type sort = term =
| TVar of int
| TNode of sort structure
type ground_sort =
| GArrow of ground_sort list
(* -------------------------------------------------------------------------- *)
(* Sort constructors. *)
......@@ -68,6 +71,21 @@ let domain (x : variable) : variable list option =
(* -------------------------------------------------------------------------- *)
(* Converting between sorts and ground sorts. *)
let rec ground (s : sort) : ground_sort =
match s with
| TVar _ ->
(* All variables are replaced with [*]. *)
GArrow []
| TNode (Arrow ss) ->
GArrow (List.map ground ss)
let rec unground (GArrow ss : ground_sort) : sort =
TNode (Arrow (List.map unground ss))
(* -------------------------------------------------------------------------- *)
(* A name generator for unification variables. *)
let make_gensym () : unit -> string =
......
......@@ -16,6 +16,9 @@ type sort =
| TVar of int
| TNode of sort structure
type ground_sort =
| GArrow of ground_sort list
(* -------------------------------------------------------------------------- *)
(* Sort unification. *)
......@@ -39,6 +42,11 @@ val unify: variable -> variable -> unit
val decode: variable -> sort
(* Grounding a sort replaces all sort variables with the sort [*]. *)
val ground: sort -> ground_sort
val unground: ground_sort -> sort
(* -------------------------------------------------------------------------- *)
(* A sort can be printed. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment