Menhir parser

src/haz3lcore/dune

@@ -2,7 +2,7 @@
 
 (library
  (name haz3lcore)
- (libraries util re sexplib unionFind uuidm)
+ (libraries util re sexplib unionFind uuidm hazel_menhir)
  (js_of_ocaml
   (flags
    (:include js-of-ocaml-flags-%{profile})))

src/haz3lcore/dynamics/DH.re

@@ -1,4 +1,5 @@
 open Sexplib.Std;
+open Hazel_menhir.AST;
 
 module rec DHExp: {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -52,6 +53,8 @@ module rec DHExp: {
   let strip_casts: t => t;
 
   let fast_equal: (t, t) => bool;
+
+  let of_menhir_ast: Hazel_menhir.AST.exp => t;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
@@ -312,6 +315,56 @@ module rec DHExp: {
        )
     && i1 == i2;
   };
+
+  let rec rule_of_menhir_ast = ((pat: Hazel_menhir.AST.pat, exp: Hazel_menhir.AST.exp)) : rule => {
+        Rule(DHPat.of_menhir_ast(pat), of_menhir_ast(exp));
+  } 
+  and of_menhir_ast = (exp: Hazel_menhir.AST.exp) : t => {
+    switch (exp) {
+        | Int(i) => IntLit(i)
+        | Float(f) => FloatLit(f)
+        | String(s) => StringLit(s)
+        | Bool(b) => BoolLit(b)
+        | Var(x) => BoundVar(x)
+        | ArrayExp(l) => ListLit(Id.mk(), 0, Unknown(SynSwitch), List.map(of_menhir_ast, l))
+        | TupleExp(t) => Tuple(List.map(of_menhir_ast, t))
+        | Let(p, e1, e2) => Let(DHPat.of_menhir_ast(p), of_menhir_ast(e1), of_menhir_ast(e2))
+        | Fun(p, e) => Fun(DHPat.of_menhir_ast(p), Unknown(SynSwitch), of_menhir_ast(e), None)
+        | Unit => EmptyHole(Id.mk(), 0)
+        | ApExp(e1, e2) => Ap(of_menhir_ast(e1), of_menhir_ast(e2))
+        | BinExp(e1, op, e2) => 
+        {
+            switch (op) {
+                | IntOp(op) => BinIntOp(TermBase.UExp.int_op_of_menhir_ast(op), of_menhir_ast(e1), of_menhir_ast(e2))
+                | FloatOp(op) => BinFloatOp(TermBase.UExp.float_op_of_menhir_ast(op), of_menhir_ast(e1), of_menhir_ast(e2))
+                | BoolOp(op) => BinBoolOp(TermBase.UExp.bool_op_of_menhir_ast(op), of_menhir_ast(e1), of_menhir_ast(e2))
+
+            }
+        }
+        | If(e1, e2, e3) => {
+            let d_scrut = of_menhir_ast(e1)
+            let d1 = of_menhir_ast(e2)
+            let d2 = of_menhir_ast(e3)
+
+            let d_rules =
+          DHExp.[Rule(BoolLit(true), d1), Rule(BoolLit(false), d2)];
+        let d = DHExp.Case(d_scrut, d_rules, 0);
+            ConsistentCase(d);
+            }
+
+        | CaseExp(e, l) => {
+            let d_scrut = of_menhir_ast(e)
+            let d_rules = List.map(rule_of_menhir_ast, l);
+            ConsistentCase(Case(d_scrut, d_rules, 0))
+
+            // raise(Invalid_argument("Menhir Case -> DHExp not yet implemented")); //TODO: add in the slightly irritating translation of the list from the AST form to the DHExp form ConsistentCase(case(of_menhir_ast(e), , 0))
+        }
+
+        | Cast(e, t1, t2) => Cast(of_menhir_ast(e), Typ.of_menhir_ast(t1), Typ.of_menhir_ast(t2))
+
+        // | _ => raise(Invalid_argument("Menhir AST -> DHExp not yet implemented"))
+    }
+  }
 }
 
 and Environment: {

src/haz3lcore/dynamics/DHPat.re

@@ -49,3 +49,15 @@ let rec binds_var = (x: Var.t, dp: t): bool =>
     List.fold_left((||), false, new_list);
   | Ap(_, _) => false
   };
+
+let rec of_menhir_ast = (pat: Hazel_menhir.AST.pat): t => {
+    switch (pat) {
+        | IntPat(i) => IntLit(i)
+        | FloatPat(f) => FloatLit(f)
+        | VarPat(x) => Var(x)
+        | StringPat(s) => StringLit(s)
+        | TypeAnn(pat, _typ) => of_menhir_ast(pat);
+        | TuplePat(pats) => Tuple(List.map(of_menhir_ast, pats))
+        | ApPat(pat1, pat2) => Ap(of_menhir_ast(pat1), of_menhir_ast(pat2))
+    }
+};

src/haz3lcore/dynamics/Elaborator.re

@@ -341,10 +341,15 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
 
 //let dhexp_of_uexp = Core.Memo.general(~cache_size_bound=1000, dhexp_of_uexp);
 
-let uexp_elab = (m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t =>
+let uexp_elab = (m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t => {
+  let _ = print_endline("uexp_elab");
   switch (dhexp_of_uexp(m, uexp)) {
-  | None => DoesNotElaborate
+  | None => {
+        print_endline("dne");
+      DoesNotElaborate
+  }
   | Some(d) =>
+     print_endline(DH.DHExp.show(d));
     //let d = uexp_elab_wrap_builtins(d);
     let ty =
       switch (fixed_exp_typ(m, uexp)) {
@@ -353,3 +358,4 @@ let uexp_elab = (m: Statics.Map.t, uexp: Term.UExp.t): ElaborationResult.t =>
       };
     Elaborates(d, ty, Delta.empty);
   };
+};

src/haz3lcore/statics/TermBase.re

@@ -135,6 +135,10 @@ and UExp: {
   let int_op_to_string: op_bin_int => string;
   let float_op_to_string: op_bin_float => string;
   let string_op_to_string: op_bin_string => string;
+
+  let int_op_of_menhir_ast: Hazel_menhir.AST.op_bin_int => op_bin_int;
+  let bool_op_of_menhir_ast: Hazel_menhir.AST.op_bin_bool => op_bin_bool;
+  let float_op_of_menhir_ast: Hazel_menhir.AST.op_bin_float => op_bin_float;
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type op_un_bool =
@@ -194,6 +198,50 @@ and UExp: {
     | Bool(op_bin_bool)
     | String(op_bin_string);
 
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  let int_op_of_menhir_ast = (op: Hazel_menhir.AST.op_bin_int): op_bin_int => {
+    switch (op) {
+    | Plus => Plus
+    | Minus => Minus
+    | Times => Times
+    | Power => Power
+    | Divide => Divide
+    | LessThan => LessThan
+    | LessThanOrEqual => LessThanOrEqual
+    | GreaterThan => GreaterThan
+    | GreaterThanOrEqual => GreaterThanOrEqual
+    | Equals => Equals
+    | NotEquals => NotEquals
+    };
+  };
+
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  let float_op_of_menhir_ast =
+          (op: Hazel_menhir.AST.op_bin_float): op_bin_float => {
+    switch (op) {
+    | Plus => Plus
+    | Minus => Minus
+    | Times => Times
+    | Power => Power
+    | Divide => Divide
+    | LessThan => LessThan
+    | LessThanOrEqual => LessThanOrEqual
+    | GreaterThan => GreaterThan
+    | GreaterThanOrEqual => GreaterThanOrEqual
+    | Equals => Equals
+    | NotEquals => NotEquals
+    };
+  };
+
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  let bool_op_of_menhir_ast =
+          (op: Hazel_menhir.AST.op_bin_bool): op_bin_bool => {
+    switch (op) {
+    | And => And
+    | Or => Or
+    };
+  };
+
   [@deriving (show({with_path: false}), sexp, yojson)]
   type term =
     | Invalid(string)

src/haz3lcore/statics/TypBase.re

@@ -1,6 +1,7 @@
 open Sexplib.Std;
 open Util;
 open OptUtil.Syntax;
+open Hazel_menhir.AST;
 
 let precedence_Prod = 1;
 let precedence_Arrow = 2;
@@ -68,6 +69,9 @@ module rec Typ: {
   let sum_entry: (Constructor.t, sum_map) => option(sum_entry);
   let get_sum_constructors: (Ctx.t, t) => option(sum_map);
   let is_unknown: t => bool;
+
+  let of_menhir_ast: Hazel_menhir.AST.typ => t;
+
 } = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type type_provenance =
@@ -424,6 +428,21 @@ module rec Typ: {
     | Unknown(_) => true
     | _ => false
     };
+
+  let rec of_menhir_ast = (typ: Hazel_menhir.AST.typ) : t => {
+        switch (typ) {
+            | IntType => Int
+            | FloatType => Float
+            | BoolType => Bool
+            | StringType => String
+            | UnitType => Prod([])
+            | TupleType(ts) => Prod(List.map(of_menhir_ast, ts))
+            | ArrayType(t) => List(of_menhir_ast(t))
+            | ArrowType(t1, t2) => Arrow(of_menhir_ast(t1), of_menhir_ast(t2))
+            // | _ => raise(Invalid_argument("Menhir AST -> DHExp not yet implemented"))
+        }
+  }
+
 }
 and Ctx: {
   [@deriving (show({with_path: false}), sexp, yojson)]

src/menhir-parser/AST.re

@@ -0,0 +1,93 @@
+open Sexplib.Std;
+
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type op_bin_float =
+    | Plus
+    | Minus
+    | Times
+    | Power
+    | Divide
+    | LessThan
+    | LessThanOrEqual
+    | GreaterThan
+    | GreaterThanOrEqual
+    | Equals
+    | NotEquals;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+  type op_bin_bool =
+    | And
+    | Or;
+
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type op_bin_int =
+     | Plus
+    | Minus
+    | Times
+    | Power
+    | Divide
+    | LessThan
+    | LessThanOrEqual
+    | GreaterThan
+    | GreaterThanOrEqual
+    | Equals
+    | NotEquals;
+  // | Equals
+  // | NotEqual
+  // | Plus
+  // | Minus
+  // | Times
+  // | Divide
+  // | Power
+  // | LessThan
+  // | GreaterThan
+  // | LessThanEqual
+  // | GreaterThanEqual
+  // | Logical_And
+  // | Logical_Or
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type binOp = 
+    | IntOp(op_bin_int)
+    | FloatOp(op_bin_float)
+    | BoolOp(op_bin_bool);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type typ =
+  | IntType
+  | StringType
+  | FloatType
+  | BoolType
+  | UnitType
+  | TupleType(list(typ))
+  | ArrayType(typ)
+  | ArrowType(typ, typ);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type pat =
+  | IntPat(int)
+  | FloatPat(float)
+  | VarPat(string)
+  | StringPat(string)
+  | TypeAnn(pat, typ)
+  | TuplePat(list(pat))
+  | ApPat(pat, pat);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type exp =
+  | Int(int)
+  | Float(float)
+  | Var(string)
+  | String(string)
+  | ArrayExp(list(exp))
+  | TupleExp(list(exp))
+  | Unit
+  | BinExp(exp, binOp, exp)
+  | Let(pat, exp, exp)
+  | Fun(pat, exp)
+  | CaseExp(exp, list((pat, exp)))
+  | ApExp(exp, exp)
+  | Bool(bool)
+  | Cast(exp, typ, typ)
+  | If(exp, exp, exp);

src/menhir-parser/Interface.re

@@ -0,0 +1,22 @@
+open Lexing;
+let column_num = (pos: position) => {
+  pos.pos_cnum - pos.pos_bol - 1;
+};
+
+let string_of_pos = (pos: position) => {
+  let l = string_of_int(pos.pos_lnum);
+  let c = string_of_int(column_num(pos) + 1);
+  "line " ++ l ++ ", column " ++ c;
+};
+
+let parse = (f, s) => {
+  let lexbuf = Lexing.from_string(s);
+  let result =
+    try(f(Lexer.token, lexbuf)) {
+    | Parser.Error =>
+      raise(Failure("Parse error at: " ++ string_of_pos(lexbuf.lex_curr_p)))
+    };
+  result;
+};
+
+let parse_program = s => parse(Parser.program, s);