"Expand" prose fix

Author: 702fbtngus

spectec/src/backend-interpreter/relation.ml

@@ -141,12 +141,23 @@ let val_type = function
     with exn -> raise (Exception.Invalid (exn, Printexc.get_raw_backtrace ())))
   | vs -> Numerics.error_values "$Val_type" vs
 
+let expand = function
+  | [ v ] ->
+    (try
+      v
+      |> Construct.al_to_def_type
+      |> Types.expand_def_type
+      |> Construct.al_of_str_type
+    with exn -> raise (Exception.Invalid (exn, Printexc.get_raw_backtrace ())))
+  | vs -> Numerics.error_values "$Expand" vs
+
 let manual_map =
   FuncMap.empty
   |> FuncMap.add "Ref_type" ref_type
   |> FuncMap.add "Module_ok" module_ok
   |> FuncMap.add "Val_type" val_type
   |> FuncMap.add "Externaddr_type" externaddr_type
+  |> FuncMap.add "Expand" expand
 
 let mem name =
 

spectec/src/backend-prose/render.ml

@@ -253,25 +253,25 @@ and al_to_el_expr expr =
       | Some _ ->
         None
       | _ ->
-          let elid = id $ no_region in
-          let* elal = al_to_el_args al in
-          (* Unwrap parenthsized args *)
-          let elal = List.map
-            (fun elarg ->
-              let elarg = match elarg with
-              | El.Ast.ExpA exp ->
-                let exp = match exp.it with
-                | ParenE exp' -> exp'
-                | _ -> exp
-                in
-                El.Ast.ExpA exp
-              | _ -> elarg
+        let elid = id $ no_region in
+        let* elal = al_to_el_args al in
+        (* Unwrap parenthsized args *)
+        let elal = List.map
+          (fun elarg ->
+            let elarg = match elarg with
+            | El.Ast.ExpA exp ->
+              let exp = match exp.it with
+              | ParenE exp' -> exp'
+              | _ -> exp
               in
-              (ref elarg) $ no_region
-            )
-            elal
-          in
-          Some (El.Ast.CallE (elid, elal))
+              El.Ast.ExpA exp
+            | _ -> elarg
+            in
+            (ref elarg) $ no_region
+          )
+          elal
+        in
+        Some (El.Ast.CallE (elid, elal))
       )
     | Al.Ast.CatE (e1, e2) ->
       let* ele1 = al_to_el_expr e1 in
@@ -598,14 +598,20 @@ and render_expr' env expr =
     if id = "Eval_expr" then
       (match args with
       | [instrs] ->
-        "the result of :ref:`evaluating <exec-expr>` " ^ instrs
+        sprintf "the result of :ref:`evaluating <exec-expr>` %s" instrs
       | _ -> error expr.at (Printf.sprintf "Invalid arity for relation call: %d ([ %s ])" (List.length args) (String.concat " " args));
       )
+    else if id = "Expand" then
+      (match args with
+      | [arg1] ->
+        sprintf "the :ref:`expansion <aux-expand-deftype>` of %s" arg1
+      | _ -> error expr.at "Invalid arity for relation call";
+      )
     else if String.ends_with ~suffix:"_type" id || String.ends_with ~suffix:"_ok" id then
       (match args with
       | [arg1; arg2] ->
-        arg1 ^ " is :ref:`valid <valid-val>` with type " ^ arg2
-      | [arg] -> "the type of " ^ arg
+        sprintf "%s is :ref:`valid <valid-val>` with type %s" arg1 arg2
+      | [arg] -> sprintf "the type of %s" arg
       | _ -> error expr.at "Invalid arity for relation call";
       )
     else error expr.at ("Not supported relation call: " ^ id);

spectec/src/il2al/preprocess.ml

@@ -128,43 +128,27 @@ let rec preprocess_prem prem =
     prem
     |> preprocess_prem
     |> List.map (fun new_prem -> IterPr (new_prem, iterexp) $ prem.at)
-  | RulePr (id, mixop, exp) when id.it = "Expand" ->
-    (match mixop, exp.it with
-    (* Expand: `dt` ~~ `ct` *)
-    | [[]; [approx]; []], TupE [dt; ct] when approx.it = Approx ->
-      (* `$expanddt(dt) = ct` *)
-      let expanddt =
-        CallE ("expanddt" $ prem.at, [ExpA dt $ dt.at]) $$ prem.at % ct.note
-      in
-      let new_prem =
-        IfPr (CmpE (`EqOp, `BoolT, expanddt, ct) $$ prem.at % (BoolT $ no_region))
-      in
-
-      (* Add function definition to AL environment *)
-      if not (Env.mem_def !Al.Valid.il_env id) then (
-        let param = ExpP ("_" $ no_region, dt.note) $ dt.at in
-        Al.Valid.il_env := Env.bind_def !Al.Valid.il_env id ([param], ct.note, [])
-      );
-
-      [ new_prem $ prem.at ]
-    (* Expand: ??? *)
-    | _ -> [ prem ]
-    )
   | RulePr (id, mixop, exp) ->
-    (match mixop, exp.it with
-    (* `id`: |- `lhs` : `rhs` *)
-    | [[turnstile]; [colon]; []], TupE [lhs; rhs]
-    (* `id`: C |- `lhs` : `rhs` *)
-    | [[]; [turnstile]; [colon]; []], TupE [_; lhs; rhs]
-    when turnstile.it = Turnstile && colon.it = Colon ->
-      typing_functions := id.it :: !typing_functions;
-
-      (* $`id`(`lhs`) = `rhs` *)
-      let typing_function_call =
+    let lhs_rhs_opt = 
+      match mixop, exp.it with
+      (* `id`: |- `lhs` : `rhs` *)
+      | [[turnstile]; [colon]; []], TupE [lhs; rhs]
+      (* `id`: C |- `lhs` : `rhs` *)
+      | [[]; [turnstile]; [colon]; []], TupE [_; lhs; rhs]
+      when turnstile.it = Turnstile && colon.it = Colon ->
+        typing_functions := id.it :: !typing_functions;
+        Some (lhs, rhs)
+      (* `lhs` ~~ `rhs` *)
+      | [[]; [approx]; []], TupE [lhs; rhs] when approx.it = Approx -> Some (lhs, rhs)
+      | _ -> None
+    in
+    (match lhs_rhs_opt with
+    | Some (lhs, rhs) -> 
+      let function_call =
         CallE (id, [ExpA lhs $ lhs.at]) $$ exp.at % rhs.note
       in
       let new_prem =
-        IfPr (CmpE (`EqOp, `BoolT, typing_function_call, rhs) $$ exp.at % (BoolT $ no_region))
+        IfPr (CmpE (`EqOp, `BoolT, function_call, rhs) $$ prem.at % (BoolT $ no_region))
       in
 
       (* Add function definition to AL environment *)
@@ -174,8 +158,7 @@ let rec preprocess_prem prem =
       );
 
       [ new_prem $ prem.at ]
-    | _ -> [ prem ]
-    )
+    | None -> [ prem ])
   (* Split -- if e1 /\ e2 *)
   | IfPr ( { it = BinE (`AndOp, _, e1, e2); _ } ) ->
     preprocess_prem (IfPr e1 $ prem.at) @ preprocess_prem (IfPr e2 $ prem.at)