Add Absurd in ML.

This commit is contained in:
Olivier 2023-03-01 10:05:44 +01:00
parent 7679076de4
commit dabb2bd699
12 changed files with 129 additions and 33 deletions

View File

@ -92,7 +92,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
List.map (translate_branch env) brs
)
| F.Absurd (_, ty) ->
P.Absurd (translate_type env ty)
P.Absurd (Some (translate_type env ty))
| F.Refl (_, ty) ->
P.Refl (translate_type env ty)
| F.Use (_, t, u) ->

View File

@ -104,6 +104,7 @@ type error =
| Cycle of F.nominal_type
| VariableConflict of ML.tevar
| VariableScopeEscape of int * int
| ContextNotAbsurd
| Unsupported of string
exception Error of Utils.loc * error
@ -282,7 +283,8 @@ let get_loc t =
| ML.Var (pos, _) | ML.Hole (pos, _) | ML.Abs (pos, _, _)
| ML.App (pos, _, _) | ML.Let (pos, _, _, _, _) | ML.Annot (pos, _, _)
| ML.For (pos, _, _) | ML.Some_ (pos, _, _) | ML.Tuple (pos, _)
| ML.LetProd (pos, _, _, _) | ML.Variant (pos, _, _) | ML.Match (pos, _, _)
| ML.LetProd (pos, _, _, _) | ML.Variant (pos, _, _) | ML.Absurd pos
| ML.Match (pos, _, _)
-> pos
let correlate loc c =
@ -505,6 +507,11 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
and+ ty = decode w
in F.Match (loc, ty, t, branches')
| ML.Absurd loc ->
let+ () = absurd
and+ ty = decode w
in F.Absurd (loc, ty)
| ML.Hole (loc, ts) ->
(* A hole ...[t1, t2, .., tn] has any type, and its subterms
[t1, .., tn] can themselves have any type; our return type
@ -708,6 +715,7 @@ let translate_with_hook ~hook ~rectypes env t =
| Solver.Cycle (ty) -> Cycle (ty)
| Solver.VariableScopeEscape (rank, scope) ->
VariableScopeEscape (rank, scope)
| Solver.ContextNotAbsurd -> ContextNotAbsurd
in
raise (Error (loc, error))
@ -735,6 +743,9 @@ let emit_error loc (error : error) =
| VariableScopeEscape (_, _) ->
Printf.printf
"A rigid variable escapes its scope.\n"
| ContextNotAbsurd ->
Printf.printf
"Unexpected typing context.\n"
| VariableConflict (x) ->
Printf.printf
"Scope error: variable %s is already bound in this pattern."

View File

@ -4,6 +4,7 @@ type error =
| Cycle of F.nominal_type
| VariableConflict of ML.tevar
| VariableScopeEscape of int * int
| ContextNotAbsurd
| Unsupported of string
exception Error of Utils.loc * error

View File

@ -42,6 +42,7 @@ type term =
| LetProd of loc * tevar list * term * term
| Variant of loc * Datatype.LabelId.t * term Option.t
| Match of loc * term * branch list
| Absurd of loc
and branch = pattern * term

View File

@ -109,6 +109,8 @@ let term_atom :=
| ts = tuple (term) ; { Tuple (Some $loc, ts) }
| "." ; { Absurd (Some $loc) }
| MATCH ; t = term ; WITH ;
brs = branches ;
END ; { Match (Some $loc, t, brs) }

View File

@ -45,6 +45,8 @@ let rec translate_term (t : ML.term) : P.term =
P.Variant (lbl, None, Option.map self t)
| ML.Match (_, t, brs) ->
P.Match (None, self t, List.map translate_branch brs)
| ML.Absurd _ ->
P.Absurd None
and translate_branch (pat, t) =
(translate_pattern pat, translate_term t)

View File

@ -35,7 +35,7 @@ type term =
| Inj of (typ list) option * int * term
| Variant of Datatype.label_id * datatype option * term option
| Match of typ option * term * branch list
| Absurd of typ
| Absurd of typ option
| Refl of typ
| Use of term * term

View File

@ -45,6 +45,8 @@ module Shrinker = struct
ML.Variant (pos, ty, Option.map (fun t -> subst t x u) t)
| ML.Match (pos, t, brs) ->
ML.Match (pos, subst t x u, List.map (fun br -> subst_branch br x u) brs)
| ML.Absurd pos ->
ML.Absurd pos
(* (y.t)[u/x] *)
and subst_under ys t x u =
@ -180,6 +182,10 @@ module Shrinker = struct
| ML.Match (_, _t, _branches) ->
failwith "unsupported"
| ML.Absurd _ ->
empty
)
)
end

