ocaml: simple let case

ocaml/libsyntax/expr.ml

@@ -97,6 +97,27 @@ and parse_letbinds ps acc = match ps.lt () with
   | _ -> (acc, ps)
 
 and parse_expr ps = match ps.lt () with
+  | Seq.Cons ((Let, s), lt) ->
+      let (pat, ps) = Pattern.parse { ps with lt; offset = loc_span_end s; } in
+      let (pty, ps) = match parse_ty_annot ps with
+        | Some (x, y, ps) -> (Some (x, y), ps)
+        | None -> (None, ps)
+      in
+      let (_, ps) = require_token XLet Assign ps in
+      let value_start = ps.offset in
+      let (value_, ps) = parse_expr ps in
+      let value_span = loc_span_of_start_end value_start ps.offset in
+      let old_names = ps.names in
+      let new_names = Pattern.exports ps.names pat in
+      let ps = { ps with names = new_names } in
+      let (_, ps) = require_token XLet SemiColon ps in
+      let body_span_start = ps.offset in
+      let (body, ps) = parse_expr ps in
+      if ps.names <> new_names then failwith "invalid name book-keeping detected";
+      let ps = { ps with names = old_names } in
+      let lam = { pat; pty; body_span = Asai.Range.make (body_span_start, ps.offset); body; } in
+      (Apply (lam, value_span, value_), ps)
+    )
   | Seq.Cons ((Lambda, s), lt) -> (
       let ps = { ps with lt; offset = loc_span_end s; } in
       let (pat, ps) = Pattern.parse ps in

ocaml/libsyntax/literal.ml

@@ -17,6 +17,7 @@ type lit =
   | LNatural of int
   | LInterval0
   | LInterval1
+  | LRefl
   [@@deriving show, eq]
 
 let lty x = LTy x
@@ -51,8 +52,9 @@ let of_string = function
   | "String"    -> LTy String   |> Option.some
   | "Interval"  -> LTy Interval |> Option.some
   | "IntSize"   -> LTy TIntSize |> Option.some
-  | "Intv0"     -> LInterval0   |> Option.some
-  | "Intv1"     -> LInterval1   |> Option.some
+  | "intv0"     -> LInterval0   |> Option.some
+  | "intv1"     -> LInterval1   |> Option.some
+  | "refl"      -> LRefl        |> Option.some
 
   | s ->  (if String.starts_with ~prefix:"ZI" s then
                str_post 2 s |> isz_of_str |> Option.map (fun x -> LIntSize x)
@@ -76,5 +78,6 @@ let to_string = function
   | LTy (UnsInt sz) -> "UI" ^ (isz_to_str sz)
   | LTy (SigInt sz) -> "SI" ^ (isz_to_str sz)
   | LNatural n      -> Int.to_string n
-  | LInterval0      -> "Intv0"
-  | LInterval1      -> "Intv1"
+  | LInterval0      -> "intv0"
+  | LInterval1      -> "intv1"
+  | LRefl           -> "refl"

ocaml/libsyntax/literal.mli

@@ -17,6 +17,7 @@ type lit =
   | LNatural of int
   | LInterval0
   | LInterval1
+  | LRefl
   [@@deriving show, eq]
 
 val isz_to_pow : int_size -> char