11{-# LANGUAGE CPP #-}
2+ {-# LANGUAGE LambdaCase #-}
23{-# LANGUAGE PatternGuards #-}
34{-# LANGUAGE ScopedTypeVariables #-}
45{-# LANGUAGE ViewPatterns #-}
@@ -29,6 +30,7 @@ import qualified Data.Vector as V
2930import Text.Read (readMaybe )
3031import Text.URI
3132
33+ import Verifier.SAW.Name
3234import Verifier.SAW.SharedTerm
3335import Verifier.SAW.TypedAST
3436
@@ -101,6 +103,11 @@ scWriteExternal t0 =
101103 do (m, nms, lns, x) <- State. get
102104 State. put (m, Map. insert (ecVarIndex ec) (ecName ec) nms, lns, x)
103105
106+ stashPrimName :: PrimName Int -> WriteM ()
107+ stashPrimName pn =
108+ do (m, nms, lns, x) <- State. get
109+ State. put (m, Map. insert (primVarIndex pn) (ModuleIdentifier (primName pn)) nms, lns, x)
110+
104111 go :: Term -> WriteM Int
105112 go (Unshared tf) = do
106113 tf' <- traverse go tf
@@ -133,28 +140,38 @@ scWriteExternal t0 =
133140 FTermF ftf ->
134141 case ftf of
135142 Primitive ec ->
136- do stashName ec
137- pure $ unwords [" Primitive" show (ecVarIndex ec), show (ecType ec)]
143+ do stashPrimName ec
144+ pure $ unwords [" Primitive" show (primVarIndex ec), show (primType ec)]
138145 UnitValue -> pure $ unwords [" Unit"
139146 UnitType -> pure $ unwords [" UnitT"
140147 PairValue x y -> pure $ unwords [" Pair" show x, show y]
141148 PairType x y -> pure $ unwords [" PairT" show x, show y]
142149 PairLeft e -> pure $ unwords [" ProjL" show e]
143150 PairRight e -> pure $ unwords [" ProjR" show e]
144- CtorApp i ps es -> pure $
145- unwords (" Ctor" : show i : map show ps ++ argsep : map show es)
146- DataTypeApp i ps es -> pure $
147- unwords (" Data" : show i : map show ps ++ argsep : map show es)
151+ CtorApp i ps es ->
152+ do stashPrimName i
153+ pure $ unwords (" Ctor" : show (primVarIndex i) : show (primType i) :
154+ map show ps ++ argsep : map show es)
155+ DataTypeApp i ps es ->
156+ do stashPrimName i
157+ pure $ unwords (" Data" : show (primVarIndex i) : show (primType i) :
158+ map show ps ++ argsep : map show es)
148159
149- RecursorType d ps motive motive_ty -> pure $
150- unwords ([" RecursorType" show d] ++
160+ RecursorType d ps motive motive_ty ->
161+ do stashPrimName d
162+ pure $ unwords
163+ ([" RecursorType" show (primVarIndex d), show (primType d)] ++
164+ map show ps ++
165+ [argsep, show motive, show motive_ty])
166+ Recursor (CompiledRecursor d ps motive motive_ty cs_fs ctorOrder) ->
167+ do stashPrimName d
168+ mapM_ stashPrimName ctorOrder
169+ pure $ unwords
170+ ([" Recursor" show (primVarIndex d), show (primType d)] ++
151171 map show ps ++
152- [argsep, show motive, show motive_ty])
153- Recursor (CompiledRecursor i ps motive motive_ty cs_fs ctorOrder) -> pure $
154- unwords ([" Recursor" show i] ++ map show ps ++
155172 [ argsep, show motive, show motive_ty
156173 , show (Map. toList cs_fs)
157- , show ctorOrder
174+ , show ( map ( \ ec -> (primVarIndex ec, primType ec)) ctorOrder)
158175 ])
159176 RecursorApp rec ixs e -> pure $
160177 unwords ([" RecursorApp" show rec ] ++
@@ -219,29 +236,57 @@ scReadExternal sc input =
219236 readIdx :: String -> ReadM Term
220237 readIdx tok = getTerm =<< readM tok
221238
222- readElimsMap :: String -> ReadM (Map Ident (Term ,Term ))
239+ readElimsMap :: String -> ReadM (Map VarIndex (Term ,Term ))
223240 readElimsMap str =
224- do (ls :: [(Ident ,(Int Int <- readM str
241+ do (ls :: [(VarIndex ,(Int Int <- readM str
225242 elims <- forM ls (\ (c,(e,ty)) ->
226243 do e' <- getTerm e
227244 ty' <- getTerm ty
228245 pure (c, (e',ty')))
229246 pure (Map. fromList elims)
230247
248+ readCtorList :: String -> ReadM [PrimName Term ]
249+ readCtorList str =
250+ do (ls :: [(VarIndex ,Int <- readM str
251+ forM ls (\ (vi,i) -> readPrimName' vi =<< getTerm i)
252+
253+ readPrimName' :: VarIndex -> Term -> ReadM (PrimName Term )
254+ readPrimName' vi t' =
255+ do EC _ nmi tp <- readEC' vi t'
256+ case nmi of
257+ ModuleIdentifier ident -> pure (PrimName vi ident tp)
258+ _ -> lift $ fail $ " scReadExternal: primitive name must be a module identifier" ++ show nmi
259+
260+ readEC' :: VarIndex -> Term -> ReadM (ExtCns Term )
261+ readEC' vi t' =
262+ do (ts, nms, vs) <- State. get
263+ nmi <- case Map. lookup vi nms of
264+ Just nmi -> pure nmi
265+ Nothing -> lift $ fail $ " scReadExternal: ExtCns missing name info: " ++ show vi
266+ case nmi of
267+ ModuleIdentifier ident ->
268+ lift (scResolveNameByURI sc (moduleIdentToURI ident)) >>= \ case
269+ Just vi' -> pure (EC vi' nmi t')
270+ Nothing -> lift $ fail $ " scReadExternal: missing module identifier: " ++ show ident
271+ _ ->
272+ case Map. lookup vi vs of
273+ Just vi' -> pure $ EC vi' nmi t'
274+ Nothing ->
275+ do vi' <- lift $ scFreshGlobalVar sc
276+ State. put (ts, nms, Map. insert vi vi' vs)
277+ pure $ EC vi' nmi t'
278+
231279 readEC :: String -> String -> ReadM (ExtCns Term )
232280 readEC i t =
233281 do vi <- readM i
234282 t' <- readIdx t
235- (ts, nms, vs) <- State. get
236- nmi <- case Map. lookup vi nms of
237- Just nmi -> pure nmi
238- Nothing -> lift $ fail $ " scReadExternal: ExtCns missing name info: " ++ show vi
239- case Map. lookup vi vs of
240- Just vi' -> pure $ EC vi' nmi t'
241- Nothing ->
242- do vi' <- lift $ scFreshGlobalVar sc
243- State. put (ts, nms, Map. insert vi vi' vs)
244- pure $ EC vi' nmi t'
283+ readEC' vi t'
284+
285+ readPrimName :: String -> String -> ReadM (PrimName Term )
286+ readPrimName i t =
287+ do vi <- readM i
288+ t' <- readIdx t
289+ readPrimName' vi t'
245290
246291 parse :: [String -> ReadM (TermF Term )
247292 parse tokens =
@@ -251,35 +296,37 @@ scReadExternal sc input =
251296 [" Pi" -> Pi (Text. pack s) <$> readIdx t <*> readIdx e
252297 [" Var" -> pure $ LocalVar (read i)
253298 [" Constant" -> Constant <$> readEC i t <*> readIdx e
254- [" Primitive" -> FTermF <$> (Primitive <$> readEC i t)
299+ [" Primitive" -> FTermF <$> (Primitive <$> readPrimName i t)
255300 [" Unit" -> pure $ FTermF UnitValue
256301 [" UnitT" -> pure $ FTermF UnitType
257302 [" Pair" -> FTermF <$> (PairValue <$> readIdx x <*> readIdx y)
258303 [" PairT" -> FTermF <$> (PairType <$> readIdx x <*> readIdx y)
259304 [" ProjL" -> FTermF <$> (PairLeft <$> readIdx x)
260305 [" ProjR" -> FTermF <$> (PairRight <$> readIdx x)
261- (" Ctor" : i : (separateArgs -> Just (ps, es))) ->
262- FTermF <$> (CtorApp (parseIdent i) <$ >traverse readIdx ps <*> traverse readIdx es)
263- (" Data" : i : (separateArgs -> Just (ps, es))) ->
264- FTermF <$> (DataTypeApp (parseIdent i) <$ >traverse readIdx ps <*> traverse readIdx es)
306+ (" Ctor" : i : t : (separateArgs -> Just (ps, es))) ->
307+ FTermF <$> (CtorApp <$> readPrimName i t <* >traverse readIdx ps <*> traverse readIdx es)
308+ (" Data" : i : t : (separateArgs -> Just (ps, es))) ->
309+ FTermF <$> (DataTypeApp <$> readPrimName i t <* >traverse readIdx ps <*> traverse readIdx es)
265310
266- (" RecursorType" : i :
311+ (" RecursorType" : i : t :
267312 (separateArgs ->
268313 Just (ps, [motive,motive_ty]))) ->
269- do tp <- RecursorType (parseIdent i) <$>
314+ do tp <- RecursorType <$>
315+ readPrimName i t <*>
270316 traverse readIdx ps <*>
271317 readIdx motive <*>
272318 readIdx motive_ty
273319 pure (FTermF tp)
274- (" Recursor" : i :
320+ (" Recursor" : i : t :
275321 (separateArgs ->
276322 Just (ps, [motive, motiveTy, elims, ctorOrder]))) ->
277- do rec <- CompiledRecursor (parseIdent i) <$>
323+ do rec <- CompiledRecursor <$>
324+ readPrimName i t <*>
278325 traverse readIdx ps <*>
279326 readIdx motive <*>
280327 readIdx motiveTy <*>
281328 readElimsMap elims <*>
282- readM ctorOrder
329+ readCtorList ctorOrder
283330 pure (FTermF (Recursor rec ))
284331 (" RecursorApp" : rec : (splitLast -> Just (ixs, arg))) ->
285332 do app <- RecursorApp <$>
0 commit comments