View File

@ -74,6 +74,10 @@ module EqEnv : sig
and structure =
S of vertex Abs.structure [@@unboxed]
val is_consistent_env: unit -> bool
val make_inconsistent: unit -> unit
val add: vertex -> unit
val remove_edges_at_scope: scope -> unit
@ -108,61 +112,105 @@ end = struct
(* For each equality, we store a scope, that corresponds to the scope
where the equality is well-defined. We represent our graph with a
hash-table mapping vertices to pairs of vertex and scope.
For every mapping (v1 -> (v2,scope)) we store a mapping
(v2 -> (v1,scope)) as well, so as to provide an undirected graph. *)
hash-table mapping vertices to pairs of vertex and scope. For every
mapping (v1 -> (v2,scope)) we store a mapping (v2 -> (v1,scope)) as well,
so as to provide an undirected graph. *)
let table : (vertex, (vertex * scope) option) StructTable.t =
StructTable.create 64
type equalities_graph = (vertex, (vertex * scope) option) StructTable.t
(* Each time we add a new edge, we add its two vertices in a stack with
the corresponding scope. *)
let stack : (scope * vertex * vertex) Stack.t =
Stack.create ()
type edges_stack = (scope * vertex * vertex) Stack.t
type eqenv = { table: equalities_graph ; added_edges : edges_stack}
type env =
| Equations of eqenv
| Inconsistent of eqenv
let env : env ref =
let table = StructTable.create 64 in
let added_edges = Stack.create () in
ref (Equations { table ; added_edges })
let table () =
match !env with
| Equations { table ; _ } ->
table
| Inconsistent _ ->
assert false
let added_edges () =
match !env with
| Equations { added_edges ; _ } ->
added_edges
| Inconsistent _ ->
assert false
let is_consistent_env () =
match !env with
| Equations _ ->
true
| Inconsistent _ ->
false
let make_inconsistent () =
match !env with
| Equations eqenv ->
env := Inconsistent eqenv
| Inconsistent _ ->
assert false
let restore_consistent_env () =
match !env with
| Equations _ ->
assert false
| Inconsistent eqenv ->
env := Equations eqenv
(* ------------------------------------------------------------------------ *)
(* Add vertices and edges. *)
let add v =
if not (StructTable.mem table v) then
StructTable.add table v None
if not (StructTable.mem (table ()) v) then
StructTable.add (table ()) v None
(* [add_directed_edge v1 v2 scope] adds an edge between [v1] and [v2] with
[scope]. If [v1] pointed to None, then remove this binding beforehand. *)
let add_directed_edge scope v1 v2 =
if StructTable.find table v1 = None then
StructTable.remove table v1;
StructTable.add table v1 (Some (v2,scope))
if StructTable.find (table ()) v1 = None then
StructTable.remove (table ()) v1;
StructTable.add (table ()) v1 (Some (v2,scope))
(* Add a binding in both ways. *)
let add_edge scope v1 v2 =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
assert (StructTable.mem (table ()) v1);
assert (StructTable.mem (table ()) v2);
add_directed_edge scope v1 v2;
add_directed_edge scope v2 v1;
Stack.push (scope, v1, v2) stack
Stack.push (scope, v1, v2) (added_edges ())
let remove_directed_edge scope v =
(* The last created edge should have the maximum scope and [remove_edge]
should be used to remove maximum scope. *)
assert (StructTable.find table v |> Option.get |> snd = scope);
StructTable.remove table v;
if not (StructTable.mem table v) then
StructTable.add table v None
assert (StructTable.find (table ()) v |> Option.get |> snd = scope);
StructTable.remove (table ()) v;
if not (StructTable.mem (table ()) v) then
StructTable.add (table ()) v None
let remove_edge (scope,v1,v2) =
remove_directed_edge scope v1;
remove_directed_edge scope v2
let rec remove_edges_at_scope scope =
match Stack.top_opt stack with
match Stack.top_opt (added_edges ()) with
| None ->
()
| Some (top_scope, _, _) ->
if top_scope = scope then begin
remove_edge (Stack.pop stack);
remove_edge (Stack.pop (added_edges ()));
remove_edges_at_scope scope
end
@ -170,15 +218,15 @@ end = struct
S (Abs.Abstract n)
let is_bounded v =
StructTable.mem table v
StructTable.mem (table ()) v
(* ------------------------------------------------------------------------ *)
(* Searching through the graph. *)
let get_neighbours v =
assert (StructTable.mem table v);
let vs = StructTable.find_all table v in
assert (StructTable.mem (table ()) v);
let vs = StructTable.find_all (table ()) v in
match vs with
(* [v] is either disconnected, and its only neighbour is None ... *)
| [None] ->
@ -229,8 +277,8 @@ end = struct
search stop [(v1,scope)] []
let path_exists v1 v2 =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
assert (StructTable.mem (table ()) v1);
assert (StructTable.mem (table ()) v2);
let stop =
( = ) v2
in
@ -241,7 +289,7 @@ end = struct
true
let get_structure v : vertex Abs.structure * scope =
assert (StructTable.mem table v);
assert (StructTable.mem (table ()) v);
let stop v =
match v with
| S (Abs.User _) ->
@ -332,8 +380,8 @@ end = struct
(* Equality test. *)
let eq v1 v2 : scope option =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
assert (StructTable.mem (table ()) v1);
assert (StructTable.mem (table ()) v2);
(* The stopping condition of the search is a succeeding unification with
the vertex [v2]. *)
let stop v1 =
@ -800,6 +848,12 @@ type variable =
let get : variable -> variable Data.data =
U.get
let is_consistent_env =
EqEnv.is_consistent_env
exception InconsistentContext =
EqEnv.InconsistentContext
exception VariableScopeEscape =
U.VariableScopeEscape

