Merge pull request #287 from Beluga-lang/ext/prop-eq

Merge the prop equality extension

Author: Ailrun

.gitignore

@@ -1,3 +1,5 @@
+.vscode
+
 # Dune outputs
 _build
 *.opam

driver/Lexer.mll

@@ -43,7 +43,12 @@
     | DOT _ -> "."
     | LET _ -> "let"
     | IN _ -> "in"
-    | EQ _ -> ":="
+    | DEF _ -> ":="
+    | EQ _ -> "="
+    | LANGLE _ -> "<"
+    | RANGLE _ -> ">"
+    | REFL _ -> "refl"
+    | AS _ -> "as"
 
   let get_range_of_token : token -> (position * position) =
     function
@@ -69,7 +74,12 @@
     | DOT r
     | LET r
     | IN r
+    | DEF r
     | EQ r
+    | LANGLE r
+    | RANGLE r
+    | REFL r
+    | AS r
     | VAR (r, _) -> r
 
   let format_token (f: Format.formatter) (t: token): unit =
@@ -109,7 +119,12 @@ rule read =
   | "." { DOT (get_range lexbuf) }
   | "let" {LET (get_range lexbuf) }
   | "in" {IN (get_range lexbuf) }
-  | ":=" {EQ (get_range lexbuf) }
+  | ":=" {DEF (get_range lexbuf) }
+  | "=" {EQ (get_range lexbuf) }
+  | "<" {LANGLE (get_range lexbuf) }
+  | ">" {RANGLE (get_range lexbuf) }
+  | "refl" {REFL (get_range lexbuf) }
+  | "as" {AS (get_range lexbuf) }
   | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) }
   | _ as c { failwith (Format.asprintf "@[<v 2>Lexer error:@ @[<v 2>Unexpected character %C@ at %a@]@]@." c format_position lexbuf.lex_start_p) }
 and comment =

driver/PrettyPrinter.ml

@@ -41,6 +41,7 @@ let rec get_pi_params_of_obj : Cst.obj -> (string * Cst.obj) list * Cst.obj =
 let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
   let open Format in
   function
+  | Cst.Coq_var x -> pp_print_string f x
   | Cst.Coq_typ i -> fprintf f "Type@%d" i
   | Cst.Coq_nat -> fprintf f "Nat"
   | Cst.Coq_zero -> fprintf f "0"
@@ -61,17 +62,10 @@ let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
          format_obj escr mx format_obj em format_obj ez sx sr format_obj es
      in
      pp_print_paren_if (p >= 1) impl f ()
-  | Cst.Coq_app (ef, ea) ->
-     let impl f () =
-       fprintf f "%a@ %a" (format_obj_prec 1) ef (format_obj_prec 2) ea
-     in
-     pp_open_hvbox f 2;
-     pp_print_paren_if (p >= 2) impl f ();
-     pp_close_box f ()
-  | Cst.Coq_fn (px, ep, ebody) ->
-     let params, ebody' = get_fn_params_of_obj ebody in
+  | Cst.Coq_pi (px, ep, eret) ->
+     let params, eret' = get_pi_params_of_obj eret in
      let impl f () =
-       pp_print_string f "fun ";
+       pp_print_string f "forall ";
        pp_open_tbox f ();
        pp_set_tab f ();
        pp_print_list ~pp_sep:pp_print_tab format_obj_param f ((px, ep) :: params);
@@ -81,15 +75,15 @@ let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
          then pp_print_space f ()
          else pp_force_newline f ()
        end;
-       fprintf f "-> @[<hov 2>%a@]" format_obj ebody'
+       fprintf f "-> @[<hov 2>%a@]" format_obj eret'
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 1) impl f ();
      pp_close_box f ()
-  | Cst.Coq_pi (px, ep, eret) ->
-     let params, eret' = get_pi_params_of_obj eret in
+  | Cst.Coq_fn (px, ep, ebody) ->
+     let params, ebody' = get_fn_params_of_obj ebody in
      let impl f () =
-       pp_print_string f "forall ";
+       pp_print_string f "fun ";
        pp_open_tbox f ();
        pp_set_tab f ();
        pp_print_list ~pp_sep:pp_print_tab format_obj_param f ((px, ep) :: params);
@@ -99,12 +93,49 @@ let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
          then pp_print_space f ()
          else pp_force_newline f ()
        end;
-       fprintf f "-> @[<hov 2>%a@]" format_obj eret'
+       fprintf f "-> @[<hov 2>%a@]" format_obj ebody'
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 1) impl f ();
      pp_close_box f ()
