'define' instead of 'def' in Modlog

bobatkey · Aug 21, 2017 · 9635edb · 9635edb
1 parent 657c6b1
commit 9635edb
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 17 deletions.
diff --git a/expr.mlog b/expr.mlog
@@ -37,19 +37,19 @@ module ExprGrammar = struct
 
   type rhs = [ `E1_0 | `E1_1 | `E2_0 | `E2_1 | `E2_2 | `E2_3 ]
 
-  def nt_to_rhs : non_terminal * rhs
+  define nt_to_rhs : non_terminal * rhs
       nt_to_rhs (`E, `E1_0)
       nt_to_rhs (`E, `E2_0)
 
-  def rhs_tok : rhs * token * rhs
+  define rhs_tok : rhs * token * rhs
       rhs_tok (`E1_0, `x, `E1_1)
       rhs_tok (`E2_1, `plus, `E2_2)
 
-  def rhs_nt : rhs * non_terminal * rhs
+  define rhs_nt : rhs * non_terminal * rhs
       rhs_nt (`E2_0, `E, `E2_1)
       rhs_nt (`E2_2, `E, `E2_3)
 
-  def rhs_stop : rhs
+  define rhs_stop : rhs
       rhs_stop (`E1_1)
       rhs_stop (`E2_3)
 end
@@ -61,7 +61,7 @@ struct
   (* parse (i, nt, j) if the symbol 'nt' is recognised between 'i' and
   'j' in the input. *)
 
-  def
+  define
     parse : I.index * G.non_terminal * I.index
     parse (?i, ?nt, ?j) :-
       G.nt_to_rhs (?nt, ?rhs), parse_rhs (?i, ?rhs, ?j)
@@ -78,7 +78,7 @@ struct
        G.rhs_nt (?rhs, ?nt, ?rhs'),
        parse (?i, ?nt, ?i'), parse_rhs (?i', ?rhs', ?j)
 
-  def
+  define
     parse_between : I.index * I.index
     parse_between (?i, ?j) :- parse (?i, G.start, ?j)
 
@@ -89,13 +89,13 @@ module TestInput = struct
 
   type token = [`x | `plus]
 
-  def is_index : index
+  define is_index : index
       is_index (0)
       is_index (1)
       is_index (2)
       is_index (3)
 
-  def token_at : index * token * index
+  define token_at : index * token * index
       token_at (0,`x,1)
       token_at (1,`plus,2)
       token_at (2,`x,3)

diff --git a/modlog/core_syntax.ml b/modlog/core_syntax.ml
@@ -176,7 +176,7 @@ module Make (Names : Modules.Syntax.NAMES) = struct
     | [] -> ()
     | decl :: decls ->
        Format.pp_open_vbox pp 0;
-       Format.fprintf pp "def %a" pp_decl decl;
+       Format.fprintf pp "define %a" pp_decl decl;
        List.iter (Format.fprintf pp "@ @,and %a" pp_decl) decls;
        Format.pp_close_box pp ()
 

diff --git a/modlog/datalog_grammar.mly b/modlog/datalog_grammar.mly
@@ -7,7 +7,7 @@ open Syntax.Mod
 %token COLON_DASH
 %token COLON
 %token STAR DOT ARROW EQUALS BAR UNDERSCORE
-%token MODULE TYPE STRUCT SIG END FUNCTOR INT AND DEF CONSTANT WITH
+%token MODULE TYPE STRUCT SIG END FUNCTOR INT AND DEFINE CONSTANT WITH
 %token LPAREN RPAREN LBRACE RBRACE
 %token<int32> INT_LITERAL
 %token<string> IDENT ENUM_IDENT MV_IDENT
@@ -87,7 +87,7 @@ pred_decl:
 
 %public
 str_value:
-| DEF; d=pred_decl; ds=list(AND; d=pred_decl {d})
+| DEFINE; d=pred_decl; ds=list(AND; d=pred_decl {d})
     { PredicateDefs (d :: ds) }
 | CONSTANT; name=IDENT; COLON; ty=domain_type; EQUALS; e=expr
     { ConstantDef { const_loc  = Location.mk $startpos $endpos

diff --git a/modlog/lexer.mll b/modlog/lexer.mll
@@ -21,7 +21,7 @@ rule token = parse
 | "functor"  { FUNCTOR }
 | "int"      { INT }
 | "and"      { AND }
-| "def"      { DEF }
+| "define"   { DEFINE }
 | "constant" { CONSTANT }
 | "with"     { WITH }
 | '('        { LPAREN }

diff --git a/paths2.mlog b/paths2.mlog
@@ -7,18 +7,17 @@ end
 module MyEdges = struct
   type vertex = int
 
-  def
-    edge : vertex * vertex
+  define edge : vertex * vertex
     edge(1, 2)
     edge(2, 3)
+    edge(3, 4)
 end
 
-module Path = functor (E : Edges) -> struct
+module Path (E : Edges) = struct
 
   type vertex = E.vertex
 
-  def
-    path : E.vertex * E.vertex
+  define path : E.vertex * E.vertex
     path(?X,?Y) :- E.edge(?X,?Y)
     path(?X,?Z) :- path(?X,?Y), E.edge(?Y,?Z)