Commit 700064dc authored by POTTIER Francois's avatar POTTIER Francois

Split [GroundSort] off [SortUnification].

parent 1968e4f8
(******************************************************************************)
(* *)
(* Menhir *)
(* *)
(* François Pottier, Inria Paris *)
(* Yann Régis-Gianas, PPS, Université Paris Diderot *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU General Public License version 2, as described in the *)
(* file LICENSE. *)
(* *)
(******************************************************************************)
type sort =
| GArrow of sort list
let star =
GArrow []
let domain sort =
let GArrow sorts = sort in
sorts
(******************************************************************************)
(* *)
(* Menhir *)
(* *)
(* François Pottier, Inria Paris *)
(* Yann Régis-Gianas, PPS, Université Paris Diderot *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU General Public License version 2, as described in the *)
(* file LICENSE. *)
(* *)
(******************************************************************************)
(* The syntax of sorts is:
sort ::= (sort, ..., sort) -> *
where the arity (the number of sorts on the left-hand side of the arrow)
can be zero. *)
type sort =
| GArrow of sort list
val star: sort
val domain: sort -> sort list
......@@ -13,8 +13,8 @@
let value = Positions.value
let unknown = Positions.unknown_pos
let star = SortUnification.ground_star
open Syntax
open GroundSort
(* -------------------------------------------------------------------------- *)
......
......@@ -215,7 +215,7 @@ let check_grammar env g =
(* -------------------------------------------------------------------------- *)
type sorts =
ground_sort Env.t
GroundSort.sort Env.t
let infer (g : grammar) : sorts =
......
......@@ -12,12 +12,12 @@
(******************************************************************************)
open Syntax
open SortUnification
open GroundSort
(* [infer_grammar g] performs sort inference for the grammar [g],
rejecting the grammar if it is ill-sorted. It returns a map of
(terminal and nonterminal) symbols to ground sorts. *)
type sorts = ground_sort StringMap.t
type sorts = sort StringMap.t
val infer: grammar -> sorts
......@@ -57,12 +57,6 @@ type sort = term =
| TVar of int
| TNode of sort structure
type ground_sort =
| GArrow of ground_sort list
let ground_star =
GArrow []
(* -------------------------------------------------------------------------- *)
(* Sort constructors. *)
......@@ -89,15 +83,15 @@ let domain (x : variable) : variable list option =
(* Converting between sorts and ground sorts. *)
let rec ground (s : sort) : ground_sort =
let rec ground s =
match s with
| TVar _ ->
(* All variables are replaced with [*]. *)
GArrow []
GroundSort.GArrow []
| TNode (Arrow ss) ->
GArrow (List.map ground ss)
GroundSort.GArrow (List.map ground ss)
let rec unground (GArrow ss : ground_sort) : sort =
let rec unground (GroundSort.GArrow ss) =
TNode (Arrow (List.map unground ss))
(* -------------------------------------------------------------------------- *)
......
......@@ -20,7 +20,7 @@
sort ::= (sort, ..., sort) -> *
where the arity (the number of sorts on the left-hand side of the arrow)
can be zero. *)
can be zero. See [GroundSort]. *)
type 'a structure =
| Arrow of 'a list
......@@ -29,11 +29,6 @@ type sort =
| TVar of int
| TNode of sort structure
type ground_sort =
| GArrow of ground_sort list
val ground_star: ground_sort
(* -------------------------------------------------------------------------- *)
(* Sort unification. *)
......@@ -59,8 +54,8 @@ val decode: variable -> sort
(* Grounding a sort replaces all sort variables with the sort [*]. *)
val ground: sort -> ground_sort
val unground: ground_sort -> sort
val ground: sort -> GroundSort.sort
val unground: GroundSort.sort -> sort
(* -------------------------------------------------------------------------- *)
......
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