-  | Cst.Coq_var x -> pp_print_string f x
+  | Cst.Coq_app (ef, ea) ->
+     let impl f () =
+       fprintf f "%a@ %a" (format_obj_prec 1) ef (format_obj_prec 2) ea
+     in
+     pp_open_hvbox f 2;
+     pp_print_paren_if (p >= 2) impl f ();
+     pp_close_box f ()
+  | Cst.Coq_prop_eq (e1, et, e2) ->
+     let impl f () =
+       fprintf f "%a@ =<%a>@ %a" (format_obj_prec 1) e1 (format_obj_prec 0) et (format_obj_prec 1) e2
+     in
+     pp_open_hvbox f 2;
+     pp_print_paren_if (p >= 1) impl f ();
+     pp_close_box f ()
+  | Cst.Coq_refl (et, ex) ->
+     let impl f () =
+       fprintf f "refl@ %a@ %a" (format_obj_prec 2) et (format_obj_prec 2) ex
+     in
+     pp_open_hvbox f 2;
+     pp_print_paren_if (p >= 1) impl f ();
+     pp_close_box f ()
+  | Cst.Coq_eqrec (escr, mx, my, mz, em, rx, er, e1, ea, e2) ->
+     let impl f () =
+       fprintf f
+         "@[<hv 0>@[<hov 2>rec %a@ as %a =<%a> %a@ return %s %s %s . %a@]@ @[<hov 2>| refl %s =>@ \
+          %a@]@ end@]"
+         format_obj escr
+         format_obj e1
+         format_obj ea
+         format_obj e2
+         mx
+         my
+         mz
+         format_obj em
+         rx
+         format_obj er
+     in
+     pp_print_paren_if (p >= 1) impl f ()
 
 and format_obj_param f (px, ep) = Format.fprintf f "(%s : %a)" px format_obj ep
 and format_obj f = format_obj_prec 0 f
@@ -128,6 +159,9 @@ let exp_to_obj =
       fun () -> suffix := 0 )
   in
   let rec impl (ctx : string list) : exp -> Cst.obj = function
+    | Coq_a_var x -> Cst.Coq_var (List.nth ctx x)
+    | Coq_a_typ i -> Cst.Coq_typ i
+    | Coq_a_nat -> Cst.Coq_nat
     | Coq_a_zero -> Cst.Coq_zero
     | Coq_a_succ e -> Cst.Coq_succ (impl ctx e)
     | Coq_a_natrec (em, ez, es, escr) ->
@@ -139,9 +173,11 @@ let exp_to_obj =
        let ez' = impl ctx ez in
        let es' = impl (sr :: sx :: ctx) es in
        Cst.Coq_natrec (escr', mx, em', ez', sx, sr, es')
-    | Coq_a_nat -> Cst.Coq_nat
-    | Coq_a_typ i -> Cst.Coq_typ i
-    | Coq_a_var x -> Cst.Coq_var (List.nth ctx x)
+    | Coq_a_pi (ep, eret) ->
+       let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let ep' = impl ctx ep in
+       let eret' = impl (px :: ctx) eret in
+       Cst.Coq_pi (px, ep', eret')
     | Coq_a_fn (ep, ebody) ->
        let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
        let ep' = impl ctx ep in
@@ -151,11 +187,27 @@ let exp_to_obj =
        let ef' = impl ctx ef in
        let ea' = impl ctx ea in
        Cst.Coq_app (ef', ea')
-    | Coq_a_pi (ep, eret) ->
-       let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
-       let ep' = impl ctx ep in
-       let eret' = impl (px :: ctx) eret in
-       Cst.Coq_pi (px, ep', eret')
+    | Coq_a_eq (et, e1, e2) ->
+       let et' = impl ctx et in
+       let e1' = impl ctx e1 in
+       let e2' = impl ctx e2 in
+       Cst.Coq_prop_eq (e1', et', e2')
+    | Coq_a_refl (et, ex) ->
+       let et' = impl ctx et in
+       let ex' = impl ctx ex in
+       Cst.Coq_refl (et', ex')
+    | Coq_a_eqrec (ea, em, er, e1, e2, escr) ->
+       let ea' = impl ctx ea in
+       let mx = match ea with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let my = match ea with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let mz = new_tyvar () in
+       let em' = impl (mz :: my :: mx :: ctx) em in
+       let rx = match em with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
+       let er' = impl (rx :: ctx) er in
+       let e1' = impl ctx e1 in
+       let e2' = impl ctx e2 in
+       let escr' = impl ctx escr in
+       Cst.Coq_eqrec (escr', mx, my, mz, em', rx, er', e1', ea', e2')
     | Coq_a_sub _ -> failwith "Invalid internal language construct"
   in
   fun exp ->