[wip] TOYML

elpi.opam

@@ -24,6 +24,7 @@ depends: [
   "cmdliner" {with-test}
   "dune" {>= "1.6"}
   "conf-time" {with-test}
+  "ppx_import" {with-test}
 ]
 synopsis: "ELPI - Embeddable λProlog Interpreter"
 description: """

tests/sources/toyml/ast.ml

@@ -0,0 +1,31 @@
+type pos = [%import: Lexing.position] [@@deriving show, ord, eq]
+type position = pos * pos [@@deriving show, ord, eq]
+
+type term =
+ | Const of string (* global name  or  bound variable *)
+ | Int of int      (* literals *)
+ | App of ast * ast
+ | Lam of string * ast
+ | Let of string * ast * ast
+ | Eq  of ast * ast
+and ast = { loc : position; v : term }
+[@@deriving show]
+
+type tye =
+ | Var of string
+ | Integer
+ | Boolean
+ | Arrow of tye * tye
+ | List of tye
+ | Pair of tye * tye
+[@@deriving show]
+
+type quantification =
+ | Any
+ | EqualityType
+[@@deriving show]
+
+type typ =
+ | All of string * quantification * typ
+ | Mono of tye
+[@@deriving show]

tests/sources/toyml/dune

@@ -0,0 +1,8 @@
+(executable
+    (name toyml)
+    (modules ast lexer parser pmap toyml)
+    (preprocess (per_module ((pps ppx_import ppx_deriving.std) ast)))
+    (libraries elpi ppx_import ppx_deriving.std))
+
+(ocamllex lexer)
+(ocamlyacc parser)

tests/sources/toyml/input

@@ -0,0 +1,10 @@
+3 = 2
+(fun x -> x) = (fun x -> x)
+let id x = x in id []
+let id x = x in (id [], id 1)
+let refl x = x = x in refl []
+let refl x = x = x in refl (fun x -> x)
+let card x = size (undup x) in card []
+let f y = let g x = (x,y) in g y in f 1
+size 1
+[1] = (1,1)

tests/sources/toyml/lexer.mll

@@ -0,0 +1,21 @@
+(* File lexer.mll *)
+{
+open Parser        (* The type token is defined in parser.mli *)
+exception Eof
+}
+rule token = parse
+    [' ' '\t' '\n']     { token lexbuf }     (* skip blanks *)
+  | ['0'-'9']+ as lxm { INT(int_of_string lxm) }
+  | "let"            { LET }
+  | "in"           { IN }
+  | "fun"           { LAM }
+  | ['a'-'z']+ as lxm  { IDENT lxm }
+  | '('            { LPAREN }
+  | ')'            { RPAREN }
+  | '['            { LBRK }
+  | ']'            { RBRK }
+  | '='            { EQ }
+  | ','            { COMMA }
+  | ';'            { SEMICOLON }
+  | "->"            { ARROW }
+  | eof            { EOF }

tests/sources/toyml/output

@@ -0,0 +1,136 @@
+
+========= builtins ==========
+
+
+external pred type-error % raise a fatal type inference error
+  i:any, % the term
+  i:any, % its type
+  i:any. % the type expected by its context
+
+external pred eqtype-error % raise a fatal equality type error
+  i:any. % the term
+
+
+
+
+
+============= W: 3 = 2 ==============
+The term:
+  3 = 2
+  ^^^^^
+has type: mono boolean
+
+
+============= W: (fun x -> x) = (fun x -> x) ==============
+The term:
+  (fun x -> x) = (fun x -> x)
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+has type: mono boolean
+
+Equality type constraint unsatisfied at:
+  (fun x -> x) = (fun x -> x)
+   ^^^^^^^^^^                
+
+============= W: let id x = x in id [] ==============
+The term:
+  let id x = x in id []
+  ^^^^^^^^^^^^^^^^^^^^^
+has type: mono (list X0)
+
+The term:
+  let id x = x in id []
+         ^^^^^         
+has type: all any c0 \ mono (c0 ==> c0)
+
+
+============= W: let id x = x in (id [], id 1) ==============
+The term:
+  let id x = x in (id [], id 1)
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+has type: mono (pair (list X1) integer)
+
+The term:
+  let id x = x in (id [], id 1)
+         ^^^^^                 
+has type: all any c0 \ mono (c0 ==> c0)
+
+
+============= W: let refl x = x = x in refl [] ==============
+The term:
+  let refl x = x = x in refl []
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+has type: mono boolean
+
+The term:
+  let refl x = x = x in refl []
+           ^^^^^^^^^           
+has type: all eqt c0 \ mono (c0 ==> boolean)
+
+
+============= W: let refl x = x = x in refl (fun x -> x) ==============
+The term:
+  let refl x = x = x in refl (fun x -> x)
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+has type: mono boolean
+
+The term:
+  let refl x = x = x in refl (fun x -> x)
+           ^^^^^^^^^                     
+has type: all eqt c0 \ mono (c0 ==> boolean)
+
+Equality type constraint unsatisfied at:
+  let refl x = x = x in refl (fun x -> x)
+                        ^^^^             
+
+============= W: let card x = size (undup x) in card [] ==============
+The term:
+  let card x = size (undup x) in card []
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+has type: mono integer
+
+The term:
+  let card x = size (undup x) in card []
+           ^^^^^^^^^^^^^^^^^^           
+has type: all eqt c0 \ mono (list c0 ==> integer)
+
+
+============= W: let f y = let g x = (x,y) in g y in f 1 ==============
+The term:
+  let f y = let g x = (x,y) in g y in f 1
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+has type: mono (pair integer integer)
+
+The term:
+  let f y = let g x = (x,y) in g y in f 1
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^       
+has type: all any c0 \ mono (c0 ==> pair c0 c0)
+
+The term:
+  let f y = let g x = (x,y) in g y in f 1
+                  ^^^^^^^^^              
+has type: all any c0 \ mono (c0 ==> pair c0 X2)
+
+
+============= W: size 1 ==============
+The term:
+  size 1
+  ^^^^^^
+has type: mono integer
+
+Type error:
+  size 1
+       ^
+has type integer
+but is expected to have type list X3
+
+============= W: [1] = (1,1) ==============
+The term:
+  [1] = (1,1)
+  ^^^^^^^^^^^
+has type: mono boolean
+
+Type error:
+  [1] = (1,1)
+          ^  
+has type X4 ==> X5 ==> pair X4 X5
+but is expected to have type X6 ==> X7 ==> list integer

tests/sources/toyml/parser.mly

@@ -0,0 +1,54 @@
+    /* File parser.mly */
+    %{
+open Ast
+            let mkloc i j = (Parsing.rhs_start_pos i, Parsing.rhs_end_pos j)
+            let rec mklam = function
+              | [] -> fun x -> x
+              | (loc,x)::xs -> fun b -> { loc = (fst loc, snd b.loc); v = Lam(x,mklam xs b) }
+            let rec mklist loc = function
+                    | [] -> { loc; v = Const "[]" }
+              | (loc,x) :: xs -> { loc; v = App( { loc; v = App( { loc; v = Const "::" }, x) }, mklist loc xs) }
+            %}
+        %token <int> INT
+        %token <string> IDENT
+        %token LET IN LAM ARROW
+        %token LPAREN RPAREN EQ LBRK RBRK COMMA SEMICOLON
+        %token EOF
+        %start main             /* the entry point */
+        %type <Ast.ast> main
+        %%
+        main: term EOF { $1 } ;
+
+        term0:
+          | INT                     { { loc = mkloc 1 1;
+                                        v = Int $1 }}
+          | LPAREN term RPAREN      { $2 }
+          | LPAREN term COMMA term RPAREN      
+              { { loc = mkloc 1 5; v = App( { loc = mkloc 1 3; v = App({ loc = mkloc 3 3; v = Const "," } ,$2) }, $4 ) } }
+          | LBRK term_list RBRK { mklist (mkloc 1 3) $2 }
+          | IDENT { { loc = mkloc 1 1; v = Const $1 } }
+        ;
+
+        term_list:
+          | term SEMICOLON term_list { (mkloc 1 2, $1) :: $3 }
+          | term { [(mkloc 1 1, $1)] }
+          | { [] }
+          ;
+
+        term:
+          | LET idlist EQ term IN term { { loc = mkloc 1 6; v = Let(snd (List.hd $2),mklam (List.tl $2) $4,$6) }}
+          | LAM IDENT ARROW term { { loc = mkloc 1 4; v = Lam($2,$4) }}
+          | term EQ term { { loc = mkloc 1 3; v = Eq($1,$3) } }
+          | app { $1 }
+          ;
+        app:      
+          | app term0 { { loc = mkloc 1 2; v = App($1,$2) } }
+          | term0 { $1 }
+          ;
+
+        idlist:
+          | IDENT { [(mkloc 1 1, $1)] }
+          | IDENT idlist { (mkloc 1 2, $1) :: $2 }
+          ;
+
+

tests/sources/toyml/pmap.ml

@@ -0,0 +1,28 @@
+module type T = sig
+  type t
+  val hash : t -> int
+end
+
+module Make(X : T) = struct
+  module M = Map.Make(struct
+    type t = int
+    let compare x y = x - y
+  end)
+  type 'a t = (X.t * 'a) list M.t
+  let empty = M.empty
+  let add k v m =
+    let h = X.hash k in
+    try
+      let l = M.find h m in
+      let l = List.remove_assq k l in
+      M.add h ((k,v) :: l) m
+    with Not_found ->
+      M.add h [k,v] m
+  let find_opt k m =
+    try
+      let h = Hashtbl.hash k in
+      let l = M.find h m in
+      Some (List.assq k l)
+    with Not_found -> None
+
+end