Isabelle/HOL translation: fix undefined identifiers due to syntax alias (#3050)

* Closes #3047 
* Depends on #3049

Author: lukaszcz

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -1093,7 +1093,7 @@ entryToScopedIden name e = do
                 return
                   ScopedIden
                     { _scopedIdenAlias = Just scopedName',
-                      _scopedIdenFinal = setConcrete e'
+                      _scopedIdenFinal = e'
                     }
   si <- scopedIdenSrcName getFixityAndIterator si0
   registerScopedIden False si

tests/positive/Isabelle/Program.juvix

@@ -248,3 +248,17 @@ getMessageFromTrigger' {M H} (t : Trigger M H) : Maybe M :=
               message := m })})})
               := just m
       | _ := nothing;
+
+-- Syntax aliases
+
+Name : Type := Nat;
+
+syntax alias T := Name;
+
+idT (x : T) : T := x;
+
+t : T := 0;
+
+type RR := mkRR {
+  x : T
+};

tests/positive/Isabelle/isabelle/Program.thy

@@ -18,25 +18,25 @@ definition id2 :: "'A \<Rightarrow> 'A" where
 fun add_one :: "nat list \<Rightarrow> nat list" where
   "add_one [] = []" |
   (* hello! *)
-  "add_one (x # xs) = ((x + 1) # add_one xs)"
+  "add_one (x' # xs) = ((x' + 1) # add_one xs)"
 
 fun sum :: "nat list \<Rightarrow> nat" where
   "sum [] = 0" |
-  "sum (x # xs) = (x + sum xs)"
+  "sum (x' # xs) = (x' + sum xs)"
 
 fun f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
-  "f x y z = ((z + 1) * x + y)"
+  "f x' y z = ((z + 1) * x' + y)"
 
 fun g :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-  "g x y = (if x = f x (N.g y) (M_N.g (M_Main.f y)) then False else True)"
+  "g x' y = (if x' = f x' (N.g y) (M_N.g (M_Main.f y)) then False else True)"
 
 fun inc :: "nat \<Rightarrow> nat" where
-  "inc x = (Suc x)"
+  "inc x' = (Suc x')"
 
 (* dec function *)
 fun dec :: "nat \<Rightarrow> nat" where
   "dec 0 = 0" |
-  "dec (Suc x) = x"
+  "dec (Suc x') = x'"
 
 (* dec' function *)
 fun dec' :: "nat \<Rightarrow> nat" where
@@ -45,23 +45,23 @@ fun dec' :: "nat \<Rightarrow> nat" where
   (* the zero case  *)
   (* return zero  *)
   (* the suc case  *)
-  "dec' x =
-    (case x of
+  "dec' x' =
+    (case x' of
        0 \<Rightarrow> 0 |
        (Suc y) \<Rightarrow> y)"
 
 fun optmap :: "('A \<Rightarrow> 'A) \<Rightarrow> 'A option \<Rightarrow> 'A option" where
   "optmap f' None = None" |
-  "optmap f' (Some x) = (Some (f' x))"
+  "optmap f' (Some x') = (Some (f' x'))"
 
 fun pboth :: "('A \<Rightarrow> 'A') \<Rightarrow> ('B \<Rightarrow> 'B') \<Rightarrow> 'A \<times> 'B \<Rightarrow> 'A' \<times> 'B'" where
-  "pboth f' g' (x, y) = (f' x, g' y)"
+  "pboth f' g' (x', y) = (f' x', g' y)"
 
 fun bool_fun :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
-  "bool_fun x y z = (x \<and> (y \<or> z))"
+  "bool_fun x' y z = (x' \<and> (y \<or> z))"
 
 fun bool_fun' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
-  "bool_fun' x y z = (x \<and> y \<or> z)"
+  "bool_fun' x' y z = (x' \<and> y \<or> z)"
 
 (* Queues *)
 text \<open>
@@ -71,7 +71,7 @@ datatype 'A Queue
   = queue "'A list" "'A list"
 
 fun qfst :: "'A Queue \<Rightarrow> 'A list" where
-  "qfst (queue x v') = x"
+  "qfst (queue x' v') = x'"
 
 fun qsnd :: "'A Queue \<Rightarrow> 'A list" where
   "qsnd (queue v' v'0) = v'0"
@@ -85,10 +85,10 @@ fun pop_front :: "'A Queue \<Rightarrow> 'A Queue" where
           v' \<Rightarrow> q')"
 
 fun push_back :: "'A Queue \<Rightarrow> 'A \<Rightarrow> 'A Queue" where
-  "push_back q x =
+  "push_back q x' =
     (case qfst q of
-       [] \<Rightarrow> queue [x] (qsnd q) |
-       q' \<Rightarrow> queue q' (x # qsnd q))"
+       [] \<Rightarrow> queue [x'] (qsnd q) |
+       q' \<Rightarrow> queue q' (x' # qsnd q))"
 
 text \<open>
 Checks if the queue is empty
@@ -294,11 +294,26 @@ fun getMessageFromTrigger :: "('M, 'H) Trigger \<Rightarrow> 'M option" where
        v'1 \<Rightarrow> None)"
 
 fun getMessageFromTrigger' :: "('M, 'H) Trigger \<Rightarrow> 'M option" where
-  "getMessageFromTrigger' t =
-    (case t of
+  "getMessageFromTrigger' t' =
+    (case t' of
        (MessageArrived v') \<Rightarrow>
          (case (EnvelopedMessage.packet v') of
             (v'0) \<Rightarrow> Some (MessagePacket.message v'0)) |
        v'2 \<Rightarrow> None)"
 
+(* Syntax aliases *)
+type_synonym Name = nat
+
+fun idT :: "nat \<Rightarrow> Name" where
+  "idT x' = x'"
+
+definition t :: Name where
+  "t = 0"
+
+record RR =
+  x :: nat
+
+fun x :: "RR \<Rightarrow> Name" where
+  "x (| RR.x = x' |) = x'"
+
 end