a7217f1 · Idris-dev · git.iko.soy

76 ctxt <- getContext

77 i <- getIState

78

79− logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'

79+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

80 ty' <- addUsingConstraints syn fc ty'

81 ty' <- implicit syn n ty'

82

83 let ty = addImpl i ty'

84− logLvl 1 $ show n ++ " type " ++ showTmImpls ty

84+ logLvl 3 $ show n ++ " type " ++ showTmImpls ty

85 ((tyT, defer, is), log) <-

86 tclift $ elaborate ctxt n (TType (UVal 0)) []

87 (errAt "type of " n (erun fc (build i info False [] n ty)))

656 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)

657 [Erased, e])

658 let rhs' = normalise ctxt [] rhs

659− logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

659+ logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

660

661 -- Extract the provided term or postulate from the type provider

662 provided <- getProvided fc rhs'

667 do -- Finally add a top-level definition of the provided term

668 elabType info syn "" [] fc [] n ty

669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

670− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

670+ logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

671 | otherwise ->

672 ierror . Msg $ "Attempted to provide a term where a postulate was expected."

673 Postulate

674 | what `elem` [ProvPostulate, ProvAny] ->

675 do -- Add the postulate

676 elabPostulate info syn "Provided postulate" fc [] n ty

677− logLvl 1 $ "Elaborated provided postulate " ++ show n

677+ logLvl 3 $ "Elaborated provided postulate " ++ show n

678 | otherwise ->

679 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

680

1165 elabType info defaultSyntax "" [] fc opts newnm specTy

1166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1167 elabClauses info fc opts newnm def

1168− logLvl 1 $ "Specialised " ++ show newnm)

1168+ logLvl 2 $ "Specialised " ++ show newnm)

1169 -- if it doesn't work, just don't specialise. Could happen for lots

1170 -- of valid reasons (e.g. local variables in scope which can't be

1171 -- lifted out).

1419 -- Elaborate those with a type *before* RHS, those without *after*

1420 let (wbefore, wafter) = sepBlocks wb

1421

1422− logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1422+ logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1423 mapM_ (elabDecl' EAll info) wbefore

1424 -- Now build the RHS, using the type of the LHS as the goal.

1425 i <- getIState -- new implicits from where block

1563 _ -> []

1564 let params = getParamsInType i [] fn_is fn_ty

1565 let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1566− logLvl 1 ("LHS: " ++ show lhs)

1566+ logLvl 2 ("LHS: " ++ show lhs)

1567 ((lhs', dlhs, []), _) <-

1568 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1569 (errAt "left hand side of with in " fname

1921 -- get the implicit parameters that need passing through to the

1922 -- where block

1923 wparams <- mapM (\p -> case p of

1924− PApp _ _ args -> getWParams args

1924+ PApp _ _ args -> getWParams (map getTm args)

1925 _ -> return []) ps

1926 let pnames = map pname (concat (nub wparams))

1927 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

1947 logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

1948 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

1949 show (concat (nub wparams))

1950+

1951+ -- Bring variables in instance head into scope

1952+ ist <- getIState

1953+ let headVars = mapMaybe (\p -> case p of

1954+ PRef _ n ->

1955+ case lookupTy n (tt_ctxt ist) of

1956+ [] -> Just n

1957+ _ -> Nothing

1958+ _ -> Nothing) ps

1959+-- let lhs = PRef fc iname

1950− let lhs = PRef fc iname

1960+ let lhs = PApp fc (PRef fc iname)

1961+ (map (\n -> pimp n (PRef fc n) True) headVars)

1951 let rhs = PApp fc (PRef fc (instanceName ci))

1962 let rhs = PApp fc (PRef fc (instanceName ci))

1952 (map (pexp . mkMethApp) mtys)

1963 (map (pexp . mkMethApp) mtys)

1964+

1965+ logLvl 5 $ "Instance LHS " ++ show lhs

1966+ logLvl 5 $ "Instance RHS " ++ show rhs

1967+

1953 let idecls = [PClauses fc [Dictionary] iname

1968 let idecls = [PClauses fc [Dictionary] iname

1954 [PClause fc iname lhs [] rhs wb]]

1969 [PClause fc iname lhs [] rhs wb]]

1955 iLOG (show idecls)

1970 iLOG (show idecls)

2031

2046

2032 getWParams [] = return []

2047 getWParams [] = return []

2033 getWParams (p : ps)

2048 getWParams (p : ps)

2034− | PRef _ n <- getTm p

2049+ | PRef _ n <- p

2035 = do ps' <- getWParams ps

2050 = do ps' <- getWParams ps

2036 ctxt <- getContext

2051 ctxt <- getContext

2037 case lookupP n ctxt of

2052 case lookupP n ctxt of