diff --git a/coq-osiris/theories/lang/syntax.v b/coq-osiris/theories/lang/syntax.v
index 107823ea4f75bf9a167daeb2adce52c600c479d2..0b74046be3d252213cc19ab2a9b0a0df79adeac6 100644
--- a/coq-osiris/theories/lang/syntax.v
+++ b/coq-osiris/theories/lang/syntax.v
@@ -86,10 +86,9 @@ Inductive pat :=
(* A data constructor pattern in an ordinary algebraic data type. *)
| PData (c : data) (p : pat)
(* A data constructor pattern in an extensible algebraic data type.
- In [PXData (c, p)], the variable [c] appears free: it is not
- bound by this pattern. This variable is expected to denote a
- memory location, which serves as a dynamically-allocated name. *)
- | PXData (c : var) (p : pat)
+ In [PXData (π, p)], the path [π] is expected to denote a memory
+ location, which serves as a dynamically-allocated name. *)
+ | PXData (π : path) (p : pat)
(* A record pattern. *)
| PRecord (fps : list (field * pat))
(* A literal integer pattern. *)
@@ -172,7 +171,7 @@ Inductive expr :=
(* Data constructor application: [A (e)]. *)
(* Every data constructor is considered unary. *)
| EData (c : data) (e : expr)
- | EXData (c : var) (e : expr)
+ | EXData (π : path) (e : expr)
(* Record construction: [{ fs = es }]. *)
| ERecord (fes : list fexpr)
diff --git a/coq-osiris/theories/semantics/eval.v b/coq-osiris/theories/semantics/eval.v
index 9378189e935ffa43b0b0d0f1b4ead1c21c916254..371bbe8927f0a73299a9defda6f19ad046cec9dd 100644
--- a/coq-osiris/theories/semantics/eval.v
+++ b/coq-osiris/theories/semantics/eval.v
@@ -451,11 +451,11 @@ Fixpoint extend δ p v : micro env unit :=
match. If the data constructors do not match, a meta-level exception
is raised. *)
if c =? c' then extend δ p v else throw ()
- | PXData c p, VXData l v =>
+ | PXData π p, VXData l v =>
(* A data pattern for an extensible data type matches a data value, provided
the data constructors correspond to the same location in the environment.
If the data constructors do not match, a meta-level exception is raised. *)
- l' ← as_loc (widen (lookup_name δ c)) ;
+ l' ← as_loc (widen (lookup_path δ π)) ;
if (locations.eqb l l') then extend δ p v else throw()
| PRecord fps, VRecord fvs =>
(* A record pattern matches a record value. *)
@@ -1062,8 +1062,8 @@ Fixpoint eval η e {struct e} : microvx :=
| EData c e =>
v ← eval η e ;
ret (VData c v)
- | EXData c e =>
- l ← as_loc (widen (lookup_name η c)) ;
+ | EXData π e =>
+ l ← as_loc (widen (lookup_path η π)) ;
v ← eval η e ;
ret (VXData l v)
| ERecord fes =>
diff --git a/coq-osiris/theories/semantics/evalprime.v b/coq-osiris/theories/semantics/evalprime.v
index 4e71222041da6671a0165e938ef19a968f161772..286f4f30e9643d59f8ed2c3f79e4ff02a1d50584 100644
--- a/coq-osiris/theories/semantics/evalprime.v
+++ b/coq-osiris/theories/semantics/evalprime.v
@@ -38,8 +38,8 @@ Definition eval' η e : microvx :=
| EData c e =>
v ← eval η e ;
ret (VData c v)
- | EXData c e =>
- l ← as_loc (widen (lookup_name η c)) ;
+ | EXData π e =>
+ l ← as_loc (widen (lookup_path η π)) ;
v ← eval η e ;
ret (VXData l v)
| ERecord fes =>
diff --git a/coq-osiris/theories/test/test.v b/coq-osiris/theories/test/test.v
index 918dd45623fb892c9da86e2611b3dfd1e262d1a1..b149a9437245e5773949a259e7792cbd9100f516 100644
--- a/coq-osiris/theories/test/test.v
+++ b/coq-osiris/theories/test/test.v
@@ -444,7 +444,7 @@ Notation "'cont'" := (K _).
Lemma test_handle_nocont :
let e :=
- EPerform (EXData "Choose" (ETuple []))
+ EPerform (EXData ["Choose"] (ETuple []))
in
let m :=
EMatch e
@@ -456,7 +456,7 @@ Proof. reduces. Qed.
Lemma test_handle :
let e :=
- EPerform (EXData "Choose" (ETuple []))
+ EPerform (EXData ["Choose"] (ETuple []))
in
let m :=
EMatch e
@@ -474,7 +474,7 @@ Proof. reduces. Qed.
Lemma test_handle_compute_head :
let e :=
- (21 + EPerform (EXData "Choose" (ETuple [])))%expr
+ (21 + EPerform (EXData ["Choose"] (ETuple [])))%expr
in
let m :=
EMatch e
@@ -492,7 +492,7 @@ Proof. reduces. Qed.
Lemma test_handle_compute_branch :
let e :=
- (20 + EPerform (EXData "Choose" (ETuple [])))%expr
+ (20 + EPerform (EXData ["Choose"] (ETuple [])))%expr
in
let m :=
EMatch e
@@ -512,7 +512,7 @@ Proof. reduces. Qed.
Lemma test_handle_reinstall_ret :
let e1 :=
- EPerform (EXData "Choose" (ETuple []))
+ EPerform (EXData ["Choose"] (ETuple []))
in
let e2 :=
EMatch e1
@@ -537,17 +537,17 @@ Proof. reduces. Qed.
Lemma test_handle_exception :
let e :=
- EPerform (EXData "Choose" (ETuple []))
+ EPerform (EXData ["Choose"] (ETuple []))
in
let m :=
EMatch e
[ (* | effect _, k -> discontinue k Not_found *)
Branch
(CEff PAny (PVar "k"))
- (EDiscontinue (EVar "k") (EXData "Not_found" (ETuple [])));
+ (EDiscontinue (EVar "k") (EXData ["Not_found"] (ETuple [])));
(* | exception Not_found -> 42 *)
Branch
- (CExc (PXData "Not_found" (PTuple [])))
+ (CExc (PXData ["Not_found"] (PTuple [])))
(EInt 42)]
in
∃ n σ, steps n (∅, eval [("Not_found", (VLoc (Loc 1)));
@@ -557,7 +557,7 @@ Proof. reduces. Qed.
Lemma test_shallow_handle :
let η := [("Choose", (VLoc (Loc 0)))] in
let e :=
- EPerform (EXData "Choose" (ETuple []))
+ EPerform (EXData ["Choose"] (ETuple []))
in
let m :=
Handle (eval η e)
@@ -574,14 +574,14 @@ Lemma test_nested_handlers :
let η := [("Get22", (VLoc (Loc 22))); ("Get20", (VLoc (Loc 20)))] in
let e :=
ELet1 (PVar "y")
- (EPerform (EXData "Get20" (ETuple [])))
- (EVar "y" + EPerform (EXData "Get22" (ETuple [])))%expr
+ (EPerform (EXData ["Get20"] (ETuple [])))
+ (EVar "y" + EPerform (EXData ["Get22"] (ETuple [])))%expr
in
let m1 :=
EMatch e
[ (* | effect Get22, k -> continue k 22 *)
Branch
- (CEff (PXData "Get22" (PTuple [])) (PVar "k"))
+ (CEff (PXData ["Get22"] (PTuple [])) (PVar "k"))
(EContinue (EVar "k") (EInt 22));
(* | x -> x *)
Branch (CVal (PVar "x")) (EVar "x") ]
@@ -590,7 +590,7 @@ Lemma test_nested_handlers :
EMatch m1
[ (* | effect Get20, k -> continue k 20 *)
Branch
- (CEff (PXData "Get20" (PTuple [])) (PVar "k"))
+ (CEff (PXData ["Get20"] (PTuple [])) (PVar "k"))
(EContinue
(EVar "k")
(EInt 20));
@@ -603,13 +603,13 @@ Proof. intros. subst e m1 m2. reduces. Qed.
Lemma test_repeat_handle :
let η := [("Get21", (VLoc (Loc 21)))] in
let e :=
- (EPerform (EXData "Get21" (ETuple [])) + EPerform (EXData "Get21" (ETuple [])))%expr
+ (EPerform (EXData ["Get21"] (ETuple [])) + EPerform (EXData ["Get21"] (ETuple [])))%expr
in
let m :=
EMatch e
[ (* | effect Get21, k -> continue k 21 *)
Branch
- (CEff (PXData "Get21" (PTuple [])) (PVar "k"))
+ (CEff (PXData ["Get21"] (PTuple [])) (PVar "k"))
(EContinue (EVar "k") (EInt 21));
(* | x -> x *)
Branch
@@ -622,15 +622,15 @@ Proof. reduces. Qed.
Lemma test_shallow_ret_reinstall :
let η := [("Get32", (VLoc (Loc 32))); ("Get10", (VLoc (Loc 10)))] in
let e := (ELet1 (PVar "x")
- (EPerform (EXData "Get32" (ETuple [])))
- (EVar "x" + EPerform (EXData "Get10" (ETuple []))))%expr
+ (EPerform (EXData ["Get32"] (ETuple [])))
+ (EVar "x" + EPerform (EXData ["Get10"] (ETuple []))))%expr
in
let m1 :=
Handle (eval η e)
(λ o, shallow_eval_match η o
[ (* | effect Get10, k -> continue k 10 *)
Branch
- (CEff (PXData "Get10" (PTuple [])) (PVar "k"))
+ (CEff (PXData ["Get10"] (PTuple [])) (PVar "k"))
(EContinue (EVar "k") (EInt 10))])
in
let m2 :=
@@ -638,7 +638,7 @@ Lemma test_shallow_ret_reinstall :
(λ o, deep_eval_match η o
[ (* | effect Get32, k -> continue k 32 *)
Branch
- (CEff (PXData "Get32" (PTuple [])) (PVar "k"))
+ (CEff (PXData ["Get32"] (PTuple [])) (PVar "k"))
(EContinue (EVar "k") (EInt 32));
(* | x -> x *)
Branch (CVal (PVar "x")) (EVar "x")])
diff --git a/coq-osiris/tutorial/tutorial.html b/coq-osiris/tutorial/tutorial.html
index 7db483051acce91b80953fb5ccbb184a1b349e22..95fa5dccf2d43ade67d7df54b1fda136514dff55 100644
--- a/coq-osiris/tutorial/tutorial.html
+++ b/coq-osiris/tutorial/tutorial.html
@@ -37,7 +37,7 @@ two syntactic categories, <em>patterns</em> and <em>expressions</em>.</p>
| POr : pat → pat → pat
| PTuple : list pat → pat
| PData : data → pat → pat
- | PXData : var → pat → pat
+ | PXData : path → pat → pat
| PRecord : list (<span class="bp">field</span> * pat) → pat
| PInt : Z → pat
| PChar : char → pat
@@ -48,7 +48,7 @@ two syntactic categories, <em>patterns</em> and <em>expressions</em>.</p>
<span class="kn">Arguments</span> POr p1 p2
<span class="kn">Arguments</span> PTuple ps%list_scope
<span class="kn">Arguments</span> PData c p
-<span class="kn">Arguments</span> PXData c p
+<span class="kn">Arguments</span> PXData π p
<span class="kn">Arguments</span> PRecord fps%list_scope
<span class="kn">Arguments</span> PInt i%Z_scope
<span class="kn">Arguments</span> PChar c
@@ -60,7 +60,7 @@ two syntactic categories, <em>patterns</em> and <em>expressions</em>.</p>
| EApp : expr → expr → expr
| ETuple : list expr → expr
| EData : data → expr → expr
- | EXData : var → expr → expr
+ | EXData : path → expr → expr
| ERecord : list fexpr → expr
| ERecordUpdate : expr → list fexpr → expr
| ERecordAccess : expr → <span class="bp">field</span> → expr
@@ -136,7 +136,7 @@ two syntactic categories, <em>patterns</em> and <em>expressions</em>.</p>
<span class="kn">Arguments</span> EApp e1 e2
<span class="kn">Arguments</span> ETuple es%list_scope
<span class="kn">Arguments</span> EData c e
-<span class="kn">Arguments</span> EXData c e
+<span class="kn">Arguments</span> EXData π e
<span class="kn">Arguments</span> ERecord fes%list_scope
<span class="kn">Arguments</span> ERecordUpdate e fes%list_scope
<span class="kn">Arguments</span> ERecordAccess e f
diff --git a/osiris/src/Coqify.ml b/osiris/src/Coqify.ml
index 85d678434b5f14af21085f4b7f6db3e6647b8e09..2f84830131f232c0cad32206e058b2d33df4384e 100644
--- a/osiris/src/Coqify.ml
+++ b/osiris/src/Coqify.ml
@@ -31,6 +31,9 @@ let data =
let field =
quote
+let path (pi : path) : expression =
+ list (map var pi)
+
(* -------------------------------------------------------------------------- *)
(* Integer literals. *)
@@ -96,8 +99,8 @@ let rec pat (p : pat) =
| PData (d, p) ->
c "PData" [ data d; pat p ]
- | PXData (d, p) ->
- c "PXData" [ data d; pat p ]
+ | PXData (pi, p) ->
+ c "PXData" [ path pi; pat p ]
| PRecord fps ->
c "PRecord" [ fpats fps ]
@@ -165,7 +168,7 @@ let rec expr (e : expr) =
c "EUnsupported" []
| EPath pi ->
- clist "EPath" (map var pi)
+ c "EPath" [path pi]
| EAnonFun a ->
c "EAnonFun" [ cut "fun" (anonfun a) ]
@@ -179,8 +182,8 @@ let rec expr (e : expr) =
| EData (d, e) ->
c "EData" [ data d; expr e ]
- | EXData (d, e) ->
- c "EXData" [ data d; expr e ]
+ | EXData (pi, e) ->
+ c "EXData" [ path pi; expr e ]
| ERecord fs ->
c "ERecord" [ fexprs fs ]
@@ -408,7 +411,7 @@ and mexpr (me : mexpr) =
c "MUnsupported" []
| MPath pi ->
- clist "MPath" (map var pi)
+ c "MPath" [path pi]
| MStruct items ->
clist "MStruct" (structure_items items)
diff --git a/osiris/src/Syntax.ml b/osiris/src/Syntax.ml
index 315527ced0770d0989178603e5f699bd570b1549..932decbaac067e80ed209a08075d8ec06d01b7d7 100644
--- a/osiris/src/Syntax.ml
+++ b/osiris/src/Syntax.ml
@@ -63,10 +63,9 @@ type pat =
In [PData (d, p)], the data constructor [d] is a fixed string. *)
| PData of data * pat
(* A data constructor pattern in an extensible algebraic data type.
- In [PXData (c, p)], the variable [c] appears free: it is not
- bound by this pattern. This variable is expected to denote a
- memory location, which serves as a dynamically-allocated name. *)
- | PXData of var * pat
+ In [PXData (π, p)], the path [π] is expected to denote a memory
+ location, which serves as a dynamically-allocated name. *)
+ | PXData of path * pat
(* A record pattern. *)
| PRecord of fpats
(* A literal integer pattern. *)
@@ -161,7 +160,7 @@ type expr =
(* Data constructor application: [A (e)]. *)
(* Every data constructor is considered unary. *)
| EData of data * expr
- | EXData of var * expr
+ | EXData of path * expr
(* Record construction: [{ fs = es }]. *)
| ERecord of fexprs
diff --git a/osiris/src/Translate.ml b/osiris/src/Translate.ml
index f034c5fb021bbe09b346d887636c43be574ce423..ab8588b66f2c65e0564f375d8e6e2e05cf78f9a9 100644
--- a/osiris/src/Translate.ml
+++ b/osiris/src/Translate.ml
@@ -181,14 +181,12 @@ let debug_ident kind path id =
debug " path = %s\n" (show_path path)
let translate_exp_ident path id : path =
- let id = txt id in
debug_ident "Texp_ident" path id;
(* For the moment, we ignore [path] and keep [id]. However, [path]
could be used to identify references to the OCaml standard library. *)
translate_longident id
let translate_mod_ident path id : path =
- let id = txt id in
debug_ident "Tmod_ident" path id;
translate_longident id
@@ -297,11 +295,12 @@ let rec translate_pat (pat: pattern) : pat =
| Tpat_construct (id, constructor_desc, pats, _optional_type_annotation) ->
(* An OCaml data constructor application is always translated as an
application of the data constructor to a tuple of its arguments. *)
- let data = translate_data_constructor id constructor_desc in
+ let tuple = PTuple (translate_pats pats) in
if is_extensible constructor_desc then
- PXData (data, PTuple (translate_pats pats))
+ PXData (translate_longident (txt id), tuple)
else
- PData (data, PTuple (translate_pats pats))
+ let data = translate_data_constructor id constructor_desc in
+ PData (data, tuple)
| Tpat_variant _ ->
punsupported loc "polymorphic variant pattern"
@@ -367,7 +366,7 @@ let rec translate_expr (e: expression) : expr =
match e.exp_desc with
| Texp_ident (path, id, _) ->
- EPath (translate_exp_ident path id)
+ EPath (translate_exp_ident path (txt id))
| Texp_constant c ->
translate_exp_constant loc c
@@ -405,11 +404,14 @@ let rec translate_expr (e: expression) : expr =
ETuple (translate_exprs es)
| Texp_construct (id, constructor_desc, es) ->
- let data = translate_data_constructor id constructor_desc in
+ (* An OCaml data constructor application is always translated as an
+ application of the data constructor to a tuple of its arguments. *)
+ let tuple = ETuple (translate_exprs es) in
if is_extensible constructor_desc then
- EXData (data, ETuple (translate_exprs es))
+ EXData (translate_longident (txt id), tuple)
else
- EData (data, ETuple (translate_exprs es))
+ let data = translate_data_constructor id constructor_desc in
+ EData (data, tuple)
| Texp_variant _ ->
eunsupported loc "polymorphic variant"
@@ -1002,7 +1004,7 @@ and translate_mod_expr (me : module_expr) : mexpr =
match me.mod_desc with
| Tmod_ident (path, id) ->
- MPath (translate_mod_ident path id)
+ MPath (translate_mod_ident path (txt id))
| Tmod_structure str ->
translate_structure str