View File

@ -67,6 +67,9 @@ module Make
type variable =
U.variable
val is_consistent_env: unit -> bool
exception InconsistentContext
(** {2 Schemes} *)
(**A {i scheme} is usually described in the literature under the form [∀V.T],

View File

@ -82,6 +82,8 @@ type _ co =
| CTrue : unit co
(**The trivial constraint [CTrue] is always true. *)
| CFalse : unit co
| CMap : 'a co * ('a -> 'b) -> 'b co
(**The constraint [CMap (c, f)] is equivalent to the constraint [c]. The
transformation function [f] is used to postprocess the result of solving
@ -155,6 +157,7 @@ type _ co =
| Unify of O.ty * O.ty
| Cycle of O.ty
| VariableScopeEscape of int * int
| ContextNotAbsurd
exception Error of loc option * error
@ -251,6 +254,8 @@ module Printer = struct
self c
| CTrue | CPure _ ->
string "True"
| CFalse ->
string "False"
| CDecode v ->
separate space [string "wit"; var v]
| CEq (v1, v2) ->
@ -456,7 +461,7 @@ let rec ok : type a . a co -> bool =
function
| CLoc (_, c) ->
ok c
| CTrue | CPure _ ->
| CTrue | CPure _ | CFalse ->
true
| CMap (c, _) ->
ok c
@ -532,6 +537,10 @@ let rec solve : type a . loc:loc option -> a co -> a on_sol =
| CEq (v, w) ->
unify ~loc (uvar v) (uvar w);
On_sol (fun () -> ())
| CFalse ->
if not (G.is_consistent_env ()) then
raise (Error (loc, ContextNotAbsurd));
On_sol (fun () -> ())
| CAddEq (v1, v2, c) ->
G.enter_equality (uvar v1) (uvar v2);
let result = solve ~loc c in
@ -729,6 +738,9 @@ let (--) v1 v2 =
let (---) v t =
lift (--) v t
let absurd =
CFalse
let add_eq v1 v2 c =
CAddEq (v1, v2, c)

View File

@ -156,6 +156,8 @@ module Make
val add_eq: variable -> variable -> 'a co -> 'a co
val absurd: unit co
(* ---------------------------------------------------------------------- *)
(* Introducing type variables. *)
@ -423,6 +425,8 @@ module Make
the constraints [α. β. α = β] or [α. β. γ. α = β γ]
causes this error. *)
| ContextNotAbsurd
exception Error of loc option * error
(**[solve ~rectypes c] determines whether the constraint [c] is satisfiable,