Keep hints in EL representation

Wasm-DSL · Jun 17, 2024 · 32e0dc4 · 32e0dc4
1 parent 854e1f4
commit 32e0dc4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 7 deletions.
diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml
@@ -460,12 +460,7 @@ let elab_hint tid mixop {hintid; hintexp} : Il.hint =
     )
   in
   IterAtoms.exp hintexp;
-  let ss =
-    match hintexp.it with
-    | SeqE es -> List.map Print.string_of_exp es
-    | _ -> [Print.string_of_exp hintexp]
-  in
-  {Il.hintid; Il.hintexp = ss}
+  {Il.hintid; Il.hintexp}
 
 let elab_hints tid mixop = List.map (elab_hint tid mixop)
 

diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
@@ -170,7 +170,7 @@ and hintdef' =
   | RelH of id * hint list
   | DecH of id * hint list
 
-and hint = {hintid : id; hintexp : string list}       (* hint *)
+and hint = {hintid : id; hintexp : El.Ast.exp}        (* hint *)
 
 
 (* Scripts *)