Commit 97661837 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Use abstract labels instead of explicit strings

parent 8ca37b4e
......@@ -44,7 +44,8 @@ def Expr := dk_obj.Expr.
(; Not really an encodding of naturals but just a concrete type in wich
we declare two distinct constants 42 and 24. ;)
def nat_ : type := type_cons "nat_label" type_nil type_nil.
def nat_label : label.
def nat_ : type := type_cons nat_label type_nil type_nil.
def Nat := Expr nat_.
_42 : Nat.
_24 : Nat.
......@@ -52,11 +53,11 @@ _24 : Nat.
(; Booleans ;)
def l_if : label := "if".
def l_if : label.
def l_then : label := "then".
def l_then : label.
def l_else : label := "else".
def l_else : label.
def boolT : A : type -> type
:=
......@@ -134,9 +135,9 @@ def test2 :=
(; Lambda-calculus ;)
def l_arg : label := "arg".
def l_arg : label.
def l_val : label := "val".
def l_val : label.
def arrow : type -> type -> type
:=
......@@ -205,14 +206,14 @@ def test3 :=
(; Points and color points ;)
def l_x := "x".
def l_y := "y".
def l_x : label.
def l_y : label.
def point :=
type_cons l_x nat_ (type_cons l_y nat_ type_nil).
def Point := Expr point.
def l_c := "c".
def l_c : label.
color : type.
def Color := Expr color.
......@@ -245,9 +246,9 @@ def test4 : Nat := dk_obj_dec.select point myPoint l_x.
(; Subtyping example ;)
def l_get := "get".
def l_set := "set".
def l_contents := "contents".
def l_get : label.
def l_set : label.
def l_contents : label.
(; Storage cells ;)
......@@ -363,7 +364,7 @@ def test8 := dk_obj_dec.select
(; Classes ;)
def l_new : label := "new".
def l_new : label.
(; def filtermaptype : (label -> dk_bool.Bool) -> ;)
(; (type -> type) -> ;)
......
......@@ -56,9 +56,9 @@ let print_label out_fmter (Label l) = Format.fprintf out_fmter "lab_%s" l
let compile_string out_fmter = Format.fprintf out_fmter "\"%s\""
let declare_label out_fmter (Label l) =
Format.fprintf out_fmter "@[<h>def lab_%s@ := %a.@]@."
Format.fprintf out_fmter "@[<h>def lab_%s@ : string.@]@."
l
compile_string l
(* compile_string l *)
let declare_labels out_fmter = List.iter (declare_label out_fmter)
......
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