unique ref

src/GF/Grammar/LookAbs.hs

@@ -81,15 +81,15 @@ lookupRef gr binds at = case at of
   K _    -> return valAbsString
   _      -> prtBad "cannot refine with complex term" at ---
 
-refsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Binds -> Val -> [(Term,Val)]
+refsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Binds -> Val -> [(Term,(Val,Bool))]
 refsForType compat gr binds val =     
-  -- bound variables
+    -- bound variables --- never recursive?
-  [(vr i, t) | (i,t) <- binds, Ok ty <- [val2exp t], compat val ty] ++
+    [(vr i, (t,False)) | (i,t) <- binds, Ok ty <- [val2exp t], compat val ty] ++
     -- integer and string literals
-  [(EInt i, val) | val == valAbsInt, i <- [0,1,2,5,11,1978]] ++
+    [(EInt i, (val,False)) | val == valAbsInt, i <- [0,1,2,5,11,1978]] ++
-  [(K s, val) | val == valAbsString, s <- ["foo", "NN", "x"]] ++
+    [(K s, (val,False)) | val == valAbsString, s <- ["foo", "NN", "x"]] ++
     -- functions defined in the current abstract syntax
-  [(qq f, vClos t) | (f,t) <- funsForType compat gr val]
+    [(qq f, (vClos t,isRecursiveType t)) | (f,t) <- funsForType compat gr val]
 
 
 funRulesOf :: GFCGrammar -> [(Fun,Type)]

src/GF/Shell/Commands.hs

@@ -310,7 +310,7 @@ mkRefineMenuAll env sstate =
        [(CSelectCand i,   prCand (t,i))    | (t,i) <- zip cands [0..]]
 
  where
-  prRef (f,t) = 
+  prRef (f,(t,_)) = 
     (ifShort "r" "Refine" +++ prOrLinRef f +++ ifTyped (":" +++ prt_ t),
      "r" +++ prRefinement f)
   prClip i t =
@@ -474,7 +474,9 @@ displaySState env state =
   (prState (stateSState state), msgSState state, menuSState env state)
 
 menuSState :: CEnv -> SState -> [(String,String)]
-menuSState env state = [(s,c) | (_,(s,c)) <- mkRefineMenuAll env state]
+menuSState env state = if null cs then [("[NO ALTERNATIVE]","")] else cs 
+  where
+    cs = [(s,c) | (_,(s,c)) <- mkRefineMenuAll env state]
 
 printname :: CEnv -> SState -> G.Fun -> String
 printname env state f = case getOptVal opts menuDisplay of

src/GF/UseGrammar/Editing.hs

@@ -232,6 +232,7 @@ contextRefinements gr = refineAllNodes contextRefine where
 
 uniqueRefine :: CGrammar -> Action
 uniqueRefine gr state = case refinementsState gr state of
+  [(e,(_,True))] -> Bad "only circular refinement"
   [(e,_)] -> refineWithAtom False gr e state
   _ -> Bad "no unique refinement"
 
@@ -347,7 +348,7 @@ solveAll gr st0 = do
 
 -- active refinements
 
-refinementsState :: CGrammar -> State -> [(Term,Val)]
+refinementsState :: CGrammar -> State -> [(Term,(Val,Bool))]
 refinementsState gr state = 
   let filt = possibleRefVal gr state in 
   if actIsMeta state 

src/GF/UseGrammar/Randomized.hs

@@ -37,7 +37,8 @@ mkStateFromInts ints gr = mkRandomState ints where
     return state
   mkRandomState (n:ns) state = do 
     let refs  = refinementsState gr state
-    testErr (not (null refs)) $ "no refinements available for" +++ 
+        refs0 = map (not . snd . snd) refs
+    testErr (not (null refs0)) $ "no nonrecursive refinements available for" +++ 
                                               prt (actVal state)
     (ref,_) <- (refs !? (n `mod` (length refs)))
     state1  <- refineWithAtom False gr ref state