Base parser

Relates to #2

.merlin

@@ -7,4 +7,5 @@ FLG -rectypes
 FLG -w a
 
 PKG batteries
+PKG menhirLib
 PKG num

_tags

@@ -3,10 +3,11 @@ true : debug
 true : warn_a
 true : -traverse
 true : bin_annot
+true : use_menhir, menhir_explain
 
 # --------------------------------------------------------------------
 <src> : include
 
 # --------------------------------------------------------------------
-<src/*.{ml,mli}> : package(batteries,num)
-<tests/*.{ml,mli}> : package(batteries,num)
+<src/*.{ml,mli}> : package(batteries,menhirLib,num)
+<tests/*.{ml,mli}> : package(batteries,menhirLib,num)

src/utils.ml → src/core.ml

@@ -1,50 +1,53 @@
 (* -------------------------------------------------------------------- *)
-let rec itlist f l b =
-  match l with
-    [] -> b
-  | (h::t) -> f h (itlist f t b);;
-
 let rec lexord ord l1 l2 =
   match (l1,l2) with
-    (h1::t1,h2::t2) -> if ord h1 h2 then List.length t1 = List.length t2
-                       else h1 = h2 && lexord ord t1 t2
-  | _ -> false;;
+  | (h1::t1,h2::t2) ->
+      if   ord h1 h2
+      then List.length t1 = List.length t2
+      else h1 = h2 && lexord ord t1 t2
+  | _ -> false
 
 
 let rec lexord_lt ord l1 l2 =
   match (l1,l2) with
-    ([],[]) -> false
-   |([],_) -> true
-   |(_,[]) -> false
-   | (h1::t1,h2::t2) -> if ord h1 h2 then true
-                       else h1 = h2 && lexord_lt ord t1 t2;;
+   | ([],[]) -> false
+   | ([],_ ) -> true
+   | (_ ,[]) -> false
 
-let rec distinctpairs l =
-  match l with
-   x::t -> itlist (fun y a -> (x,y) :: a) t (distinctpairs t)
-  | [] -> [];;
+   | (h1::t1,h2::t2) ->
+       if   ord h1 h2
+       then true
+       else h1 = h2 && lexord_lt ord t1 t2
 
 (* -------------------------------------------------------------------- *)
 include BatPervasives
 
 (* -------------------------------------------------------------------- *)
-module String = BatString
-module Int    = BatInt
-module Ord    = BatOrd
-module Set    = BatSet
-module Map    = BatMap
-module Num    = BatNum
-module Opt    = BatOption
+module String  = BatString
+module Int     = BatInt
+module Ord     = BatOrd
+module Set     = BatSet
+module Map     = BatMap
+module Num     = BatNum
+module Opt     = BatOption
+module IO      = BatIO
+module Big_int = BatBig_int
 
 (* -------------------------------------------------------------------- *)
 module List : sig
   include module type of BatList
 
   val lex : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+  val product : 'a list -> ('a * 'a) list
 end = struct
   include BatList
 
   let lex = BatList.compare
+
+  let rec product (xs : 'a list) : ('a * 'a) list =
+    match xs with
+    | []   -> []
+    | x::t -> List.fold_right (fun y a -> (x, y) :: a) t (product t)
 end
 
 (* -------------------------------------------------------------------- *)
@@ -53,4 +56,3 @@ module Format = struct
 
   type 'a pp = Format.formatter -> 'a -> unit
 end
-

src/groebnerBasis.ml

@@ -2,7 +2,7 @@
 
 (* Imports and abbreviations *)
 
-open Utils
+open Core
 open Num.TaggedInfix
 open Monalg
 
@@ -111,7 +111,7 @@ let rec grobner priv basis pairs =
 (* ------------------------------------------------------------------------- *)
 
 let groebner priv basis =
-  grobner priv basis (distinctpairs basis)
+  grobner priv basis (List.product basis)
 
 let deduc priv basis secret =
 	let basis = groebner priv basis in

src/io.ml

@@ -0,0 +1,30 @@
+(* -------------------------------------------------------------------- *)
+open Core
+
+module P = Parser
+module L = Lexing
+
+(* -------------------------------------------------------------------- *)
+let parserfun_entry =
+    MenhirLib.Convert.Simplified.traditional2revised P.program
+
+(* -------------------------------------------------------------------- *)
+let lexbuf_from_channel = fun name channel ->
+  let lexbuf = Lexing.from_channel (IO.to_input_channel channel) in
+    lexbuf.Lexing.lex_curr_p <- {
+        Lexing.pos_fname = name;
+        Lexing.pos_lnum  = 1;
+        Lexing.pos_bol   = 0;
+        Lexing.pos_cnum  = 0
+      };
+    lexbuf
+
+(* -------------------------------------------------------------------- *)
+let lexer (lexbuf : L.lexbuf) =
+  let token = Lexer.main lexbuf in
+  (token, L.lexeme_start_p lexbuf, L.lexeme_end_p lexbuf)
+
+(* -------------------------------------------------------------------- *)
+let parse_program ?(name = "") (inc : IO.input) =
+  let reader = lexbuf_from_channel name inc in
+  parserfun_entry (fun () -> lexer reader)

src/io.mli

@@ -0,0 +1,2 @@
+(* -------------------------------------------------------------------- *)
+val parse_program : ?name:string -> Core.IO.input -> Syntax.pprogram

src/lexer.mll

@@ -0,0 +1,54 @@
+(* -------------------------------------------------------------------- *)
+{
+  open Core
+  open Parser
+
+  module L = Location
+
+  (* ------------------------------------------------------------------ *)
+  let lex_error lexbuf msg =
+    let loc = L.of_lexbuf lexbuf in
+    raise (Syntax.ParseError (Some loc, PE_LexicalError msg))
+
+  (* ------------------------------------------------------------------ *)
+  let _keywords = [
+    ("check", CHECK);
+    ("var"  , VAR  );
+  ]
+
+  (* ------------------------------------------------------------------ *)
+  let keywords =
+    let table = Hashtbl.create 0 in
+    List.iter (uncurry (Hashtbl.add table)) _keywords; table
+}
+
+let empty   = ""
+let blank   = [' ' '\t' '\r']
+let newline = '\n'
+let upper   = ['A'-'Z']
+let lower   = ['a'-'z']
+let letter  = upper | lower
+let digit   = ['0'-'9']
+let uint    = digit+
+let ichar   = (letter | digit | '_' | '\'')
+let ident   = (letter | '_') ichar*
+
+(* -------------------------------------------------------------------- *)
+rule main = parse
+  | newline       { Lexing.new_line lexbuf; main lexbuf }
+  | blank+        { main lexbuf }
+  | ident  as id  { try Hashtbl.find keywords id with Not_found -> IDENT id }
+  | digit+ as num { INT (Big_int.big_int_of_string num) }
+
+  | '+' { PLUS   }
+  | '*' { STAR   }
+  | '^' { HAT    }
+  | '(' { LPAREN }
+  | ')' { RPAREN }
+  | '{' { LBRACE }
+  | '}' { RBRACE }
+
+  | eof { EOF   }
+
+  | _ as c
+      { lex_error lexbuf (Printf.sprintf "illegal character: `%c'" c) }

src/libsolveq.mllib

@@ -1,4 +1,9 @@
-utils
-groebnerBasis
-nc_gasbi
-monalg
+Core
+Location
+Lexer
+Parser
+Syntax
+Io
+GroebnerBasis
+Nc_gasbi
+Monalg

src/location.ml

@@ -0,0 +1,85 @@
+(* -------------------------------------------------------------------- *)
+open Lexing
+
+(* -------------------------------------------------------------------- *)
+type t = {
+  loc_fname : string;
+  loc_start : int * int;
+  loc_end   : int * int;
+  loc_bchar : int;
+  loc_echar : int;
+}
+
+let _dummy : t = {
+  loc_fname = "";
+  loc_start = (-1, -1);
+  loc_end   = (-1, -1);
+  loc_bchar = -1;
+  loc_echar = -1;
+}
+
+(* -------------------------------------------------------------------- *)
+let make (p1 : position) (p2 : position) =
+  let mkpos (p : position) =
+    (p.pos_lnum, p.pos_cnum - p.pos_bol)
+  in
+    { loc_fname = p1.pos_fname;
+      loc_start = mkpos p1    ;
+      loc_end   = mkpos p2    ;
+      loc_bchar = p1.pos_cnum ;
+      loc_echar = p2.pos_cnum ; }
+
+let of_lexbuf (lb : lexbuf) =
+  let p1 = Lexing.lexeme_start_p lb in
+  let p2 = Lexing.lexeme_end_p lb in
+  make p1 p2
+
+(* --------------------------------------------------------------------- *)
+let merge (p1 : t) (p2 : t) =
+  { loc_fname = p1.loc_fname;
+    loc_start = min p1.loc_start p2.loc_start;
+    loc_end   = max p1.loc_end   p2.loc_end  ;
+    loc_bchar = min p1.loc_bchar p2.loc_bchar;
+    loc_echar = max p1.loc_echar p2.loc_echar; }
+
+let mergeall (p : t list) =
+  match p with
+  | []      -> _dummy
+  | t :: ts -> List.fold_left merge t ts
+
+let isdummy (p : t) =
+  p.loc_bchar < 0 || p.loc_echar < 0
+
+(* --------------------------------------------------------------------- *)
+let tostring (p : t) =
+  let spos =
+    if p.loc_start = p.loc_end then
+      Printf.sprintf "line %d (%d)"
+        (fst p.loc_start) (snd p.loc_start)
+    else if fst p.loc_start = fst p.loc_end then
+      Printf.sprintf "line %d (%d-%d)"
+        (fst p.loc_start) (snd p.loc_start) (snd p.loc_end)
+    else
+      Printf.sprintf "line %d (%d) to line %d (%d)"
+        (fst p.loc_start) (snd p.loc_start)
+        (fst p.loc_end  ) (snd p.loc_end  )
+  in
+
+  if p.loc_fname <> "" then
+    Printf.sprintf "%s: %s" p.loc_fname spos
+  else
+    spos
+
+(* -------------------------------------------------------------------- *)
+type 'a loced = { plloc : t; pldesc : 'a; }
+
+(* -------------------------------------------------------------------- *)
+let loc    x = x.plloc
+let unloc  x = x.pldesc
+let unlocs x = List.map unloc x
+
+let lmap (f : 'a -> 'b) (x : 'a loced) =
+  { x with pldesc = f x.pldesc }
+
+let mkloc (loc : t) (x : 'a) : 'a loced =
+  { plloc = loc; pldesc = x; }

src/location.mli

@@ -0,0 +1,30 @@
+(* -------------------------------------------------------------------- *)
+open Lexing
+
+(* -------------------------------------------------------------------- *)
+type t = {
+  loc_fname : string;
+  loc_start : int * int;
+  loc_end   : int * int;
+  loc_bchar : int;
+  loc_echar : int;
+}
+
+(* -------------------------------------------------------------------- *)
+val _dummy    : t
+val make      : position -> position -> t
+val of_lexbuf : lexbuf -> t
+
+val merge    : t -> t -> t
+val mergeall : t list -> t
+
+val tostring : t -> string
+
+(* -------------------------------------------------------------------- *)
+type 'a loced = { plloc : t; pldesc : 'a; }
+
+val mkloc  : t -> 'a -> 'a loced
+val loc    : 'a loced -> t
+val unloc  : 'a loced -> 'a
+val unlocs : ('a loced) list -> 'a list
+val lmap   : ('a -> 'b) -> 'a loced -> 'b loced

src/monalg.ml

@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-open Utils
+open Core
 
 (* -------------------------------------------------------------------- *)
 module type Monoid = sig

src/nc_gasbi.ml

@@ -1,7 +1,7 @@
 (* Grobner basis computations for K[X]-module *)
 
 (* Imports and abbreviations *)    
-open Utils
+open Core
 open Num.TaggedInfix
 
 (* ------------------------------------------------------------------------- *)